Reset travels with the register

A reset value belongs to a register, not to a position in the pipeline. When retiming slides the register across a gate, the reset value slides with it, and the logic now sitting on the other side transforms what the reset cycle shows at the output. Get the moved value wrong and every reset sequence mismatches, even though the steady stream is untouched.

One flop across one NAND gate

The pair below is the smallest move that changes a reset value and that no register matching can explain away. The first design samples the NAND of two inputs, so its single flop resets to 0 and the output reads 0 in the reset cycle. The second design is the same circuit after a backward move across the two-input NAND: one flop now samples each input and the NAND sits after them. For the reset cycle to still read 0, both moved flops must reset to 1, because only 1 NAND 1 reads 0 at the output. The script counts all flops, then proves the correctly reset pair over steps 2 to 6 and records what the wrongly reset variant does.

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
41
42
43
44
45
46
47
48
49
50

read_verilog <<EOV
module invb(input clk, input rst, input a, b, output y);
  reg q;
  always @(posedge clk) begin
    if (rst) q <= 1'b0;
    else q <= ~(a & b);
  end
  assign y = q;
endmodule
module inva(input clk, input rst, input a, b, output y);
  reg q1, q2;
  always @(posedge clk) begin
    if (rst) begin q1 <= 1'b1; q2 <= 1'b1; end
    else begin q1 <= a; q2 <= b; end
  end
  assign y = ~(q1 & q2);
endmodule
module inva_bad(input clk, input rst, input a, b, output y);
  reg q1, q2;
  always @(posedge clk) begin
    if (rst) begin q1 <= 1'b0; q2 <= 1'b0; end
    else begin q1 <= a; q2 <= b; end
  end
  assign y = ~(q1 & q2);
endmodule
EOV
hierarchy -check
proc
opt_clean
design -save all
hierarchy -check -top invb
tee -o stat_b.txt stat
select -assert-count 1 t:$dff
write_json net_b.json
design -load all
hierarchy -check -top inva
tee -o stat_a.txt stat
select -assert-count 2 t:$dff
write_json net_a.json
design -load all
miter -equiv invb inva miter
hierarchy -check -top miter
flatten
tee -o equiv_inv.txt sat -seq 6 -prove trigger 0 -prove-skip 1 -verify -set-init-zero -set in_rst 0 -set-at 1 in_rst 1
design -load all
miter -equiv invb inva_bad miter_bad
hierarchy -check -top miter_bad
flatten
tee -o equiv_bad.txt sat -seq 6 -prove trigger 0 -prove-skip 1 -set-init-zero -set in_rst 0 -set-at 1 in_rst 1
log PASS: NAND reset pair proved, buggy variant shown different

What the reset run recorded

The unmoved design holds 1 flop after its NAND gate and the moved design holds 2 flops, one per input: a backward move across a two-input gate adds one flop while every input-to-output path still crosses exactly one. The program below simulates the reset cycle plus four data cycles for input pairs (0,1), (1,0), (1,1), (0,1), (1,0) and asserts every entry of the table that follows. The correctly moved resets of 1 and 1 reproduce the original 0 in the reset cycle; the buggy kept resets of 0 and 0 read 1 there and rejoin only afterwards.

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

import sys

def sim(reset_b, r1, r2, aval, bval):
    yb, ya = [], []
    qb, q1, q2 = reset_b, r1, r2
    for a, b in zip(aval, bval):
        yb.append(qb)
        ya.append(1 - (q1 & q2))
        qb = 1 - (a & b)
        q1, q2 = a, b
    return yb, ya

aval = [0, 1, 1, 0, 1]
bval = [1, 0, 1, 1, 0]
yb, ya_ok = sim(0, 1, 1, aval, bval)
_, ya_bad = sim(0, 0, 0, aval, bval)

problems = []
if yb[0] != 0 or ya_ok[0] != 0:
    problems.append("reset-cycle outputs must both be 0, got %s %s" % (yb[0], ya_ok[0]))
if yb[1:] != ya_ok[1:]:
    problems.append("correct pair must agree after the reset cycle")
if ya_bad[0] != 1:
    problems.append("buggy moved resets 0 and 0 must read 1 in the reset cycle")
if ya_bad[1:] != yb[1:]:
    problems.append("buggy pair rejoins after the reset cycle")
if ya_ok != [0, 1, 1, 0, 1]:
    problems.append("after column")

if not problems:
    print("PASS: moved resets are 1 and 1, reset-cycle outputs 0 and 0, streams agree after")
    sys.exit(0)
print("FAIL: " + ", ".join(problems))
sys.exit(1)

What equivalence can still show

Combinational equivalence fails here on purpose: the two netlists place their register boundary on different sides of a two-input NAND gate, with one flop on one side and two on the other, so no stage-by-stage comparison lines up. A pure inversion would prove nothing, since commercial register matching reconciles phase-inverted flops routinely; the one-against-two boundary here is what no positional matching can reconcile. The sequential check reasons over reset sequences instead. It asserts reset at step 1, zeroes the power-up state, and compares steps 2, 3, 4, 5 and 6. Step 1 is skipped deliberately: the forced zero inits wake the moved flops at 0, which is not their justified value of 1, so the first outputs differ by construction and prove nothing about the move. The correctly reset pair passes all five compared steps; the buggy variant fires the miter trigger at exactly the reset-affected steps and stays quiet after, which the recorded counterexample table confirms.

Concretely, the buggy run's trigger is high at steps 1 and 2 and low for the rest of the trace: the mismatch is the reset cycle plus the power-up step, never the steady stream. A correct tool justifies the new initial values or refuses the move when the resulting reset state is not reachable; either way, the check that matters compares outputs after the power-up step, never from step 1.

Break it: keep resets 0 across the NAND gate

The second miter in the same script is the changed variant: identical logic, identical reset sequence, but both moved flops keep reset 0. The proof fails with a found model instead of a pass, and the trigger column of the recorded trace marks the damage. Registers with enables or asynchronous resets are restricted rather than freely movable: the move needs enable-aware handling, and in this flow the flop-passing ABC step carries enable flops through instead of moving them.

Common mistakes

Related topics

• Latency, throughput and register count

• Equivalence checking