Optimizing Model Checking Based on BDD Characterization.
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.
Document Details
- Document Type
- Technical Report
- Publication Date
- May 01, 1999
- Accession Number
- ADA366220
Entities
People
- Bwolen Yang
- David R. O'hallaron
- Edmund M. Clarke
- Randal Bryant
- Thomas R. Gross
Organizations
- Carnegie Mellon University