Record and play: a structural fixed point iteration for sequential circuit verification
- 1 January 1997
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
Abstract
This paper proposes a technique for sequential logic equivalence checking by a structural fixed point iteration. Verification is performed by expanding the circuit into an iterative circuit array and by proving equivalence of each time frame by well-known combinational verification techniques. These exploit structural similarity between designs by local circuit transformations. Starting from the initial state, for each time frame the performed circuit transformations are stored (recorded) in an instruction queue. In subsequent time frames the instruction queue is re-used (played) and updated when necessary. At some point the instruction queue does not need to be modified any more and is valid in all subsequent time frames. Thus, a fixed point is reached and machine equivalence is proved by induction. Experimental results show the great promise of this approach to verify circuits after resynthesis and retiming.Keywords
This publication has 12 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
- Improved reachability analysis of large finite state machinesPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- AND/OR reasoning graphs for determining prime implicants in multi-level combinational networksPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- High-density reachability analysisPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Logic optimization and equivalence checking by implication analysisIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 1997
- Reasoning in Boolean NetworksPublished by Springer Nature ,1997
- Symbolic Model CheckingPublished by Springer Nature ,1993
- Retiming synchronous circuitryAlgorithmica, 1991
- Graph-Based Algorithms for Boolean Function ManipulationIEEE Transactions on Computers, 1986