Computer-aided design and analysis of circuits and semiconductor – Nanotechnology related integrated circuit design
Reexamination Certificate
2000-03-14
2002-10-29
Smith, Matthew (Department: 2825)
Computer-aided design and analysis of circuits and semiconductor
Nanotechnology related integrated circuit design
C716S030000, C716S030000, C716S030000, C716S030000, C716S030000, C716S030000
Reexamination Certificate
active
06473884
ABSTRACT:
BACKGROUND OF THE INVENTION
1. Technical Field
The present invention generally relates to systems for equivalence checking of logical circuits such as verifiers and design tools, and more particularly to a computer program for equivalence checking large networks of logical circuits, wherein structural analysis and functional analysis are intertwined to improve analysis efficiency.
2. Description of the Related Art
Logic circuit synthesis and verification tools are typically required to represent integrated circuits having ten million transistors or more, such as microprocessors and Very-Large-Scale-Integration (VLSI)circuits. This level of integration represents millions of logic gates and their interconnections. A large amount of memory is required to represent and simulate the behavior of this many gates and sets a limitation on the complexity of simulation or the minimum system memory required to simulate or create a design using workstation software. Equivalence-checking is performed to find circuit equivalence between designs and to verify that networks meet their design specification, such as Very High Level Description Language(VHDL)input.
Algorithms that compare logic circuits that exhaustively analyze every input combination or structural feature are not as efficient as algorithms that can reduce search spaces while verifying a design. Large amounts of memory and processing power are required to represent large logical circuits while analyzing their structure or simulating their behavior in an exhaustive manner.
When performing equivalence checking of two circuits, there are usually many sub-circuits that will be the same for each circuit. The complexity of equivalence checking in large circuits may be reduced by merging equivalent nodes via functional analysis such as the Binary Decision Diagram (BDD) techniques described in “METHOD FOR DETERMINING FUNCTIONAL EQUIVALENCE BETWEEN DESIGN MODELS” U.S. Pat. No. 5,754,454, which is incorporated herein by reference. Likewise, structural satisfiability (SAT) solvers such as those described by “GRASP—A New Search Algorithm for Satisfiability” University of Michigan publication CSE-TR-292-96, can be used to find input combinations such that the non-equivalence of two circuits is proved. Each of these techniques has its pitfalls. BDD analysis may use a large amount of memory for circuits that are implementing certain functions. The SAT solvers are less demanding of memory resources, but can take a much longer time to complete for large circuits, and the completion time is dependent on the particular logical functions performed by the circuit. Thus, a priori determination of comparison time using a SAT solver cannot be made.
Therefore, it is desirable to implement an improved verification algorithm that can overcome the limitations of SAT solvers and BDD analyzers.
SUMMARY OF THE INVENTION
The objective of improving performance of a verification tool is achieved by comparing a first logical circuit to a second logical circuit via the construction of a combined circuit graph representing said first circuit and the second circuit. Then, binary decision diagrams (BDDs) for nodes within the combined circuit graph are computed, and nodes are merged if the BDDs have already been computed or the new BDDs are stored on a heap if their size is less than an upper size limit. The foregoing steps are performed until the BDD size has reached a lower limit value. After the lower limit is reached, the circuit is analyzed using a satisfiability analysis algorithm to check for equivalence or non-equivalence of the first and second circuit, controlled by a back-track limit. Then, the limit value is raised and the BDD computations are repeated for the new limit. The back-track limit is also raised and the structural satisfiability solver is called with the new back-track limit.
The invention may further be embodied in a workstation computer executing program instructions for carrying out the steps of the method, and in a computer program product having a storage media for those program instructions.
REFERENCES:
patent: 4942536 (1986-04-01), Watanabe et al.
patent: 5243538 (1990-08-01), Okuzawa et al.
patent: 5331568 (1991-06-01), Pixley
patent: 5469367 (1994-06-01), Puri et al.
patent: 5638381 (1995-07-01), Cho et al.
patent: 5671399 (1995-07-01), Meier
patent: 5909374 (1996-08-01), Matsunaga
patent: 5949691 (1997-08-01), Kurosaka et al.
patent: 5974242 (1997-09-01), Damaria et al.
patent: 5754454 (1998-05-01), Pixley et al.
patent: 6026222 (2000-02-01), Gupta et al.
patent: 6035107 (2000-03-01), Kuehlmann et al.
patent: 6086626 (2000-07-01), Jain et al.
patent: 6308299 (2001-10-01), Burch et al.
“GRASP—A New Search Algorithm for Satisfiability,” Joao P. Marques Silva and Karem A. Sakallah, The University of Michigan, Computer and Science and Engineering Division, CSE-TR-292-96, Apr. 10, 1996, pp. 1-17.
T. Larrabee, “Test pattern generation using boolean satisfiability” IEEE Trans. on computer-aided design of IC's vol. 11 No. 1 Jan. 1992 pp. 4-15.*
Stephan et al., “Combinational test generation using satisfiability” IEEE Trans. on computer-aided design of IC's vol. 15 No. 9 Sep. 1996 pp. 11671176.*
Hulgaard et al., “Equivalence checking of combinational circuits using boolean expression diagrams” IEEE Trans on computer-aided design . . . vol. 18 No. 7 Jul. 1999 pp. 903-917.
Ganai Malay Kumar
Janssen Geert
Krohm Florian Karl
Kuehlmann Andreas
Paruthi Viresh
Bracewell & Patterson L.L.P.
Lee Granville D.
Salys Casimer K.
Smith Matthew
LandOfFree
Method and system for equivalence-checking combinatorial... 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 system for equivalence-checking combinatorial..., we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Method and system for equivalence-checking combinatorial... will most certainly appreciate the feedback.
Profile ID: LFUS-PAI-O-2991840