Verification of sequential circuits with same state encoding

Details Verification of sequential circuits with same state encoding Verification of sequential circuits with same state encoding

1999-06-04

2002-06-18

Siek, Vuthe (Department: 2825)

Computer-aided design and analysis of circuits and semiconductor

Nanotechnology related integrated circuit design

C716S030000

Reexamination Certificate

active

06408424

ABSTRACT:

BACKGROUND OF THE INVENTION
The present invention relates generally to the field of Computer-aided design (CAD) systems and methods, and more particularly to CAD systems and methods for digital circuit verification of sequential circuits.
Computer-aided design of digital circuits and other complex digital systems is widely prevalent. The requirements of the circuit or system are defined in an abstract model of the circuit or system. The abstract model is then successively transformed into a number of intermediate stages.
The design of the circuit or system therefore proceeds from the general requirements level to the lower detailed level of the physical design. Interposed between are a number of intermediate levels. These intermediate stages often include a register transfer level model which represents a block structure behavioral design, and a structural model which is a logic level description of the system. Each successive level of the design is tested or verified to ensure that the circuit or system continues to meet the designed specifications.
These circuits or systems may be divided, among other ways, into combinational circuits and sequential circuits. The outputs of a combinational circuit depend entirely on the value of the inputs to the circuit. Thus, the outputs of a combinational circuit do not depend on the values of previous inputs applied to the circuit. The outputs of sequential circuits, however, depend on past values of the inputs with the outputs dependent on the inputs to the circuit and previously generated values of the outputs or some node within the circuit. Thus, a sequential circuit may be viewed as a plurality of combinational logic elements with some of the outputs of the plurality of combinational logic fed back to some of the inputs of the combinational logic via storage elements.
An example of combinational logic is a series of interconnected AND gates in which none of the outputs of the AND gates are fed back to previous AND gates. An example of a storage element is a clocked flip-flop. Other examples of a storage element are latches, registers, and other similar types of storage devices. Initially storage elements have unknown values and need to be forced to specific known states. These known states depend on the inputs to the circuit, i.e., the primary inputs, and the present state of the storage elements. Thus, a sequential circuit may generate different output values for the same set of input vectors depending on the boolean values of the storage elements. Therefore, design verification of a sequential circuit is often complex.
Conventionally, design verification is accomplished by simulating the circuit or system. This is done by stimulating the circuit with a set of test vectors, which represent a set of appropriately chosen inputs to the circuit, and thereafter examining the outputs of the circuit. However, for many circuits that are large and complicated, extensive simulation of the circuit is impractical. Hence, other techniques for verifying sequential circuits have also been developed, such as a Boolean Decision Diagram (BDD) based state space traversal technique, and automatic test pattern generator (ATPG) based traversal technique.
The BDD based state traversal technique however, often requires space, i.e., memory space, which is exponential in the number of primary inputs to the circuit or system. Therefore, for many large circuits memory explosion is a problem. Similarly, the ATPG based traversal technique is inefficient if the circuit is too large.
However, the verification of sequential circuits may be simplified by determining correspondences between storage elements of the two circuits. If such correspondence can be determined the verification step is simplified to a verification step for combinational circuits. Therefore, especially for large circuits, determining the correspondence between the storage elements of the circuits is desirable. Conventional techniques to determine the correspondence between the storage elements, however, are often ineffective. Therefore, the ability to determine the correspondence between the storage elements of multiple circuits quickly and effectively has become increasingly important, especially for large and complicated circuits.
SUMMARY OF THE INVENTION
The present invention provides a method and a system of verifying two sequential circuits, a first sequential circuit and a second sequential circuit. In one embodiment, the method comprises determining storage elements of the first and second sequential circuit, selecting pairs of storage elements of the first sequential circuit, establishing distinguishing criteria from the selected pairs of storage elements of the first sequential circuit and grouping the storage elements of the first and second sequential circuits based on the distinguishing criteria. The distinguishing criteria in one embodiment comprises computing a sequence of test vectors that causes outputs of one storage element in a selected pair of storage elements to differ from outputs of other storage elements.
In another embodiment, a method of verifying a first sequential circuit and a second sequential circuit both having primary inputs and primary outputs is provided. The method comprises grouping storage elements of the first and second sequential circuits, determining next states of the storage elements of the first and second sequential circuits or determining a probabilistic hash code using abstract BDDs or partitioned BDDs or using full ROBDDs without or with hash codes, comparing the hash code or the ROBDD of next state of the storage elements of the first sequential circuits to the next states of the storage elements of the second sequential circuits and regrouping the storage elements of the first and second sequential circuits based on the equivalence of the hash code or ROBDDs of the next states of the first and second sequential circuits. In one form, determining the next states of storage elements includes building sampled Boolean decision diagrams or abstract Boolean decision diagrams to represent the next states of the storage elements.


REFERENCES:
patent: 5230001 (1993-07-01), Chandra et al.
patent: 5257268 (1993-10-01), Agrawal et al.
patent: 5677915 (1997-10-01), Whetsel
patent: 5949691 (1999-09-01), Kurosaka et al.
patent: 6188934 (2001-02-01), Emura
patent: 6212669 (2001-04-01), Jain
Hoskote et al, “Automatic Verification of Implementations of Large Circuits Against HDL Specificatoins,” IEEE, Mar. 1997, pp. 217-228.*
Corno et al, “Approximate Equivalence Verification of Sequential Circuits Via Genetic Algorithms,” IEEE, Mar. 1999, pp. 754-755.*
Corno et al, “Vega: A Verification Tool Based on Genetic Algorithms,” IEEE, Oct. 1998, pp. 321-326.*
Huang et al, “Aquila: An Equivalence Verifier for Large Sequential Circuits,” IEEE, Jan. 1997, pp. 455-460.*
Mohnke et al, “Establishing Latch Correspondence for Sequential Circuits Using Distinguishing Signatures,” IEEE, Aug. 1997, pp. 472-476.*
Huang et al, “An ATPG-Based Framework for Verifying Sequential Equivalence,” IEEE, Oct. 1996, pp. 865-874.*
Masahiro Fujita, “Methods for Automatic Design Error Correction in Sequential Circuits,” IEEE, 1993, pp. 76-80.*
Alan J. Hu, “Formal Hardware Verification with BDDs: An Introduction,” IEEE, Aug. 1997, pp. 677-682.*
O. Coudert et al., “Verification of Sequential Machines using Boolean Functional Vectors”,Formal VLSI Correctness Verification, Elsevier Science Publishers, B.V. (North Holland), 1990, pp. 179-196.
O. Coudert et al., “Verfication of Synchronous Sequential Machines based on Symbolic Execution”,Proc. of Intl. Workshop on Automatic Verification Methods for Finite State Systems, vol. 407 of LNCS, Jun. 1989, pp. 365-373.
J. Burch et al., “Sequential Circuit Verification Using Symbolic Model Checking”,Proc. 27thACM/IEEE DAC, Paper 3.2, 1990, pp. 46-51.
S. Huang et al., “AQILA: An Equivalence Verifier for Large Sequential Circuits”,Proc. of Asia-South Pacific DAC, Jan. 1997, pp. 455-460.
Y. Matsunaga, “An Efficient Equivalence Checker for Combinational Circui

Affiliated with

Also associated with

Rating

Verification of sequential circuits with same state encoding does not yet have a rating. At this time, there are no reviews or comments for this patent.

If you have personal experience with Verification of sequential circuits with same state encoding, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Verification of sequential circuits with same state encoding will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFUS-PAI-O-2903262