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
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;
Conference_Titel :
Design, Automation and Test in Europe Conference and Exhibition 2000. Proceedings
Conference_Location :
Paris
Print_ISBN :
0-7695-0537-6
DOI :
10.1109/DATE.2000.840892
