Implication and vacuous success

Antecedent, implication, consequent

Most properties have the form antecedent |-> consequent. The antecedent is the trigger, a condition or sequence that starts the check. The consequent is what must then hold.

At every clock edge, the assertion starts a new attempt. If the antecedent matches at that edge, the attempt checks the consequent and passes or fails. If the antecedent does not match, the attempt ends at once with a vacuous success.

Attempts overlap. A rule with a three-cycle consequent can have three attempts in progress at once, each started by a different edge and each with its own result.

Overlapped and non-overlapped

The overlapped implication |-> starts the consequent at the same edge where the antecedent ends. The non-overlapped implication |=> starts it one edge later, and a |=> b means exactly a |-> ##1 b.

Choose from the spec, not from what makes a test pass. The rule "while rlast is high, rvalid is high" is about one edge, so it uses |->. The rule "a stalled offer is still there at the next edge" relates two edges, so it uses |=>.

Vacuous success

A vacuous success is still a success. The assertion does not fail, and its pass action, if it has one, runs as for a real pass, which is how the dashboard in the opening story counted 18,000 passes.

module tb;
  logic clk = 0;
  always #5 clk = ~clk;                 // rising edges at 5, 15, 25, ...
  logic req = 0, gnt = 0;

  gnt_next: assert property (@(posedge clk) req |=> gnt);

  initial begin
    @(negedge clk); req = 1;            // request sampled at 15
    @(negedge clk); req = 0; gnt = 1;   // grant sampled at 25 and 35
    @(negedge clk);
    @(negedge clk); req = 1; gnt = 0;   // request sampled at 45
    @(negedge clk); req = 0;            // no grant at 55
    @(negedge clk);
    $finish;
  end
endmodule

So a pass count says nothing about whether a rule was exercised. What matters is how often the antecedent matched. Count that separately, with a small counter or with a cover property on the antecedent, and treat a count of zero as a hole in the tests.

Counting the real checks

A few lines beside the assertion show how often a rule was really exercised: always @(posedge clk) if (rvalid && rready && rresp == 2) n_err++;. Print the count at the end of the test, or fail the test when it is zero.

Report the count next to the assertion's name in the regression summary. A rule with thousands of passes and zero real checks then stands out at a glance, instead of hiding behind a green status.

Longer antecedents

An antecedent can be a short sequence rather than a single condition. rvalid && !rready ##1 rvalid && !rready |-> ... triggers only on the second edge of a stall, for a rule about long stalls.

Keep antecedents short and of fixed length where you can. A long or open-ended antecedent makes it hard to see which edges started an attempt, and harder still to count real checks.

A rule with two triggers in a row, "after a, if b follows, then c", is clearest as one sequence: a ##1 b |=> c. The nested form a |=> b |=> c means the same by the standard, but it is not covered yet. In a measured run, Verilator 5.052 missed its failure, while the flat form reported it at 85.

Designing the antecedent

An antecedent that is too wide makes a rule fail on legal traffic. rvalid |=> rvalid says a valid offer is always followed by another one, which is false after the last beat of a burst. rvalid && !rready |=> rvalid triggers only on a stall, which is what the rule is about.

An antecedent that is too narrow makes a rule check almost nothing. An antecedent that requires a rare combination, such as an error response on the last beat of a 16-beat burst, may never match in a whole regression.

assert property (@(posedge clk)
  rvalid ##1 rready);

assert property (@(posedge clk)
  rvalid |=> rready);

Without an implication, a property must hold from every single edge. That is right for invariants such as !(full && empty), and wrong for any rule that starts with "when" or "after".

Try it

The error-response rule passed at all 7 edges, yet its antecedent never matched: every pass was vacuous. The sequence written without an implication failed at every edge where rvalid was low, including legal idle cycles.

Add one error transfer to the stimulus by setting rresp = 2; at the falling edge before a transfer, and predict all three counts.

Check yourself

module tb;
  logic clk = 0;
  always #5 clk = ~clk;                  // rising edges at 5, 15, 25, 35
  logic a = 0, b = 0;
  int passes, fails;
  p: assert property (@(posedge clk) a |-> b) passes++; else fails++;
  initial begin
    #40 $display("passes=%0d fails=%0d", passes, fails);
    $finish;
  end
endmodule

rvalid && rready && rresp == 2 |-> ##1 !rvalid

rvalid && rready && rresp == 2 ##1 !rvalid

rvalid && rready && rresp == 2 |=> !rvalid

if (rvalid && rready && rresp == 2) ##1 !rvalid