Tuning SAT Checkers for Bounded Model Checking

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 counter example in executions whose length is bounded by some integer k. The BMC problem can be e ciently reduced to a propositional satis ability 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 that the unique characteristics of BMC formulas can be exploited for a variety of optimizations in the SAT checking procedure. Experiments with these optimizations on real designs proved their e ciency in many of the hard test cases, comparing to both the standard SAT procedure and a BDD-based model checker.

• Type: Conference
• Year: 2000
• Where: CAV
• Authors: Ofer Strichman
• Keywords: CAV 2000, Hardware, Model Checking, SAT Methods, Sat Procedure