Adaptive techniques to improve state-space search in formal verification

The design of large and complex systems have made the verification the most critical and difficult component of the design cycle. Symbolic model checking, facilitated by Binary Decision Diagrams (BDDs), promises the scale-up of application of model checking techniques to large designs. However, state-of-the-art designs are still too large to be verified with symbolic model checking. Symbolic model checking can be applied to circuits with at most a few hundred latches and, unfortunately, are not robust even with respect to this size. The main problem is the BDD size explosion during model checking.; In this thesis, we propose adaptive techniques that address the BDD size explosion directly. The objective of these techniques is to improve automated methods in symbolic model checking to handle large circuits, i.e., increase the capacity of model checkers.; The first of these techniques is called high density reachability analysis. Fixpoint computations arising in model checking, are typically implemented as breadth-first search (BFS). Breadth-first search is an inflexible search that leaves no room to control the size of BDDs occurring in the computation. Our approach proposes to diverge from BFS in order to allow flexibility in manipulating the BDDs. Two sets of counteracting measures, control and efficiency measures, are employed to perform reachability analysis within the given computation resources (memory and CPU time). Control measures use approximations in order to manipulate small BDDs. We define the notion of density of a BDD that characterizes compact representation of large sets.; The second technique proposes to address the size explosion in image computation by simplifying the transition relation. This is done by applying hints that remove some transitions from the original system. Hints are constraints on the primary inputs and states of the system. They have the effect of constraining the environment and thereby considering only a subset of the behaviors of the system. The hints are chosen so that the resulting transition relation has a smaller BDD size or fewer variables in its support. A state traversal of each constrained system is performed. The results of each traversal is used in the next; the original system is finally restored to compute all reachable states.; The above two techniques are distinct strategies to improve traversal and can be combined to improve the capacity of invariant checking. Further, we can extend them to other least fixpoint computations and, in a restricted manner, to greatest fixpoint computations. The experimental results support the conclusion that these adaptive techniques improve the capacity of the model checker and make it more robust. (Abstract shortened by UMI.)...