Under-Constraint and Counterexample Triage

Too Few Assumptions

With no assumptions the solver may drive input sequences no legal neighbour produces. A FAIL built on one is a false failure: the design misbehaved in a world the spec forbids. That is under-constraint, the other end of the dial from F3.2.

The flow keeps you from fixing the wrong thing. Start state first, then inputs, then the check, and only then the RTL. Run A stops at question 2, and the hook's designer skipped straight to question 4.

The Handshake Rule People Get Backwards

One assumption, on the inputs arvalid and araddr, written from that row. The engine refuses $stable(araddr) on a primary input (it reports UNSUPPORTED_INPUT_HISTORY: araddr for $past(araddr) too), so the bench compares with araddr_q, last cycle's address. The response rule reads it the same way.

The capture bug fails under the honest assumption too, at reported step 3: a read accepted in its first cycle returns the stale copy. Walk that trace through the flow: step 0 is reset, every input is legal, the check matches the spec. Box 4: the RTL.

Did the Assumption Go Too Far?

Two wrong fixes silence run A just as well. assume(!arvalid) kills every cover: nothing happens. Freezing the address keeps the stall and the handshake but loses the top address, so a cover at each extreme of a data input earns its place.

Asked in Interviews

Try It

assume property (@(posedge clk) disable iff (rst) arvalid && !arready |=> arvalid && $stable(araddr));
assert property (@(posedge clk) disable iff (rst) arvalid && arready |=> rvalid && rdata == $past(araddr) + 8'd1);
assert property (@(posedge clk) disable iff (rst) rvalid && !rready |=> rvalid && $stable(rdata));

assume property (@(posedge clk) disable iff (rst) arvalid && !arready |=> arvalid && araddr == araddr_q);
assert property (@(posedge clk) disable iff (rst) arvalid && arready |=> rvalid && rdata == araddr_q + 8'd1);
assert property (@(posedge clk) disable iff (rst) rvalid && !rready |=> rvalid && $stable(rdata));

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

1. Run free

   Run as it is: FAIL at reported step 5. Walk the trace through the four questions and stop at the first "no".

2. Write one assumption

   Add the handshake assumption as the first line of props.sv and run: BMC PASS to depth 20.

3. Check it with covers

   Replace the two assertions with the three covers, mode cover: all reached.

4. Find a real bug

   Make the response always use addr_cap and run under the assumption: FAIL at reported step 3. The flow ends at box 4.

5. Try a wrong fix

   Swap the assumption for assume(!arvalid) in design.sv. Green in bmc; now run the covers.

Check Yourself

module rd_slave_sp(input clk, rst, arvalid, input [7:0] araddr, input rready,
  output arready, output reg rvalid=0, output reg [7:0] rdata=0);
  reg [7:0] addr_cap=0;   // the speculative copy
  reg waited=0;           // arvalid was high last cycle without a handshake
  assign arready = !rvalid;
  always @(posedge clk)
    if (rst) begin rvalid <= 0; waited <= 0; end
    else begin
      if (arvalid && !waited) addr_cap <= araddr;   // capture in the first arvalid cycle
      waited <= arvalid && !arready;
      if (rvalid && rready) rvalid <= 0;
      else if (arvalid && arready) begin
        rvalid <= 1;
        rdata  <= (waited ? addr_cap : araddr) + 8'd1;
      end
    end
`ifdef FORMAL
  always @(posedge clk) begin
    if ($initstate) begin assume(rst); end else begin assume(!rst); end
  end
  reg [7:0] araddr_q=0;   // last cycle's araddr, the registered form of $past(araddr)
  always @(posedge clk) araddr_q <= araddr;
`endif
endmodule

assert property (@(posedge clk) disable iff (rst) arvalid && arready |=> rvalid && rdata == araddr_q + 8'd1);
assert property (@(posedge clk) disable iff (rst) rvalid && !rready |=> rvalid && $stable(rdata));