Sequential equivalence checking without state space traversal
- 27 November 2002
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- p. 618-623
- https://doi.org/10.1109/date.1998.655922
Abstract
Because general algorithms for sequential equivalence checking require a state space traversal of the product machine, they are computationally expensive. In this paper we present a new method for sequential equivalence checking which utilizes functionally equivalent signals to prove the equivalence of both circuits, thereby avoiding the state space traversal. The effectiveness of the proposed method is confirmed by experimental results on retimed and optimized ISCAS'89 benchmarks.Keywords
This publication has 9 references indexed in Scilit:
- Incremental re-encoding for symbolic traversal of product machinesPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Exploiting functional dependencies in finite state machine verificationPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- On verifying the correctness of retimed circuitsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- A constructive approach towards correctness of synthesis-application within retimingPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Improving initialization through reversed retimingPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Disjunctive Partitioning And Partial Iterative Squaring: An Effective Approach For Symbolic Traversal Of Large CircuitsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,1997
- Record and play: a structural fixed point iteration for sequential circuit verificationPublished by Institute of Electrical and Electronics Engineers (IEEE) ,1997
- Symbolic model checking for sequential circuit verificationIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 1994
- Algorithms for approximate FSM traversalPublished by Association for Computing Machinery (ACM) ,1993