Implication anchors

|-> and |=> are both implications: a non-matching antecedent ends the attempt vacuously, a matching one obliges the consequent. |-> begins consequent evaluation in the same cycle the antecedent sequence completes. |=> begins one cycle later, and is exactly equivalent to |-> ##1.

“Same cycle” means the cycle the antecedent ends, which for a multi-cycle antecedent is its last cycle, not its first. Quote the spec to choose: “ack with the last beat” takes |->, “ack after the last beat” takes |=>.

The classic contradiction is $rose(x) |-> !x: $rose means x is high in the sampled cycle, so the consequent can never hold non-vacuously. Every pulse-width drill exists to catch exactly this slip, and the fix is |=>.

Ranges and repetition endpoints

A nondeterministic delay a ##[1:5] b forks one thread per offset, and b at any offset matches. In a consequent one surviving match suffices: existential. In an antecedent every match raises its own obligation: universal. Same operator, opposite quantification per side.

As a consequent, one match is enough and the attempt passes. As an antecedent, each match raises its own obligation, and each must pass.

Contrast with b[->1], which matches exactly once at the first b. For consequents the verdicts usually coincide. For antecedents, composition, and cover counting, the multiplicity is visible: covers on ##[1:5] can count several hits per event.

Consecutive, goto, nonconsecutive

All three repeat a boolean three times and differ in gaps and endpoint. b[*3] needs three adjacent cycles. b[->3] allows non-b gaps and ends exactly on the third b. b[=3] allows gaps and may extend past the third b through trailing non-b cycles. Within any match window the count is exactly three: a fourth b kills that thread.

One spec per operator fixes the triad. [*3]: busy stays high three cycles. [->3]: the third error interrupts now. [=3]: a frame holds exactly three parity events, then EOF whenever it comes. The endpoint distinction decides what ##1 means after the repetition, which is what the counting drills test.

Windows and first matches

Three containment relations cover conditions over windows. Expr throughout seq demands expr at every cycle of the match. Seq1 within seq2 matches seq1 somewhere inside seq2's span. Seq1 intersect seq2 demands both match over exactly the same cycles: same start, same end.

This fragment is an illustration, so the course checks skip it. Verilator 5.048 also does not support the unbounded [*1:$] repetition.

1
2
3
4
5
6
7
8
9

// snippet
p_stable_burst: assert property (@(posedge clk) disable iff (!rst_n)
  $rose(burst) |-> mode_locked throughout (burst[*1:$] ##1 !burst));

p_cal_in_init: assert property (@(posedge clk) disable iff (!rst_n)
  $rose(init) |-> (cal_done[->1]) within (init[*1:$] ##1 !init));

p_3_in_10: assert property (@(posedge clk) disable iff (!rst_n)
  $rose(win) |=> (ev[=3]) intersect 1[*10]);

Intersect is the length equalizer and and is its loose cousin: and requires a common start but lets lengths differ, so ev[=3] could sprawl past the 10-cycle window and still hold. That contrast is always the follow-up.

First_match collapses a multi-match sequence to its earliest match. A ranged antecedent without it raises one obligation per match, so a spec that says “from the first ready” fails falsely on later matches. When the spec wants every match checked, first_match would mask real bugs: the operator implements “the first”, and the spec decides.

Common mistakes

Testbench

The bench checks four answers with real assertions and covers: both implication anchors on a two-cycle antecedent, the $rose(x) |-> !x contradiction over three pulses, and the two repetition forms on the gapped trace.

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

module tb_qa_operators;
  logic clk = 0, a = 0, b = 0, c = 0, x = 0, bt = 0, st = 0;
  always #5 clk = ~clk;
  int ovl_fails = 0, novl_fails = 0, contra_fails = 0, star_hits = 0, goto_hits = 0;

  // A two-cycle antecedent: |-> checks c on b's cycle, |=> one later.
  a_ovl:  assert property (@(posedge clk) (a ##1 b) |-> c) else ovl_fails++;
  a_novl: assert property (@(posedge clk) (a ##1 b) |=> c) else novl_fails++;
  // The classic contradiction: $rose(x) means x is 1 in this cycle.
  a_contra: assert property (@(posedge clk) $rose(x) |-> !x) else contra_fails++;
  // Endpoints on the lesson's gapped trace: from st at cycle 0, b at cycles 1, 3 and 4.
  c_star: cover property (@(posedge clk) st ##1 bt [*3]) star_hits++;
  c_goto: cover property (@(posedge clk) st ##0 bt [->3]) goto_hits++;

  initial begin
    repeat (2) @(negedge clk);
    a = 1; @(negedge clk) a = 0; b = 1; c = 1;            // c on b's cycle only
    @(negedge clk) b = 0; c = 0;
    repeat (3) @(negedge clk);
    $display("c on b's cycle: |-> %0d failures, |=> %0d failures", ovl_fails, novl_fails);
    repeat (3) begin x = 1; @(negedge clk) x = 0; @(negedge clk); end
    $display("$rose(x) |-> !x over 3 pulses: %0d failures", contra_fails);
    st = 1; @(negedge clk) st = 0; bt = 1; @(negedge clk) bt = 0; @(negedge clk) bt = 1; @(negedge clk); @(negedge clk) bt = 0;   // b: 0 1 0 1 1
    repeat (4) @(negedge clk);
    $display("trace b = 0 1 0 1 1: b [*3] matched %0d times, b [->3] matched %0d times", star_hits, goto_hits);
    if (ovl_fails != 0 || novl_fails != 1 || contra_fails != 3 || star_hits != 0 || goto_hits != 1)
      $fatal(1, "FAIL: %0d %0d %0d %0d %0d", ovl_fails, novl_fails, contra_fails, star_hits, goto_hits);
    $display("PASS: the anchors, the contradiction and the two repetition endpoints all behaved as the answers say");
    $finish;
  end
endmodule

c on b's cycle: |-> 0 failures, |=> 1 failures
$rose(x) |-> !x over 3 pulses: 3 failures
trace b = 0 1 0 1 1: b [*3] matched 0 times, b [->3] matched 1 times
PASS: the anchors, the contradiction and the two repetition endpoints all behaved as the answers say

Related topics

• Ordering & Counting Drills

• Q&A: Assertion Fundamentals