Match exactly the obligation

The consequent states the obligation, but the antecedent decides when it applies. Both failure modes of a bad assertion live there.

Anchor events with edges

A level antecedent rematches every tick it stays true. On a held request each early window can expire before the legitimate grant, so one transaction reports several false failures.

$rose(req) anchors one attempt per transaction. Levels stay right for per-cycle invariants with same-cycle consequents.

The diagram applies the level check req |-> ##[1:2] gnt to a request held from slot 1 until its grant at slot 5.

• Slot 0: req 0, gnt 0. Idle.

• Slot 1: req rises. First attempt starts; its window is slots 2 to 3.

• Slot 2: req still 1. Second attempt starts; its window is slots 3 to 4.

• Slot 3: gnt 0. The slot-1 window expires: spurious failure.

• Slot 4: gnt 0. The slot-2 window expires: second spurious failure.

• Slot 5: gnt 1. The slot-3 and slot-4 attempts pass. An edge-anchored check whose window reaches the grant, $rose(req) |-> ##[1:4] gnt, passes once here.

• Slot 6: req 0. Idle; the slot-5 attempt is still pending past the shown window.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15

// snippet
// Level antecedent on a held-request protocol: every held tick
// starts its own window, so early windows expire spuriously.
a_bad: assert property (@(posedge clk) disable iff (!rst_n)
  req |-> ##[1:2] gnt);

// Edge-anchored, window sized from the request event to the
// latest legal grant (4 cycles in the diagram above).
a_good: assert property (@(posedge clk) disable iff (!rst_n)
  $rose(req) |-> ##[1:4] gnt);

// Level form kept where it belongs: a per-cycle invariant.
// Comparison spelling: Verilator rejects unary negation in sequences.
a_inv: assert property (@(posedge clk) disable iff (!rst_n)
  fifo_full |-> (wr_en == 1'b0));

Qualify in the antecedent

Every qualifier the spec attaches belongs in the antecedent. In the consequent its absence becomes a failure instead of a non-obligation.

1
2
3
4
5
6
7
8
9
10
11
12
13

// snippet
// Qualifier in the wrong place: a legitimately idle cycle fails.
// Assumes wr_cmd, wvalid, wdata, and MAX are declared nearby.
a_w1: assert property (@(posedge clk)
  wr_cmd |-> (wvalid && (wdata inside {[0:MAX]})));

// Qualifier in the right place: no qualified data means no obligation.
a_w2: assert property (@(posedge clk)
  (wr_cmd && wvalid) |-> (wdata inside {[0:MAX]}));

// Enable-gated protocol rule, edge-anchored.
a_en: assert property (@(posedge clk) disable iff (!rst_n)
  $rose(start) && chan_en |-> ##[1:8] done);

Reuse without clocks

Named properties take untyped, typed, sequence, and property formals. Delay and repetition bounds must be elaboration-time constants.

1
2
3
4
5
6
7
8
9
10
11
12
13

// snippet
// Workhorse template; min/max default to the common window.
property req_gets_grant(req, gnt, int min = 1, int max = 4);
  $rose(req) |-> ##[min:max] gnt;
endproperty

// Sequence formal accepts any trigger; property formal wraps any check.
property after_trigger_resp(sequence trigger, resp, int max);
  trigger |-> ##[1:max] resp;
endproperty
property gated(property p, en);
  if (en) p;
endproperty

Keep library properties clockless and resetless, and bind clock plus disable iff at each assert site. A buried clock samples the wrong domain while looking healthy.

1
2
3
4
5
6
7
8
9
10
11
12
13
14

// snippet
// Library style: no clock, no reset inside.
property handshake(req, gnt, int max);
  $rose(req) |-> ##[1:max] gnt;
endproperty

// Caller binds its own clock and reset.
a_core: assert property (@(posedge core_clk) disable iff (!core_rst_n)
  handshake(c_req, c_gnt, 4));

// Buried clock: samples whatever clk was in elaboration scope.
property handshake_bad(req, gnt);
  @(posedge clk) $rose(req) |-> ##[1:4] gnt;
endproperty

1. Event or invariant: transactions get edge anchors, per-cycle invariants may use levels.

2. Every spec qualifier present in the antecedent, none borrowed into the consequent.

3. No extra qualifier the spec never imposed.

4. Paired cover on the antecedent sequence, tracked in the merged regression.

5. Window bounds derived from the spec.

6. Retrigger behavior known for a held trigger.

7. Thread estimate acceptable across attempts, ranges, and instances.

A level antecedent true for L cycles before ##[1:N] holds about L times N threads live. Edge-anchoring collapses that to one attempt.

Testbench

A five-cycle hold counted both ways. Only the edge form is asserted, since the level form fails spuriously.

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
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53

module tb_impl_ante;
  timeunit 1ns; timeprecision 1ps;
  localparam int HOLD = 5;
  localparam int LAT = 4;
  logic clk = 0;
  always #5 clk = ~clk;
  logic rst_n = 0;
  logic req = 0;
  logic gnt = 0;
  logic req_q = 0;
  int timer = 0;
  int level_cnt = 0;
  int edge_cnt = 0;
  int gnt_seen = 0;

  always @(posedge clk) begin
    if (!rst_n) begin
      timer <= 0;
      gnt <= 1'b0;
    end else begin
      if (req && !req_q) timer <= LAT;
      else if (timer > 0) timer <= timer - 1;
      gnt <= (timer == 1);
    end
    req_q <= req;
    if (rst_n && req) level_cnt <= level_cnt + 1;
    if (rst_n && req && !req_q) edge_cnt <= edge_cnt + 1;
  end

  a_good: assert property (@(posedge clk) disable iff (!rst_n)
    $rose(req) |-> ##[1:5] gnt);

  always @(posedge clk) begin
    if (rst_n && gnt) gnt_seen <= 1;
  end

  initial begin
    rst_n = 0;
    req = 0;
    repeat (2) @(negedge clk);
    rst_n = 1;
    @(negedge clk);
    req = 1;
    repeat (HOLD) @(negedge clk);
    req = 0;
    repeat (6) @(negedge clk);
    if (level_cnt == HOLD && edge_cnt == 1 && gnt_seen == 1)
      $display("PASS: 1 edge attempt covered a 5-cycle hold; level form would start 5 attempts");
    else
      $fatal(1, "FAIL: attempt bookkeeping off");
    $finish;
  end
endmodule

PASS: 1 edge attempt covered a 5-cycle hold; level form would start 5 attempts

Related topics

• Sampled Value Functions

• Protocol Assertions