Optimizing model checking based on bdd characterization
Bwolen Yang, David R. O’Hallaron · 1999
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 ...