Symbolic Model Checking using SAT procedures instead of BDDs

Abstract

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 he 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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Feb 01, 1999
Accession Number
ADA366223

Entities

People

  • A. Biere
  • A. Cimatti
  • E. M. Clarke
  • M. Fujita
  • Yupeng Zhu

Organizations

  • Carnegie Mellon University

Tags

Communities of Interest

  • C4I

DTIC Thesaurus Topics

  • Algorithms
  • Artificial Intelligence
  • Coding
  • Computations
  • Computer Science
  • Computers
  • Language
  • Notation
  • Optimization
  • Sequences
  • Simulations
  • Specifications
  • Splitting
  • Transitions
  • Translations
  • United States
  • Verification

Fields of Study

  • Computer science

Readers

  • Applied Combinatorial Optimization and Logic Circuit Design.
  • Mathematical Modeling and Probability Theory.