Sequential equivalence checking based on k-th invariants and circuit SAT solving
- 18 January 2006
- proceedings article
- Published by Institute of Electrical and Electronics Engineers (IEEE)
Abstract
In this paper, we first present the concept of the k-th invariant. In contrast to the traditional invariants that hold for all cycles, k-th invariants guarantee to hold only after the k-th cycle from the initial state. We then present a bounded model checker BMChecker and an invariant prover IProver, both of which are based on circuit SAT techniques. Jointly, BMChecker and IProver are used to compute the k-th invariants, and are further integrated with a sequential SAT solver for checking sequential equivalence. Experimental results demonstrate that the sequential equivalence checking framework can efficiently verify large industrial designs.Keywords
This publication has 17 references indexed in Scilit:
- An Efficient Sequential SAT Solver With Improved Search StrategiesPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2005
- Dynamic transition relation simplification for bounded property checkingPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2005
- BerkMin: A fast and robust SAT-solverPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- SAT-based unbounded symbolic model checkingPublished by Association for Computing Machinery (ACM) ,2003
- Symbolic model checking using SAT procedures instead of BDDsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- Efficient Computation of Recurrence DiametersPublished by Springer Nature ,2002
- A unified framework for the formal verification of sequential circuitsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Property Checking via Structural AnalysisPublished by Springer Nature ,2002
- Circuit-based Boolean ReasoningPublished by Association for Computing Machinery (ACM) ,2001
- A theory and implementation of sequential hardware equivalenceIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 1992