Transformation | Equivalence concern |
|---|---|
Retiming | State points move; sequential equivalence setup required |
Clock gating | Enable and test-mode modeling |
Memory inference | Array abstraction and read-during-write semantics |
FSM recoding | State mapping and unreachable values |
Constant propagation | Mode constraints must match legal operation |
ECO patch | Changed compare boundary and intended functional delta |
The added checksum register preserves packet-level behavior but changes cycle correspondence. The proof therefore compares accepted inputs and tagged outputs across the documented latency, while reset and legal-mode assumptions remain explicit review items.
Settled observation | C0 output | C1 output | Latency-aware comparison |
|---|---|---|---|
After E0: accept tag A, words 1,2,3,4 | A / 10 / valid | invalid (pipeline empty) | Save C0 A/10; do not compare same-edge outputs |
After E1: accept tag B, words 16,1,2,3 | B / 22 / valid | A / 10 / valid | Compare C1 against previous C0 including tag |
After E2: input bubble | invalid | B / 22 / valid | Compare B; propagate bubble through valid history |
Reset before next edge with pending tag C | invalid | invalid | Flush alignment history and count C as cancelled |
Each slot shows values just after one rising edge; an output tag of x means that pipeline has no valid output.
Slots 1 to 3: C0 shows a, b, x (the bubble); C1 shows the same sequence one slot later. That is C1[k] = C0[k-1].
Slot 2: the input bubble enters both pipelines and comes out as x, so valid history must be compared, not just data.
Slot 4: tag c was captured at edge 4, then rst_n fell. Both pipelines clear before any consumer edge, so c is cancelled, not delivered.
Slot 5: reset is released with nothing pending; the comparison history starts again empty.
Proof obligation, not a reported proof: outside reset, C1.valid[k] = C0.valid[k-1]; when valid, C1.tag/sum[k] = C0.tag/sum[k-1]. Reset clears the history and both valid pipelines. Track accepted = delivered + pending + cancelled across reset epochs. Assume known legal inputs and a common clock/reset contract, not constant data or no bubbles. A finite scoreboard can check this trace; sequential equivalence must establish all legal histories with reviewed assumptions.
Keep reset semantics explicit and consistent.
Avoid simulation-only initialization in synthesizable state.
Preserve stable compare points around risky transformations when useful.
Provide assumptions for legal modes without over-constraining real behavior.
Review every unmatched point; do not waive by pattern alone.
Registers move across combinational logic, so internal state correspondence changes. Sequential equivalence must compare behavior across cycles rather than identical internal flops.