Vacuity

An implication a |-> b passes in every cycle where a is false, without looking at b. If a is never true, the property passes forever and checks nothing. This is called a vacuous pass. It happens through typos, through assumptions that are too strong, and through depths that are too small, and it looks exactly like a real pass. This article shows a vacuous property that hides a bug in a state machine, and how to catch it.

8 min read | Intermediate

What You'll Learn

• Explain what a vacuous pass is and why it is dangerous
• List the common causes: unreachable triggers, over-constraining, small depth
• Detect vacuity with a cover for the trigger, or a meant-to-fail check in the lab
• Fix a property whose trigger can never happen

Passing Without Checking

An implication is a conditional rule: "if the trigger happens, the consequence must hold". In a cycle without the trigger, there is nothing to check, so the property holds. That is correct and necessary: req |=> ack should not fail in cycles without a request.

The trouble starts when the trigger never happens at all. Then every cycle is a cycle without the trigger, and the property passes without ever evaluating its consequence. The result is PASS, the same word as for a property that was checked a thousand times.

Common Causes

• A trigger that cannot happen in the design: a typo in a state value, a comparison with a value wider than the signal, two conditions that exclude each other.
• A trigger removed by assumptions: an over-constraint, as in the over-constraining article, makes the trigger impossible.
• A trigger out of reach of the depth: a bounded run that stops before the trigger can happen, like the saturating counter in the first formal run, which never reached 12 at depth 10.
• A trigger tied off by the setup: an input held at a constant by an assumption or a wrapper, so the feature it enables is never used.

Commercial tools detect vacuity automatically and report a vacuous pass as a separate status. With open-source tools you check it yourself.

The Design: a Small State Machine

A controller goes from IDLE to RUN on start, to DONE on stop, and back to IDLE. This version has a bug: after DONE it goes back to RUN:

module fsm_vac (input clk, input rst, input start, input stop, output reg [1:0] state);
  localparam IDLE = 2'd0, RUN = 2'd1, DONE = 2'd2;
  always @(posedge clk)
    if (rst) state <= IDLE;
    else case (state)
      IDLE:    if (start) state <= RUN;
      RUN:     if (stop)  state <= DONE;
      DONE:               state <= RUN;     // bug: should go to IDLE
      default:            state <= IDLE;
    endcase
endmodule

The engineer writes the rule "after DONE, the machine is IDLE", but types the state value by hand and gets it wrong:

a_done: assert property (@(posedge clk) disable iff (rst) state == 2'd3 |=> state == IDLE);  // typo: DONE is 2

State 3 does not exist in this machine. The property passes on the buggy design, and it would pass on any design.

Catching It: Cover the Trigger

For every implication, cover its trigger:

c_done: cover property (@(posedge clk) disable iff (rst) state == 2'd3);

The cover is unreachable, and that is the alarm. In SymbiYosys cover mode the log says "Unreached cover statement". Once you see it, the typo is easy to find. Use the named state instead of a number:

a_done: assert property (@(posedge clk) disable iff (rst) state == DONE |=> state == IDLE);
c_done: cover  property (@(posedge clk) disable iff (rst) state == DONE);

Now the cover is reachable, and the assertion fails at step 5 with a trace in which the machine goes from DONE back to RUN. Fix the design and it passes.

Running It in ChipVerify Lab

The lab panel does not run covers, so the trigger check is written as an assertion that is meant to fail: "the trigger never happens". If it fails, the trigger is reachable. If it passes, every implication with that trigger is vacuous.

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  // intended: after DONE the machine goes to IDLE
  // typo: compares with 3 instead of DONE (2), so the trigger never happens
  always @(posedge clk) if (!init && !$past(rst) && $past(state) == 2'd3) assert (state == IDLE);
  // trigger reachable? meant to fail
  always @(posedge clk) if (!init && !$past(rst)) assert (!($past(state) == 2'd3));
`endif

On the lab engine everything passes, including the check that was meant to fail. That pass is the warning: the trigger $past(state) == 2'd3 never happens within the depth.

Common Mistakes