A method for implementing an integrated circuit using integrated circuit design tools (420, 520) running on computing equipment, comprising: retiming an original circuit design of the integrated circuit to produce a retimed circuit design for the integrated circuit, wherein the original circuit design comprises circuit elements and wherein retiming the original circuit comprises: representing any two circuit elements u and v which are connected and have registers between them as a retiming graph having nodes u and v and an edge that connects node u to node v, wherein the edge has a weight W o which reflects the number of registers between nodes u and v wherein nodes u and v maintain retiming variables r u and r v associated with the movement of registers across nodes u and v; wherein all non-justifiable circuit elements are modeled as separate nodes; updating the graph with a new weight W new for the edge after moving registers across nodes u and/or v using the following equation: w new = r v + w o − r u determining a count value c for a clock domain, wherein the original circuit design is properly reset using an initialization sequence, and wherein the retimed circuit is reset using a delayed initialization sequence that is delayed with respect to the initialization sequence by c clock cycles for the clock domain; and verifying that the original circuit design using the initialization sequence and the retimed circuit using the c-cycle delayed initialization sequence are sequentially equivalent, wherein verifying that the original circuit design and the retimed circuit design are c-cycle sequentially equivalent comprises performing rewind structural verification, wherein performing the rewind structural verification comprises retiming the retimed circuit design back to the original circuit design, wherein retiming the retimed circuit comprises solving the equation W new = r v + w o - r u for each edge in the graph, where W new is now substituted by w o of the original circuit and where w o is substituted by W retimed of the retimed circuit with the constraint r i ≤ c, wherein r i designates a retiming variable associated with movement of registers across a non-justifiable circuit element i. retiming an original circuit design of the integrated circuit to produce a retimed circuit design for the integrated circuit, wherein the original circuit design comprises circuit elements and wherein retiming the original circuit comprises: representing any two circuit elements u and v which are connected and have registers between them as a retiming graph having nodes u and v and an edge that connects node u to node v, wherein the edge has a weight W o which reflects the number of registers between nodes u and v wherein nodes u and v maintain retiming variables r u and r v associated with the movement of registers across nodes u and v; wherein all non-justifiable circuit elements are modeled as separate nodes; updating the graph with a new weight W new for the edge after moving registers across nodes u and/or v using the following equation: w new = r v + w o − r u representing any two circuit elements u and v which are connected and have registers between them as a retiming graph having nodes u and v and an edge that connects node u to node v, wherein the edge has a weight W o which reflects the number of registers between nodes u and v wherein nodes u and v maintain retiming variables r u and r v associated with the movement of registers across nodes u and v; wherein all non-justifiable circuit elements are modeled as separate nodes; updating the graph with a new weight W new for the edge after moving registers across nodes u and/or v using the following equation: w new = r v + w o − r u determining a count value c for a clock domain, wherein the original circuit design is properly reset using an initialization sequence, and wherein the retimed circuit is reset using a delayed initialization sequence that is delayed with respect to the initialization sequence by c clock cycles for the clock domain; and verifying that the original circuit design using the initialization sequence and the retimed circuit using the c-cycle delayed initialization sequence are sequentially equivalent, wherein verifying that the original circuit design and the retimed circuit design are c-cycle sequentially equivalent comprises performing rewind structural verification, wherein performing the rewind structural verification comprises retiming the retimed circuit design back to the original circuit design, wherein retiming the retimed circuit comprises solving the equation W new = r v + w o - r u for each edge in the graph, where W new is now substituted by w o of the original circuit and where w o is substituted by W retimed of the retimed circuit with the constraint r i ≤ c, wherein r i designates a retiming variable associated with movement of registers across a non-justifiable circuit element i.