Sequential Equivalence Checking After RTL Retiming

State Mapping Reset and Counterexample Debug

Moving a register can improve an implementation while changing what its internal state represents. A direct comparison of the old and new register values may then fail even when the required output sequence is preserved. Sequential equivalence checking after RTL retiming must establish the right relationship between the two implementations, including how that relationship begins at reset.

The practical task is to define the observations that must agree, model the permitted starting conditions and show that the relationship survives every allowed transition. A counterexample is useful only when engineers understand which of those obligations it violates. This article develops that reasoning through an eight-bit example and a repeatable verification workflow.

Define the equivalence contract before matching registers

Retiming relocates registers across combinational logic. The classical formulation treats register placement as a graph transformation; practical verification also has to account for initial states and the transformed implementation’s structure [1], [2]. A legal register move in a retiming model is not sufficient evidence for every reset or interface contract used in a product.

This article considers a single-clock block whose required external cycle alignment remains unchanged. Both designs receive the same legal inputs. The comparison includes the specified outputs after the relevant RTL events have settled. If an architectural change deliberately adds latency, engineers need a separate alignment contract. Silently shifting one output trace changes the question being proved.

State correspondence is a relation

A combinational comparison between register boundaries can be effective when the boundaries still represent corresponding functions. After retiming, requiring internal registers to be identical can impose the wrong obligation. The term used by a tool, including SEC or LEC, does not replace checking what that particular flow actually compares.

Let the reference state be Sref and the implementation state be Simp. A relation R(Sref, Simp) describes their permitted correspondence. A sufficient invariant-based argument establishes three things: the permitted paired starting states satisfy R; every legal transition from related states preserves R; and related states produce the required equal observations. The relation is a proof obligation, not an assumption to insert simply because it makes the outputs agree.

Retiming does not require a one-to-one register-name match. A relationship may involve several state elements, combinational functions or correlations created by duplication. Not every function is invertible, so deriving a new initial state from an old one can require more than copying reset bits [2], [3].

Figure 1. Illustrative register move across an eight-bit increment function. The required relation and different reset values preserve the stated settled output behaviour.

Figure 1 shows the deliberately simple case used below. Both implementations contain one eight-bit register. The increment function crosses that register boundary; no extra pipeline stage is inserted. The illustrated relation applies to this example, rather than every retimed design.

A worked eight-bit retiming example

The reference captures x in r and then increments r. The implementation increments x before capturing it in s. The example uses known two-state, unsigned eight-bit data; additions wrap modulo 256. There are no clock enables, stalls, additional clock domains or hardware side effects.

Both modules use the same rising-edge clock and asynchronous active-low reset. A common reset assertion must first establish their reset states. Reset is released away from a clock edge, and inputs meet the intended sampling conditions. The comparison begins after reset updates have settled, includes settled outputs while reset is active and before the first functional edge, and continues after functional clock events. Arbitrary unrelated power-up states are outside this example’s claim.

Reference RTL

module retime_ref (

  input  logic   clk,

  input  logic   rst_n,

  input  logic [7:0] x,

  output logic [7:0] y_ref

);

  logic [7:0] r;

  always_ff @(posedge clk or negedge rst_n) begin

if (!rst_n) r <= 8’h00;

else        r <= x;

  end

  assign y_ref = r + 8’h01;

endmodule

Retimed RTL

module retime_impl (

  input  logic   clk,

  input  logic   rst_n,

  input  logic [7:0] x,

  output logic [7:0] y_imp

);

  logic [7:0] s;

  always_ff @(posedge clk or negedge rst_n) begin

if (!rst_n) s <= 8’h01;

else        s <= x + 8’h01;

  end

  assign y_imp = s;

endmodule

These modules illustrate a state transformation and its reset requirement. They do not demonstrate a timing improvement or describe a synthesis tool’s automatic retiming support.

Establish the relationship and its reset value

For this example, the required relation is:

Initial correspondence. After reset assertion settles, r is 0x00 and s is 0x01. The relation holds, and both outputs are 0x01. Giving the registers identical reset values would break the required output relationship.

