Method and system for sequential netlist reduction through trace-containment

A software product comprising a non-transitory machine readable medium including a program of instructions for identifying trace-containment for a sequential circuitry design netlist by execution of instructions, wherein the program of instructions upon being executed on a computer causes the computer to perform activities comprising:

• identify, by the execution of said instructions, a cut of the netlist comprising an input i;
• enumerate, by the execution of said instructions, a set of mismatch traces;
• derive, by the execution of said instructions, a set of inputs ‘J’ from the mismatch traces for equivalence checking to detect trace containment;
• perform, by the execution of said instructions, time-bounded unfolding of a cofactored version of the cut reflecting sequential cofactor for the input i and temporal uncorrelation constraints for the set of inputs ‘J’;
• determine, by the execution of said instructions, whether there is trace containment;
• in response to detecting trace containment, recognize, by the execution of said instructions, a constraining relation over the set of inputs ‘J’;
• and
• seek, by the execution of said instructions, to prove sequential equivalence of said cut subject to the constraining relation.

A computer system configured for identifying trace-containment for a sequential circuitry design netlist, the system comprising:

• input means for receiving the circuitry design netlist, a cut of the netlist being identified that comprises an input i;
• memory configured to store an enumerated set of mismatch traces;
• means for deriving a set of inputs ‘J’ from the mismatch traces for equivalence checking to detect trace containment;
• a processor suitably disposed to execute instructions for performing time-bounded unfolding of a cofactored version of the cut reflecting sequential cofactor for the input i and temporal uncorrelation constraints for the set of inputs ‘J’;
• means for determining whether there is trace containment, and in response to detecting trace containment, recognizing a constraining relation over the set of inputs ‘J’;
• and
• wherein said processor is suitably disposed to execute instructions for seeking to prove sequential equivalence of said cut subject to the constraining relation.