Trace equivalence identification through structural isomorphism detection with on the fly logic writing

A method for performing trace equivalent identification by structural isomorphism detection, the method comprising:

• synthesizing a first netlist into a second netlist, the second netlist including two-input AND gates, inversions, inputs, constants, and registers;
• constructing a third netlist from the second netlist, the third netlist being a pseudo-canonical netlist that uses calls to algorithms for constructing a netlist for gate g1 and for constructing a netlist for gate g2, where g1 and g2 are gates in the second netlist;
• and
• performing an isomorphism check of gates g1 and g2, the isomorphism check mapping gate g1 to an inverted gate g1 and inverting a mapped input to inverted gate g1, the isomorphism check mapping gate g2 to an inverted gate g2 and inverting a mapped input to inverted gate g2;
• wherein an algorithm for constructing the third netlist for gate g1 includes:
• identifying a high-level type gate, the high-level type gate being used to represent a local function of g1;
• collecting input gates to be connected to inputs of the high-level type gate used to represent the local function of g1;
• reducing the input gates collected in the collecting step by using semantics-preserving rules;
• updating the high-level type gate to alter the type of the high-level type gate to an updated type;
• creating a second gate having the updated type;
• connecting the reduced inputs gates collected in the collecting step to the second gate;
• and
• replacing the high-level type gate with the second gate.