Weak and strong: what the end of a test means

Attempts still running at the end

A safety rule, such as "rlast never rises without rvalid", fails at a definite edge. A liveness rule, such as "every read is answered", fails only if the answer never comes. A simulation always stops after a finite time, so that moment never arrives.

When $finish runs, some attempts are still waiting. Each property has a strength that decides their fate. A weak attempt that is still waiting ends with no verdict. A strong attempt that is still waiting fails at the end of the run.

The first row holds the surprise. The weakness comes from that default, not from any operator, so a bounded window is weak too. If the test stops while the window is still open, that attempt never fails, however close it was to its deadline.

Pending at the end

Both figures check the same traffic: one request answered two edges later, one request the DUT drops, and one legal request still in flight when the test stops at 120.

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

  ack_within_4: assert property (@(posedge clk) req |-> ##[1:4] ack);

  initial begin
    @(negedge clk); req = 1;            // request at 15
    @(negedge clk); req = 0;
    @(negedge clk); ack = 1;            // answered at 35
    @(negedge clk); ack = 0; req = 1;   // request at 45: the DUT drops it
    @(negedge clk); req = 0;
    repeat (5) @(negedge clk);
    req = 1;                            // request at 105, legal, answer due at 125
    @(negedge clk); req = 0;
    @(negedge clk);
    $finish;                            // the test stops at 120
  end
endmodule

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

  ack_some_time: assert property (@(posedge clk) req |-> s_eventually ack);

  initial begin
    @(negedge clk); req = 1;            // request at 15
    @(negedge clk); req = 0;
    @(negedge clk); ack = 1;            // answered at 35
    @(negedge clk); ack = 0; req = 1;   // request at 45: the DUT drops it
    @(negedge clk); req = 0;
    repeat (5) @(negedge clk);
    req = 1;                            // request at 105, legal, answer due at 125
    @(negedge clk); req = 0;
    @(negedge clk);
    $finish;                            // the test stops at 120
  end
endmodule

Read the two figures together. The bounded rule caught the dropped request at a definite edge, but skipped the last one without a word. The strong rule caught both, and blamed a legal request as well. Neither is trustworthy until the test stops cleanly.

Weak with no deadline checks nothing

In arvalid |-> ##[1:$] rvalid the consequent is a plain sequence, so it is weak, and $ takes away the deadline. A dropped request waits forever, so in simulation its attempt can never fail. In the example below it stays silent where both other rules report.

Treat such a rule in a simulation suite as a check that cannot fire. Replace it with a bound, or with s_eventually and a clean end of test.

Bounds are what simulation can use

A bound turns liveness into safety. arvalid |-> ##[1:16] rvalid says that no read waits more than 16 edges. It fails at a definite edge, close to the bug, and the number records a real requirement.

Take the bound from the specification or from the design's worst case, then add a margin. A bound that is too tight fails on legal traffic. One that is too loose, such as 1,000,000, behaves like ##[1:$] in a short test.

assert property (@(posedge clk)
  arvalid |-> ##[1:$] rvalid);

assert property (@(posedge clk)
  arvalid |-> ##[1:16] rvalid);

Choosing a strength

Each form has its own job. A bound states a latency requirement and reports at a definite edge, so it is the main check in simulation. s_eventually states that something must happen when no limit is given, and it only makes sense in a test that drains. A weak consequent with no deadline states nothing that a simulation can refute.

Strong rules also help when a test hangs. If a watchdog stops a stuck test with $finish, every strong attempt still open fails at that moment, and each failure names a request that never completed. That is a far better starting point for debugging than a bare timeout message.

Ending a test cleanly

Both kinds of rule need the same thing from the test. Stop new traffic, wait until every outstanding request has been answered, then call $finish. After this drain, every bounded window has closed, and a strong failure at the end can only mean a lost request.

Drain on state rather than on a guess: wait until the scoreboard has nothing outstanding, with a timeout of the longest bound. Then check that count at the end of the test, as Module 2 did. The assertions and the scoreboard agree when everything is correct, and each catches mistakes in the other.

Explicit strong(...) and weak(...) wrappers are not covered yet.

Try it

All the traffic was legal. The test stopped at 80 while the request from 75 was still waiting for its answer, so the strong rule failed. The bounded rule stayed silent because its open window is weak, and the rule with no deadline cannot fail at all.

Add a drain before the $display: raise ack at the next falling edge, clear it, wait two more edges, and predict the output.

Check yourself

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

  // Three ways to say "every request is answered".
  bounded:           assert property (@(posedge clk) req |-> ##[1:4] ack)
    else $display("t=%0t bounded failed", $time);
  strong_eventually: assert property (@(posedge clk) req |-> s_eventually ack)
    else $display("t=%0t strong_eventually failed", $time);
  weak_unbounded:    assert property (@(posedge clk) req |-> ##[1:$] ack)
    else $display("t=%0t weak_unbounded failed", $time);

  initial begin                         // legal traffic: each answer two edges later
    @(negedge clk); req = 1;            // request at 15
    @(negedge clk); req = 0;
    @(negedge clk); ack = 1;            // answered at 35
    @(negedge clk); ack = 0; req = 1;   // request at 45
    @(negedge clk); req = 0;
    @(negedge clk); ack = 1;            // answered at 65
    @(negedge clk); ack = 0; req = 1;   // request at 75, answer due at 95
    @(negedge clk); req = 0;
    @(negedge clk); ack = 1;            // answered at 95
    @(negedge clk); ack = 0;
    repeat (2) @(negedge clk);          // drain
    $display("t=%0t test ended", $time);
    $finish;
  end
endmodule

req |-> ##[1:4] ack

req |=> ##[0:5] ack

req |-> ##[1:8] ack

req |-> ##[1:$] ack

Practice

• Answer in time Verify · Medium