Title :
Verification of digital circuits based on formal semantics of a hardware description language
Author_Institution :
Passau Univ., Germany
Abstract :
The author presents basic concepts of defining semantics of the hardware description language VIOLA based on higher-order logic (HOL). The verification procedures of the hardware verification system VERENA are based on transformations of VIOLA terms. The correctness of these transformation steps can be formally verified based on the HOL semantics of the related VIOLA terms. As a mechanical tool, the HOL prove assistant is used. Basic concepts of a special verification system for the formal verification of digital circuits are presented. HOL serves as the formalism to define the underlying theory
Keywords :
formal verification; logic CAD; specification languages; HOL prove assistant; VIOLA; digital circuits verification; formal semantics; formal verification; hardware description language; hardware verification system VERENA; higher-order logic; Algebra; Carbon capture and storage; Digital circuits; Equations; Formal verification; Hardware design languages; Logic; Switches; Timing;
Conference_Titel :
Design Automation Conference, 1992., EURO-VHDL '92, EURO-DAC '92. European
Conference_Location :
Hamburg
Print_ISBN :
0-8186-2780-8
DOI :
10.1109/EURDAC.1992.246258
