Your First Proof: The Same SVA, No Testbench

Two Benches, One Rule

A simulation bench drives one sequence. The A1.3 driver walked 18,000 addresses below F0, so rresp was never SLVERR, the antecedent never held, and every attempt of the assertion passed without checking anything. A formal bench has no driver. The design, the property and a reset assumption are the whole setup; the inputs are free, and at every step the solver may give them any value.

Three words from here on. A property is the rule. A counterexample is a trace that breaks it. A proof is the tool's statement that no counterexample exists within what it checked, bounded or unbounded (F1.5).

Read the Counterexample

The tool found the one sequence that breaks the rule and wrote it down: a .vcd with every signal, step by step. The shaded rows are the inputs it chose; the marked step is where the assertion fails. A formal counterexample is a directed test the tool wrote for you, and SBY also writes trace_tb.v, a testbench that replays it in any simulator.

The |-> row fails one step earlier because the overlapping implication asks for !rvalid in the same cycle as the handshake, while rvalid is still high by definition. That is the wrong property, not a second bug; F1.4 sorts the two apart.

The Property in Two Forms

assert property (@(posedge clk) disable iff (rst) rvalid && rready && rresp == 2'b10 |=> !rvalid);

reg err_done=0;
always @(posedge clk) begin
  err_done <= !rst && rvalid && rready && rresp == 2'b10;
  if (!rst && err_done) assert(!rvalid);
end

Both forms say the same thing. |=> becomes a flop that remembers "an SLVERR completed last cycle" and an assert guarded by it. The page shows the SVA because that is what the industry writes, and the engine form because that is what runs here; F3.1 teaches the translation table. In a real project the formal file is bound to the design, never edited into it (A7.1 Packaging and binding).

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

What the Result Establishes

The fixed twin passes BMC at depth 20: no input sequence of up to 20 cycles from reset breaks the rule. That is a bounded result with its depth attached, not a proof for all time. The buggy twin fails at reported step 4; a FAIL is a reachable counterexample from the assumed reset.

Asked in Interviews

Try It

1. Run and read

   Run as it is: FAIL at reported step 4. In the trace find the address the solver chose; any value at or above F0 breaks the rule, and the exact value may differ between solvers.

2. Change the implication

   Clear the err_done block, paste the concurrent property into props.sv, change |=> to |-> and run. FAIL one step earlier: the same-cycle check asks for !rvalid while the handshake is happening.

3. Fix the RTL

   Replace the condition rresp == 2'b10 && !extra with 1'b0, leave props.sv blank, and run: BMC PASS to depth 20.

Check Yourself

module rd_slave(input clk, rst, arvalid, input [7:0] araddr,
  input rready, output arready, output reg rvalid=0,
  output reg [1:0] rresp=0, output reg [7:0] rdata=0);
  reg extra=0;
  assign arready = !rvalid;
  always @(posedge clk) begin
    if (rst) begin rvalid<=0; rresp<=0; rdata<=0; extra<=0; end
    else if (rvalid && rready) begin
      if (rresp == 2'b10 && !extra) extra<=1;
      else begin rvalid<=0; extra<=0; end
    end else if (arvalid && arready) begin
      rvalid<=1; rresp <= araddr >= 8'hf0 ? 2'b10 : 2'b00;
      rdata<=araddr; extra<=0;
    end
  end
  always @(posedge clk) begin
    if ($initstate) begin assume(rst); end else begin assume(!rst); end
  end
  reg err_done=0;
  always @(posedge clk) begin
    err_done <= !rst && rvalid && rready && rresp == 2'b10;
    if (!rst && err_done) assert(!rvalid);
  end
endmodule