Accelerating Bounded Model Checking of Safety Properties

Author: Strichman Ofer  

Publisher: Springer Publishing Company

ISSN: 0925-9856

Source: Formal Methods in System Design, Vol.24, Iss.1, 2004-01, pp. : 5-24

Disclaimer: Any content in publications that violate the sovereignty, the constitution or regulations of the PRC is not accepted or approved by CNPIEC.

Previous Menu Next

Abstract

Bounded Model Checking based on SAT methods has recently been introduced as a complementary technique to BDD-based Symbolic Model Checking. The basic idea is to search for a counterexample in executions whose length is bounded by some integer k. The BMC problem can be efficiently reduced to a propositional satisfiability problem, and can therefore be solved by SAT methods rather than BDDs. SAT procedures are based on general-purpose heuristics that are designed for any propositional formula. We show how the unique characteristics of BMC invariant formulas (Gp) can be exploited for a variety of optimizations in the SAT checking procedure. Experiments with these optimizations on real designs prove their efficiency in many of the hard test cases, in comparison to both the standard SAT procedure and a BDD-based model checker.