Efficient reachability algorithms in symbolic model checking

The size of VLSI designs is getting larger as the VLSI fabrication technology can handle smaller feature size and VLSI CAD tools can deal with larger circuits. As the design size grows, verification of the designs is getting harder and it is already the bottleneck in design cycle.; Simulation is the most widely used functional verification method. However, a major limitation of simulation is that an exhaustive check of all possible input patterns is infeasible. Therefore, it is very hard for simulation to find corner-case bugs.; Formal verification is the method to verify correctness of implementation of a design with respect to its specification by means of mathematical proof. Hence, formal verification conducts an exhaustive exploration of all possible behaviors.; In this thesis, we restrict our attention to symbolic model checking that is the most widely used formal method for sequential verification. In symbolic model checking by Binary Decision Diagrams (BDDs) the implementation is represented implicitly as a transition relation using BDDs and the specification is formulated as a set of properties in temporal logic. BDDs provide a canonical and compact representation of Boolean formulae and very efficient algorithms have been developed for manipulating them.; However, the design size that symbolic model checking can handle is still limited. Therefore, the main challenge in symbolic model checking is how to deal with large circuits, that is, how to address the state space explosion problem.; In this thesis, we propose two approaches to cope with the problem. The first approach is to improve image and preimage computations that are key operations in model checking as well as in reachability analysis. The second approach is to improve approximate reachability analysis for the computation of approximate don't cares that are used to simplify the transition relation and sets of states in model checking and reachability analysis.; In the first approach, we propose a hybrid algorithm for image and preimage computations. There are two existing methods for image and preimage computations. One is the transition function method based on recursive splitting and the other is the transition relation method based on conjunctions and quantifications. The hybrid method combines these two methods and decides when to split or to conjoin by computing variable lifetimes from the system dependence matrix. We also propose a conjunction and quantification scheduling algorithm that solves a subproblem of image and preimage computations. This algorithm tries to minimize variable lifetimes in the dependence matrix.; In the second approach, we propose two algorithms for approximate reachability analysis that significantly improve over the existing ones. One algorithm gets more accurate reachable states and is as fast as the existing method; hence, the improved algorithm produces a better trade-off between accuracy and speed when compared to the existing algorithms. The other algorithm deals with larger circuits and computes faster than the existing algorithm with marginal loss of accuracy.; By combining the two approaches, we were able to get significant improvements in time and space.