Retiming is one pass inside mapping, not a separate synthesis stage. The generic flow synthesises the RTL, hands the gate network plus its flops to the mapper, and the mapper first repositions flops and then covers the logic with library cells. Verification closes the loop afterwards, and it must compare reset-state streams rather than stage-by-stage logic. The script below runs that middle step twice on a two-flop pipeline, loose then tight, and records whatever the retiming pass actually does.
No. Both runs keep 16 flops: the retiming step executes in each, as the recorded log line shows, but the only legal single move on this structure adds flops instead of removing them, so a delay-driven pass with nothing to gain leaves every flop where synthesis put it.
read_verilog <<EOV
module pipe2(input clk, input [7:0] a, b, c, output [7:0] y);
reg [7:0] ri, ro;
wire [7:0] s1, s2;
always @(posedge clk) ri <= a;
assign s1 = ri + b;
assign s2 = s1 + c;
always @(posedge clk) ro <= s2;
assign y = ro;
endmodule
EOV
hierarchy -check -top pipe2
synth -top pipe2 -flatten
tee -o stat_gen2.txt stat -liberty course.lib
select -assert-count 16 t:$_DFF_P_
design -save generic
tee -o abc_loose.txt abc -liberty course.lib -constr typical.constr -D 100000 -dff
tee -o stat_loose.txt stat -liberty course.lib
select -assert-count 16 t:$_DFF_P_
design -load generic
tee -o abc_tight.txt abc -liberty course.lib -constr typical.constr -D 1000 -dff
tee -o stat_tight.txt stat -liberty course.lib
select -assert-count 16 t:$_DFF_P_
check
design -reset
read_verilog <<EOV
module areademo(input clk, input a, b, output y);
reg ra, rb, ry;
always @(posedge clk) begin ra <= a; rb <= b; ry <= ra & rb; end
assign y = ry;
endmodule
module areademo_rt(input clk, input a, b, output y);
reg q1, q2;
always @(posedge clk) begin q1 <= a & b; q2 <= q1; end
assign y = q2;
endmodule
EOV
hierarchy -check
proc
opt
miter -equiv areademo areademo_rt miter
hierarchy -check -top miter
flatten
design -save flat
tee -o equiv_anystate.txt sat -seq 1 -prove trigger 0
design -load flat
tee -o equiv_seq.txt sat -seq 6 -prove trigger 0 -verify -set-init-zero
log PASS: dff sweep moved no flops and reset-state check proved over 6 cyclesThe generic netlist holds 16 flops. The loose run reports 83 gates at area 270 and 1213.75 ps with 16 flops; the tight run reports identical figures down to the last digit, 83 gates at area 270 and 1213.75 ps with 16 flops. The chart below draws that non-result honestly: two bars of exactly the same height. The retiming step did run in both cases; the recorded log carries its line several lines ahead of the mapping step that follows it:
ABC: + retime -o -D 1000
ABC: + &nf -D 1000
Why nothing moved is visible in the same recording. At the point the retime step executes, the network is still pre-mapping: every gate carries unit delay, so a target of 1000 units is already satisfied and the delay pass has nothing to chase, while the min-area pass finds no cheaper legal move on this structure. The only single move available here, pushing the output flop back across its adder, would add 8 flops instead of removing any. Contrast that with the first lesson of this topic, where the same flag on a different structure merged 3 flops into 2 and the arrival moved from 133.96 ps plain to 122.37 ps flagged: the flag enables the step, the structure decides the outcome. Never claim a tool retimed because the flag was set; the flop count is the only witness that matters.
Not every flop is movable, and the refusals below are documented tool behaviour rather than runs on this page: the flop-passing help text states that multi-clock designs are partitioned by clock domain first, and commercial flows add the same guards under their own option names, which are named differently per tool and are not run here.
Guard | What it forbids | Why |
|---|---|---|
Clock domains | No moves across asynchronous clock boundaries | The pass partitions by domain first; crossing would mix unrelated sample times. |
Don't-touch and keep registers | No moves through marked flops | Marked state is an interface the tools must preserve bit for bit. |
Scan flops | No moves through scan chains | Test structure must survive synthesis unchanged. |
Enables and async resets | Moves restricted | The move needs enable-aware handling; Yosys' flop-passing step carries enable flops through instead of moving them. |
Memories | No moves through macro boundaries | A RAM macro is a fixed box, not logic to slide across. |
The same areademo pair from the first lesson shows why the check must be sequential and reset-state. Compared from an arbitrary state over a single step, the two designs already differ: both copies start from unconstrained independent initial states, so the free bits can disagree before any logic is even exercised. That failure proves nothing about the move, since a miter of a design against itself fails the same way. Compared from the zeroed reset state over 6 steps, the pair agrees everywhere. A combinational comparison that cannot match key points across the moved boundary behaves like the first check and fails on any retimed netlist; a retiming-aware flow behaves like the second, aligning reset sequences before it compares. The recorded trigger fires in the any-state run and stays quiet in the reset-state run, which is exactly the gap a retiming-aware equivalence mode exists to bridge.
Concretely, the any-state run fires the trigger at step 1 of its single compared step, while the reset-state run passes all 6 compared steps from the zeroed state. Quote those two recordings whenever someone proposes comparing a retimed netlist stage by stage.
That it ran and changed nothing: identical counts and identical delays under both targets. The flag enables the step; only the flop count proves a move.
The any-state check resembles it: both compare without aligning reset sequences, so both trip on moved boundaries. A retiming-aware flow aligns reset states first, like the passing check, and only then compares.
Flop counts, ABC areas and delays, the retime log line and step order, and both sat outcomes on this page come from one Yosys 0.70 run of the script shown, recorded by the course checker (scripts/tools/run-rtl-testbenches.mjs with COURSE=synth): the two-flop pipeline swept loose then tight with the flop-passing flag, plus the any-state failure and reset-state pass on the areademo pair from the first lesson. The guard table is documented tool behaviour, labelled so, and the commercial-tool line is stated practice, not a run.