Automatic equivalence check of circuit descriptions at clocked algorithmic and register transfer level Abschnitt eines Buches uri icon

Open Access

  • false

Peer Reviewed

  • false

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.

Veröffentlichungszeitpunkt

  • Januar 1, 2000