Automatic abstraction in model checking
Edmund M. Clarke, Yuan Lu · 2000
As technology advances and demand for higher performance increases hardware designs are becoming more and more sophisticated. A typical chip design may contain over ten million switching devices. Since the systems become more and more complex, detecting design errors for systems of such scale becomes extremely difficult. Formal verification methodologies can potentially catch subtle design errors. However, many state-of-the-art formal verification tools suffer from the state explosion problem. This thesis explores abstraction techniques to avoid the state explosion problem. In our methodology, atomic formulas extracted from an SMV-like concurrent program are used to construct abstraction functions . The initial abstract structure is built by using existential abstraction techniques. When the model checker disproves a universal property on the abstract structure, it generates a counterexample. However, this abstract counterexample might be spurious because abstraction is not complete. We provide a new symbolic algorithm to determine whether an abstract counterexample is spurious. When a counterexample is identified to be spurious, the algorithm will compute the shortest prefix of the abstract counterexample that does not correspond to an actual trace in the concrete model. The last abstract state in this prefix is split into less abstract states so that the spurious counterexample is eliminated. Thus, a more refined abstraction function is obtained. It is usually desirable to obtain the coarsest refinement which eliminates the counterexample because this corresponds to the smallest abstract model that avoids the spurious counterexample. We prove, however, that finding the coarsest refinement is NP-hard. Because of this, we use a polynomial-time algorithm which gives a suboptimal but sufficiently good refinement of the abstraction function. The applicability of our heuristic algorithm is confirmed by our experiments. Using the refined abstraction function obtained in this manner, a new abstract model is built and the entire process is repeated. Our methodology is complete for ACTL, i.e., we are guaranteed to either find a valid counterexample or prove that the system satisfies the desired property. On the other hand, this thesis also discusses a new data structure - abstract BDDs. Intuitively, an abstract BDD is obtained from a BDD by collapsing paths that have the same abstract value with respect to some abstraction function. There are many ways to collapse the paths corresponding to different types of abstract BDDs. We identify four types of abstract BDDs : S-type, 0-type, 1-type and ∨ -type abstract BDDs for different applications. In this thesis, we show three applications of abstract BDDs. First, we will show how to check inequivalence between two combinational circuits using S-type and 0-type abstract BDDs. Then, we describe a methodology to generate an initial variable ordering using 0-type abstract BDDs. Finally, we demonstrate how to represent abstract Kripke structures using ∨ -type abstract BDDs. Our experiments clearly show the efficiency of abstract BDDs. We believe that abstract BDDs can be applied to many other applications as well.