Fixed delay: ##N

a ##N b means: a is true at some clock tick, then exactly N clock ticks later, b is true. The count is in sampled clock ticks, not time units — SVA has no notion of nanoseconds, only clock edges of the sequence's clock. ##1 is the next tick; ##2 is two ticks later.

1
2
3
4
5
6
7
8
9
10

// Grant must come exactly 2 cycles after request
property p_fixed_gnt;
  @(posedge clk) req ##2 gnt;
endproperty
// As a checker you would normally wrap this in an implication
// (next topic); here we study the raw sequence semantics.

sequence s_req_gnt;
  req ##2 gnt;   // matches iff req at tick T and gnt at tick T+2
endsequence

WAVEFORM — req ##2 gnt   (attempt starting at tick 2)

clk   :  1    2    3    4    5    6    7    8
req   :  0    1    0    0    0    0    0    0
gnt   :  0    0    0    1    0    0    0    0
              A         M
A = attempt: req sampled 1 at tick 2
M = match:   gnt sampled 1 at tick 4 = exactly ##2 later

clk   :  1    2    3    4    5    6    7    8
req   :  0    1    0    0    0    0    0    0
gnt   :  0    0    1    0    0    0    0    0
              A    X
X = no match: gnt arrived at tick 3 (##1) — ##2 requires tick 4.
    Early is just as much a failure as late.

Ranged delay: ##[M:N] and match threads

a ##[1:3] b means b arrives 1, 2, or 3 ticks after a. The crucial semantics: the simulator does not wait and decide — it forks three parallel match threads at the attempt, one per legal delay. The sequence matches when any thread sees b at its scheduled tick. Several threads can match, which means a ranged sequence can have multiple matches from one attempt — this matters later for first_match and for the not operator.

1
2
3
4
5
6
7
8
9

// Response within a 1-to-3 cycle window
sequence s_resp_window;
  req ##[1:3] rsp;
endsequence

property p_resp_window;
  @(posedge clk) req |-> ##[1:3] rsp;  // typical checker form
endproperty
a_resp: assert property (p_resp_window);

WAVEFORM — req ##[1:3] rsp   (threads forked at attempt, tick 2)

clk      :  1    2    3    4    5    6    7    8
req      :  0    1    0    0    0    0    0    0
rsp      :  0    0    0    1    0    0    0    0
                 A
thread T1 (##1): expects rsp @3 → rsp=0 → thread dies
thread T2 (##2): expects rsp @4 → rsp=1 → MATCH at tick 4
thread T3 (##3): expects rsp @5 → rsp=0 → thread dies
Sequence matches because T2 matched; T1/T3 dying is irrelevant.

clk      :  1    2    3    4    5    6    7    8
req      :  0    1    0    0    0    0    0    0
rsp      :  0    0    1    0    1    0    0    0
                 A    M1        M2
Both T1 (tick 3) and T3 (tick 5) match → TWO matches from one
attempt. Nondeterminism is normal, not an error.

Unbounded delays: ##[0:$] and ##[1:$]

The $ upper bound means no upper limit: a ##[1:$] b matches if b eventually arrives any number of cycles after a. In simulation this is a weak obligation — if the simulation ends with the thread still waiting, the assertion does not fail; it simply never completed. Contrast s_eventually, the strong property-level operator: at end of (formal) evaluation an unfulfilled s_eventually is a failure. In simulation, an unbounded delay that never completes is silently dropped — a passing log can hide a dead handshake.

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

// Weak: never fails in simulation if ack never comes
property p_weak_ack;
  @(posedge clk) req |-> ##[1:$] ack;
endproperty

// Strong flavor: fails at end-of-evaluation if ack never comes
property p_strong_ack;
  @(posedge clk) req |-> s_eventually ack;
endproperty

// Practical simulation answer: bound the window instead
property p_bounded_ack;
  @(posedge clk) req |-> ##[1:64] ack;  // timeout = checkable
endproperty

WAVEFORM — req ##[1:$] ack   (unbounded, weak)

clk   :  1    2    3    4    5  ...  998  999  1000(end of sim)
req   :  0    1    0    0    0  ...   0    0    0
ack   :  0    0    0    0    0  ...   0    0    0
              A    .    .    .  ...   .    .    ~
A = attempt at tick 2; threads keep extending forever
~ = sim ends, thread still pending → NOT a failure (weak)
    With s_eventually (strong), end-of-evaluation → FAIL.

##[0:$] additionally includes the zero-delay thread:
clk   :  1    2    3
a     :  0    1    0
b     :  0    1    0
              AM        a ##[0:$] b matches at tick 2 itself
                        (a and b true in the same cycle).

Zero delay: ##0 fusion

s1 ##0 s2 is fusion: s2 starts in the same cycle where s1 ends — the end tick of s1 and the start tick of s2 overlap. Between two plain booleans, a ##0 b is just a && b. Fusion becomes powerful when joining multi-cycle sequences: it stitches the endpoint of one onto the start of the next without consuming an extra cycle. It is also the exact relationship behind overlapped implication: |-> fuses the consequent onto the antecedent endpoint.

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

sequence s_addr_phase;
  valid ##1 addr_done;       // ends on the addr_done cycle
endsequence

sequence s_data_phase;
  data_valid ##1 data_done;
endsequence

// Data phase begins ON the cycle the address phase ends
sequence s_back_to_back;
  s_addr_phase ##0 s_data_phase;
endsequence

// Compare: ##1 would insert one idle cycle between the phases

WAVEFORM — (valid ##1 addr_done) ##0 (data_valid ##1 data_done)

clk        :  1    2    3    4    5
valid      :  0    1    0    0    0
addr_done  :  0    0    1    0    0
data_valid :  0    0    1    0    0
data_done  :  0    0    0    1    0
                   A    F         M
A = attempt: valid at tick 2
F = fusion tick 3: s_addr_phase ENDS (addr_done) and
    s_data_phase STARTS (data_valid) in the SAME cycle
M = match at tick 4 (data_done)

With ##1 instead of ##0, data_valid would be required at
tick 4 and the match would land at tick 5 — one cycle later.

Interview angle and review

Interview angle

• "What does a ##[1:3] b do when b appears twice in the window?" — both threads match; a sequence can have multiple matches per attempt. Saying "it takes the first one" is wrong unless wrapped in first_match.

• "Difference between ##[1:$] b and s_eventually b?" — weak vs strong. The unbounded delay never fails in simulation; s_eventually fails at end of evaluation (mainly meaningful in formal).

• "What is a ##0 b?" — fusion / same-cycle overlap; for booleans it degenerates to a && b. Bonus point: |-> is fusion of consequent onto antecedent endpoint.

• "Is ##2 two nanoseconds?" — trap. Delays count sampled clock ticks of the property clock, never time.

Key takeaways

• ##N counts clock ticks of the sequence clock — never simulation time.

• ##[M:N] forks one match thread per legal delay; any completing thread is a match, and several can match.

• $ as upper bound is unbounded and weak in simulation — bound your windows or use strong operators in formal.

• ##0 fuses sequences end-to-start in the same cycle; it is the semantic core of overlapped implication.

Common pitfalls

• Treating ##[1:3] as "wait up to 3 cycles then check" — it is three parallel threads, not a polled timeout.

• Shipping ##[1:$] in a simulation testbench and believing the green log — a never-arriving ack passes silently.

• Confusing ##0 with ##1 when chaining phase sequences — off-by-one-cycle protocol checkers.

• Forgetting that ##[0:M] includes a zero-delay thread where both expressions are checked in the same cycle.

• Assuming an early response satisfies ##2 — fixed delay means exactly N, so early arrival is a miss too.