Transition preservation. On a functional rising edge, both modules sample the same x. The next reference state is x and the next implementation state is the eight-bit result of x + 1. The relation therefore holds for every input value, including x = 0xFF. A subsequent reset assertion re-establishes the same related reset pair.

Observation equality. The reference output is the eight-bit value r + 1 and the implementation output is s. The relation makes those outputs equal. Register equality, r = s, is neither required nor correct here.

This argument establishes settled-value behaviour in the stated RTL model. It does not establish equal physical propagation delays, absence of glitches, timing closure, metastability behaviour or recovery/removal timing. Those require the appropriate implementation and clock/reset analyses.

Reset must be observed where the contract requires it

Change the implementation’s reset assignment to s <= 8’h00. The reference still produces 0x01 after reset settles, but the faulty implementation produces 0x00. The difference remains after reset release until a functional clock edge updates the implementation. A proof that starts comparison only after that edge may miss the required reset observation.

Some interfaces specify that data is irrelevant during reset or while valid is low. In that case, compare the validity/control behaviour and the data observations that the specification actually requires. A mask or warm-up interval needs a documented justification; it must not be introduced solely to remove a failing trace.

Equivalent initial-state calculation is a recognised retiming problem [3]. For blocks without a known reset state, engineers must choose an appropriate initial-state or refinement semantics. Merely assuming equal internal starting bits does not establish a retiming relationship. Unknowns and don’t-cares also need explicit treatment: EQY, for example, documents safe-replacement semantics and different interpretations of unknown values on the reference and implementation sides [5].

Debug the first relevant divergence

Figure 2. Derived settled-value sequence for the correct and wrong-reset implementations. The reset mismatch is observable before the first functional edge; later agreement does not remove it.

The values in Figure 2 are derived from the worked RTL. At the first functional edge with x = 0x05, both outputs settle to 0x06, even in the wrong-reset variant. That later agreement does not remove the earlier reset mismatch under this article’s observation contract. At x = 0xFF, the expected eight-bit result is 0x00.

Preserve the failing configuration and identify the earliest violated comparison. Check the observation event, reset history, input sequence and initial state before changing RTL. When a trace arises from a partition or abstraction, determine whether its local stimulus and state are reachable in the complete comparison model.

A practical sequential equivalence workflow

Alpinum’s guide to unproven and bounded formal results provides wider context on proof outcomes. The workflow below focuses on correspondence and reset after retiming.

1 Freeze the baseline and observation contract

Record both RTL revisions, top modules, parameters, compile definitions and library or memory models. List the required observations and their timing. Preserve the reset specification and every environmental assumption with a reason for using it. Equivalence preserves the chosen reference behaviour; it does not establish that the reference itself implements every requirement correctly.

2 Identify what crossed a register boundary

Review the transformation or synthesis history. Locate moved, removed or duplicated registers and the affected combinational functions. Check fanout, feedback, clock enables and control dependencies. Confirm that external latency and protocol behaviour remain within the agreed contract. The example’s simple relation is not a template for moving registers through arbitrary control logic.

3 Build a consistent comparison model

Drive the designs with the same legal interface stimulus and consistent clock/reset events. Review signedness, widths, modes, black boxes and unknown-value semantics. Distinguish independently justified environmental constraints from state relationships that must be proved. Investigate constraints that remove reset reassertion, backpressure or relevant operating modes allowed by the specification.

4 Establish starting-state correspondence

Apply the specified initialisation or prove the permitted starting relation. Include the required reset observations and any justified comparison-enable condition. For the worked RTL, the reset pair is r = 0x00 and s = 0x01. Restricting only the implementation’s starting states to convenient values can weaken the claim if the actual implementation can start elsewhere.

5 Establish transition and output obligations

Use a suitable sequential method to establish preservation of the relation and equality of the required observations. Track supporting invariants and partition dependencies. If a clock enable is present, the relation must survive hold cycles as well as update cycles. A state mapping that works on continuously enabled data is insufficient evidence for a stalled pipeline.

6 Triage failures and rerun after corrections

Distinguish a legal output mismatch from an invalid internal match, an abstraction artefact or an unresolved proof. Trace a suspect cut point back to its drivers and state history. Correct the RTL or proof setup according to the established cause, then rerun affected obligations and dependencies. Do not suppress an output comparison merely because its cone is difficult.

