Efficient and effective symbolic model checking

The main bottleneck in practical symbolic model checking is that it is restricted by the ability to efficiently represent and perform operations on sets of states. Symbolic representations, like Binary Decision Diagrams, grow very large quickly due to their necessity to cover the state space in a breadth first fashion. Satisfiability based techniques result in a proliferation of clauses, one reason being that they have to replicate the transition relation numerous times. We propose techniques to increase the capacity of automatic state-based verification as applied to sequential designs, i.e., symbolic model checking. Firstly, we propose the use of dynamically partitioned ordered Binary Decision Diagrams as a capable data structure. This leads to vast improvements in state space traversal in general and error detection in buggy designs, in particular. Secondly, we propose a partitioned approach to model checking, which splits the problem into multiple partitions handled independently of each other. State space partitioning-based approaches have been proposed in the literature to address the state explosion problem in model checking. These approaches, whether sequential or distributed, perform a large amount of work in the form of inter-partition (cross-over) image computations, which can be expensive. We present a model checking algorithm that aggregates these expensive cross-over images by localizing computation to individual partitions. This algorithm is more suited to parallelization than existing model checking approaches. It reduces the number of cross-over images and drastically outperforms extant approaches in terms of cross-over image computation cost as well as total model checking time, often by two orders of magnitude. We address the issue of time scalability in verification, whereby the availability of larger amounts of computation time enables greater exploration of the state space. From a practical standpoint, we observe that extant verification approaches are unable to proceed very deep into the state space. It is our conjecture that partitioning can help in this context and we explore this issue further. Finally, we study the combination of partitioned binary decision diagrams with bounded model checking for more scalable and efficient model checking. We give a technique to scale formal verification to a large grid of processors that demonstrates marked superiority over existing approaches. The contributions of this dissertation are in improving the capacity of symbolic model checking approaches to formal verification, in terms of time and memory requirements, as well as in the development of techniques that are more readily amenable to parallel and distributed model checking.