DAG-aware circuit compression for formal verification
- 22 February 2005
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
Abstract
The choice of representation for circuits and Boolean formulae in a formal verification tool is important for two reasons. First of all, representation compactness is necessary in order to keep the memory consumption low. This is witnessed by the importance of maximum processable design size for equivalence checkers. Second, many formal verification algorithms are sensitive to redundancies in the design that is processed. To address these concerns, three different auto-compressing representations for Boolean circuit networks and formulas have been suggested in the literature. We attempt to find a blend of features from these alternatives that allows us to remove as much redundancy as possible while not sacrificing runtime. By studying how the network representation size varies when we change parameters, we show that the use of only one operator node is suboptimal, and demonstrate that the most powerful of the proposed reduction rules, two-level minimization, actually can be harmful. We correct the bad behavior of two-level optimization by devising a simple linear simplification algorithm that can remove tens of thousands of nodes on examples where all obvious redundancies already have been removed. The combination of our compactor with the simplest representation outperforms all of the alternatives we have studied, with a theoretical runtime bound that is at least as good as the three studied representations.Keywords
This publication has 13 references indexed in Scilit:
- Equivalence Checking Using Cuts And HeapsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2005
- NuSMV 2: An OpenSource Tool for Symbolic Model CheckingPublished by Springer Nature ,2002
- Combining strengths of circuit-based and CNF-based algorithms for a high-performance SAT solverPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Circuit-based Boolean ReasoningPublished by Association for Computing Machinery (ACM) ,2001
- Bypassing BDD construction for reliability analysisInformation Processing Letters, 2000
- SAT-Based Verification without State Space TraversalPublished by Springer Nature ,2000
- Combining Decision Diagrams and SAT Procedures for Efficient Symbolic Model CheckingPublished by Springer Nature ,2000
- Equivalence checking of combinational circuits using Boolean expression diagramsIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 1999
- Boolean expression diagramsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,1997
- Graph-Based Algorithms for Boolean Function ManipulationIEEE Transactions on Computers, 1986