What a Proof Covers

The Cone of One Property

read_verilog -formal -sv design.sv
prep -top ctr_dbg
flatten
opt_clean
write_json net.json
cd ctr_dbg
select -write cone_a_cnt.txt a_cnt %ci* t:$dff t:$mem_v2 %u %i
select -write cone_a_dbg.txt a_dbg %ci* t:$dff t:$mem_v2 %u %i

# cone_a_cnt.txt   count fast
# cone_a_dbg.txt   count count_q dbg fast past

A property reads a few signals. Those depend on registers, which depend on inputs and other registers. Everything reachable backwards from the property is its cone of influence. Logic outside the cone cannot change the verdict, so tools drop it before solving.

One More Property, a Bigger Map

The first run was a true proof of a true property. It said nothing about dbg, because dbg was not in its cone. Coverage starts by asking which logic your properties read at all.

The Map of the Module Spine

White logic is unverified, not wrong. Here the white part is the data, the one thing a FIFO exists to keep. COI coverage is cheap and runs early, so run it before you believe a green dashboard. The next lesson measures what that white memory hides.

Inside the Cone: The Proof Core

fast is in the cone, yet the proof survives its cut: the counter stays at or below 9 at either speed. The part of the cone a proof needs is its proof core. The open tools do not print it; one cut per register measures it.

Logic in the cone but outside the core is a review question. It may be dead, redundant, or simply checked by no property. Here the speed mode needs its own property.

Bounded Coverage

Cover mode prints the step each cover was reached at. The deepest one, step 8, is the shortest trace that shows that behaviour. A bounded proof below it never saw that behaviour; F7.3 turns this into a required depth.

Asked in Interviews

Try It

The lab is ctr_dbg with the mirror bug and only the count property: Prove PASS (k = 10) in 0.5 s. Both rules in concurrent SVA; the design carries their immediate forms.

assert property (@(posedge clk) disable iff (rst) count <= 4'd9);
assert property (@(posedge clk) disable iff (rst) dbg == $past(count));

1. Read the claim

   Run as it is. PASS: but is dbg verified? Check the cone listing above.

2. Grow the map

   Add if (past) a_dbg: assert(dbg == count_q); to the check block and run. Read the step where dbg falls behind.

3. Cut inside the cone

   Fix the mirror, delete the new check, and turn fast into $anyseq. Then cut count instead. Which register is in the core?

Check Yourself

module ctr_dbg(input clk, rst, en, fast_in, output [3:0] count_o, dbg_o);
  reg [3:0] count = 0;   // the counter
  reg fast = 0;          // speed mode, loaded by software
  reg [3:0] dbg = 0;     // debug mirror: count, one cycle late
  assign count_o = count;
  assign dbg_o = dbg;
  always @(posedge clk)
    if (rst) begin count <= 0; fast <= 0; dbg <= 0; end
    else begin
      fast <= fast_in;
      if (en) count <= (count == 4'd9 || fast && count == 4'd8) ? 4'd0 : count + (fast ? 4'd2 : 4'd1);
      if (!(en && count == 4'd9)) dbg <= count;   // bug: skips the wrap cycle
    end
  always @(posedge clk) begin
    if ($initstate) begin assume(rst); end else begin assume(!rst); end
  end
  reg past = 0;
  reg [3:0] count_q = 0;           // registered copy for the mirror check
  always @(posedge clk) begin past <= !rst; count_q <= count; end
  always @(posedge clk) if (!rst) begin
    a_cnt: assert(count <= 4'd9);
  end
endmodule

module ctr_dbg(input clk, rst, en, fast_in, output [3:0] count_o, dbg_o);
  reg [3:0] count = 0;   // the counter
  reg fast = 0;          // speed mode, loaded by software
  reg [3:0] dbg = 0;     // debug mirror: count, one cycle late
  assign count_o = count;
  assign dbg_o = dbg;
  always @(posedge clk)
    if (rst) begin count <= 0; fast <= 0; dbg <= 0; end
    else begin
      fast <= fast_in;
      if (en) count <= (count == 4'd9 || fast && count == 4'd8) ? 4'd0 : count + (fast ? 4'd2 : 4'd1);
      if (!(en && count == 4'd9)) dbg <= count;   // bug: skips the wrap cycle
    end
  always @(posedge clk) begin
    if ($initstate) begin assume(rst); end else begin assume(!rst); end
  end
  reg past = 0;
  reg [3:0] count_q = 0;           // registered copy for the mirror check
  always @(posedge clk) begin past <= !rst; count_q <= count; end
  always @(posedge clk) if (!rst) begin
    a_cnt: assert(count <= 4'd9);
    if (past) a_dbg: assert(dbg == count_q);
  end
endmodule