US6086626A
Expired / Lapsed
US
⏱️ 0.0 years remaining
Method for verification of combinational circuits using a filtering oriented approach
Assignee: Fujitsu Ltd
•
Filing: 1997-05-16
•
Granted: 2000-07-11
•
Expires: 2017-05-16
Abstract
Abstract A set of filters are arranged in sequence for verification and analysis of digital circuit designs. The filters are either active filters, which are directly involved in verification of circuit designs (e.g., a Binary Decision Diagram (BDD)-based verifier or an automatic test pattern generation (ATPG)-based verifier), or passive filters, which gather information about the circuit or transform the circuit structure in order to simplify the verification problem (e.g., random pattern simulation or circuit partitioning). Given a pair of circuits to be verified, the filter approach first subjects the circuits to very simple, fast techniques having very low memory usage requirements. These steps are followed by a series of increasingly powerful methods that are more time consuming and often require more computer memory for their operation. In between the simpler active filters and the more sophisticated active filters, information about potential equivalent nodes in the circuits is collected and a decision is made as to whether to partition the circuits. The verification methodology is structured such that circuit designs that are easier to verify are never unnecessarily subjected to more expensive techniques. The method provides for a gradual increase in the sophistication of verification techniques applied, according to the difficulty of the verification problem.
Inventors
- 👤 Jawahar Jain
- 👤 Rajarshi Mukherjee
- 👤 Koichiro Takayama
Bibliographic Details
Application Number
—
Jurisdiction
US
Data Source
google_patents
Last Synchronized
2026-11-08 23:01
CPC Classifications
G; G01; G01R; G01R31/00; G01R31/28; G01R31/317; G01R31/3181; G01R31/3183; G01R31/318342; G01R31/318357; G01R31/318371; G01R31/318385; G06; G06F; G06F30/00; G06F30/30; G06F30/32; G06F30/33; G06F30/3323
Claims Analysis
Total Claims: 65
Claim 1
Independent Claim
110 words
A computer-implemented method of verifying a combinational circuit being represented by a circuit data structure comprising the steps of: executing a plurality of complete verification techniques and a plurality of supporting techniques arranged in a sequence for the combinational circuit, each of the plurality of complete verification techniques being capable of determining a verification result and each of the plurality of supporting techniques being capable of altering the circuit data structure; providing the verification result to one of subsequent complete verification techniques; providing the altered circuit data structure to one of subsequent supporting techniques; and repeating the executing and providing steps until a resultant altered circuit data structure is determined.
Claim 2
Dependent Claim
110 words
A computer-implemented method of verifying a combinational circuit being represented by a circuit data structure comprising the steps of: executing a plurality of complete verification techniques and a plurality of supporting techniques arranged in a sequence for the combinational circuit, each of the plurality of complete verification techniques being capable of determining a verification result and each of the plurality of supporting techniques being capable of altering the circuit data structure; providing the verification result to one of subsequent complete verification techniques; providing the altered circuit data structure to one of subsequent supporting techniques; and repeating the executing and providing steps until a resultant altered circuit data structure is determined.
Claim 3
Independent Claim
108 words
A system for verifying a combinational circuit represented by a circuit data structure comprising: means for executing a plurality of complete verification techniques and a plurality of supporting techniques arranged in a sequence for the combinational circuit, each of the plurality of complete verification techniques being capable of determining a verification result and each of the plurality of supporting techniques being capable of altering the circuit data structure, for passing the verification result to one of subsequent complete verification techniques in the sequence, for passing the altered circuit data structure to one of subsequent supporting techniques in the sequence, and for providing a resultant altered circuit data structure.
Claim 4
Independent Claim
108 words
A system for verifying a combinational circuit represented by a circuit data structure comprising: means for executing a plurality of complete verification techniques and a plurality of supporting techniques arranged in a sequence for the combinational circuit, each of the plurality of complete verification techniques being capable of determining a verification result and each of the plurality of supporting techniques being capable of altering the circuit data structure, for passing the verification result to one of subsequent complete verification techniques in the sequence, for passing the altered circuit data structure to one of subsequent supporting techniques in the sequence, and for providing a resultant altered circuit data structure.
Claim 5
Dependent Claim
108 words
A computer-implemented method of verifying a combinational circuit being represented by a circuit data structure comprising the steps of: executing a plurality of complete verification techniques and a plurality of supporting techniques arranged in a sequence for the combinational circuit, each of the plurality of complete verification techniques being capable of determining a verification result and each of the plurality of supporting techniques being capable of altering the circuit data structure; providing the verification result to one of subsequent complete verification techniques; providing the altered circuit data structure to one of subsequent supporting techniques; and repeating the executing and providing steps until a final verification result is determined.
Claim 6
Dependent Claim
108 words
A computer-implemented method of verifying a combinational circuit being represented by a circuit data structure comprising the steps of: executing a plurality of complete verification techniques and a plurality of supporting techniques arranged in a sequence for the combinational circuit, each of the plurality of complete verification techniques being capable of determining a verification result and each of the plurality of supporting techniques being capable of altering the circuit data structure; providing the verification result to one of subsequent complete verification techniques; providing the altered circuit data structure to one of subsequent supporting techniques; and repeating the executing and providing steps until a final verification result is determined.
Claim 7
Dependent Claim
26 words
The computer-implemented method of claim 3, wherein the executing and providing steps are repeated until a predetermined set of constraints on computer memory usage are exceeded.
Claim 8
Dependent Claim
22 words
The computer-implemented method of claim 3, wherein one of the plurality of complete verification techniques is a naive cutset based verification technique.
Claim 9
Dependent Claim
22 words
The computer-implemented method of claim 3, wherein one of the plurality of complete verification techniques is a smart cutset based verification technique.
Claim 10
Dependent Claim
24 words
The computer-implemented method of claim 3, wherein one of the plurality of complete verification techniques is an automatic test pattern generation based verification technique.
Claim 11
Dependent Claim
92 words
The computer-implemented method of claim 3, wherein the plurality of complete verification techniques include a first one of the complete verification techniques is a smart cutset based verification technique and a second one of the complete verification techniques is an automatic test pattern generation based verification technique, and further comprising the steps of performing the smart cutset based verification technique followed by the automatic test pattern generation technique and repeating performance of the smart cutset based verification technique and the automatic test pattern generation technique until a final verification result is determined.
Claim 12
Dependent Claim
81 words
The computer-implemented method of claim 3, wherein the plurality of complete verification techniques and the plurality of supporting techniques include a first technique in the sequence which is weaker than a second, succeeding technique in the sequence, weakness being empirically determined on a sample set of benchmark circuits similar to the combinational circuit wherein computational time and memory space requirements for verification of the sample set of benchmark circuits according to the first technique are less than for the second technique.
Claim 13
Dependent Claim
37 words
The computer-implemented method of claim 3, wherein the combinational circuit is partitioned into a plurality of partitions, each partition being another combinational circuit, and the executing and providing steps operate on individual partitions of the combinational circuit.
Claim 14
Dependent Claim
21 words
The computer-implemented method of claim 3, wherein one of the plurality of supporting techniques is a subgraph isomorphism-based structural filter technique.
Claim 15
Dependent Claim
20 words
The computer-implemented method of claim 3, wherein one of the plurality of supporting techniques is a hashing-based functional filter technique.
Claim 16
Dependent Claim
20 words
The computer-implemented method of claim 3, wherein one of the plurality of supporting techniques is a random pattern generation technique.
Claim 17
Dependent Claim
22 words
The computer-implemented method of claim 3, wherein one of the plurality of supporting techniques is a binary decision diagram (BDD) partitioning technique.
Claim 18
Dependent Claim
24 words
The computer-implemented method of claim 3, wherein one of the plurality of supporting techniques is an observability don't care (ODC) and learning-based resynthesis technique.
Claim 19
Dependent Claim
27 words
The computer-implemented method of claim 3, wherein the executing and providing steps are repeated until a predetermined set of constraints on computer execution time usage are exceeded.
Claim 20
Dependent Claim
21 words
The computer-implemented method of claim 3, wherein the executing and providing steps are repeated until the final verification result is determined.
Claim 21
Dependent Claim
23 words
The computer-implemented method of claim 3, wherein the executing and providing steps are repeated until the resultant altered circuit data structure is determined.
Claim 22
Dependent Claim
117 words
The computer-implemented method of claim 3, wherein the plurality of complete verification techniques include a first one of the complete verification techniques is a smart cutset based verification technique and a second one of the complete verification techniques is an automatic test pattern generation based verification technique, and further comprising the steps of performing the smart cutset based verification technique followed by the automatic test pattern generation technique and repeating performance of the smart cutset based verification technique and the automatic test pattern generation technique until the plurality of complete verification techniques exceed a predetermined maximum set of resources defined in terms of space, time, or number of backtracks used in the automatic test pattern generation technique.
Claim 23
Independent Claim
198 words
A method for increasing similarities between a pair of circuits and rendering the circuits easier to be verified by creating a new circuit, the circuits being comprised of a plurality of logic gates, the method comprising the steps of: associating each logic gate with a set of corresponding technology decompositions for every gate of each of the pair of circuits; simulating each logic gate of the circuits for each of the associated technology decompositions with a common set of Boolean assignments made to primary input variables of the circuits to produce signatures for each gate in each of the associated technology decompositions; associating one of the technology decompositions with each logic gate of each circuit, with each technology decomposition chosen such that after application of the technology decompositions, primitive logic gates in the two circuits have associated signatures such that when the signatures of the gates of the two decomposed circuits are compared, a highest number of pairs of gates with equivalent or complemented signatures are obtained; and creating the new circuit in terms of primitive logic gates by replacing each logic gate in the pair of circuits with the technology decompositions associated in the second associating step.
Claim 24
Independent Claim
198 words
A method for increasing similarities between a pair of circuits and rendering the circuits easier to be verified by creating a new circuit, the circuits being comprised of a plurality of logic gates, the method comprising the steps of: associating each logic gate with a set of corresponding technology decompositions for every gate of each of the pair of circuits; simulating each logic gate of the circuits for each of the associated technology decompositions with a common set of Boolean assignments made to primary input variables of the circuits to produce signatures for each gate in each of the associated technology decompositions; associating one of the technology decompositions with each logic gate of each circuit, with each technology decomposition chosen such that after application of the technology decompositions, primitive logic gates in the two circuits have associated signatures such that when the signatures of the gates of the two decomposed circuits are compared, a highest number of pairs of gates with equivalent or complemented signatures are obtained; and creating the new circuit in terms of primitive logic gates by replacing each logic gate in the pair of circuits with the technology decompositions associated in the second associating step.
Claim 25
Independent Claim
108 words
A system for analyzing a combinational circuit represented by a circuit data structure comprising: means for executing a plurality of complete analysis techniques and a plurality of supporting techniques arranged in a sequence for the combinational circuit, each of the plurality of complete verification techniques being capable of determining an analysis result and each of the plurality of supporting techniques being capable of altering the circuit data structure, for passing the analysis result to one of subsequent complete analysis techniques in the sequence, for passing the altered circuit data structure to one of the supporting techniques in the sequence, and for providing a resultant altered circuit data structure.
Claim 26
Independent Claim
108 words
A system for analyzing a combinational circuit represented by a circuit data structure comprising: means for executing a plurality of complete analysis techniques and a plurality of supporting techniques arranged in a sequence for the combinational circuit, each of the plurality of complete verification techniques being capable of determining an analysis result and each of the plurality of supporting techniques being capable of altering the circuit data structure, for passing the analysis result to one of subsequent complete analysis techniques in the sequence, for passing the altered circuit data structure to one of the supporting techniques in the sequence, and for providing a resultant altered circuit data structure.
Claim 27
Dependent Claim
110 words
A computer-implemented method of analyzing a combinational circuit being represented by a circuit data structure comprising the steps of: executing a plurality of complete analysis techniques and a plurality of supporting techniques arranged in a sequence for the combinational circuit, each of the plurality of complete verification techniques being capable of determining an analysis result and each of the plurality of supporting techniques being capable of altering the circuit data structure; providing the analysis result to one of the subsequent complete analysis techniques; providing the altered circuit data structure to one of the subsequent supporting techniques; and repeating the executing and providing steps until a final analysis result is determined.
Claim 28
Dependent Claim
110 words
A computer-implemented method of analyzing a combinational circuit being represented by a circuit data structure comprising the steps of: executing a plurality of complete analysis techniques and a plurality of supporting techniques arranged in a sequence for the combinational circuit, each of the plurality of complete verification techniques being capable of determining an analysis result and each of the plurality of supporting techniques being capable of altering the circuit data structure; providing the analysis result to one of the subsequent complete analysis techniques; providing the altered circuit data structure to one of the subsequent supporting techniques; and repeating the executing and providing steps until a final analysis result is determined.
Claim 29
Dependent Claim
26 words
The computer-implemented method of claim 22, wherein the executing and providing steps are repeated until a predetermined set of constraints on computer memory usage are exceeded.
Claim 30
Dependent Claim
84 words
The computer-implemented method of claim 22, wherein of the plurality of complete verification techniques and each of the plurality of supporting techniques include a first technique in the sequence which is weaker than a second, succeeding technique in the sequence, weakness being empirically determined on a sample set of benchmark circuits similar to the combinational circuit wherein computational time and memory space requirements for analysis of the sample set of benchmark circuits according to the first technique are less than for the second technique.
Claim 31
Dependent Claim
26 words
The computer-implemented method of claim 22, wherein the executing and providing steps are repeated until a predetermined set of constraints on computer memory usage are exceeded.
Claim 32
Dependent Claim
21 words
The computer-implemented method of claim 22, wherein the executing and providing steps are repeated until the final analysis result is determined.
Claim 33
Dependent Claim
23 words
The computer-implemented method of claim 22, wherein the executing and providing steps are repeated until the resultant altered circuit data structure is determined.
Claim 34
Dependent Claim
112 words
A computer-implemented method of analyzing a combinational circuit being represented by a circuit data structure comprising the steps of: executing a plurality of complete analysis techniques and a plurality of supporting techniques arranged in a sequence for the combinational circuit, each of the plurality of complete verification techniques being capable of determining an analysis result and each of the plurality of supporting techniques being capable of altering the circuit data structure; providing the analysis result to one of the subsequent complete analysis techniques; providing the altered circuit data structure to one of the subsequent supporting techniques; and repeating the executing and providing steps until a resultant altered circuit data structure is determined.
Claim 35
Dependent Claim
112 words
A computer-implemented method of analyzing a combinational circuit being represented by a circuit data structure comprising the steps of: executing a plurality of complete analysis techniques and a plurality of supporting techniques arranged in a sequence for the combinational circuit, each of the plurality of complete verification techniques being capable of determining an analysis result and each of the plurality of supporting techniques being capable of altering the circuit data structure; providing the analysis result to one of the subsequent complete analysis techniques; providing the altered circuit data structure to one of the subsequent supporting techniques; and repeating the executing and providing steps until a resultant altered circuit data structure is determined.
Claim 36
Dependent Claim
197 words
A computer-implemented method of verifying a pair of combinational circuits represented by circuit data structures comprising the steps of: (a) simulating, using random pattern simulation, the circuit data structures to produce candidate lists; (b) pruning the candidate lists; (c) partitioning the pair of combinational circuits into a plurality of partitions; (d) applying a macro-filter to at least one of the plurality of partitions, the macro-filter comprising at least a naive cutset based verification technique, a smart cutset based verification technique, and an automatic test pattern generation verification technique; (e) re-synthesizing the at least one of the plurality of partitions using an observability don't care (ODC) and learning-based resynthesis technique; (f) applying the random pattern simulation to select candidates from the candidate lists pruned for equivalence checking and applying the macro-filter to the at least one of the plurality of partitions resynthesized; (g) checking the at least one of the plurality of partitions resynthesized using binary decision diagram (BDD) partitioning; (h) repeating steps (d)-(g) until resultant circuit data structures are determined for the at least one of the plurality of partitions; and (i) repeating steps (d)-(h) for all the plurality of partitions of the pair of combinational circuits.
Claim 37
Dependent Claim
197 words
A computer-implemented method of verifying a pair of combinational circuits represented by circuit data structures comprising the steps of: (a) simulating, using random pattern simulation, the circuit data structures to produce candidate lists; (b) pruning the candidate lists; (c) partitioning the pair of combinational circuits into a plurality of partitions; (d) applying a macro-filter to at least one of the plurality of partitions, the macro-filter comprising at least a naive cutset based verification technique, a smart cutset based verification technique, and an automatic test pattern generation verification technique; (e) re-synthesizing the at least one of the plurality of partitions using an observability don't care (ODC) and learning-based resynthesis technique; (f) applying the random pattern simulation to select candidates from the candidate lists pruned for equivalence checking and applying the macro-filter to the at least one of the plurality of partitions resynthesized; (g) checking the at least one of the plurality of partitions resynthesized using binary decision diagram (BDD) partitioning; (h) repeating steps (d)-(g) until resultant circuit data structures are determined for the at least one of the plurality of partitions; and (i) repeating steps (d)-(h) for all the plurality of partitions of the pair of combinational circuits.
Claim 38
Dependent Claim
178 words
A computer-implemented method of analyzing a pair of combinational circuits represented by circuit data structures comprising the steps of: (a) simulating, using random pattern simulation, the circuit data structures to produce candidate lists; (b) pruning the candidate lists; (c) partitioning the pair of combinational circuits into a plurality of partitions; (d) applying a macro-filter to at least one of the plurality of partitions, the macro-filter comprising a circuit analysis technique; (e) re-synthesizing the at least one of the plurality of partitions using an observability don't care (ODC) and learning-based resynthesis technique; (f) applying random pattern simulation to select candidates from the candidate lists pruned for equivalence checking and applying the macro-filter to the at least one of the plurality of partitions resynthesized; (g) checking the at least one of the plurality of partitions resynthesized using binary decision diagram (BDD) partitioning; (h) repeating steps (d)-(g) until resultant circuit data structures are determined for the at least one of the plurality of partitions; and (i) repeating steps (d)-(h) for all the plurality of partitions of the pairs of combinational circuits.
Claim 39
Dependent Claim
178 words
A computer-implemented method of analyzing a pair of combinational circuits represented by circuit data structures comprising the steps of: (a) simulating, using random pattern simulation, the circuit data structures to produce candidate lists; (b) pruning the candidate lists; (c) partitioning the pair of combinational circuits into a plurality of partitions; (d) applying a macro-filter to at least one of the plurality of partitions, the macro-filter comprising a circuit analysis technique; (e) re-synthesizing the at least one of the plurality of partitions using an observability don't care (ODC) and learning-based resynthesis technique; (f) applying random pattern simulation to select candidates from the candidate lists pruned for equivalence checking and applying the macro-filter to the at least one of the plurality of partitions resynthesized; (g) checking the at least one of the plurality of partitions resynthesized using binary decision diagram (BDD) partitioning; (h) repeating steps (d)-(g) until resultant circuit data structures are determined for the at least one of the plurality of partitions; and (i) repeating steps (d)-(h) for all the plurality of partitions of the pairs of combinational circuits.
Claim 40
Dependent Claim
178 words
A computer-implemented method of analyzing a pair of combinational circuits represented by circuit data structures comprising the steps of: (a) simulating, using random pattern simulation, the circuit data structures to produce candidate lists; (b) pruning the candidate lists; (c) partitioning the pair of combinational circuits into a plurality of partitions; (d) applying a macro-filter to at least one of the plurality of partitions, the macro-filter comprising a circuit analysis technique; (e) re-synthesizing the at least one of the plurality of partitions using an observability don't care (ODC) and learning-based resynthesis technique; (f) applying random pattern simulation to select candidates from the candidate lists pruned for equivalence checking and applying the macro-filter to the at least one of the plurality of partitions resynthesized; (g) checking the at least one of the plurality of partitions resynthesized using binary decision diagram (BDD) partitioning; (h) repeating steps (d)-(g) until a final analysis result is determined for the at least one of the plurality of partitions; and (i) repeating steps (d)-(h) for all the plurality of partitions of the pairs of combinational circuits.
Claim 41
Dependent Claim
178 words
A computer-implemented method of analyzing a pair of combinational circuits represented by circuit data structures comprising the steps of: (a) simulating, using random pattern simulation, the circuit data structures to produce candidate lists; (b) pruning the candidate lists; (c) partitioning the pair of combinational circuits into a plurality of partitions; (d) applying a macro-filter to at least one of the plurality of partitions, the macro-filter comprising a circuit analysis technique; (e) re-synthesizing the at least one of the plurality of partitions using an observability don't care (ODC) and learning-based resynthesis technique; (f) applying random pattern simulation to select candidates from the candidate lists pruned for equivalence checking and applying the macro-filter to the at least one of the plurality of partitions resynthesized; (g) checking the at least one of the plurality of partitions resynthesized using binary decision diagram (BDD) partitioning; (h) repeating steps (d)-(g) until a final analysis result is determined for the at least one of the plurality of partitions; and (i) repeating steps (d)-(h) for all the plurality of partitions of the pairs of combinational circuits.
Claim 42
Dependent Claim
26 words
The computer-implemented method of claim 31, further comprising the step of applying a functional filter to the circuit data structures prior to performing the simulating step.
Claim 43
Dependent Claim
26 words
The computer-implemented method of claim 32, further comprising the step of applying a structural filter to the circuit data structures prior to applying the functional filter.
Claim 44
Dependent Claim
25 words
The computer-implemented method of claim 33, further comprising the step of performing targeted decomposition of the circuit data structures prior to applying the structural filter.
Claim 45
Dependent Claim
82 words
The computer-implemented method of claim 31, wherein the pruning step comprises the steps of: associating, for each gate in the pair of combinational circuits, corresponding primary outputs that each gate affects; applying random pattern simulation to determine a signature of each gate for a set of applied random simulation vectors; and assigning each pair of gates which has either the same or the complement signature and whose output lists intersect, to a group for subsequent checking of functional equivalence or functional complement.
Claim 46
Dependent Claim
197 words
A computer-implemented method of verifying a pair of combinational circuits represented by circuit data structures comprising the steps of: (a) simulating, using random pattern simulation, the circuit data structures to produce candidate lists; (b) pruning the candidate lists; (c) partitioning the pair of combinational circuits into a plurality of partitions; (d) applying a macro-filter to at least one of the plurality of partitions, the macro-filter comprising at least a naive cutset based verification technique, a smart cutset based verification technique, and an automatic test pattern generation verification technique; (e) re-synthesizing the at least one of the plurality of partitions using an observability don't care (ODC) and learning-based resynthesis technique; (f) applying the random pattern simulation to select candidates from the candidate lists pruned for equivalence checking and applying the macro-filter to the at least one of the plurality of partitions resynthesized; (g) checking the at least one of the plurality of partitions resynthesized using binary decision diagram (BDD) partitioning; (h) repeating steps (d)-(g) until a final verification result is determined for the at least one of the plurality of partitions; and (i) repeating steps (d)-(h) for all the plurality of partitions of the pair of combinational circuits.
Claim 47
Dependent Claim
197 words
A computer-implemented method of verifying a pair of combinational circuits represented by circuit data structures comprising the steps of: (a) simulating, using random pattern simulation, the circuit data structures to produce candidate lists; (b) pruning the candidate lists; (c) partitioning the pair of combinational circuits into a plurality of partitions; (d) applying a macro-filter to at least one of the plurality of partitions, the macro-filter comprising at least a naive cutset based verification technique, a smart cutset based verification technique, and an automatic test pattern generation verification technique; (e) re-synthesizing the at least one of the plurality of partitions using an observability don't care (ODC) and learning-based resynthesis technique; (f) applying the random pattern simulation to select candidates from the candidate lists pruned for equivalence checking and applying the macro-filter to the at least one of the plurality of partitions resynthesized; (g) checking the at least one of the plurality of partitions resynthesized using binary decision diagram (BDD) partitioning; (h) repeating steps (d)-(g) until a final verification result is determined for the at least one of the plurality of partitions; and (i) repeating steps (d)-(h) for all the plurality of partitions of the pair of combinational circuits.
Claim 48
Dependent Claim
26 words
The computer-implemented method of claim 36, further comprising the step of applying a functional filter to the circuit data structures prior to performing the simulating step.
Claim 49
Dependent Claim
26 words
The computer-implemented method of claim 37, further comprising the step of applying a structural filter to the circuit data structures prior to applying the functional filter.
Claim 50
Dependent Claim
25 words
The computer-implemented method of claim 38, further comprising the step of performing targeted decomposition of the circuit data structures prior to applying the structural filter.
Claim 51
Dependent Claim
66 words
The computer-implemented method of claim 36, wherein the step of applying the macro-filter comprises the steps of performing the smart cutset based verification technique followed by the automatic test pattern generation technique and repeating performance of the smart cutset based verification technique and the automatic test pattern generation technique until a final verification result is determined for the at least one of the plurality of partitions.
Claim 52
Dependent Claim
82 words
The computer-implemented method of claim 36, wherein the pruning step comprises the steps of: associating, for each gate in the pair of combinational circuits, corresponding primary outputs that each gate affects; applying random pattern simulation to determine a signature of each gate for a set of applied random simulation vectors; and assigning each pair of gates which has either the same or the complement signature and whose output lists intersect, to a group for subsequent checking of functional equivalence or functional complement.
Claim 53
Independent Claim
106 words
A system for verifying a combinational circuit represented by a circuit data structure comprising: means for executing a plurality of complete verification techniques and a plurality of supporting techniques arranged in a sequence for the combinational circuit, each of the plurality of complete verification techniques being capable of determining a verification result and each of the plurality of supporting techniques being capable of altering the circuit data structure, for passing the verification result to one of subsequent complete verification techniques in the sequence, for passing the altered circuit data structure to one of subsequent supporting techniques in the sequence, and for providing a final verification result.
Claim 54
Independent Claim
106 words
A system for verifying a combinational circuit represented by a circuit data structure comprising: means for executing a plurality of complete verification techniques and a plurality of supporting techniques arranged in a sequence for the combinational circuit, each of the plurality of complete verification techniques being capable of determining a verification result and each of the plurality of supporting techniques being capable of altering the circuit data structure, for passing the verification result to one of subsequent complete verification techniques in the sequence, for passing the altered circuit data structure to one of subsequent supporting techniques in the sequence, and for providing a final verification result.
Claim 55
Dependent Claim
31 words
The system of claim 42, wherein the executing means executes the plurality of complete verification techniques and supporting techniques until a predetermined set of constraints on computer memory usage are exceeded.
Claim 56
Dependent Claim
32 words
The system of claim 42, wherein the executing means executes the plurality of complete verification techniques and supporting techniques until a predetermined set of constraints on computer execution time usage are exceeded.
Claim 57
Dependent Claim
26 words
The system of claim 42, wherein the executing means executes the plurality of complete verification techniques and supporting techniques until the final verification result is determined.
Claim 58
Independent Claim
106 words
A system for analyzing a combinational circuit represented by a circuit data structure comprising: means for executing a plurality of complete analysis techniques and a plurality of supporting techniques arranged in a sequence for the combinational circuit, each of the plurality of complete verification techniques being capable of determining an analysis result and each of the plurality of supporting techniques being capable of altering the circuit data structure, for passing the analysis result to one of subsequent complete analysis techniques in the sequence, for passing the altered circuit data structure to one of the supporting techniques in the sequence, and for providing a final analysis result.
Claim 59
Independent Claim
106 words
A system for analyzing a combinational circuit represented by a circuit data structure comprising: means for executing a plurality of complete analysis techniques and a plurality of supporting techniques arranged in a sequence for the combinational circuit, each of the plurality of complete verification techniques being capable of determining an analysis result and each of the plurality of supporting techniques being capable of altering the circuit data structure, for passing the analysis result to one of subsequent complete analysis techniques in the sequence, for passing the altered circuit data structure to one of the supporting techniques in the sequence, and for providing a final analysis result.
Claim 60
Dependent Claim
53 words
The system of claim 46, wherein the executing means executes the complete analysis techniques and supporting techniques until a predetermined set of constraints on computer memory usage, computer execution time usage, or number of backtracks when at least one of the complete analysis techniques is an automatic test pattern generation technique, are exceeded.
Claim 61
Dependent Claim
24 words
The system of claim 46, wherein the executing means further comprises means for determining existence or absence of a fault in the combinational circuit.
Claim 62
Dependent Claim
24 words
The system of claim 46, wherein the executing means executes the complete analysis techniques and supporting techniques until the final analysis result is determined.
Claim 63
Dependent Claim
20 words
The system of claim 46, wherein the executing means further comprises means for determining timing constraints of the combinational circuit.
Claim 64
Dependent Claim
23 words
The system of claim 46, wherein the executing means further comprises means for determining minimum cost engineering change solutions for the combinational circuit.
Claim 65
Dependent Claim
19 words
The system of claim 46, wherein the executing means further comprises means for determining correctness of a sequential circuit.
References Cited (Backward Citations)
US5243538A
Cited
US5243538B1
Cited
US5469367A
Cited
US5671399A
Cited
US5649165A
Cited
US5787006A
Cited
USPTO Annuity & Maintenance Windows
| Annuity Stage | Window Opens | Payment Deadline | Surcharge Period Until | Estimated Fee | Status |
|---|---|---|---|---|---|
| 3.5 Years (Year 4) | 2003-07-11 | 2004-01-10 | 2004-07-11 | $2000.00 | Window Closed / Lapsed |
| 7.5 Years (Year 8) | 2007-07-11 | 2008-01-10 | 2008-07-11 | $3760.00 | Window Closed / Lapsed |
| 11.5 Years (Year 12) | 2011-07-11 | 2012-01-10 | 2012-07-11 | $7700.00 | Window Closed / Lapsed |