Reading a Counterexample

When a formal check fails, the tool gives you a counterexample: a short waveform that starts at reset and ends with the broken rule. Reading it well is the most important practical skill in formal verification. This article takes a real counterexample from the lab engine, for a FIFO occupancy counter with a bug, and reads it step by step, from the failure back to the cause.

9 min read | Beginner to Intermediate

What You'll Learn

• Find the failing step and the failing assertion in the formal log
• Read a counterexample waveform backwards from the failure to the cause
• Tell the inputs that cause a failure from the inputs that are only there by chance
• Explain why a counterexample is as short as possible

The Design: A FIFO Occupancy Counter

A FIFO (first in, first out buffer) keeps track of how many entries it holds. This is the counter part of a FIFO with 4 entries. A push adds an entry, a pop removes one, full blocks pushes when there is no room, and empty blocks pops when there is nothing to read:

module fifo_count (input clk, input rst, input push, input pop,
                   output reg [2:0] count, output full, output empty);
  assign full  = (count == 3'd5);     // bug: a 4-entry FIFO is full at 4
  assign empty = (count == 3'd0);
  always @(posedge clk)
    if (rst)                count <= 3'd0;
    else if (push && !full) count <= count + 3'd1;
    else if (pop && !empty) count <= count - 3'd1;
endmodule

If a push and a pop arrive in the same cycle, the push wins. That keeps the example short. A real FIFO would let both happen and keep the count unchanged.

The designer typed 5 instead of 4 in the full condition. The rule that catches it is simple: a FIFO with 4 entries never holds more than 4.

a_count: assert property (@(posedge clk) disable iff (rst) count <= 3'd4);

In the form the lab reads:

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  always @(posedge clk) if (!init) assert (count <= 3'd4);
`endif

Step 1: Read the Log

Run the check at depth 10. The log ends like this (shortened):

SBY [run] engine_0: ##   0:00:00  Checking assertions in step 7..
SBY [run] engine_0: ##   0:00:00  BMC failed!
SBY [run] engine_0: ##   0:00:00  Assert failed in fifo_count: design.sv:14.36-14.58
SBY [run] engine_0: ##   0:00:00  Writing trace to VCD file: engine_0/trace.vcd
SBY [run] summary: engine_0 (smtbmc bitwuzla) returned FAIL
SBY [run] summary: counterexample trace: run/engine_0/trace.vcd
SBY [run] summary:   failed assertion fifo_count._witness_.check_assert_design_sv_14_15 at design.sv:14.36-14.58 step 7
SBY [run] DONE (FAIL, rc=2)

Three facts come from the log before you open any waveform:

• Which property failed: the one at design.sv, line 14, columns 36 to 58. That is the assert (count <= 3'd4). When a design has several assertions, the line number tells you which one.
• When it failed: step 7. Steps start at 0, so the failure happens in the eighth clock cycle.
• Where the trace is: trace.vcd, a standard waveform file. The lab opens it for you in the waveform viewer.

The tool stopped at step 7 although the depth was 10. A bounded check looks at step 0, then step 1, and so on, and stops at the first step in which an assertion can fail. So the counterexample is always as short as possible: there is no way to break this rule in fewer than 8 cycles.

Step 2: Read the Waveform Backwards

A counterexample is read from the end. Start at the failure and ask "why" until you reach a line of RTL. Here is the trace from the lab engine:

Working backwards:

1. Step 7: the assertion fails. The value it checked is the one from step 6, where count is 5. An assert inside a clocked block samples its signals at the clock edge, so the tool reports the failure one step after the bad value appears.
2. Why is count 5 in step 6? In step 5, count was 4 and push was 1. The counter only adds 1 when full is 0, and full was 0.
3. Why was full 0 with 4 entries? Because full is defined as count == 3'd5. With 4 entries the FIFO is already full, but the design does not say so. That is the bug.

Three questions led from the symptom to the line of RTL. This is the normal way to debug a counterexample, and with practice it often takes less than a minute.

Step 3: Ignore What Does Not Matter

The trace also shows pop going high in steps 3 and 5. A beginner might think the pops are part of the bug. They are not. The solver picks a value for every input in every step, and any value that does not stop the failure is allowed. In steps 3 and 5 push is also high, and push has priority, so the pops have no effect at all.

To tell the important inputs from the accidental ones, ask: "would the failure still happen if this input had the other value?" For the pops the answer is yes, so they are noise. For the push in step 5 the answer is no: without it, count stays at 4 and the rule holds.

Step 4: Fix and Rerun

Change the full condition to count == 3'd4 and run again. The run passes: within 10 cycles no input sequence can push the count above 4. Always rerun after a fix. A fix can be incomplete, or it can break a different rule, and the next counterexample shows that at once.

A good habit is to add a second assertion that states the meaning of full directly, so that a similar mistake is caught by a clearer property next time:

a_nofull: assert property (@(posedge clk) disable iff (rst) full |-> count == 3'd4);

The operator |-> means "if the left side is true, the right side must be true in the same cycle". Chapter 3 covers it. In the lab form it is if (!init && full) assert (count == 3'd4);.

Running It in ChipVerify Lab

The example below is the buggy FIFO counter with the assertion. When the check fails, the lab loads the counterexample into the waveform viewer, where you can add count, push, pop and full and step through the cycles yourself.

Common Mistakes

always @(posedge clk) if (!init && empty) assert (count == 3'd0);
always @(posedge clk) if (!init) assert (!(full && empty));