Anzeige
Erschienen in:
2000 | OriginalPaper | Buchkapitel
Tuning SAT Checkers for Bounded Model Checking
verfasst von : Ofer Shtrichman
Erschienen in: Computer Aided Verification
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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 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 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 efficiency in many of the hard test cases, comparing to both the standard SAT procedure and a BDD-based model checker.