Safety and Liveness, Bounded and Unbounded

A Failing Step, or a Loop

If a safety property is violated, there is a step where it breaks, and a finite trace shows it. A liveness property has no such step: the grant might still come, so no finite trace can refute it. Its counterexample is a loop, a cycle of states the design can repeat forever without granting. A tool must reason about loops to check it, which is why live mode uses a different engine and needs fairness assumptions about the environment (F3.7).

What PASS at Depth 20 Promises

bmc at depth N checks every input sequence from reset up to its bound and nothing beyond. PASS means "no violation within the bound". A bug at sampled state 26 is invisible at depth 20 and visible at 28. Write the depth into every bounded result, because a bounded PASS without its depth is not a result.

How deep is deep enough? Count the deepest counter and the longest transaction in the design. Here the idle timer alone needs 24 idle cycles after reset to reach 24, so a bound of 20 could never have seen the bug. The sign-off team could have known that before running. F4.1 turns this count into a required depth and F7.3 into a sign-off rule.

A Bounded Check or a Proof

prove mode asks for an unbounded answer: the property holds in every reachable state, forever. SBY's smtbmc proves it by k-induction (F2.4), abc pdr by IC3 (F2.5). Here both close on the fixed design, and the property is inductive on its own: when idle_cnt is at most 24, the next value is 0 or at most 24. A prove PASS is a proof. A bmc PASS is a bounded result and must carry its depth.

On the buggy design the base case passes and the induction step fails, so prove returns UNKNOWN: a proof not yet found, which is neither PASS nor FAIL. Only bmc at depth 28 or more turns the bug into a FAIL with a trace from reset.

Asked in Interviews

Try It

assert property (@(posedge clk) disable iff (rst) idle_cnt <= 5'd24);

always @(posedge clk) if (!rst)
  assert(idle_cnt <= 5'd24);

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

1. Depth 20

   Run as it is: BMC PASS to depth 20. Read the summary line. Is the design proven?

2. Depth 30

   Set the depth to 30 and run: FAIL at reported step 27. In the trace find the timer at 24 with start high, then 25.

3. The boundary

   Try depths 27 and 28. The smallest depth that fails is 28: it checks samples 0 to 26, and the violation is sample 26.

4. Prove it

   Fix the clear (else if (expired) idle_cnt <= 0;), set the mode to prove and the depth to 2, run: Prove PASS. Switch the engine to abc pdr: PASS again. Then run prove on the buggy design and read UNKNOWN.

Check Yourself

module seq25(input clk, rst, busy, start, output expired, output reg [1:0] phase=0);
  reg [4:0] idle_cnt=0;
  assign expired = idle_cnt == 5'd24;
  always @(posedge clk) begin
    if (rst) begin idle_cnt<=0; phase<=0; end
    else begin
      if (busy) idle_cnt <= 0;
      else if (expired && !start) idle_cnt <= 0;   // bug: start on the expiry cycle skips the clear
      else idle_cnt <= idle_cnt + 5'd1;
      if (expired) phase <= start ? 2'd3 : 2'd0;
      else if (start) phase <= phase + 2'd1;
    end
  end
  always @(posedge clk) begin
    if ($initstate) begin assume(rst); end else begin assume(!rst); end
  end
  always @(posedge clk) if (!rst) assert(idle_cnt <= 5'd24);
endmodule