Improving SAT-based Bounded Model Checking by Means of BDD-based Approximate Traversals

Gianpiero Cabodi (Politecnico di Torino, Dip. di Automatica e Informatica, Italy)

Sergio Nocco (Politecnico di Torino, Dip. di Automatica e Informatica, Italy)

Stefano Quer (Politecnico di Torino, Dip. di Automatica e Informatica, Italy)

Abstract: Binary Decision Diagrams (BDDs) have been widely used in synthesis and verification. Boolean Satisfiability (SAT) Solvers, on the other hand, have been gaining ground only recently, with the introduction of efficient implementation procedures. Specifically, while BDDs have been mainly adopted to formally verify the correctness of hardware devices, SAT-based Bounded Model Checking (BMC) has been widely used for debugging.

In this paper, we combine BDD and SAT-based methods to increase the efficiency of BMC. We first exploit affordable BDD-based symbolic approximate reachability analysis to gather information on the state space. Then, we use the collected overestimated reachable state sets to restrict the search space of a SAT-based BMC. This is possible by feeding the SAT solver with a description that is the combination of the original BMC problem with the extra information coming from BDD-based symbolic analysis. We develop specific strategies to appropriately mix BDD and SAT efforts, and to efficiently convert BDD-based symbolic state set representations into SAT-oriented ones.

Experimental results prove the validity of our strategy to reduce the amount of variable assignments and variable conflicts generated by SAT solvers, with a subsequent significant performance gain. We gather results with four among the most used SAT solvers, namely Chaff, Limmat, BerkMin, and Siege. We could reduce the number of conflicts up to more than 100x, and the verification time up to 30x.

Keywords: binary decision diagrams (BDDs), bounded model checking (BMC), reachability analysis, satisfiability (SAT)

Categories: I.6.4, J.4