Efficient fixpoint computation for invariant checking
- 20 January 2003
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- p. 467-474
- https://doi.org/10.1109/iccd.1999.808582
Abstract
Techniques for the computation of fixpoints are key to the success of many formal verification algorithms. To be efficient, these techniques must take into account how sets of states are represented. When BDDs are used, this means controlling, directly or indirectly, the size of the BDDs. Traditional fixpoint computations do little to keep BDD sizes small, apart from reordering variables. In this paper, we present a new strategy that attempts to keep the size of the BDDs under control at every stage of the computation. Our contribution includes also new techniques to compute partial images, and to speed up and test convergence. We present experimental results that prove the effectiveness of our strategy by demonstrating up to 40 orders of magnitude improvement in the number of states computed.Keywords
This publication has 16 references indexed in Scilit:
- Improved reachability analysis of large finite state machinesPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Implicit manipulation of equivalence classes using binary decision diagramsPublished 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
- Reachability analysis using partitioned-ROBDDsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,1997
- Forward model checking techniques oriented to buggy designsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,1997
- Automatic state space decomposition for approximate FSM traversal based on circuit analysisIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 1996
- Symbolic model checking for sequential circuit verificationIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 1994
- An improved algorithm for the evaluation of fixpoint expressionsPublished by Springer Nature ,1994
- Model checking and abstractionPublished by Association for Computing Machinery (ACM) ,1992
- Graph-Based Algorithms for Boolean Function ManipulationIEEE Transactions on Computers, 1986