A standard approach to improving circuit performance is to use an N-phase design style where combinational logic is interspersed freely between level sensitive latches controlled by separate clocks. Unfortunately, the use of an N-phase design style will increase the number of state variables by a factor of N, making formal verification many orders of magnitude harder. Previous approaches to solving this problem restrict the kind of designs that can be handled severely and construct an abstracted netlist with fewer state variables by a syntactic analysis that requires the user to identify clocks. We extend the current state of the art by introducing a phase abstraction algorithm that (1) poses no restrictions on the design style that can be used, that (2) avoids an error prone syntactic analysis, that (3) requires no input from users, and that (4) can be integrated into any model checker without requiring HDL code analysis.

In this paper, we present a method for finding failure traces for safety properties that are out of reach for traditional approaches to counter example generation. We do this by guiding bounded model checking (BMC) with information gathered from counter example guided abstraction refinement. Unlike previously described approaches based on reconstructing abstract counter examples on the concrete machines, we do not limit ourselves to search for failures of the same length as the current abstract counterexample. We also describe a combination of previously known methods for choosing registers to include in the abstraction that we have found works very well together with our technique for finding failures. Our experimental results show that the resulting method can find counter examples that are out of range for both standard BMC and two previously published approaches to abstraction-guided BMC.

Procedures for Boolean satisfiability most commonly work with Conjunctive Normal Form. Powerful SAT techniques based on implications and conflicts can be retained when the usual CNF clauses are replaced with BDDs. BDDs provide more powerful implication analysis, which can reduce the computational effort required to determine satisfiability.

We describe new techniques for model checking in the counterexample guided abstraction/refinement framework. The abstraction phase ‘hides’ the logic of various variables, hence considering them as inputs. This type of abstraction may lead to ‘spurious’ counterexamples, i.e. traces that can not be simulated on the original (concrete) machine. We check whether a counterexample is real or spurious with a SAT checker. We then use a combination of Integer Linear Programming (ILP) and machine learning techniques for refining the abstraction based on the counterexample. The process is repeated until either a real counterexample is found or the property is verified. We have implemented these techniques on top of the model checker NuSMV and the SAT solver Chaff. Experimental results prove the viability of these new techniques. These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Symbolic simulation is a formal verification technique which combines the flexibility of conventional simulation with powerful symbolic methods. Some constructs, however, which are easy to handle in conventional simulation need special consideration in symbolic simulation. This paper discusses some special constructs that require unique treatment in symbolic simulation such as the symbolic representation of arrays, an efficient This paper discusses some special constructs that are unique to symbolic simulation such as the symbolic representation of arrays, an efficient symbolic method for storing arrayed instances and the handling of symbolic data-dependent delays. We present results which demonstrate the effectiveness of our symbolic array model in the simulation of highly regular structures like FPGAs, memories or cellular automata.

Circuits can be simplified for combinational equivalence checking by transforming internal functions, while preserving their ranges. In this paper, we investigate how to effectively apply the idea to improve equivalence checking. We propose new heuristics to identify groups of nets in a cut, and elaborate detailed aspects of the new equivalence checking method. With a given miter, we identify a group of nets in a cut and transform the function of each net into a more compact representation with less variables. These new compact parametric representations preserve the range of nets as well as of the cut. This transformation significantly reduces the size of intermediate BDDs and enables the verification to be conclusive for many designs which state-of-the-art equivalence checkers fail to verify. Iterative groupings and transformations are performed until no grouping is possible for a cut. Then we proceed to the next cut and continue until the compare point is reached. Our experimental results show the effectiveness of our strategy and new grouping heuristics on the new method.

Symbolic simulation is a promising formal verification technique combining the flexibility of conventional simulation with powerful symbolic methods. Unfortunately, existing symbolic simulators are restricted to gate level simulation or handle just a synthesizable subset of an HDL. Simulation of systems composed of design, testbench and correctness checkers, however, requires the complete set of HDL constructs. We present an approach that enables symbolic simulation of the complete set of RT-level Verilog constructs with full delay support. Additionally, we propose a flexible scheme for introducing symbolic variables and demonstrate how error traces can be simulated with this new scheme. Finally, we present some experimental results on an 8051 micro-controller design which prove the effectiveness of our approach.

