Symbolic model checking using SAT procedures instead of BDDs
Top Cited Papers
- 20 January 2003
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- p. 317-320
- https://doi.org/10.1109/dac.1999.781333
Abstract
In this paper, we study the application of propositional decision procedures in hardware verification. In particular, we apply bounded model checking to equivalence and invariant checking. We present several optimizations that reduce the size of generated propositional formulas. In many instances, our SAT-based approach can significantly outperform BDD-based approaches. We observe that SAT-based techniques are particularly efficient in detecting errors in both combinational and sequential designs.Keywords
This publication has 7 references indexed in Scilit:
- Design and synthesis of synchronization skeletons using branching time temporal logicPublished by Springer Nature ,2005
- Symbolic model checking: 1020 States and beyondPublished by Elsevier ,2004
- HANNIBAL: An efficient tool for logic verification based on recursive learningPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Symbolic Model CheckingPublished by Springer Nature ,1993
- A Structure-preserving Clause Form TranslationJournal of Symbolic Computation, 1986
- Graph-Based Algorithms for Boolean Function ManipulationIEEE Transactions on Computers, 1986
- A Computing Procedure for Quantification TheoryJournal of the ACM, 1960