Over-Constraint and Vacuity

Too Many Assumptions

An assumption removes input sequences. Remove the right ones and the tool checks the legal environment. Remove one too many and it checks a world the chip never sees: over-constraint. Nothing in a PASS says which zone you are in (F1.3).

The internal assumption also breaks the master rule of F3.1: it constrains the design through its own register. The FIFO bug lives exactly in the gap between full and count == 16.

restrict is an assumption that only formal honours, and it hides the bug just as well. It exists for case splits (F4.3), never for silencing a failure.

The Cover Is the Alarm

For every behaviour an assumption touches, cover the case you still expect to happen. A push at sixteen is legal for this producer, and the internal assumption made it unreachable. SBY names the unreached cover in its log: that line is the alarm.

Vacuity in Formal

push && count == 16 |-> ...
// this test never filled the FIFO

assume(!(push && count == 5'd16));
// no legal input sequence fills it and pushes

In simulation (A1.3 Implication and vacuous success) vacuity is a weak test. In formal it is a statement about the whole environment, caused by the assumptions or by dead logic (F3.5). Commercial tools flag some of it automatically; in SBY you write the cover yourself, so make it a habit.

The habit is cheap: one cover per assumption, naming the legal behaviour closest to what the assumption forbids. For !(push && full) that is a push at sixteen, which an honest producer may still make in the lag cycle.

Asked in Interviews

Try It

assert property (@(posedge clk) disable iff (rst) count <= 5'd16);
assume property (@(posedge clk) disable iff (rst) !(push && full));
// the dishonest variant:
assume property (@(posedge clk) disable iff (rst) !(push && count == 5'd16));

always @(posedge clk) if (!rst) begin
  assume(!(push && count == 5'd16));
  assert(count <= 5'd16);
end

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

1. Run the internal assumption

   Run as it is: BMC PASS to depth 20. Fixed?

2. Cover under it

   Swap the assert for the three covers and set mode cover. Read which cover the log names as unreached.

3. Honest assumption

   Back in mode bmc, assume !(push && full) instead: FAIL at reported step 19. Find the lag cycle in the trace.

4. Cover under the honest one

   Run the three covers again: all reached.

5. Fix the RTL

   Drive full from count == 16 combinationally and rerun the honest bench: BMC PASS to depth 20.

Check Yourself

module fifo16(input clk, rst, push, pop, input [7:0] wdata,
  output [7:0] rdata, output empty, output reg full=0);
  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;
  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; full <= 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;
      full <= count == 5'd16;   // bug: one cycle behind count
    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
    assume(!(push && count == 5'd16));
    c_full:      cover(full);
    c_push_at16: cover(count == 5'd16 && push);
    c_pop_empty: cover(pop && empty);
  end
`endif
endmodule