DocumentCode
1982328
Title
Automatic equivalence check of circuit descriptions at clocked algorithmic and register transfer level
Author
Schönherr, Jens ; Straube, Bernd
Author_Institution
Fraunhofer-Arbeitsgruppe fur Integrierte Schaltungen, Dresden, Germany
fYear
2000
fDate
2000
Firstpage
759
Abstract
One of the big challenges in circuit design is the formal verification at clocked algorithmic or register-transfer level. To overcome the limits of BDD based approaches we apply an abstraction of the datapath by uninterpreted functions. Symbolic execution is used to generate potential invariants. Then the equivalence is proven by automatic induction proofs of the lemmas
Keywords
formal verification; high level synthesis; symbol manipulation; abstraction; automatic equivalence check; automatic induction proofs; circuit descriptions; circuit design; clocked algorithmic level; formal verification; register transfer level; symbolic execution; uninterpreted functions; Automata; Binary decision diagrams; Circuit synthesis; Clocks; Formal verification; Induction generators; Registers; Sequential circuits; Static VAr compensators; Writing;
fLanguage
English
Publisher
ieee
Conference_Titel
Design, Automation and Test in Europe Conference and Exhibition 2000. Proceedings
Conference_Location
Paris
Print_ISBN
0-7695-0537-6
Type
conf
DOI
10.1109/DATE.2000.840892
Filename
840892
Link To Document