Cover: Reachability, Witnesses and Dead Code

The First Run on Every Bench

A cover asks the tool to reach a condition and to show the shortest sequence that does (F1.3). From reset, full on a sixteen-entry FIFO needs sixteen pushes, so count before you run: step 0 is reset, and sixteen pushes end at step 16. The measured trace has full at step 17, reported at 18.

Run the covers before you trust any assertion. They show the design moving under the assumptions you wrote. This is the "wiggling" stage of a new bench (F1.4).

One Leftover Line, Every Cover Gone

With the leftover assumption, nothing can enter the FIFO and all three covers fail. Every assertion in that bench was checked against an empty FIFO only. The covers took one line each.

Write the first covers from the spec, not from the RTL: each queue empty and full, each state of each machine, each input at its extremes, each documented flow. One sentence of the spec, one cover.

Why a Cover Is Unreached

wire wr_en = push && !full;
...
if (wr_en && full) overflow <= 1;

if (push && full) overflow <= 1;

overflow is unreached with no assumption in the way: dead logic. The depth is the boring third reason. At depth 10, cover(full) gives "Cover unreached within the depth", because sixteen pushes do not fit in ten steps.

Dead logic is either a bug or a register to delete, and only the designer can say which. Here the designer meant to report a refused push, so the flag is a bug. Either way, an unreached cover on it was the first sign.

Asked in Interviews

Try It

cover property (@(posedge clk) !rst && full);
cover property (@(posedge clk) !rst && push && pop && full);
cover property (@(posedge clk) !rst && overflow);

always @(posedge clk) if (!rst) begin
  c_full:      cover(full);
  c_both_full: cover(push && pop && full);
  c_overflow:  cover(overflow);
end

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

1. Run the covers

   Run as it is: Cover unreached within the depth. Two covers are reached at reported step 18; read which one the log names.

2. Count the pushes

   Delete the other two covers and run cover(full) alone. Count the pushes in the trace.

3. Plant the leftover

   Add assume(!push); above the covers and run. Which assumption would you look for first?

4. Read the overflow RTL

   Decide which of the three reasons applies to overflow, and what the designer meant.

5. Shrink the depth

   Set depth 10 and run cover(full): Cover unreached within the depth.

Check Yourself

module fifo16(input clk, rst, push, pop, input [7:0] wdata,
  output [7:0] rdata, output empty, output full);
  reg [7:0] mem [0:15];
  reg [3:0] wr_ptr=0, rd_ptr=0;
  reg [4:0] count=0;
  assign empty = count == 5'd0;
  assign full  = count == 5'd16;
  wire wr_en = push && !full, rd_en = pop && !empty;
  assign rdata = mem[rd_ptr];
  always @(posedge clk)
    if (rst) begin wr_ptr <= 0; rd_ptr <= 0; count <= 0; end
    else begin
      if (wr_en) begin mem[wr_ptr] <= wdata; wr_ptr <= wr_ptr + 4'd1; end
      if (rd_en) rd_ptr <= rd_ptr + 4'd1;
      count <= count + wr_en - rd_en;
    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
    c_full: cover(full);
  end
`endif
endmodule