A comparison of BDDs, BMC, and sequential SAT for model checking

BDD-based model checking and bounded model checking (BMC) are the main techniques currently used in formal verification. In general, there are robustness issues in SAT-based versus BDD-based model checking. The research reported in this paper attempts to analyze the asymptotic run-time behavior of modern BDD-based and SAT based techniques for model checking to determine the circuit characteristics which lead to worst-case behavior in these approaches. We show evidence for a run-time characterization based on sequential correlation and clause density. We demonstrate that it is possible to predict the worst-case behavior of BMC based on these characterizations. This leads to some interesting insights into the behavior of these techniques on a variety of example circuits.