Computer Science Department
School of Computer Science, Carnegie Mellon University
Optimizing Model Checking Based on
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.