Retiming moves a register across a multiplier and the netlist still matches the RTL cycle by cycle at the outputs, while nothing matches in the middle. A one-to-one comparison of registers fails everywhere, correctly, because the states genuinely differ. Sequential equivalence compares the machines from reset on the same inputs and asserts equal outputs, with an invariant that relates the two state spaces where they legitimately diverge.

Suggested order: top to bottom. The product machine is the shared idea; the retimed pipeline is its main workout; alignment and reset are the two traps inside every sequential comparison; recoding and gating close with the transformations that break one-to-one matching. The induction behind the product machine is taught at k-induction.

Two conditions hold for every proof in this topic. First, the equivalence is from reset: the first step of every miter is held in reset, so both machines start from their reset states and the proof says nothing about arbitrary power-up contents. Second, the model is two-state: a register that is not reset is an arbitrary 0 or 1, never an unknown, so a two-state equivalence cannot show a difference in X-pessimism or X-optimism between two descriptions. Whether state after reset is independent of power-up values is a reset-determinism question, answered by its own proof and not by the miter.