CMU-CS-99-145
Computer Science Department
School of Computer Science, Carnegie Mellon University


CMU-CS-99-145

Symbolic Model Checking using SAT procedures instead of BDDs

Armin Biere, Alessandro Cimatti*, Edmund M. Clarke, Masahiro Fujita**, Yunshan Zhu

February 1999

CMU-CS-99-145.ps
CMU-CS-99-145.pdf


Keywords: Hardware verification, out-of-order execution, temporal logic, symbolic model checking, boolean satisfiability


In this paper, we study the application of propositional decision procedures in hardware verification. We introduce the concept of bounded model checking. We show that bounded model checking for linear temporal logic formulas can be reduced to propositional satisfiability. We also present several optimizations that reduce the size of generated propositional formulas. To demonstrate our approach, we have implemented a tool BMC. BMC accepts a subset of the SMV language and uses state of the art SAT procedures to decide propositional satisfiability. As special cases, equivalence checking and invariant checking can also be handled. 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.

17 pages

*Istituto per la Ricerca Scientifica e Tecnolgica (IRST), via Sommarive 18, 38055 Povo (TN), Italy.
**Fujitsu Laboratories of America, Inc., 595 Lawrence Expressway, Sunnyvale, CA 94086-3922.

Return to: SCS Technical Report Collection
School of Computer Science homepage

This page maintained by reports@cs.cmu.edu