Bwolen Yang

Optimizing Model Checking Based on BDD Characterization Degree Type: Ph.D. in Computer Science
Advisor(s): David O'Hallaron
Graduated: May 1999

Abstract:

Symbolic model checking has been successfully applied in verification of various finite state systems, ranging from hardware circuits to software protocols. A core technology underlying this success is the Binary Decision Diagram (BDD) representation. Given the importance of BDDs in model checking, it is surprising that there has been little or no work on studying BDD computations in the context of model checking. As a result, the computational aspects of BDDs are not well understood and many BDD-based algorithms tend to be unstable in terms of performance. This thesis addresses the performance instability issue both by developing a general evaluation methodology for studying BDD computations and by proposing new BDD-based optimizations to stabilize and to improve the overall performance.

The evaluation methodology consists of two parts: (1) a set of evaluation metrics characterizing key components of BDD computations, and (2) a trace-based evaluation platform for generating realistic benchmarks from computational traces of BDD-based tools and for replaying these traces on BDD packages. This methodology allows BDD-package designers to study and tune their packages based on realistic computations. This is the first evaluation methodology for studying BDD computation systematically.

Based on this evaluation methodology, we have designed and conducted a BDD performance study in the context of model checking. This study is a collaborative effort among six BDD designers using their own BDD packages. The study has resulted in significant performance improvements (with some speedups over 100) and several characterizations of model-checking computations; e.g., this study showed that computational characteristics of model checking are inherently different from those of combinational equivalence checking. These results demonstrate the importance of systematic evaluation and validate our methodology.

Using a similar systematic approach, I have stabilized and improved the performance of an important model-checking optimization called conjunctive partitioning and have derived a new algorithm for verifying constraint-rich systems. In both cases, the information encoded in the BDD representation is used to drive the optimizations. For conjunctive partitioning, the set of variables, the graph sizes, and tentative BDD operations are used to heuristically order and merge the partitions of the transition relation. For verifying constraint-rich systems, I developed a new BDD-based algorithm, called assignment-extraction algorithm, to establish relationships between state variables. This assignment-extraction algorithm decomposes any Boolean expression into assignment expressions. From these assignments, we can more precisely determine the set of variables that can be replaced with equivalent expressions (macro expansion)). The goal is to remove unnecessary state variables to reduce the overall state space. As with the improvements to conjunctive partitioning, BDD characteristics are used here to stabilize the optimization.

Our systematic approach to study and to improve the underlying BDD computations culminated in a significantly improved version of the SMV model checker that has helped other researchers tackle real-world applications. In particular, our approach has enabled the verification of the fault diagnosis model of NASA's Deep Space One spacecraft.

Thesis Committee:
David R. O’Hallaron (Chair)
Randal E. Bryant
Edmund M. Clarke
Thomas R. Gross
Kenneth L. McMillan (Cadence Berkeley Labs)

James Morris, Head, Computer Science Department
Raj Reddy Dean, School of Computer Science

Keywords:
Formal verification, model checking, time-invariant constraints, conjunctive partitioning, Symbolic Model Verifier (SMV), Binary Decision Diagram (BDD), BDD evaluation methodology, BDD performance study