The backend retimes the pipeline for timing, gates half the clocks for power, and hands back a netlist with a passing one-to-one report. The report is checked, the tape moves, and the mismatch surfaces in silicon because the pass compared points the transformations had already moved. Somebody needed to say: this transformation is outside the method. This lesson is that boundary, drawn before the tape moves.
This lesson has one job: state exactly what a one-to-one PASS covers, and route everything else to the method that does.
One-to-one comparison covers transformations that preserve the state correspondence: resynthesis of combinational cones, redundancy removal, constant propagation with aligned constants, buffer and inverter insertion. It does not cover transformations that move, merge, split or re-encode state: retiming across logic, FSM recoding, duplication or merging that changes which values exist (retiming splits, gated copies), and clock gating that changes which cycles update state. Duplicates that always hold equal values are matched by function, with the functional proof listed in the report. The rest need sequential equivalence, as the previous topic proves, or the dedicated modes the flow provides for retiming and gating.
The statement a PASS makes is therefore conditional twice over: equivalent to the RTL under the listed assumptions, and only for the transformations the method covers. It never says the RTL is correct. The full signoff for a transformed netlist is the one-to-one pass for the preserved part plus sequential proofs for the moved part plus the property proofs on the RTL that say it does the right thing.
Transformation | Covered by one-to-one | Route otherwise |
|---|---|---|
Cone resynthesis, redundancy removal | Yes | None needed |
Constant propagation, aligned tie-offs | Yes | Align constants first |
Buffer, inverter, polarity with inversion accounted | Yes | Account the inversion in the setup |
Retiming across combinational logic | No | Sequential equivalence with a cut invariant |
FSM recoding | No | Sequential equivalence with a state map |
Register duplication or merging of registers that hold equal values | Yes, matched by function: the functional proof is listed in the report | Review the functional matches |
Duplication or merging that changes which values exist (retiming splits, gated copies) | No | Key-point remap plus sequential proof |
Clock gating | No, or dedicated gating mode only | Sequential equivalence with the gate condition |
Three reports arrive on the same morning. Report one fails on every vector with all bits differing: setup, align the constants and rerun. Report two fails on one output bit in a carry corner: real mismatch, read it as the failing-miter lesson teaches. Report three fails everywhere from cycle 1 on a retimed block: method error, move it to sequential equivalence with a cut invariant instead of debugging the cones. The tree is: all-vectors means setup, corner means logic, everywhere-from-reset on moved state means wrong method.
# not-run: illustrative trace, not executable here
report 1: all vectors, all bits differ -> setup (constants/tie-offs)
report 2: one bit, complementary-input corner -> real mismatch (read the cone)
report 3: retimed block, fails from cycle 1 -> wrong method (go sequential)
a PASS then claims: equivalent to the RTL under the listed assumptions,
for covered transformations only; correctness comes from RTL propertiesThe netlist change list is mapped row by row to the table: every transformation has its method named.
No retimed, recoded, duplicated or gated block is claimed under a one-to-one pass alone.
The PASS statement carries both conditions: the assumptions and the transformation coverage.
For each transformation in the change list, ask which row of the table it sits in before reading any report. A block that moved rows between releases without a new proof is the escape. Keep the method column in the regression: when synthesis settings change, the table is rechecked, not the old verdict reused.
No. Both transformations sit below the line: the pass cannot see them. Route the pipelines to sequential equivalence with cut invariants and the FSM to its state-map proof, and keep the one-to-one pass for the preserved remainder.