DocumentCode
3375420
Title
Verification of digital circuits based on formal semantics of a hardware description language
Author
Mutz, Matthias
Author_Institution
Passau Univ., Germany
fYear
1992
fDate
7-10 Sep 1992
Firstpage
98
Lastpage
101
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;
fLanguage
English
Publisher
ieee
Conference_Titel
Design Automation Conference, 1992., EURO-VHDL '92, EURO-DAC '92. European
Conference_Location
Hamburg
Print_ISBN
0-8186-2780-8
Type
conf
DOI
10.1109/EURDAC.1992.246258
Filename
246258
Link To Document