Combining Decision Diagrams and SAT Procedures for Efficient Symbolic Model Checking

Poul F. Williams
Armin Biere
Edmund M. Clarke
Anubhav Gupta

September 2000

Abstract

In this paper we show how to do symbolic model checking using Boolean Expression Diagrams (BEDs), a non-canonical representation for Boolean formulas, instead of Binary Decision Diagrams (BDDs), the traditionally used canonical representation. The method is based on standard fixed point algorithms, combined with BDDs and SAT-solvers to perform satisfiability checking. As a result we are able to model check systems for which standard BDD-based methods fail. For example, we model check a 256 bit shift-and-add multiplier. As opposed to Bounded Model Checking (BMC) our method is complete in practice.

Our technique is based on a quantification procedure that allows us to eliminate quantifiers in Quantified Boolean Formulas (QBF). The basic step of this procedure is the up-one operation for BEDs. In addition we list a number of important optimizations to reduce the number of basic steps. In particular the optimization rule of quantification-by-substitution turned out to be very useful: exists x : {g /\ ( x <-> f )} = g[f/x]. The rule is used (1) during fixed point iterations, (2) for deciding whether an initial set of states is a subset of another set of states, and finally (3) for iterative squaring.

Presented at the SRC's Sixth Premier Technical Conference TECHCON 2000 in Phoenix, Arizone, September 2000.

Available as PostScript(gzip'ed), PostScript, PDF, and BibTeX.

This is a short version of my CAV 2000 paper.

Poul Frederick Williams

E-mail: pfw@it-c.dk

Homepage: www.it-c.dk/people/pfw