throughout: an invariant over a sequence

expr throughout seq matches when seq matches AND the boolean expr is true at every tick of that match, from its first cycle to its last inclusive. The left side must be a boolean expression (not a sequence). It is sugar for (expr) [*0:$] intersect seq — replicate the condition for exactly the sequence's length. This is THE operator for "X must not happen during Y": no abort during a burst, stable configuration during a transaction, reset never asserting mid-handshake.

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

// No abort for the whole burst: start through last beat
sequence s_burst;
  burst_start ##1 beat [->4] ##0 beat_last;
endsequence

property p_no_abort_in_burst;
  @(posedge clk) burst_start |-> (!abort) throughout s_burst;
endproperty
a_no_abort: assert property (p_no_abort_in_burst);

// Stable config during a transaction (classic register-stability check)
property p_cfg_stable;
  @(posedge clk) txn_start |->
    $stable(cfg_mode) throughout (txn_active [*1:$] ##1 txn_done);
endproperty
a_cfg: assert property (p_cfg_stable);

WAVEFORM — (!abort) throughout (burst_start ##1 beat[->4])

PASS:
clk   :  1    2    3    4    5    6    7
bstart:  0    1    0    0    0    0    0
beat  :  0    0    1    1    0    1    0
abort :  0    0    0    0    0    0    0
              A    b1   b2        b4*  (b3 omitted for width)
              i----i----i----i----i    invariant !abort holds
                                  M    sequence matches → MATCH

FAIL — abort pulses mid-burst:
clk   :  1    2    3    4    5    6
bstart:  0    1    0    0    0    0
beat  :  0    0    1    1    0    1
abort :  0    0    0    1    0    0
              A         X
X = abort=1 at tick 4, inside the match window → the invariant
thread dies THERE — failure reported at tick 4, not at burst end.
throughout fails early, at the first violating tick.

within: containment

s1 within s2 matches when a match of s1 happens somewhere inside a match of s2: s1 starts no earlier than s2 starts, and ends no later than s2 ends. Both ends may coincide. The LRM definition: (1[*0:$] ##1 s1 ##1 1[*0:$]) intersect s2 — pad s1 with don't-care cycles on both sides and require equal length with s2. Where throughout pins a one-tick boolean over a window, within places a whole sequence inside a window.

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

// The req/ack handshake must complete inside the frame window
sequence s_frame;
  frame_start ##1 frame_act [*1:$] ##1 frame_end;
endsequence

property p_hs_in_frame;
  @(posedge clk) frame_start |-> ((req ##[1:4] ack) within s_frame);
endproperty
a_hs_frame: assert property (p_hs_in_frame);

// Response within a bounded window — within against a pure timer
property p_resp_window;
  @(posedge clk) $rose(req) |->
    ((rsp_vld ##1 rsp_done) within 1 [*1:10]);
endproperty
a_resp: assert property (p_resp_window);  // 2-cycle response inside 10 ticks

WAVEFORM — (req ##[1:2] ack) within (fstart ##1 fact[*3] ##1 fend)

clk    :  1    2    3    4    5    6    7
fstart :  0    1    0    0    0    0    0
fact   :  0    0    1    1    1    0    0
fend   :  0    0    0    0    0    1    0
req    :  0    0    1    0    0    0    0
ack    :  0    0    0    1    0    0    0
              S══════════════════E      s2 (frame): ticks 2..6
                   s────M                s1 (handshake): ticks 3..4
s1 starts @3 >= s2 start @2  ✓
s1 ends   @4 <= s2 end   @6  ✓   → within MATCH (endpoint = tick 6)

FAIL case: ack at tick 7 → s1 ends after s2 ends → containment
violated → no match (handshake leaked past the frame).

Classic uses and the throughout-vs-within choice

Pattern catalog

• No-abort/no-reset during operation: (!abort) throughout s_burst — invariant condition, use throughout.

• Stable mode/config during a transaction: $stable(cfg) throughout s_txn.

• Response completes inside a timeout window: s_resp within 1[*1:N] — containment, use within.

• Sub-protocol inside super-protocol: (arb_req ##1 arb_gnt) within s_bus_frame.

• Rule of thumb: ONE boolean held over a window → throughout; a multi-cycle PATTERN placed inside a window → within.

CHOOSING — throughout vs within

  need: condition C true at EVERY tick of seq S
        C throughout S            (C is a boolean)
        C ────────────────►  i i i i i i   (every tick checked)
        S ────────────────►  ├─────────┤

  need: pattern P occurs SOMEWHERE inside seq S
        P within S                (P is a sequence)
        P ────────────────►        ├──┤   (floats inside)
        S ────────────────►  ├─────────┤  (start/end contain P)

Interview angle and review

Interview angle

• "Write: abort must never assert during a burst." — (!abort) throughout s_burst, behind a |-> with the burst-start antecedent. The expected one-liner in protocol-assertion interviews.

• "When does throughout report the failure?" — at the first tick the invariant breaks, not at the end of the sequence; good answers mention early-failure semantics.

• "Express within using intersect." — (1[*0:$] ##1 s1 ##1 1[*0:$]) intersect s2; quoting the padding construction is a senior-level signal.

• "Can the left side of throughout be a sequence?" — no, boolean expression only; for sequence-in-window you switch to within.

Key takeaways

• throughout = boolean invariant over every tick of a sequence match, failing early at the first violation.

• within = sequence containment: s1 starts and ends inside (or exactly on) s2's span.

• Both are intersect sugar — throughout replicates a boolean; within pads with don't-care cycles.

• Heuristic: one condition over a window → throughout; a pattern placed in a window → within.

Common pitfalls

• Putting a sequence on the left of throughout — illegal; the left operand must be a boolean expression.

• Checking the invariant only at sequence endpoints with ##-chains instead of throughout — gaps where mid-window glitches escape.

• Assuming within forces s1 to start strictly after s2 starts — coincident starts and ends are allowed.

• Forgetting the within composite's endpoint is s2's endpoint — follow-on ##1 elements time from the window end, not from s1's match.

• Using throughout under a level antecedent that retriggers every cycle — overlapping invariant windows and noisy duplicate failures (see antecedent design).