The state explosion problem remains a major hurdle in applying symbolic model checking to large hardware designs. State space abstraction, having been essential for verifying designs of industrial complexity, is typically a manual process, requiring considerable creativity and insight.In this article, we present an automatic iterative abstraction-refinement methodology that extends symbolic model checking. In our method, the initial abstract model is generated by an automatic analysis of the control structures in the program to be verified. Abstract models may admit erroneous (or "spurious") counterexamples. We devise new symbolic techniques that analyze such counterexamples and refine the abstract model correspondingly. We describe aSMV, a prototype implementation of our methodology in NuSMV. Practical experiments including a large Fujitsu IP core design with about 500 latches and 10000 lines of SMV code confirm the effectiveness of our approach.

Counter examples for specification violations provide engineers with important debugging information. Although counterexamples are considered one of the main advantages of model checking, state-of the art model checkers are restricted to relatively simple counterexamples, and surprisingly little research effort has been put into counterexamples. In this paper, we introduce a new general framework for counterexamples. The paper has three main contributions: (i) We determine the general form of ACTL counterexamples. To this end, we investigate the notion of counterexample and show that a large class of temporal logics beyond ACTL admits counterexamples with a simple tree-like transition relation. We show that the existence of tree-like counterexamples is related to a universal fragment of extended branching time logic based on w-regular temporal operators. (ii) We present new symbolic algorithms to generate tree-like counterexamples for ACTL specifications. (iii) Based on tree-like counterexamples we extend the abstraction refinement methodology developed recently by Clarke et al. (CAV'2000) to full ACTL. This demonstrates the conceptual simplicity and elegance of tree-like counterexamples.

We discuss an open problem in ROBDD construction using composition and prove that the worst case complexity of the construction is truly cubic. With this insight we show that the process of composition naturally leads to construction of (even exponentially) compact partitioned-OBDDs (POBDDs)[17]. Our algorithm which incorporates dynamic partitioning, leads to the most general (and compact) form of POBDDs - graphs with multiple root variables. To show our algorithm is robust and practical, we have analyzed some well known problems in Boolean function representation, verification and finite state machine analysis where our approach generates graphs which are even orders of magnitude smaller.

Variable ordering for BDDs has been extensively investigated. Recently, sampling based ordering techniques have been proposed to overcome problems with structure based static ordering methods and sifting based dynamic reordering techniques. However, existing sampling techniques can lead to an unacceptably large deviation in the size of the final BDD. In this paper, we propose a new sampling technique based on abstract BDDs (aBDDs) that does not suffer from this problem. This new technique, easy to implement and automate, consistently creates high quality variable orderings for both combinational as well as sequential functions. Experimental results show that for many applications our approach is significantly superior to existing techniques.

We introduce a new equivalence checking method based on abstract BDDs (aBDDs). The basic idea is the following: given an abstraction function, aBDDs reduce the size of BDDs by merging nodes that have the same abstract value. An aBDD has bounded size and can be constructed without constructing the original BDD. We show that this method of equivalence checking is always sound. It is complete for an important class of arithmetic circuits that includes integer multiplication. We also suggest heuristics for findings suitable abstraction functions based on the structure of the circuit. The efficiency of this technique is illustrated by experiments on ISCAS'85 benchmark circuits.