The report

A small block, csum16, computes the 16-bit ones'-complement checksum of a packet, one word per cycle: add the words with end-around carry (a carry out of bit 15 goes back into bit 0) and output the complement of the sum. It has been in the nightly random regression for weeks. This week someone lengthened the packets to 32 words and made half the words ffff padding, and the nightly turned red:

$ for s in $(seq 11 20); do vvp -n c0.vvp +SEED=$s | grep -E "^(MISMATCH|PASS)"; done
PASS: seed 11, 2000 packets, dut matches model
PASS: seed 12, 2000 packets, dut matches model
MISMATCH seed=13 packet=387 words=32: csum dut=ffea model=ffeb
PASS: seed 14, 2000 packets, dut matches model
PASS: seed 15, 2000 packets, dut matches model
MISMATCH seed=16 packet=118 words=32: csum dut=fffb model=fffc
PASS: seed 17, 2000 packets, dut matches model
MISMATCH seed=18 packet=1618 words=9: csum dut=fffa model=fffb
MISMATCH seed=19 packet=459 words=19: csum dut=fff8 model=fff9
PASS: seed 20, 2000 packets, dut matches model

The bug report says: csum16 is one off in rare packets; looks like the end-around carry is added twice. Please fix the RTL. Here is the RTL:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23

