Method and apparatus for verifying initial state equivalence of changed registers in retimed circuits

A method for designing a system on a target device, comprising:

• performing register retiming on an initial design to generate a retimed design;
• determining whether the retimed design is structurally correct by performing retiming on the retimed design, and determining whether performing register retiming on the retimed design results in the initial design by generating a first retiming graph of the initial design, by generating a second retiming graph of the retimed design, wherein the first and second retiming graphs comprise vertices representing combinatorial gates and edges representing connections between the combinatorial gates, each of the edges comprising an edge weight that represents a number of flip-floDs on that edge, and by computing retiming labels of each of the vertices based on the edge weights of the first and second retiming graphs;
• determining whether unchanged registers in the retimed design have initial states that are correct in response to determining whether the retimed design is structurally correct by representing the initial states for the unchanged registers in the initial design and the retimed design as arrays of values, by computing indices for each of the arrays using the retiming labels, and by comparing values of the unchanged registers in one of the arrays representing the retimed design and in one of the arrays representing the initial design to determine equivalence of the initial states of the unchanged registers;
• identifying compare points in the initial design and the retimed design that reflect behavior of changed registers by using the retiming labels that reflect a number and direction of register movement relative to a node in the retimed design;
• performing bounded seauential logic simulation within a time frame, wherein the time frame is determined from a maximum absolute value of the retiming labels;
• determining whether the changed registers in the retimed design have initial states that are correct by comparing signal values at the compare points from the bounded seauential logic simulation in response to determining that the unchanged registers in the retimed design have initial states that are correct;
• generating a data file that describes the retimed design for the system in response to determining that the changed and unchanged registers in the retimed design have correct initial states;
• and
• programming the target device with the data file to physically transform components on the target device to implement the system.

A non-transitory computer readable medium including a sequence of instructions stored thereon for causing a computer to execute a method for designing a system on a target device, comprising:

• performing register retiming on an original design to generate a retimed design of the system;
• generating a first retiming graph of the original design;
• generating a second retiming graph of the retimed design, wherein the first and second retiming graphs comprise vertices representing combinatorial gates and edges representing connections between the combinatorial gates, and wherein each of the edges comprises an edge weight that represents a number of flip-flops on that edge;
• computing retiming labels of each of the edges from the edge weights of the first and second retiming graphs during verification of structural correctness of the retimed design;
• identifying compare points from the original design and the retimed design where signal values reflect initial states of one or more flip-flops, wherein the compare points are identified from the retiming labels that reflect a number and direction of register movement relative to a node on the system after register retiming;
• performing bounded sequential logic simulation within a time frame, wherein the time frame is determined by a maximum absolute value of the retiming labels;
• determining whether changed flip-flops in the retimed design have initial states that are correct by comparing signal values at the compare points from the bounded sequential logic simulation;
• generating a data file that describes the retimed design for the system in response to determining that the changed flip-flops in the retimed design have correct initial states;
• and
• programming the target device with the data file to physically transform components on the target device to implement the system.