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.

Only very small designs can be verified currently using property checking due to state-space explosion. Abstractions have been developed to simplify the design in an attempt to address this problem. However, the properties themselves may involve large state spaces, and practical property checking is generally confined to the control behavior. This paper describes an elegant technique for verifying properties of complex designs where the abstraction is applied to both the property and the design, thereby allowing us to verify properties which may deal with the data space. We demonstrate the technique on a processor by checking properties which are intractable using existing model checking techniques.

Despite great advances in Formal Verification (FV) simulation is still the primary means for design validation. The definition of pragmatic measures for the coverage achieved and the problem of automatic test generation (ATG) are of great importance. In this paper we introduce a new set of metrics, the Event Sequence Coverage Metrics (ESCMs). Our approach is based on an automatic method to extract the control flow of a circuit which can be explored for coverage analysis and ATG. We combine FV and traditional ATPG techniques to automatically generate sequences which traverse uncovered parts of the control graph or exercise uninstantiated control event sequences.

The enormous state spaces which must be searched when verifying the correctness of, or generating tests for, complex circuits precludes the use of traditional approaches. Hard-to-find abstractions are often required to simplify the circuits and make the problems tractable. This paper presents a simple and automatic method to extract the control flow of a circuit so that the resulting state space can be explored for validation coverage analysis and automatic test generation. This control flow, capturing the essential "behavior" of the circuit, is represented as a finite state machine called the ECFM (Extracted Control Flow Machine). Simulation is currently the primary means of verifying large circuits, but the definition of a coverage measure for simulation vectors is an open problem. We define functional coverage as the amount of control behavior covered by the test suite. We then combine formal verification techniques, using BDDs as the underlying representation, with traditional ATPG techniques to automatically generate additional sequences which traverse uncovered parts of the control state graph. We also demonstrate how the same abstraction techniques can complement ATPG techniques when attacking hard-to-detect faults in the control part of the design for which conventional ATPG alone proves to be inadequate or inefficient at best. Results on large designs show significant improvement over conventional algorithms.

Binary Decision Diagrams (BDDs) are widely used for efficiently representing logic designs and for verifying their equivalence. However, they often require large amounts of memory even for relatively small circuits. This paper presents a new mechanism for alleviating the memory consumption problem by exploiting the memory available in a cluster of workstations. The memory required for a BDD node may be allocated in other machines on the network, and any reference to a BDD node returns the value from the appropriate machine in a transparent fashion. Using this technique we are able to verify the sequential benchmark s1423, even though the BDDs required for verification exceed 2 gigabytes of storage.

New approaches to address the difficult problems in test are necessary if its current status as a major bottleneck in the production of quality integrated circuits is to be changed. The authors propose a new direction for solving the test problem using powerful methods already employed for the formal verification of large circuits. More specifically, they discuss how abstraction techniques can assist conventional ATPG tools when attacking hard to detect faults. The same abstractions can also be used in design verification to increase the level of confidence in a design following simulation, by providing a meaningful measure of the coverage achieved by the verification vectors. In this sense, the authors' approach is geared toward providing a unified fled framework for design validation and manufacturing test.

Simulation is still the primary, although inadequate, resource for verifying the conformity of a design to its functional specification. Fortunately, most errors in the early stages of design involve only the control flow in the circuit. We define the functional coverage of a given sequence of verification vectors as the amount of control behavior exercised by them. We present a novel technique for automatically extracting the control flow of a design on the basis of the underlying mathematical model. Significantly, this extraction is independent of the circuit description style. The Extracted Control Flow Machine (ECFM) is then used for estimation of functional coverage and to provide information that will help the designer improve the quality of his or her tests.

Introduces some new methods for estimating the "importance" of a variable in a Boolean function, and uses them to compute variable orders for OBDD construction. These measures are based on information theoretic criteria, and require the computation of the entropy of a variable in a given function. These entropy measures prove quite effective in distinguishing the importance of variables. Experimental results show this to be a very encouraging approach to help in the solution of this well known problem.>