Method and Apparatus for Reducing Constraints During Rewind Structural Verification of Retimed Circuits

A method for performing rewind functional verification, comprising:

• identifying random variables that model retiming labels representing a number and direction of register movement relative to a node on a retiming graph for a retimed design;
• identifying an edge on a retiming graph for an original design and a retimed design;
• designating random variables for nodes associated with the edge to be in an equivalence class in response to determining that a number of registers on the edge is unchanged after register retiming;
• identifying a next edge on the retiming graph for the original design and the retimed design that is connected to a node having a random variable in the equivalence class;
• designating random variables for nodes associated with the next edge to be in the equivalence class in response to determining that a number of registers on the next edge is unchanged after the register retiming;
• substituting the random variables in the equivalence class with a new single variable;
• and
• determining whether the retimed design is structurally correct in response to identifying solutions for remaining random variables after the substituting.

A non-transitory computer readable medium including a sequence of instructions stored thereon for causing a computer to execute a method for performing rewind functional verification, comprising:

• identifying state variables that model a number of registers on each edge of a retiming graph for an original design and a retimed design;
• identifying random variables that model retiming labels representing a number and direction of register movement relative to a node on a retiming graph for the retimed design;
• and
• identifying a retiming constraint for each edge on the retiming graph for the design, wherein the retiming constraint reflects a relationship between the state variables and the random variables;
• and
• substituting a random variable that models a retiming label at a source of an edge for a random variable that models a retiming label at a sink of the edge when a number of registers on the edge is unchanged after register retiming.