An attempt every tick

A concurrent assertion is not one watcher that rearms. At every clock tick a brand-new evaluation attempt begins, independent of all earlier attempts, and attempts overlap freely while each runs its own evaluation.

The diagram shows two requests in flight at once under req |-> ##2 ack. A hand-rolled wait-for-ack watcher would have missed the second request entirely.

Watch ack against the two requests. Each attempt needs ack exactly two slots after its own request.

• Slot 0: req 0, ack 0. Idle, and the attempt passes vacuously.

• Slot 1: req 1. Attempt A opens; it needs ack at slot 3.

• Slot 2: req 1. Attempt B opens; it needs ack at slot 4.

• Slot 3: ack 1. Attempt A passes, while B is still waiting.

• Slot 4: ack 1. Attempt B passes.

• Slot 5: idle, vacuous. Slot 6: idle, vacuous.

This design is universal quantification over time. Every request gets an ack means an attempt per tick, and it explains assertion cost: an always-true antecedent on a hot clock starts millions of live attempts.

Threads within an attempt

Inside one attempt, nondeterministic constructs fork multiple evaluation threads. A windowed delay ##[1:3] ack forks three threads: ack in 1, in 2, in 3. Repetition ranges and disjunctions do the same.

For an assert directive the attempt passes when at least one thread matches. It fails only when every thread has died without matching, so windowed failures always report late.

1
2
3
4
5

// snippet
// constructs that fork threads inside one attempt
// ap_win: assert property (@(posedge clk) req |-> ##[1:3] ack);
// ap_unbnd: assert property (@(posedge clk) req |-> ##[1:$] ack);
// ap_or: assert property (@(posedge clk) start |-> (fast_done or ##[2:5] slow_done));

Vacuity and the cover pairing

Every attempt ends in exactly one of three ways. A non-vacuous pass matched the antecedent and held the consequent, a vacuous pass never matched the antecedent and checked nothing, and a fail broke the rule. Simulators count the three buckets separately.

The standard hygiene pairs every assert with a cover on its antecedent. If the cover never hits, the assert only ever passed vacuously.

1
2
3
4
5

// snippet
// ap_req_ack: assert property (@(posedge clk) disable iff (!rst_n)
//   req |-> ##[1:3] ack) else $error("ack window missed");
// if this cover never hits, ap_req_ack only ever passed vacuously
// cp_req_seen: cover property (@(posedge clk) disable iff (!rst_n) req);

The bench runs req |-> ##2 ack for real over the two-request script in the diagram. The pass action counts every passing attempt, vacuous ones included, and the paired cover counts the real ones. A second script plants the trap: two requests, one ack.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37

module tb_attempts;
  logic clk = 0;
  always #5 clk = ~clk;
  logic req = 0, ack = 0;
  int passes = 0, fails = 0, real_req = 0, ticks = 0;

  // The pass action runs for every attempt that passes, vacuous ones included.
  ap_req_ack: assert property (@(posedge clk) req |-> ##2 ack) passes++; else fails++;
  // The paired cover counts only attempts whose antecedent matched.
  cp_req: cover property (@(posedge clk) req) real_req++;
  always @(posedge clk) ticks++;

  task automatic idle(int n); repeat (n) @(negedge clk); endtask

  initial begin
    // Two overlapping requests, each answered two cycles later.
    @(negedge clk); req = 1;
    @(negedge clk); req = 1;
    @(negedge clk); req = 0; ack = 1;
    @(negedge clk); ack = 1;
    @(negedge clk); ack = 0;
    idle(3);
    $display("script 1: %0d ticks, %0d passes (%0d real, %0d vacuous), %0d failures",
             ticks, passes, real_req, passes - real_req, fails);
    if (fails != 0 || real_req != 2) $fatal(1, "FAIL: script 1");
    // The trap: two requests, one ack. Attempts are independent.
    @(negedge clk); req = 1;
    @(negedge clk); req = 1;
    @(negedge clk); req = 0; ack = 1;
    @(negedge clk); ack = 0;
    idle(3);
    $display("script 2: requests at two ticks, one ack: %0d failure (the second attempt)", fails);
    if (fails != 1) $fatal(1, "FAIL: script 2 gave %0d failures", fails);
    $display("PASS: every tick started an attempt; overlapping attempts passed or failed on their own");
    $finish;
  end
endmodule

script 1: 8 ticks, 8 passes (2 real, 6 vacuous), 0 failures
script 2: requests at two ticks, one ack: 1 failure (the second attempt)
PASS: every tick started an attempt; overlapping attempts passed or failed on their own

Performance

Attempt count times thread count times lifetime is the simulation bill. Three habits keep it small: bounded windows, specific antecedents, and thread pruning.

• Prefer bounded windows from the spec. Unbounded windows keep threads alive until a match or the end of simulation.

• Sharpen the antecedent. A specific condition kills most attempts at birth as cheap vacuous passes.

• Prune redundant threads with first_match and goto repetition in long windows.

• When assertions slow a regression, profile attempts first. One unbounded property on a hot clock usually dominates.

Common mistakes

Related topics

• Implication and properties

• Assertion debug