Q&A: Operators & Semantics

Q: Explain |-> vs |=> precisely.

Direct answer: both are implications — antecedent match obliges the consequent; antecedent non-match ends the attempt vacuously. |-> (overlapped) begins consequent evaluation in the same cycle in which the antecedent sequence completes its match. |=> (non-overlapped) begins it one cycle later — it is exactly equivalent to |-> ##1. The subtlety juniors miss: 'same cycle' means the cycle the antecedent ends , which for a multi-cycle antecedent is its last cycle, not its first.

(a ##1 b) |-> c        antecedent ends on b's cycle
cycle :   0    1    2
          a    b    .
               c?           ← |-> : c checked on b's cycle (1)
                    c?      ← |=> : c checked one later   (2)

Choose by quoting the spec: "ack WITH the last beat" → |->
                            "ack AFTER the last beat" → |=>

Follow-up: 'When is |-> on a boolean antecedent actually a contradiction?'

Whenever the consequent denies something the antecedent asserts in that same cycle: $rose(x) |-> !x can never pass non-vacuously, because $rose(x) means x is high in the sampled cycle. The pulse-width family of drills exists to catch exactly this slip — the fix is |=>.

Junior vs senior answer

• Junior: 'same cycle vs next cycle'.

• Senior: anchors 'same cycle' to the antecedent's END cycle, gives the |-> ##1 equivalence, and names the $rose(x) |-> !x contradiction class.

Q: What exactly does ##[1:5] mean, and how many matches does it create?

Direct answer: a nondeterministic delay — the sequence a ##[1:5] b matches if b occurs 1, 2, 3, 4, or 5 cycles after a. Operationally the simulator forks up to five threads, one per offset; the sequence 'matches' on every offset where b is true. In a consequent , one surviving match suffices (existential — the assert passes). In an antecedent , every match raises its own consequent obligation (universal — all must pass). Same operator, opposite quantification depending on which side of the implication it sits.

req ##[1:5] ack with ack high at offsets 2 AND 4:

  threads:   +1   +2   +3   +4   +5
  ack    :   0    1    0    1    0
  match? :   .    M         M

As consequent:  one M is enough → PASS (extra match irrelevant)
As antecedent:  TWO antecedent matches → TWO obligations,
                each must satisfy the consequent → see first_match Q.

Follow-up: 'Difference between ##[1:5] b and b[->1] bounded to 5?'

##[1:5] b matches at EVERY offset where b holds (possibly several); b[->1] matches exactly once, at the FIRST b. For asserts-as-consequents the verdicts usually coincide; for antecedents, sequence composition, and cover counting, the multiplicity difference is visible — covers on ##[1:5] can count multiple hits per event.

Junior vs senior answer

• Junior: 'b within 1 to 5 cycles'.

• Senior: thread-per-offset model, existential-in-consequent vs universal-in-antecedent, and the [->1] single-match contrast.

Q: [*3] vs [->3] vs [=3] — go.

Direct answer: all repeat a boolean three times, differing in gaps and endpoint. b[*3] — three consecutive cycles of b; no gaps. b[->3] (goto) — three occurrences with arbitrary non-b gaps allowed, and the match ends exactly on the third b . b[=3] (nonconsecutive) — same three-with-gaps, but the match may extend past the third b through additional non-b cycles; and within any given match window the count is exactly three — a fourth b inside kills that thread.

trace  b :  0  1  0  1  1  0  0
            cycles 1,3,4 carry the three b's

b[*3]  : needs b,b,b adjacent → only matches a run like 3,4,5-if-b.
         Here: NO match (gap at cycle 2).
b[->3] : matches cycles 1..4 exactly — ends ON cycle 4 (3rd b).
b[=3]  : matches 1..4, and ALSO 1..5, 1..6 (absorbing trailing 0s).

Mnemonic: * adjacent | -> lands on the Nth | = lands anywhere after

Follow-up: 'Show one spec for each.'

• [*3] — 'busy must stay high three cycles': continuous level, no gaps by nature.

• [->3] — 'interrupt fires on the third error': the third occurrence triggers something immediately.

• [=3] — 'a frame contains exactly three parity events, then EOF whenever it comes': closing event trails at its leisure.

Junior vs senior answer

• Junior: recites 'consecutive, goto, non-consecutive' without the endpoint rule.

• Senior: leads with the endpoint distinction (ends ON the Nth vs may trail) because that is what decides ##1-composition after the repetition — and is what anti-pattern 5 tests.

Q: throughout vs within vs intersect.

Direct answer: three different containment relations between a condition/sequence and a window. expr throughout seq — boolean expr must hold at every cycle of seq's match. seq1 within seq2 — seq1 matches somewhere inside seq2's span (start at or after seq2 starts, end at or before it ends). seq1 intersect seq2 — both match over exactly the same cycles : same start, same end. Intersect is the length-equalizer; and is its loose cousin (same start, lengths may differ).

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

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

// intersect: exact-length pinning (count in window)
p_3_in_10: assert property (@(posedge clk) disable iff (!rst_n)
  $rose(win) |=> (ev[=3]) intersect 1[*10]);

Follow-up: 'Why intersect and not and in that last property?'

and requires both operands to match starting together but each at its own length — ev[=3] could match over 14 cycles while 1[*10] matches over 10, and the property would still hold. intersect forces identical spans, which is what pins the count to the 10-cycle window. This is the standard trap behind every counting-window question.

Junior vs senior answer

• Junior: defines the three in isolation.

• Senior: classifies them — invariant-over-window, containment, exact-span — and contrasts intersect with and, since that is always the follow-up.

Q: What is first_match for?

Direct answer: first_match(seq) collapses a multi-match sequence to its earliest match and discards the rest. You need it in two places. One: a ranged antecedent — without it, every match raises an obligation and a spec that says 'from the first occurrence' will falsely fail on later matches. Two: inside sequence composition — e.g. first_match(a ##[1:10] b) ##1 c anchors c after the earliest b rather than after every candidate b.

(start ##[1:5] ready) |-> data_ok      ready at +3 and +4

  match A ends @+3 : data_ok=1 ✓
  match B ends @+4 : data_ok=0 ✗  → assertion FAILS

first_match(start ##[1:5] ready) |-> data_ok
  only match A survives → PASS

But CAREFUL: if the spec is "data_ok whenever ready in the
window", the multi-obligation behavior was CORRECT and
first_match would mask real bugs. The operator implements
"the first"; the spec decides if you want it.

Follow-up: 'Does first_match change anything in a consequent?'

Rarely the verdict: consequents are existential, so any match passing suffices, with or without first_match. It can matter for performance (kill redundant threads early) and for local-variable flows where you want values from the earliest match only.

Junior vs senior answer

• Junior: 'takes the first match of a sequence'.

• Senior: the antecedent multi-obligation problem, the composition anchor, the consequent near-no-op, and the warning that first_match is only right when the spec says 'first'.

Key takeaways

• |=> is |-> ##1; the implication anchor is the antecedent's END cycle, not its start.

• Ranged operators are existential in consequents and universal in antecedents — the same syntax flips quantifiers across |->.

• The repetition triad differs at the endpoint: [*] adjacent, [->] ends on the Nth, [=] may trail — endpoint decides what ##1 means after it.

Common pitfalls

• Quoting 'same cycle' for |-> without saying WHICH cycle for multi-cycle antecedents.

• Using and where intersect is needed — window-length pinning silently lost.

• Reflexive first_match on every ranged sequence — masks bugs when the spec wanted all matches checked.