# US 10,372,850 B2 · Methods for verifying retimed circuits with delayed initialization > Agents: this data is available as JSON from the patentgrep API and MCP server — see https://patentgrep.com/llms.txt - Number: US 10,372,850 B2 - Document ID: US10372850B2 - Status: Granted - Kind: B2 - Application number: 15/354,809 - Filed: 2016-11-17 - Published: 2018-05-17 - Granted: 2019-08-06 - Earliest claimed: 2016-11-17 - Assignees: Intel Corporation - Applicants: Intel Corporation - Inventors: Mahesh A. Iyer - Web page: https://patentgrep.com/patent/US10372850B2 ## CPC - G06F 30/343: Logical level - G06F 1/24: Resetting means - G06F 30/327: Logic synthesis; Behaviour synthesis, e.g. mapping logic, HDL to netlist, high-level language to RTL or netlist - G06F 30/3312: Timing analysis - G06F 30/3323: using formal methods, e.g. equivalence checking or property checking - G06F 30/34: for reconfigurable circuits, e.g. field programmable gate arrays [FPGA] or programmable logic devices [PLD] - G06F 30/394: Routing (G06F30/396 takes precedence) - G06F 30/3947: global - G06F 30/398: Design verification or optimisation, e.g. using design rule check [DRC], layout versus schematics [LVS] or finite element methods [FEM] (optical proximity correction [OPC] design processes G03F1/36) - G06F 2111/04: Constraint-based CAD - G06F: ELECTRIC DIGITAL DATA PROCESSING (computer systems based on specific computational models G06N) ## Abstract Circuit design computing equipment may perform register moves within a circuit design. When moving the registers, counter values may be maintained for non-justifiable elements. The counter values may be maintained and updated on a per element, per clock domain basis to account for register moves across the corresponding non-justifiable elements. The maximum counter value for each clock domain may be chosen as an adjustment value that is used to generate a sequence for resetting the modified circuit design after the register moves. The adjustment value may be bound by a user-specified maximum value. This retiming operation may also be verified by performing rewind verification. The rewind verification involves retiming the retimed circuit back to the original circuit, while respecting the counter values. If verification succeeds, the circuit design may be reset using a smaller adjustment value. If verification fails, a correct counter value may be suggested for each clock domain. ## Claims ### Claim 1 A method for implementing an integrated circuit using integrated circuit design tools running on logic design computing equipment, comprising: with the logic design computing equipment, retiming an original circuit design of the integrated circuit to produce a retimed circuit design for the integrated circuit; with the logic design computing equipment, determining a count value c for a clock domain, wherein the original circuit design is properly resettable using an initialization sequence, and wherein the retimed circuit is resettable using a delayed initialization sequence that is delayed with respect to the initialization sequence by c clock cycles for the clock domain; and with the logic design computing equipment, verifying that the original circuit design using the initialization sequence and the retimed circuit using the c-cycle delayed initialization sequence are sequentially equivalent. ### Claim 2 (depends on 1) The method of claim 1, wherein verifying that the original circuit design and the retimed circuit design are c-cycle sequentially equivalent comprises performing rewind structural verification. ### Claim 3 (depends on 2) The method of claim 2, wherein performing the rewind structural verification comprises retiming the retimed circuit design back to the original circuit design, wherein each routing path in the original circuit design is assigned an original weighting factor based on a number of registers in that routing path of the original circuit design, wherein each routing path in the retimed circuit design is assigned a retimed weighting factor based on a number of registers in that routing path of the retimed circuit design, and wherein the original weighting factor and the retimed weighting factor are known prior to performing the rewind structural verification. ### Claim 4 (depends on 2) The method of claim 2, further comprising: with the logic design computing equipment, taking into account the count value c while performing the rewind structural verification, wherein performing the rewind structural verification comprises solving for retiming variables that are constrained to be less than or equal to the count value c. ### Claim 5 (depends on 4) The method of claim 4, further comprising: with the logic design computing equipment, in response to determining that the original circuit design and the retimed circuit design are not c-cycle sequentially equivalent, attempting to perform the rewind structural verification without taking into account the count value c. ### Claim 6 (depends on 5) The method of claim 5, further comprising: with the logic design computing equipment, if the rewind structural verification succeeds without taking into account the count value c, identifying a new count value cverify that is different than the count value c; and with the logic design computing equipment, updating the delayed initialization sequence such that the retimed circuit design is resettable using an updated delayed initialization sequence that is delayed with respect to the initialization sequence by cverify clock cycles. ### Claim 7 (depends on 5) The method of claim 5, further comprising: with the logic design computing equipment, if the rewind structural verification fails without taking into account the count value c, reporting a verification error and identifying a minimal set of constraints that might have caused the failure. ### Claim 8 (depends on 2) The method of claim 2, further comprising: with the logic design computing equipment, taking into account a maximum number of registers on the integrated circuit while performing the rewind structural verification. ### Claim 9 (depends on 1) The method of claim 1, further comprising: with the logic design computing equipment, in response to confirming that the original circuit design and the retimed circuit design are c-cycle sequentially equivalent, identifying a new count value cverify that is different than the count value c. ### Claim 10 (depends on 9) The method of claim 9, further comprising: with the logic design computing equipment, updating the delayed initialization sequence such that the retimed circuit design is resettable using an updated delayed initialization sequence that is delayed with respect to the initialization sequence by cverify clock cycles. ### Claim 11 A method of configuring an integrated circuit by operating an integrated circuit design tool implemented on logic design computing equipment, comprising: with the logic design computing equipment, receiving an original circuit design; with the logic design computing equipment, retiming the original circuit design to produce a retimed circuit design; with the logic design computing equipment, determining a count value c for a clock domain, wherein the original circuit design is properly resettable using an initialization sequence, and wherein the retimed circuit is resettable using a delayed initialization sequence that is delayed with respect to the initialization sequence by c clock cycles for the clock domain; and with the logic design computing equipment, determining whether the retimed circuit design is c-cycle sequentially equivalent to the original circuit design by performing rewind structural verification. ### Claim 12 (depends on 11) The method of claim 11, wherein performing the rewind structural verification comprises retiming the retimed circuit design back to the original circuit design. ### Claim 13 (depends on 11) The method of claim 11, wherein performing the rewind structural verification comprises using an equation solver to compute retiming variables for each combinational element in the retimed circuit design while taking into account the count value c. ### Claim 14 (depends on 13) The method of claim 13, wherein the computed retiming variables solved using the equation solver are constrained to be less than or equal to the count value c. ### Claim 15 (depends on 13) The method of claim 13, further comprising: with the logic design computing equipment, in response to determining that the retimed circuit design is not sequentially equivalent to the original circuit design, using the equation solver to re-compute the retiming variables without using the count value c as a constraint. ### Claim 16 A non-transitory computer-readable storage medium including instructions executable by circuit design computing equipment, the instructions comprising: with the circuit design computing equipment, retiming an original circuit design to produce a retimed circuit design; with the circuit design computing equipment, determining a count value c for delaying a reset sequence for the retimed circuit design; and with the circuit design computing equipment, verifying that the retimed circuit design is c-cycle sequentially equivalent to the original circuit design by performing structural rewind verification. ### Claim 17 (depends on 16) The non-transitory computer-readable storage medium of claim 16, wherein the instructions for performing the structural rewind verification comprises instructions for retiming the retimed circuit design back to the original circuit design, wherein each routing path in the original circuit design is assigned an original weighting factor based on the number of registers in that routing path of the original circuit design, wherein each routing path in the retimed circuit design is assigned a retimed weighting factor based on the number of registers in that routing path of the retimed circuit design, and wherein the original weighting factor and the retimed weighting factor are known prior to performing the structural rewind verification. ### Claim 18 (depends on 16) The non-transitory computer-readable storage medium of claim 16, the instructions further comprising: with the circuit design computing equipment, constraining the structural rewind verification by ensuring that all retiming variables for non-justifiable circuit elements obtained using an equation solver are less than or equal to the count value c, wherein the non-justifiable elements each have inputs and outputs, and wherein all possible output values at the outputs of each non-justifiable circuit element are not obtainable using some combination of input values received at the inputs of that non-justifiable element. ### Claim 19 (depends on 16) The non-transitory computer-readable storage medium of claim 16, the instructions further comprising: with the circuit design computing equipment, modeling a fan-out node that has a single input and multiple outputs as a non-justifiable circuit element. ### Claim 20 (depends on 16) The non-transitory computer-readable storage medium of claim 16, the instructions further comprising: with the circuit design computing equipment, constraining the structural rewind verification by ensuring that the absolute value of all retiming variables obtained using an equation solver are less than or equal to a total number of registers in the retimed circuit design. ### Claim 21 (depends on 16) The non-transitory computer-readable storage medium of claim 16, the instructions further comprising: with the circuit design computing equipment, in response to verifying that the retimed circuit design is c-cycle sequentially equivalent to the original circuit design, suggesting a reduced count value that is less than the count value c for delaying the reset sequence for the retimed circuit design. ### Claim 22 (depends on 16) The non-transitory computer-readable storage medium of claim 16, the instructions further comprising: with the circuit design computing equipment, in response to verifying that the retimed circuit design is not c-cycle sequentially equivalent to the original circuit design, suggesting a larger count value that is greater than the count value c. ### Claim 23 (depends on 16) The non-transitory computer-readable storage medium of claim 16, the instructions further comprising: with the circuit design computing equipment, in response to verifying that the retimed circuit design is not c-cycle sequentially equivalent to the original circuit design, attempting to perform the structural rewind verification without taking into account the count value c; and with the circuit design computing equipment, if the structural rewind verification fails without taking into account the count value c, reporting a verification error and identifying a minimal set of constraints that might have caused the failure.