Dynamic transition relation simplification for bounded property checking
- 22 February 2005
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
Abstract
Bounded model checking (BMC) is an incomplete property checking method that is based on a finite unfolding of the transition relation to disprove the correctness of a set of properties or to prove them for a limited execution length from the initial states. Current BMC techniques repeatedly concatenate the original transition relation to unfold the circuit with increasing depths. In this paper we present a method that is based on a dual unfolding scheme. The first unfolding is non-initialized and progressively simplifies concatenated frames of the transition relation. The tail of the simplified frames is then applied in the second unfolding, which starts from the initial state and checks the properties. We use a circuit graph representation for all functions and perform simplification by merging vertices that are functionally equivalent under given input constraints. In the noninitialized unfolding, previous time frames progressively tighten these constraints thus leading to an asymptotic simplification of the transition relation. As a side benefit, our method can find inductive invariants constructively by detecting when vertices are functionally equivalent across time frames. This information is then used to further simplify the transition relation and, in some cases, prove unbounded correctness of properties. Our experiments using industrial property checking problems demonstrate that the presented method significantly improves the efficiency of BMC.Keywords
This publication has 21 references indexed in Scilit:
- Automatic Abstraction without CounterexamplesPublished by Springer Nature ,2003
- Efficient Computation of Recurrence DiametersPublished by Springer Nature ,2002
- Robust Boolean reasoning for equivalence checking and functional property verificationIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2002
- Automated Abstraction Refinement for Model Checking Large State Spaces Using SAT Based Conflict AnalysisPublished by Springer Nature ,2002
- Property Checking via Structural AnalysisPublished by Springer Nature ,2002
- Pruning Techniques for the SAT-Based Bounded Model Checking ProblemPublished by Springer Nature ,2001
- Transformation-Based Verification Using Generalized RetimingPublished by Springer Nature ,2001
- Sequential equivalence checking based on structural similaritiesIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2000
- Logic optimization and equivalence checking by implication analysisIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 1997
- A Method for Symbolic Verification of Synchronous CircuitsPublished by Elsevier ,1991