We present RFN, a formal property verification tool based on abstraction refinement. Abstraction refinement is a strategy for property verification. It iteratively refines an abstract model to better approximate the behavior of the original design in the hope that the abstract model alone will provide enough evidence to prove or disprove the property.

Computing the set of states reachable in one step from a given set of states, i.e. image computation, is a crucial step in several symbolic verification algorithms, including model checking and reachability analysis. So far, the best methods for quantification scheduling in image computation, with a conjunctively partitioned transition relation, have been restricted to a linear schedule. This results in a loss of flexibility during image computation. We view image computation as a problem of constructing an optimal parse tree for the image set. The optimality of a parse tree is defined by the largest BDD that is encountered during the computation of the tree. We present dynamic and static versions of a new algorithm, VarScore, which exploits the flexibility offered by the parse tree approach to the image computation. We show by extensive experimentation that our techniques outperform the best known techniques so far.

We develop algorithms for exploring the reachable state-space of hardware designs that can be partitioned into control and data. The core procedure is a symbolic algorithm that tries to visit as many controller states as is computationally feasible. Here, we describe heuristics for making this traversal efficient. Experiments demonstrate that our approach is capable of achieving significantly greater coverage of the control state-space than conventional symbolic reachability analysis.

Image computation is the key step in fixpoint computations that are extensively used in model checking. Two techniques have been used for this step: one based on conjunction of the terms of the transition relation, and the other based on recursive case splitting. We discuss when one technique outperforms the other, and consequently formulate a hybrid approach to image computation. Experimental results show that the hybrid algorithm is much more robust than the “pure” algorithms and outperforms both of them in most cases. Our findings also shed light on the remark of several researchers that splitting is especially effective in approximate reachability analysis.

We present Ketchum, a tool that was developed to improve the productivity of simulation-based functional verification by providing two capabilities: (1) automatic test generation and (2) unreachability analysis. Given a set of "interesting" signals in the design under test (DUT), automatic test generation creates input stimuli that drive the DUT through as many different combinations (called coverage states) of these signals as possible to thoroughly exercise the DUT. Unreachability analysis identifies as many unreachable coverage states as possible.

The knowledge of the reachable states of a sequential circuit can dramatically speed up optimization and model checking. However, since exact reachability analysis may be intractable, approximate techniques are often preferable. H. Cho et al. (1996) presented the machine-by-machine (MBM) and frame-by-frame (FBF) methods to perform approximate finite state machine (FSM) traversal. FBF produces tighter upper bounds than MBM; however, it usually takes much more time and it may have convergence problems. In this paper, we show that there exists a class of methods-least fixpoint approximations-that compute the same results as RFBF ("reached FBF", one of the FBF methods). We show that one member of this class, which we call "least fixpoint MBM" (LMBM), is as efficient as MBM, but provably more accurate. Therefore, the trade-off that existed between MBM and RFBF has been eliminated. LMBM can compute RFBF-quality approximations for all the large ISCAS-89 benchmark circuits in a total of less than 9000 seconds.

We develop a verification paradigm called saturated simulation, that is applicable to designs which can be decomposed into a set of interacting controllers. The core procedure is a symbolic algorithm that explores the space of controller interactions; heuristics for making this traversal efficient are described. Experiments demonstrate that our procedure explores substantially more of the controller interactions, and is more efficient than conventional symbolic reachability analysis.

The authors develop a method based on the premise that optimal state assignment corresponds to finding an optimal general decomposition of a finite state mechanism (FSM). They discuss the use of this approach for encoding state transition graphs extracted from logic-level descriptions. The notion of transition pairing is used to decompose a given FSM into several submachines such that the state assignment problem for the submachines is simpler than the original problem, attempting to avoid compromising the optimality of the solution. A novel decomposition algorithm that can decompose a FSM into an arbitrary number of submachines and a novel constraint satisfaction algorithm to encode the different submachines are given. Experimental results validate the use of decomposition-based techniques to solve the encoding problem.>

Dynamic load balancing of cooperating tasks requires a mechanism for rerouting messages sent between the tasks. When a large number of processors and rapidly changing workloads are involved, it is important to avoid bottlenecks or global expense in the rerouting mechanism. In the Object Executive (OX), both the sending and receiving end of a communication link maintain each other's physical address. A set of auxiliary control blocks and messages are used to update these addresses when either end of the link is moved. The proposed relocation mechanism has been used by OX on a 16-processor distributed-memory parallel processor.>