Retiming slides registers across combinational gates to balance stage delays. The logic is preserved but the register positions change.
Each moved register breaks its old pairing. The correspondence must be rebuilt from the retiming log before cones can be compared.
Before retiming | After retiming | Effect on the check |
|---|---|---|
Register after a slow block | Register pushed into the block | Old pair gone; new cut points needed. |
Two registers in series | One merged register | Two pairs collapse into one. |
No register on a path | Register pulled onto the path | A new key point appears. |
Synthesis may recode state registers from binary to one-hot or Gray. The state names survive but their bit patterns change.
A binary pair and its one-hot form name the same four states with different widths. The calc block shows the exact codes.
4 states need ceil(log2(4)) = 2 binary bits
binary codes: 00, 01, 10, 11 (2 bits each)
one-hot codes: 0001, 0010, 0100, 1000 (4 bits each)
same 4 states, different bit patterns and widthsSequential comparison first aligns states, then compares next-state and output logic. Name-based pairing alone fails after recoding.
The usual fix maps old codes to new codes explicitly. Only then do the combinational checks between matched state bits apply.
Step | Action | Why |
|---|---|---|
Collect moves | Read the retiming and recoding reports. | They list which registers moved and which codes changed. |
Map states | Pair each old code with its new code. | Cones must compare equivalent states. |
Re-run cones | Prove next-state and output logic per pair. | A pass on aligned pairs is meaningful again. |
No. The pairing predates the move, so the cones compared are stale. Rebuild the correspondence and re-run.
Two bits become four. An old-code to new-code map must be supplied before comparison.