// csum16: the 16-bit ones'-complement checksum of a packet of 16-bit words, one word per cycle.
// Spec: add the words with end-around carry (a carry out of bit 15 is added back into bit 0),
// and output the complement of the sum with the last word.
`timescale 1ns/1ps
module csum16 (
  input  logic        clk, rst_n,
  input  logic        in_valid, in_last,
  input  logic [15:0] in_data,
  output logic        out_valid,
  output logic [15:0] out_csum
);
  logic [15:0] acc_q, acc_n;
  logic [16:0] s;
  assign s     = {1'b0, acc_q} + {1'b0, in_data};
  assign acc_n = s[15:0] + {15'd0, s[16]};            // end-around carry
  always_ff @(posedge clk or negedge rst_n)
    if (!rst_n) begin acc_q <= '0; out_valid <= 1'b0; out_csum <= '0; end
    else begin
      out_valid <= in_valid && in_last;
      if (in_valid && in_last) begin out_csum <= ~acc_n; acc_q <= '0; end
      else if (in_valid)       acc_q <= acc_n;
    end
endmodule

And the bench's reference model, which computes the expected checksum for each packet the bench sends:

1
2
3
4
5
6
7
8

// snippet: the bench's model as it was (FIX = 0 in the full listing at the end of the page)
  // The reference model: sum in 32 bits, fold the carries back into 16 bits, complement.
  function automatic logic [15:0] model_csum();
    logic [31:0] sum = 0;
    foreach (pkt[i]) sum += {16'h0, pkt[i]};
    sum = {16'h0, sum[15:0]} + {16'h0, sum[31:16]};
    return ~sum[15:0];
  endfunction

Stop here and try it. Four seeds in ten fail, and in every failure the design's checksum is exactly one below the model's. Is the design adding a carry it should not, or is something else going on? Before you open the RTL's carry line, decide how you would know.

The hunt

Reproduce: same packet, both simulators

$ vvp -n c0.vvp +SEED=18
MISMATCH seed=18 packet=1618 words=9: csum dut=fffa model=fffb
  packet: 1926 5fbb ffff 468f 8274 be1f ffff ffff ffff
FATAL: csum_tb.sv:112: seed 18: 1 of 2000 packets mismatch
...
$ verilator --binary --timing --assert -Wno-fatal --top-module csum_tb -GFIX=0 -Mdir vl0 csum_tb.sv > /dev/null 2>&1; vl0/Vcsum_tb +SEED=18
MISMATCH seed=18 packet=1618 words=9: csum dut=fffa model=fffb
  packet: 1926 5fbb ffff 468f 8274 be1f ffff ffff ffff
...

Seed 18 fails on packet 1,618 of 2,000, nine words long, the same in both simulators. Not a race, not X: two deterministic computations disagree. Collect what the report already says before forming any theory:

• Always exactly one apart, and always in the same direction: design = model − 1.

• Rare: one packet in a few thousand, on about one seed in four.

• Always near ffff: every failing checksum is ffxx, so every failing sum folded to a small number.

• It started when the packets got longer and fuller of `ffff`, which makes the 32-bit sum bigger, with more carries to fold.

What usually happens next, and why it is a trap

The report already blames the RTL, and the RTL has an obvious suspect: the end-around carry line. An afternoon goes into reading it, then into "fixing" it so that the design matches the model, perhaps by folding the carry differently. That afternoon assumes the answer to the only question that matters: of the two things that disagree, which one is wrong? The model is code too, written by a person on a deadline, and it was never tested against anything but this design.

The method, which when the bug is in the test states in general: check the design against the spec at the failing case, then check the checker. Here, find a referee that shares no code with either side.

Localise, referee 1: a check the spec gives for free

A ones'-complement checksum has a property that needs no model at all: a receiver that adds every word and the checksum with end-around carry must get ffff. That is how the checksum is checked in use. Written one word at a time, it shares no code with the model's 32-bit sum-then-fold, and none with the RTL:

1
2
3
4
5
6
7

// snippet: the receiver check added to the bench (full listing at the end of the page)
  function automatic bit receiver_ok(input logic [15:0] csum);
    logic [16:0] a = 0;
    foreach (pkt[i]) begin a = a[15:0] + pkt[i]; a = a[15:0] + a[16]; end
    a = a[15:0] + csum; a = a[15:0] + a[16];
    return a[15:0] == 16'hffff;
  endfunction

$ vvp -n c0.vvp +SEED=18 +VERIFY
MISMATCH seed=18 packet=1618 words=9: csum dut=fffa model=fffb
  packet: 1926 5fbb ffff 468f 8274 be1f ffff ffff ffff
  receiver check: dut ok, model BAD
receiver check: dut checksum wrong in 0 of 2000 packets
FATAL: csum_tb.sv:112: seed 18: 1 of 2000 packets mismatch
...

On the failing packet, the design's checksum passes the receiver check and the model's fails it. And over all 2,000 packets of the seed, the design's checksum never fails. One referee has voted for the design.

Localise, referee 2: work the failing packet by hand

Nine words are few enough to add on paper. The model's way first: sum in 32 bits, then fold the upper half into the lower half once.

There it is: the one fold produced a carry of its own, and the model threw it away. That can only happen when the low half of the sum plus the number of carries reaches 1_0000, so the folded value is tiny and the checksum is near ffff, which explains the third clue. The smallest packet that does it has three words. The bench's +CORNER mode sends it:

$ vvp -n c0.vvp +CORNER +VERIFY
MISMATCH seed=1 packet=1 words=3: csum dut=fffe model=ffff
  packet: ffff ffff 0001
  receiver check: dut ok, model BAD
receiver check: dut checksum wrong in 0 of 3 packets
FATAL: csum_tb.sv:112: seed 1: 1 of 3 packets mismatch
...

By hand, as the spec says, one word at a time: ffff + ffff = 1_fffe, wrap the carry, ffff; ffff + 0001 = 1_0000, wrap the carry, 0001; checksum fffe. The design says fffe. The model's sum is 0001_ffff, one fold gives 1_0000, it keeps 0000 and says ffff. Second referee, same vote.

Localise, referee 3: is it always the model?

Two packets could be luck. A sweep over 100 seeds, counting both checks:

$ for s in $(seq 1 100); do vvp -n c0.vvp +SEED=$s +VERIFY; done > sweep0.log 2>&1
$ grep -c '^PASS' sweep0.log; grep -c '^MISMATCH' sweep0.log
74
26
$ grep '^  receiver' sweep0.log | sort | uniq -c
  26   receiver check: dut ok, model BAD
$ grep '^receiver' sweep0.log | sort | uniq -c
 100 receiver check: dut checksum wrong in 0 of 2000 packets

26 seeds mismatch. In all 26 the receiver check sides with the design, and across 200,000 packets the design's checksum never fails it. The bug is in the bench, in one line of the model: it folds once where the spec's arithmetic needs a fold until no carry is left.

Hypothesise and test: does the explanation predict the pattern?

A cause is only confirmed when it explains every clue, not just the one you were looking at. This one does:

The fix and the lesson

Fix: in the bench, not in the design

// snippet: the fix, in model_csum()
    while (sum[31:16] != 0) sum = {16'h0, sum[15:0]} + {16'h0, sum[31:16]};

Fold until nothing is left above bit 15. Here is the full bench as it stands after the hunt, with the receiver check behind +VERIFY, the corner packets behind +CORNER, and FIX choosing the old model (0) or the fixed one (1, the default). csum16 is repeated so the listing runs on its own:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23

// csum16: the 16-bit ones'-complement checksum of a packet of 16-bit words, one word per cycle.
// Spec: add the words with end-around carry (a carry out of bit 15 is added back into bit 0),
// and output the complement of the sum with the last word.
`timescale 1ns/1ps
module csum16 (
  input  logic        clk, rst_n,
  input  logic        in_valid, in_last,
  input  logic [15:0] in_data,
  output logic        out_valid,
  output logic [15:0] out_csum
);
  logic [15:0] acc_q, acc_n;
  logic [16:0] s;
  assign s     = {1'b0, acc_q} + {1'b0, in_data};
  assign acc_n = s[15:0] + {15'd0, s[16]};            // end-around carry
  always_ff @(posedge clk or negedge rst_n)
    if (!rst_n) begin acc_q <= '0; out_valid <= 1'b0; out_csum <= '0; end
    else begin
      out_valid <= in_valid && in_last;
      if (in_valid && in_last) begin out_csum <= ~acc_n; acc_q <= '0; end
      else if (in_valid)       acc_q <= acc_n;
    end
endmodule

Prove: the sweep, then a design that really is broken

$ iverilog -g2012 -o c1.vvp csum_tb.sv            # FIX = 1, the default
$ for s in $(seq 1 100); do vvp -n c1.vvp +SEED=$s +VERIFY; done > sweep1.log 2>&1
$ grep -c '^PASS' sweep1.log; grep -c '^MISMATCH' sweep1.log
100
0
$ vvp -n c1.vvp +CORNER +VERIFY
receiver check: dut checksum wrong in 0 of 3 packets
PASS: seed 1, 3 packets, dut matches model
...

Every seed passes. That proves less than it looks: a bench that compares nothing would pass too. A fixed checker must still fail on a real bug, so break the design on purpose. A copy drops the end-around carry from csum16 and runs the fixed bench:

$ sed '15s|.*|  assign acc_n = s[15:0];                    // mutant: end-around carry dropped|' csum_tb.sv > mutant.sv
$ iverilog -g2012 -o m.vvp mutant.sv && vvp -n m.vvp +SEED=1 +VERIFY
MISMATCH seed=1 packet=1 words=2: csum dut=dec7 model=dec6
  packet: 2139 ffff
  receiver check: dut BAD, model ok
receiver check: dut checksum wrong in 1936 of 2000 packets
FATAL: mutant.sv:112: seed 1: 1936 of 2000 packets mismatch
...
$ vvp -n m.vvp +CORNER +VERIFY
MISMATCH seed=1 packet=1 words=3: csum dut=0000 model=fffe
  packet: ffff ffff 0001
  receiver check: dut BAD, model ok
receiver check: dut checksum wrong in 2 of 3 packets
FATAL: mutant.sv:112: seed 1: 2 of 3 packets mismatch
...

The fixed model catches the mutant on the very first packet, and this time the receiver check votes against the design, as it should: the two checks now agree with each other, and both disagree with a design that is really wrong. On the corner packets the mutant fails two of three; the one it gets right is the single word ffff, which never carries.

Prevent: test the checker, not only the design

• Keep the independent check on. The receiver property costs a few lines and shares no code with the model. Run it on every packet, every night; a disagreement between the model and the property is a bench bug by definition.

• Give the model its own known-answer tests. The three +CORNER packets are worked by hand; run them against the model alone before every regression, so a model change cannot quietly break them.

• Mutate the design when you change a checker. One deliberate bug per checker change, kept as a script, proves the checker still bites.

• The review question for every reference model: what happens at the edges of its own arithmetic: widths, carries, wrap, rounding? The design was reviewed for its carry; the model never was.

Which step won? Localise, by asking which side is wrong before asking what is wrong. Three referees that share no code with the model, the spec's own property, a hand calculation and a sweep, turned a bug report against the RTL into a one-line bench fix in under an hour. Prove closed it: a fixed checker that cannot fail is not a fix.

Related topics

• Part 10 · Case Studies

• When the bug is in the test: check the design, then the checker

• Testbench bugs that look like design bugs

• Confirmation bias and blaming the tool

• Differential debugging: references and their limits

• UVM: the mismatch playbook