Debugging Counterexamples Efficiently

A counterexample from a single small module can be read in a minute. In a design with several modules, the assertion that fails is often far from the line that is wrong: the symptom shows up at an output, the cause sits two modules away, a few cycles earlier. This article gives a routine for such cases, using the two tools that formal makes cheap: extra assertions to narrow down where the error starts, and assumptions to test a guess about its cause.

9 min read | Intermediate

What You'll Learn

• Follow a five-step routine from a failing assertion to the faulty line
• Localize an error by adding assertions at module boundaries
• Test a hypothesis about the cause by assuming it away
• Debug an end-to-end failure in a source and sink design

The Routine

1. Read the log. Which assertion failed, and in which step.
2. Read the waveform backwards from the failure, as in the reading a counterexample article, until the first value that is already wrong.
3. Localize. If the first wrong value comes from another module, add an assertion at the boundary between them and run again. The new counterexample points into the right module, and it is often shorter.
4. Test a hypothesis. If you suspect an input pattern, assume it away. If the failure disappears, the pattern is needed for the bug.
5. Fix and rerun everything, including the new assertions, which stay in the design as extra checks.

In simulation, each new idea means a new test or a rerun of a long regression. In formal, each step is a run of a few seconds over all input sequences, which is why this routine is fast.

The Design: a Source and a Sink

A source sends the numbers 1, 2, 3 and so on over a valid/ready interface. A sink adds up everything it receives and counts the words. The sink can stall, which lowers ready:

module src (input clk, input rst, input ready, output reg valid, output reg [7:0] data);
  always @(posedge clk)
    if (rst) begin
      valid <= 1'b0; data <= 8'd1;
    end else begin
      valid <= 1'b1;
      if (valid) data <= data + 8'd1;        // bug: should advance only on valid && ready
    end
endmodule

module sink (input clk, input rst, input stall, input valid, input [7:0] data,
             output ready, output reg [7:0] n, output reg [15:0] sum);
  assign ready = !stall;
  always @(posedge clk)
    if (rst) begin
      n <= 8'd0; sum <= 16'd0;
    end else if (valid && ready) begin
      n <= n + 8'd1; sum <= sum + data;
    end
endmodule

The top module link connects the two. The end-to-end rule: after receiving n words, the numbers 1 to n, the sum is n(n+1)/2.

a_sum: assert property (@(posedge clk) disable iff (rst) sum == n * (n + 1) / 2);

Steps 1 and 2: Log and Waveform

The run fails at step 5. Reading backwards: in step 4, one word has been received (n = 1) but the sum is 2, not 1. The word that arrived was 2. Word 1 never reached the sink. So the first wrong thing is the data at the interface, which comes from the source.

Step 3: Localize With a Boundary Assertion

A valid/ready interface has a known rule: data is stable while valid is high and ready is low. Add it at the boundary, in the top module:

a_stable: assert property (@(posedge clk) disable iff (rst) valid && !ready |=> $stable(data));

The new run fails one step earlier, at step 4, on the boundary assertion. That moves the search from "somewhere between source and sum" to "the source changes its data while the sink stalls". The trace shows it: word 1 is offered in step 2, the sink stalls, and in step 3 the source already offers 2.

Step 4: Test the Hypothesis

The guess is that the bug needs a stall. Assume there are none:

always @(*) assume (!stall);   // hypothesis: the bug needs a stall

The run passes. The hypothesis is confirmed: without stalls, the source and the sink agree. This assumption is a debugging tool only. Remove it again after the test, because stalls are legal.

Step 5: Fix and Rerun

The source advances its data on valid alone. Change it to if (valid && ready), remove the hypothesis assumption, and run with both assertions. Everything passes. Keep the boundary assertion: it documents the interface and will catch the next bug of this kind at once.

Running It in ChipVerify Lab

The example below has the three modules with the end-to-end assertion only. Follow the routine yourself in the exercise.

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  // end to end: after n words 1..n, the sum is n*(n+1)/2
  always @(posedge clk) if (!init) assert (sum == ({8'd0, n} * ({8'd0, n} + 16'd1)) / 16'd2);
`endif

The lab waveform viewer shows the signals of every module, so you can add u_src.data or u_sink.sum to the view while reading the trace.

Common Mistakes

// interface rule at the boundary: data is stable while waiting
always @(posedge clk) if (!init && !$past(rst) && $past(valid) && !$past(ready)) assert (data == $past(data));