Reading a Counterexample

Walk the Trace Backwards

1. Step 6: the wrong signal

   ack is 1 while pending_q (the value of pending one step earlier) is 0. The check asks for a pending request behind every ack. There is none.

2. Step 5: what made ack rise

   ack is registered, so look one step back. busy_cnt is 3 and pending_d is 1, but pending is already 0. The ack path read pending_d, a one-cycle-old copy.

3. Step 4: the cause

   The shaded abort is 1 on the last busy cycle. The spec allows an abort at any time, so this input is legal. The design was right until here and an input turned it wrong: that is the cause. The fix is in the RTL, ack <= pending && busy_cnt == 3.

A counterexample reads backwards. Start at the marked step: which signal is wrong? Go one step back: which state bit or input made it so? Repeat until you reach a step where the design was right and a value turned it wrong. The shaded values are the solver's choices; if a shaded value is something the environment would never do, the fix is an assumption, not an RTL change.

Four Causes of a FAIL

Wiggle Before You Assert

The habit for a new bench: write a cover for each behaviour you expect, run, and read the traces before you write a single assert. Short, odd-looking traces at this stage are normal; they show which flops the reset missed and which inputs still need an assumption. Here the cover shows a request, four busy cycles and an acknowledge, so the environment is fit to assert against. Only then run the assert and read its trace the same way. The $past in the property needs a value at the first tick (A1.2 Clocks and sampling); the engine's form keeps that value in pending_q, which starts at 0.

Asked in Interviews

Try It

assert property (@(posedge clk) disable iff (rst) ack |-> $past(pending));
cover property (@(posedge clk) disable iff (rst) req ##[1:5] ack);

reg pending_q=0;
always @(posedge clk) begin
  pending_q <= pending;
  if (!rst && ack) assert(pending_q);
end
reg [2:0] win=0;   // cycles since req, 1..5
always @(posedge clk) begin
  win <= rst ? 0 : req ? 1 : (win && win < 5) ? win + 1 : 0;
  if (!rst) cover(ack && win != 0);
end

[options]
mode bmc
depth 20
[engines]
smtbmc yices
[script]
read_verilog -formal -sv design.sv
prep -top hs_ctrl
[files]
design.sv

1. Wiggle

   Set the mode to cover and run. Read the trace: a request, busy_cnt 1, 2, 3, then ack. The cover is reported at step 7.

2. The bug trace

   Set the mode to bmc and run: FAIL at reported step 7. Walk back from step 6 to the shaded abort at step 4. RTL, assumption, property or reset?

3. The reset trace

   Fix the RTL (ack <= pending && busy_cnt == 2'd3), delete the two assume lines and every =0 initial value, and run. FAIL at reported step 1 with ack already high at step 0. RTL, assumption, property or reset?

4. Both green

   Put the reset assumption back (or the initial values): BMC PASS to depth 20.

Check Yourself

module hs_ctrl(input clk, rst, req, abort, output reg ack);
  reg pending;
  reg pending_d;
  reg [1:0] busy_cnt;
  always @(posedge clk) begin
    if (rst) begin pending<=0; pending_d<=0; busy_cnt<=0; ack<=0; end
    else begin
      pending_d <= pending;
      if (abort) pending <= 0;
      else if (req) pending <= 1;
      else if (busy_cnt == 2'd3) pending <= 0;
      busy_cnt <= pending ? busy_cnt + 2'd1 : 2'd0;
      ack <= pending && busy_cnt == 2'd3;
    end
  end
  reg pending_q;
  always @(posedge clk) begin
    pending_q <= pending;
    if (!rst && ack) assert(pending_q);
  end
endmodule