Automatic equivalence check of circuit descriptions at clocked algorithmic and register transfer level
Jens Schönherr, Bernd Straube · Proceedings Design, Automation and Test in Europe Conference and Exhibition 2000 (Cat. No. PR00537) · 2000
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.