×

zbMATH — the first resource for mathematics

Specification and verification of VHDL-based system-level hardware designs. (English) Zbl 0844.68006
Börger, Egon (ed.), Specification and validation methods. Oxford: Clarendon Press. International Schools for Computer Scientists. 331-409 (1995).
Summary: This chapter provides the semantic foundation of a formal verification environment for VHDL. The envisaged tool supports specification of system-level hardware designs using an extension of the classical concepts of timing diagrams allowing us to express first-order properties and causality relations between events. A formal semantics of such symbolic timing diagrams is given in terms of a linear time first-order temporal logic.
System-level designs expressed in VHDL – an IEEE standard hardware description language – can be verified against temporal logic specifications using a compositional proof system presented in this chapter. This proof-system is proved correct with respect to a formal semantics for VHDL in the style of structural operational semantics based on transition systems. For the special case of VHDL designs using finite data types only, the semantics provides a link to model-checking tools allowing automatic verification of VHDL designs against a temporal logic specification. Such a verification environment is currently under development within the ESPRIT project FORMAT.
For the entire collection see [Zbl 0831.00010].
MSC:
68M15 Reliability, testing and fault tolerance of networks and computer systems
68M99 Computer system organization
Software:
HOL; PREVAIL
PDF BibTeX XML Cite