Method and device for verification of VLSI designs

Details Method and device for verification of VLSI designs Method and device for verification of VLSI designs

2001-03-30

2003-05-20

Smith, Matthew (Department: 2825)

Computer-aided design and analysis of circuits and semiconductor

Nanotechnology related integrated circuit design

C716S030000, C716S030000, C703S015000

Reexamination Certificate

active

06567959

ABSTRACT:

FIELD OF THE INVENTION
The present invention pertains to verifying circuit designs. More particularly, the present invention pertains to an improved system for verification of VLSI (Very Large Scale Integration) designs.
BACKGROUND OF THE INVENTION
Formal verification of the functioning of a digital design is a fundamental necessity with the increasing size and complexity as well as important functions to be executed by the digital design. Even more specifically, formal verification of a digital sequential system is needed, yet lacking, for those systems that are large and complex. The mathematical modeling techniques presently available for a digital sequential system, e.g., VHDL (Very High Speed Integrated Circuits (VHSIC) Hardware Description Language, e.g., standard VHDL-1076 (1987) as developed by Institute of Electrical and Electronic Engineers) and Verilog, are incapable of providing an efficient and confident verification review of some modem large and complex systems due in part to the complexity and memory requirements of the mathematical modeling technique.
A formal equivalence verification tool (FEV) is a CAD processing method used to ensure correct implementation of chip designs. Logic design size and complexity of chip designs are growing significantly in the field and present a challenge to the formal equivalence tool.
Formal equivalence verification, in the sequential domain particularly, is traditionally based on Binary Decision Diagrams (BDDs). Binary Decision Diagrams are graph structures that encode the state space or logic behavior and symbolic traversals of a Very Large Scale Integration (VLSI) logic design for all possible input value combinations. Unfortunately, because the huge state space of some modem Very Large Scale Integration (VLSI) designs, Binary Decision Diagrams cause memory complexity that cannot be confidently handled by the formal equivalence verification tool.
While most formal equivalence verification and state space traversal techniques remain infeasible for the required amount of memory of modem designs, common random binary simulation and Automatic Test Pattern Generator (ATPG) techniques also are not feasible because those techniques cover a relatively very small portion of the state space, thus providing poor or incorrect computed results. Further, some traditional techniques only perform a combinational equivalence check, thus not recognizing the equivalence of some sequentially equivalent circuits.
In “Simulation-Based Sequential Equivalence Checking of RTL VHDL”, by Fulvio Corno et al. for Politecnico di Torino, published in 1999 by IEEE (hereinafter referred to as “Corno reference”, the Corno reference's algorithm appears based on genetic algorithms for producing meaningful test patterns for simulation, and interacts with a VHDL simulator. One shortcoming of the Corno reference is that it cannot provide any equivalence proof and is instead oriented towards finding a difference. The Corno reference discusses its prototype RAVE (RT-level Automatic Verificator) which proved in test runs to have low run times on moderately large circuits. RAVE, the RT-level Automatic Verificator, uses a genetic algorithm and when presented with two circuits to be proven equivalent, RAVE searches in the space of all possible input sequences for a counterexample, the counterexample being a sequence that generates a different output response in the two circuits. The Corno reference's algorithms do not provide useful coverage for complex chip designs and instead the algorithms suffer from poor approximation due to low coverage of the space traversal.
In view of the above, there is a need for an efficient technique which can provide larger state space coverage and simultaneously produce high quality results.


REFERENCES:
patent: 5202889 (1993-04-01), Aharon et al.
patent: 5331568 (1994-07-01), Pixley
patent: 5544067 (1996-08-01), Rostoker et al.
patent: 5724504 (1998-03-01), Aharon et al.
patent: 5801958 (1998-09-01), Dangelo et al.
patent: 6006028 (1999-12-01), Aharon et al.
patent: 6035107 (2000-03-01), Kuehlmann et al.
patent: 6035109 (2000-03-01), Ashar et al.
patent: 6086626 (2000-07-01), Jain et al.
patent: 6212669 (2001-04-01), Jain
patent: 6269467 (2001-07-01), Chang et al.
patent: 6301687 (2001-10-01), Jain et al.
patent: 6308299 (2001-10-01), Burch et al.
patent: 6378112 (2002-04-01), Martin et al.
patent: 6408424 (2002-06-01), Mukherjee et al.
patent: 6449750 (2002-09-01), Tsuchiya
patent: 6470482 (2002-10-01), Rostoker et al.
patent: 6484135 (2002-11-01), Chin et al.
patent: 2001/0025369 (2001-09-01), Chang et al.
patent: 2002/0073380 (2002-06-01), Cooke et al.
patent: 2002/0108093 (2002-08-01), Moondanos et al.
patent: 2002/0144215 (2002-10-01), Hoskote et al.
Paruthi et al., “Equivalence checking combing a structural SAT-solver, BDDs, and simulation”, Proceedings of 2000 International Conference on Computer Design, Sep. 17, 2000, pp. 459-464.*
Huang et al., “AQUILA: An Equivalence Verifier for Large Sequential Circuits”, Proceedings of the ASP-DAC '97 Asia and South Pacific Design Automation Conference, Jan. 28, 1997, pp. 455-460.*
Rho et al., “Inductive verification of iterative systems”, Proceedings of 29thACM/IEEE Design Automation Conference, Jun. 8, 1992, pp. 628-633.*
Krohm et al., “The use of random simulation in formal verification”, Proceedings of 1996 IEEE International Conference on Computer Design: VLSI in Computers and Processors, Oct. 7, 1996, pp. 371-376.*
* Fulvio Corno, Matteo Sonza Reorda, Giovanni Squillero, “Simulation-Based Sequential Equivalence Checking of RTL VHDL”, Politecnico di Torino, Dipartimineto di Automatica e Informatica, Torino, Italy, the IEEE International Conference on Electronics, Circuits, and Systems, Sep. 5, 1999, vol. 1, pp. 351-354.

Affiliated with

Also associated with

Rating

Method and device for verification of VLSI designs does not yet have a rating. At this time, there are no reviews or comments for this patent.

If you have personal experience with Method and device for verification of VLSI designs, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Method and device for verification of VLSI designs will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFUS-PAI-O-3070885