Ranges multiply threads

Every ranged operator multiplies match threads. Two nested ranges multiply them together, so counting threads is a basic review skill.

Level antecedents make it worse. An attempt every cycle into a wide range holds hundreds of threads alive at once.

Keep the earliest match

first_match(s) keeps only the earliest-ending match of s from one attempt. The moment any thread completes, its siblings die.

Ties survive together. Threads ending on the same earliest tick all pass the pruning, so first_match prunes by end time rather than to a single thread.

1
2
3
4
5
6
7
8
9
10

// snippet
sequence s_any_ack;   req ##[1:8] ack;              endsequence
sequence s_first_ack; first_match(req ##[1:8] ack); endsequence

property p_done_after_first_ack;
  // edge-anchored in real checkers; see antecedent-design
  @(posedge clk) $rose(req) |->
    first_match(req ##[1:8] ack) ##1 done;
endproperty
// Without first_match, done after ANY ack-thread endpoint passes.

Both ack ticks match the plain sequence, and only the first survives pruning. A ##1 done suffix would then time from slot 3 alone.

• Slot 0: idle, req, ack, and the endpoint flag all 0.

• Slot 1: req rises, and the window opens.

• Slot 2: quiet tick inside the window.

• Slot 3: first ack, where both the plain scan and the pruned scan report an endpoint.

• Slot 4: quiet tick.

• Slot 5: second ack, where only the plain scan reports again.

• Slot 6: both low again.

Endpoints as events

A named sequence exposes its endpoint as a boolean. s.triggered is true in any time step where an evaluation of s reaches its end, and other properties can consume it as an event.

s.matched is the multi-clock variant. It carries the endpoint across to the next tick of a destination clock instead of the same time step.

Both listings below are not run in this course's checks. Verilator 5.048 has no .triggered or .matched, and it rejects a clock inside a sequence declaration.

1
2
3
4
5
6
7
8
9
10
11

// not-run: Verilator 5.048 has no .triggered
sequence s_wr_burst;            // endpoint = last beat of a write burst
  wr_start ##1 wr_beat [->4];
endsequence

// .triggered pulses at EVERY endpoint of a multi-match sequence.
// For the earliest endpoint only, wrap first_match in a named
// sequence (s_first; first_match(s); endsequence) and use s_first.triggered.
property p_resp_after_burst;
  @(posedge clk) s_wr_burst.triggered |-> ##2 wr_resp;
endproperty

1
2
3
4
5
6

// not-run: Verilator 5.048 has no .matched and rejects a clock inside a sequence declaration
sequence s_src;   @(posedge clk_a) val_a ##1 done_a;          endsequence
sequence s_pair;  @(posedge clk_b) s_src.matched ##1 done_b;  endsequence
property p_cdc;
  @(posedge clk_b) start_b |-> s_pair;
endproperty

Testbench

The bench opens 15 windows, each with acks at +2 and +5. In 10 of them done follows the first ack; in 5, planted, it follows only the second. The rule, done after the first ack, is checked twice: with first_match as written above, and with a flag set by modeling code on the first 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
38
39
40
41
42

module tb_first_match;
  logic clk = 0, req = 0, ack = 0, done = 0;
  always #5 clk = ~clk;
  int any_hits = 0, fm_hits = 0, fm_fails = 0, flag_fails = 0;

  // Covers: an ack somewhere in the window, and the first ack followed by done.
  cp_any: cover property (@(posedge clk) $rose(req) ##[1:8] ack) any_hits++;
  cp_fm:  cover property (@(posedge clk) $rose(req) ##0 first_match(##[1:8] ack) ##1 done) fm_hits++;
  // The rule: done must follow the FIRST ack.
  ap_fm: assert property (@(posedge clk) $rose(req) |-> first_match(##[1:8] ack) ##1 done) else fm_fails++;
  // Modeling code marks the first ack; a one-step property checks done.
  logic waiting = 0;
  always @(posedge clk)
    if ($rose(req)) waiting <= 1;
    else if (ack) waiting <= 0;
  wire first_ack = waiting && ack;
  ap_flag: assert property (@(posedge clk) first_ack |=> done) else flag_fails++;

  // A window with acks at offsets a1 and a2 after req, and done at offset d.
  task automatic window(int a1, int a2, int d);
    @(negedge clk) req = 1;
    @(negedge clk) req = 0;
    for (int c = 1; c <= 9; c++) begin
      ack = (c == a1 || c == a2);
      done = (c == d);
      @(negedge clk);
    end
    ack = 0; done = 0;
    repeat (3) @(negedge clk);
  endtask

  initial begin
    repeat (2) @(negedge clk);
    for (int t = 0; t < 10; t++) window(2, 5, 3);   // done follows the first ack
    for (int t = 0; t < 5; t++)  window(2, 5, 6);   // planted: done follows only the second ack
    $display("15 windows, each with acks at +2 and +5: cp_any %0d, cp_fm %0d (10 expected)", any_hits, fm_hits);
    $display("5 windows with done after the second ack: first_match assert %0d failures, flag version %0d", fm_fails, flag_fails);
    if (any_hits != 15 || flag_fails != 5) $fatal(1, "FAIL: any %0d flag %0d", any_hits, flag_fails);
    $display("PASS: the cover counted one match per window, and the first-ack flag caught all 5 planted bugs");
    $finish;
  end
endmodule

15 windows, each with acks at +2 and +5: cp_any 15, cp_fm 0 (10 expected)
5 windows with done after the second ack: first_match assert 0 failures, flag version 5
PASS: the cover counted one match per window, and the first-ack flag caught all 5 planted bugs

On Verilator 5.048, first_match(...) followed by more sequence matched nothing, as an assert or a cover, so the first_match check reported 0 failures and its cover 0 hits. The flag version is four lines of modeling code and a one-step property, and it caught all 5. That pattern, a few flops that name the event plus a simple property on top, is the most portable assertion style there is.

Related topics

• Sequence pattern drills

• Antecedent design