Unreachability and Coverage Closure

Three Questions About One Bin

A coverage bin is a condition, and formal can ask three things of it. Does some trace reach it (a cover)? Can no trace ever reach it (an assert of its negation under prove)? Does a trace reach it within N steps (a cover at depth N)? Only the second supports a waiver.

The third is the trap. SBY's wording for it is "Unreached cover statement", and the task status is FAIL. That is a fact about N, not about the design (F3.5).

Two Bins on seq25

Bin A is the top of a five-bit counter's range: values 25 to 31 that a covergroup would list. The proof shows no trace from reset reaches them. Bin B is live: 25 steps of setup, beyond depth 20 and inside 30 (F1.5).

The last row is the dangerous one. With a leftover assume(!start) the live bin is unreached at any depth: the environment, not the design, removed it (F3.2).

The Waiver Card

bin:         idle_cnt > 24 (idle_cnt[25:31])
proof:       assert(!bin), mode prove, abc pdr
result:      Prove PASS (abc pdr)
assumptions: reset in step 0; none on inputs
revision:    seq25 as fixed in F1.5, 2026-11-07

bin:    idle_cnt == 24 && start
proof:  cover not hit, bmc depth 20
result: unreachable

A proof holds only for the environment it ran in. Running the unreachability check with no input assumptions at all is the safe default: a bin unreachable even when the inputs may do anything is unreachable for real. Every assumption you add must be listed on the card.

Asked in Interviews

Try It

assert property (@(posedge clk) disable iff (rst) !(idle_cnt > 5'd24));
cover property (@(posedge clk) !rst && idle_cnt == 5'd24 && start);

  always @(posedge clk) begin
    if ($initstate) begin assume(rst); end else begin assume(!rst); end
  end
  always @(posedge clk) if (!rst) begin
    bin_b: cover(idle_cnt == 5'd24 && start);
  end

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

1. Cover at 20

   Run as it is and read the exact log line for the unreached cover.

2. Cover at 30

   Set depth 30 and run: Cover reached, reported step 26. Count the idle steps in the trace.

3. Prove bin A

   Replace the cover with assert(!(idle_cnt > 5'd24)) and run mode prove with abc pdr: Prove PASS (abc pdr).

4. Plant an assumption

   Add always @(posedge clk) assume(!start); and rerun the depth-30 cover. Did bin B become unreachable?

5. Write the card

   Write the waiver card for bin A from the measured log: bin, proof line, assumptions, revision.

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) idle_cnt <= 0;
      else idle_cnt <= idle_cnt + 5'd1;
      if (expired) phase <= 2'd0;
      else if (start) phase <= phase + 2'd1;
    end
  end
`ifdef FORMAL
  always @(posedge clk) begin
    if ($initstate) begin assume(rst); end else begin assume(!rst); end
  end
  always @(posedge clk) if (!rst) begin
    bin_b: cover(idle_cnt == 5'd24 && start);
  end
`endif
endmodule