Approximation and Don't Cares
for Model Checking

Nowadays CTL model checking is widely used in industrial designs. However, it still suffers important size limitations. To cope with this problem, I propose to use approximation methods and don't cares for efficient model checking of large circuits.

RDCs (Reachability Don't Cares) can have a dramatic impact on the cost of CTL model checking. Unfortunately, RDCs are often much more difficult to compute than the satisfying set of typical CTL formulas. We address this problem through the use of Approximate Reachability Don't Cares (ARDCs), computed with a significant extension to the algorithms of the VERITAS sequential synthesis package. ARDCs represent an upper bound on the set of true reachable states, and thus a lower bound on the set of unreachable (Don't Care) states. ARDCs can be 10X to 1000X (or much more for very large circuits) cheaper to compute than RDCs, and in some cases have the same dramatic effect on CTL model checking as the real RDCs. We also discuss the application of ARDCs to the problem of exact reachability analysis. Experiments on industrial benchmarks show that order of magnitude speedups are possible, and occur frequently. Furthermore, ARDCs can make intractable designs tractable in many cases in model checking and reachability analysis. The experimental results presented strongly support our claim that ARDCs play a safe and important way out of a serious dilemma: RDCs are necessary for tractable model checking of many large circuits, but the computation of the RDCs themselves is often intractable.

First goal of my thesis is to improve the approximation in approximate FSM traversal to make it closer to exact reachability analysis, faster, and less memory intensive so that we can handle very large circuits efficiently. We have developed FastMBM (Fast Machine By Machine) that is faster and less memory intensive than MBM and implemented LMBM (Least fixed point MBM) that is the combination of MBM and RFBF (Reached-set Frame By Frame) and gives the same upper bounds as RFBF while being as fast as MBM. Second goal is to maximize the use of Don't Cares for CTL model checking and reachability analysis. So far I have tried to minimize the BDD sizes of the transition relation and the reachable states. Now, I am working on the minimization of the size of intermediate BDDs during image and pre-image computation. Third goal is to accelerate exact model checking (backward state traversal as well as forward state traversal) and reachability analysis. I am going to use an iterative approximation-refinement method and an hybrid method combining transition relation and transition function. The approximation-refinement method is a kind of fully automated guided search, in that, before I compute the exact image or pre-image of a set--which is usually expensive--I try to get a refined subset or superset of the image or pre-image iteratively by refining the approximation. Then eventually I compute the exact result from the subset or superset.