Method for circuit verification and multi-level circuit optimization based on structural implications

• US 5,526,514 A
• Filed: 06/21/1994
• Issued: 06/11/1996
• Est. Priority Date: 06/21/1994
• Status: Expired due to Fees

• Current Assignee: Dhiraj Pradhan, Wolfgang Kunz
• Original Assignee: Dhiraj Pradhan, Wolfgang Kunz
• Inventors: Kunz, Wolfgang, Pradhan, Dhiraj
• Primary Examiner(s): Teska, Kevin J.
• Assistant Examiner(s): NGUYEN, TAN QUANG
• Application Number:
  US08/263,721
• Time in Patent Office: 721 Days
• Field of Search: 364/489, 364/490, 364/491, 395/500, 371/11.1, 371/11.2, 371/23, 371/27, 371/67.1, 371/71
• US Class Current: 716/103
• CPC Class Codes: G06F 30/30 Circuit design
• CPC Class Codes: G06F 30/33 Design verification, e.g. functional simulation or model checking
• CPC Class Codes: G06F 30/3308 using simulation

Abstract

A method for verifies that two integrated circuits are functionally equivalent by extracting equivalencies between internal nodes of the two circuits. Values are assigned to internal nodes in the first circuit and the effects of the assignments are determined in the rest of the first circuit and the second circuit. These effects, or implications, are analyzed to find internal equivalents between the first and second circuit. These steps are repeated with different values assigned to different nodes in the first circuit. The set of stored implications is used to determine if the two circuits are functionally equivalent.

A method is also disclosed for using the equivalencies, or indirect implications determined above to remove redundancies from the second circuit using a set of predetermined transformations. Based on an indirect implication a particular transform is selected and applied to the second circuit. This transformation is intended to create redundancies elsewhere in the circuit that can be removed thus optimizing the second circuit.

Claims

1. A method for verifying that a first logic circuit is equivalent to a second logic circuit, the first logic circuit having a first plurality of inputs and a first plurality of internal nodes and the second logic circuit having a second plurality of inputs and a second plurality of internal nodes, the method comprising the steps of:

a) coupling the first plurality of inputs to the second plurality of inputs;

b) assigning a first combination of signal values to a combination of at least one of the first plurality of internal nodes, such that the corresponding assignment creates an unjustified signal in said node;

c) determining, through logic implications, signal values for the first plurality and second plurality of internal nodes not included in the combination of some or all the first plurality of internal nodes such that the signal values result in conditions which are consistent with the first combination of signal values in the the combination of at least one of the first plurality of internal nodes;

d) extracting a resulting combination of signal values from a second combination of at least one of the second plurality of internal nodes corresponding to the first combination signal values;

e) storing the resulting combination of signal values in an internal memory;

f) repeating the steps of assigning, determining, extracting and storing for a different combination of at least one of the first plurality of internal nodes of the first and the second circuit to create a list of indirect implications; and

g) using the list of indirect implications to verify that the first and second circuits are equivalent based on a set of pre-stored signal relationships in the internal memory.

2. The method of claim 1 and further comprising the step of:

h) finding internal signals in the second circuit that are functionally equivalent to internal signals of the first circuit.

3. The method of claim 1, and further comprising prior to step (f) the step of establishing a user defined recursion level for the repeating step.

4. A method for optimizing a circuit, comprising the steps of:

storing predetermined circuit transformations for optimizing the circuit;

making the circuit prime and irredundant;

resetting all nodes of the circuit to pre-determined values;

assigning a signal value to a node of the circuit such that the assignment creates an unjustified signal in said nodes;

measuring the signal values of the other nodes in the circuit to derive an indirect implication for the node using recursive learning;

modifying the circuit based on the indirect implication; and

repeating the steps of assigning, measuring and modifying on the different nodes of the circuit so as to optimize the circuit.

5. The method of claim 4, wherein said step of making the circuit prime and irredundant comprises the steps of:

determining nodes of the circuit which are constant for all input values; and

assigning a predetermined value to the node to isolate the node.

6. The method of claim 4, wherein said step of apply circuit transformations comprises the steps of:

applying the transformation y'"'"'=y₁ +ƒ

when the implication y=0 ƒ

=1 is true;

applying the transformation y'"'"'=y₀ +ƒ

when the implication y=0 ƒ

=0 is true;

applying the transformation y'"'"'=ƒ

y₁ when the implication y=1 ƒ

=1 is true;

applying the transformation y'"'"'=ƒ

y₀ when the implication y=1 ƒ

=0 is true; and

wherein y,y₁,y₀ and f are logic functions and y'"'"' is a functionally equivalent transformation of the function y.