Method for verification of combinational circuits using a filtering oriented approach

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.

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.

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.

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.

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.

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.

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.

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.