Applying sat methods in unbounded symbolic model checking

Abstract

A method of symbolic model checking is introduced that uses conjunctive normal form (CNF) rather than binary decision diagrams (BDD’s) and uses a SAT-based approach to quantifier elimination. This method is compared to a traditional BDD-based model checking approach using a set of benchmark problems derived from the compositional verification of a commercial microprocessor design.