7 Review and retain the evidence

Archive revisions, tool versions, scripts, assumptions, comparison points, mapping information, results and diagnostic traces. Identify remaining bounds or unresolved partitions explicitly. Acceptance of an equivalence claim requires the required scope to be established. Any separately authorised project waiver remains an open limitation of that claim.

Scale the proof without assuming away retiming

Structural similarities can help a checker divide the problem, but retiming can invalidate some internal equality points. Cutting at such a point may expose independent values where the full circuit enforces a relationship. A failed local obligation can then require a revised partition or a supporting invariant rather than a DUT change.

The reverse risk matters too. Assuming the desired relationship at every cut point without establishing it can make downstream output checks pass while leaving the transformation unverified. Record how each dependency is discharged. Memories, reconvergence and retiming across hierarchy or control boundaries may require different proof decomposition from the original implementation [2].

Check the semantics of the selected proof engine

Tool terminology varies. A finite induction depth can be part of a complete unbounded proof when the required base and induction obligations are established; it should not be confused with a bounded search alone. Conversely, a conditional no-divergence result is insufficient without evidence that the designs enter the required related starting condition.

Yosys 0.65 documents that equiv_induct proves a conditional no-divergence criterion after compared points have agreed for the configured number of cycles. That command’s successful status alone is not a substitute for establishing the starting condition required here [4]. This is a property of that command’s documented criterion, not a limitation of induction in general.

EQY’s official example shows separate reference/implementation preparation, partition analysis, counterexample inspection and rerunning a corrected design [6]. Its example and unknown-value semantics are useful methodological references; they do not constitute a report that these retimed modules were proved by EQY. Select and qualify a flow for the transformation and contract being checked.

Conclusion

Retiming changes where information is stored. A useful sequential equivalence argument explains how the new state represents the old behaviour, why the reset states correspond and how the relationship preserves the required observations. In the eight-bit example, resetting the implementation to 0x01 is part of that relationship; matching both reset values would be a functional error under the stated contract.

Counterexample debug should lead to an explained cause and a repeatable rerun. The resulting evidence supports an engineering decision within its documented scope. It does not replace timing analysis, independent requirements verification or the wider release process.

Develop practical formal verification capability

Alpinum’s Formal Verification Training covers SEC versus LEC, proof setup and analysis, counterexample debug, assumptions, convergence and block-level verification. Engineers can use the programme to strengthen the reasoning needed to review transformations and their evidence. The course is vendor-neutral and combines teaching with worked examples and practical exercises.

References

[1] C. E. Leiserson and J. B. Saxe, “Retiming synchronous circuitry,” MIT Laboratory for Computer Science, Tech. Memo MIT-LCS-TM-309, May 1986. https://dspace.mit.edu/entities/publication/f3476d6e-5651-41e5-a2fd-61d9695562e7 

[2] K. Netolická, “Equivalence checking of retimed circuits,” M.Eng. thesis, Dept. Electrical Engineering and Computer Science, Massachusetts Institute of Technology, 2005. https://dspace.mit.edu/entities/publication/ed1ef25f-2967-44e5-b9fa-81ec7d5005a1 

[3] G. Even, I. Y. Spillinger and L. Stok, “Retiming revisited and reversed,” IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, Dec. 1996. https://research.ibm.com/publications/retiming-revisited-and-reversed 

[4] YosysHQ, “Equivalence checking,” Yosys 0.65 documentation, sections equiv_induct and equiv_make. Accessed: 27 Oct. 2026. https://yosyshq.readthedocs.io/projects/yosys/en/v0.65/cmd/index_passes_equiv.html 

[5] YosysHQ, “Equivalence and X-Propagation,” EQY documentation. Accessed: 27 Oct. 2026. https://yosyshq.readthedocs.io/projects/yosys/en/v0.65/cmd/index_passes_equiv.html 

[6] YosysHQ, “Getting Started,” EQY documentation. Accessed: 27 Oct. 2026. https://yosyshq.readthedocs.io/projects/eqy/en/latest/quickstart.html

FAQs