A proof engine approach to solving combinational design automation problems
- 1 January 2002
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- p. 725-730
- https://doi.org/10.1109/dac.2002.1012718
Abstract
There are many approaches available for solving combinational design automation problems encoded as tautology or satisfiability checks. Unfortunately there exists no single analysis that gives adequate performance for all problems of interest, and it is therefore critical to be able to combine approaches. In this paper, we present a proof engine framework where individual analyses are viewed as strategies-functions between different proof states. By defining our proof engine in such a way that we can compose strategies to form new, more powerful, strategies we achieve synergistic effects between the individual methods. The resulting framework has enabled us to develop a small set of powerful composite default strategies. We describe several strategies and their interplay; one of the strategies, variable instantiation, is new. The strength of our approach is demonstrated with experimental results showing that our default strategies can achieve up to several magnitudes of speed-up compared to BDD-based techniques and search-based satisfiability solvers such as ZCHAFF.Keywords
This publication has 5 references indexed in Scilit:
- Verification of large synthesized designsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Equivalence checking combining a structural SAT-solver, BDDs, and simulationPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Formal Equivalence Checking and Design DebuggingPublished by Springer Nature ,1998
- Graph-Based Algorithms for Boolean Function ManipulationIEEE Transactions on Computers, 1986
- A machine program for theorem-provingCommunications of the ACM, 1962