The question

Two input registers feed one AND gate and an output register follows it: three flops where two would do. Can the input pair slide forward across the gate and merge into one, without changing what the circuit computes? This lesson answers with a real run: a flop-merging (min-area) forward move across an AND gate, with the flop count, the area, and the delay all read back from the tool's own reports. The delay-balancing version of the story waits for the Leiserson-Saxe model further down.

One script, two jobs

The design below holds two input registers and one output register around a single AND gate. The script first proves a hand-retimed copy equivalent, then maps the original twice: once with the flop-passing flag that invites retiming, once without it. Every count on this page comes from the stat and ABC reports the script writes.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37

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
design -save rtl
miter -equiv areademo areademo_rt miter
hierarchy -check -top miter
flatten
tee -o equiv_rt.txt sat -seq 6 -prove trigger 0 -verify -set-init-zero
design -load rtl
hierarchy -check -top areademo
synth -top areademo -flatten
tee -o stat_gen.txt stat -liberty course.lib
select -assert-count 3 t:$_DFF_P_
write_json net_generic.json
design -save generic
tee -o abc_dff.txt abc -liberty course.lib -constr typical.constr -D 1000 -dff
tee -o stat_dff.txt stat -liberty course.lib
select -assert-count 2 t:$_DFF_P_
write_json net_dff.json
check
design -load generic
tee -o abc_plain.txt abc -liberty course.lib -constr typical.constr -D 1000
tee -o stat_plain.txt stat -liberty course.lib
select -assert-count 3 t:$_DFF_P_
log PASS: forward retiming mapped with and without dff and pair proved over 6 cycles

What the flagged run recorded

The generic netlist holds 3 flops around one AND gate. Without the flag, the plain mapping reports 1 mapped gate at area 3 and 133.96 ps and keeps all 3 flops: that is the before. With the flop-passing flag, ABC reports 3 mapped gates at area 7 and 122.37 ps, and the netlist keeps 2 flops: the two input flops became a single flop on the AND output, in series with the output flop the design already had. Every input-to-output path still crosses 2 flops, so latency is unchanged. Note what this move does not do: the whole AND ends up ahead of both flops, so no delay is shared between stages. The gain is one fewer flop, not a balanced split. The separate sequential check proves the hand-retimed copy equivalent over all 6 compared steps, starting from the zeroed state.

Forward and backward moves

Leiserson and Saxe showed that retiming is just repositioning: give every logic vertex a delay and every edge a register count, and a legal move shifts an integer lag across a vertex so that no path changes its total count. The smallest achievable period is then bounded by the slowest cycle average of delay over registers, and every move in the table below is one lag shift that preserves all path sums.

Read the recorded pair with that lens. Before the move, the path from input a to the output crosses ra and then ry: two registers with the AND between the first and the second. After the move it crosses the merged flop and then the output flop: still two, with the AND now ahead of both. Nothing was added and nothing removed; the AND simply changed which side of the register boundary it sits on. That is the whole visual vocabulary of the two netlists above: find the gate, find which side its flops sit on, and count each path again.

The same move as stage bars

The program below is a model, not a tool run: it recomputes a classroom 6, 2 and 4 ns block split with plain arithmetic and asserts every figure it prints. The two timing bars that follow draw the model's own numbers, one per retimed stage, so read them as the shape of the idea rather than a measurement.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40

import sys

A = 6.0
B = 2.0
C = 4.0

def stage_max(stages):
    m = stages[0]
    for s in stages[1:]:
        if s > m:
            m = s
    return m

before = [A + B, C]
after = [A, B + C]
p_before = stage_max(before)
p_after = stage_max(after)

regs_before = len(before) - 1
regs_after = len(after) - 1

problems = []
if p_before != 8.0:
    problems.append("before period")
if p_after != 6.0:
    problems.append("after period")
if regs_before != 1:
    problems.append("before path registers are 1, got %s" % regs_before)
if regs_after != 1:
    problems.append("after path registers are 1, got %s" % regs_after)
if regs_after != regs_before:
    problems.append("path count changed")
if min(before) != 4.0 or min(after) != 6.0:
    problems.append("stage split")

if not problems:
    print("PASS: model period 8.0 ns before and 6.0 ns after, path registers 1 to 1")
    sys.exit(0)
print("FAIL: " + ", ".join(problems))
sys.exit(1)

Break it: drop the -dff flag

The second mapping in the same script is the changed variant: identical library, target and load, but no flop-passing flag. It reports 1 mapped gate at area 3 and keeps 3 flops: in this ABC script, mapping alone never moves a register at any target. The move belongs to the retiming step, not the mapper, and without the flag that step never sees the flops.

Common mistakes

Related topics

• Latency, throughput and register count

• Flops, resets and enables