Assert, Assume, Cover: The Three Verbs

One Statement, Three Jobs

The verb says who is responsible. Assume what the environment does. Assert what the design does. Cover what you expect to be possible. An assume on an output is the tool-side name for cheating: F3.1 makes this the master rule.

The Same Line, Four Runs

Row 2 is the trick from the hook. The assert became an assume and bmc drops the cover, so nothing is left to check. Plain SBY would print PASS anyway. This site refuses the job: a pass with no obligation means nothing. Row 3 is refused for the same reason.

Row 4 is what the inherited bench did, and no tool refuses it: the assert is "proven" because every world with two grants has been discarded. Row 6 is the sanity check that exposes it: the double grant became unreachable, and the design did not change.

Row 7 is the right shape of assumption, on an input. It also passes, and now the question is one for the spec, not the tool: does firmware ever write A5? In the F1.1 story it did. An assumption is a claim about the environment, and it goes into the sign-off list where someone must sign it (F7.3).

How the Engine Sees the Verbs

assert property (@(posedge clk) disable iff (rst) $onehot0(gnt));
assume property (@(posedge clk) disable iff (rst) $onehot0(gnt));
cover property (@(posedge clk) !rst && !$onehot0(gnt));

always @(posedge clk) if (!rst) begin
  assert($onehot0(gnt));
  assume($onehot0(gnt));
  cover(!$onehot0(gnt));
end

On this site a bmc or prove task keeps asserts and assumes and drops covers. A cover task drops asserts, keeps assumes and searches for the shortest trace to each cover. So one design file can carry all three verbs, and the mode selects the job. The reset is itself an assumption: rst high in the $initstate step and low afterwards (F1.6).

Asked in Interviews

Try It

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

1. Assert

   Run as it is: mode bmc. Read FAIL at reported step 5. The cover line is ignored in this mode.

2. Assume

   Change assert( to assume( and run again: refused, because bmc drops the cover and no assertion is left. Add the assert line under the assume, run: PASS. Is the bug fixed?

3. Cover

   Set the mode to cover and run. With the assume in place the double grant is unreached. Remove the assume: the cover is reached at reported step 5, and the trace is the F1.1 counterexample.

4. The right assumption

   Back in mode bmc, delete the assume on gnt and add assume(weight != 8'hA5); beside the assert. PASS. Then decide: does the real firmware never write A5?

Check Yourself

module arb3(input clk, rst, input [2:0] req, input [7:0] weight, output reg [2:0] gnt=0);
  reg lock=0;
  reg [1:0] reload=0;
  wire [2:0] pri  = req[0] ? 3'b001 : req[1] ? 3'b010 : req[2] ? 3'b100 : 3'b000;
  wire       hold = lock && |(req & gnt);
  always @(posedge clk) begin
    if (rst) begin gnt<=0; lock<=0; reload<=0; end
    else begin
      lock   <= weight[7];
      reload <= (weight == 8'hA5 && req == 3'b110) ? 2'd1 : (reload == 2'd1 && req == 3'b011) ? 2'd2 : 2'd0;
      if (reload == 2'd2 && req == 3'b111) gnt <= gnt | pri;   // reload cycle: lock holds, encoder grants too
      else gnt <= hold ? gnt : pri;
    end
  end
  always @(posedge clk) begin
    if ($initstate) begin assume(rst); end else begin assume(!rst); end
  end
  always @(posedge clk) if (!rst) begin
    assume($onehot0(gnt));
    assert($onehot0(gnt));
    cover(!$onehot0(gnt));
  end
endmodule