Protocol Assertions

Assertions in UVM · Module 21 · Page 21.2

The Engineering Problem

SVA integration (Module 21.1) put the sentries in place — bound to the DUT, wired into UVM reporting. But a sentry with no standing orders checks nothing; the value is in the property it enforces — the precise temporal rule. And writing that rule is a language problem: the spec says "after a request, an acknowledge must arrive within one to three cycles, and the request must hold stable until then" — and you must translate that English into a concurrent assertion that captures it exactly. Exactly is the hard part. An assertion stricter than the spec — a window of [1:2] where the spec allows [1:3] — fires on legal behavior, flooding the regression with false failures that erode trust until someone disables the assertion, after which real violations go uncaught. An assertion looser than the spec — [1:$] where the spec bounds the window — misses the too-late violation it was meant to catch. The problem this chapter solves is writing protocol assertions: the SVA language (sequences, properties, implication, delays, repetition) and the skill of translating a protocol's rules into assertions that capture the specification exactly — neither too strict nor too loose.

Protocol assertions are concurrent assertions that capture a protocol's temporal rules, written in the SVA language. The language is a stack: boolean expressions (signal conditions — req, valid && !ready) compose into sequences (temporal patterns over cycles — req ##1 ack, a ##[1:3] b), which compose into properties (checkable rules, usually with implication), which are stated by a directive (assert property — must hold; cover property — measure; assume property — constrain). Properties are clocked and sampled (@(posedge clk), with disable iff (!rst_n) for reset). The core operator is implication — |-> (overlapping: consequent starts the same cycle the antecedent matches) and |=> (non-overlapping: consequent starts the next cycle) — which gates the consequent on the antecedent. Temporal delays (##N exactly N cycles, ##[m:n] a window, ##[1:$] eventually) and repetition ([*n] consecutive, [->n] goto, [=n] non-consecutive) express timing windows and holds. The skill is translating protocol rules — handshakes (req |-> ##[1:N] ack), stability (valid && !ready |=> valid), mutual exclusion (!(g0 && g1)), ordering, timing windows — into properties that capture the spec exactly. Fidelity is the quality bar: too strict fires on legal behavior (false failures erode trust → disabled → missed bugs); too loose misses violations. This chapter is the SVA language and the precise translation of protocol rules.

How do you write protocol assertions — what is the SVA language (boolean, sequence, property, directive), how do the implication operators and temporal delays and repetition express temporal rules, and how do you translate a protocol's rules into assertions that capture the specification exactly, neither too strict nor too loose?

Motivation — why precise translation is the whole skill

Writing an assertion that compiles and fires sometimes is easy; writing one that captures the spec exactly is the skill, and the gap between them is costly. The reasons:

• The property is where the checking lives. The integration (21.1) is plumbing; the property is the rule. A vague or wrong property checks the wrong thing — the sentry enforces a garbled order.
• Too strict fires on legal behavior — and erodes trust. An assertion narrower than the spec (wrong window, wrong condition, missing reset disable) fires when the DUT is correct — and false failures are poison: they waste debug time, and worse, they train the team to ignore or disable the assertion, after which real violations are missed.
• Too loose misses violations. An assertion broader than the spec (##[1:$] instead of ##[1:3], a missing qualifier) passes on buggy behavior — the late ack, the spurious grant — silently. A loose assertion gives false confidence.
• The temporal operators are precise and must be chosen correctly. |-> vs |=> is a one-cycle difference that flips a correct assertion into an off-by-one false-failure or missed-violation. ##[1:3] vs ##[1:2] is one cycle of window. The operators encode the exact timing — and the wrong one encodes the wrong rule.
• Reusable patterns map common rules to SVA. Handshakes, stability, mutual exclusion, ordering, and timing windows have standard SVA forms — knowing them lets you translate the spec reliably and precisely.

The motivation, in one line: the property is the rule, and writing it to capture the spec exactly is the whole skill — too strict fires on legal behavior (false failures that erode trust and get the assertion disabled, then miss real bugs), too loose misses violations (false confidence), and the temporal operators (|->/|=>, ##[m:n], [*n]) encode the exact timing — so protocol assertions demand precise translation of the spec's temporal rules into the SVA language.

Mental Model

Hold writing a protocol assertion as translating a spec sentence, phrase by phrase, into a precise temporal formula — and fidelity to the spec is the whole quality bar:

A protocol rule in the spec is a sentence: "after a request, an acknowledge must arrive within one to three cycles." Writing the assertion is translating that sentence, phrase by phrase, into the SVA language. "After a request" becomes the antecedent and the implication — req implies. "Within one to three cycles" becomes the timed delay — hash-hash one-to-three. "An acknowledge" becomes the consequent — ack. The building blocks are the grammar: boolean expressions are the words, sequences are the phrases, the property is the sentence, implication is the if-then, delays are within-N-cycles, repetition is held-for-N. And the quality of the translation is fidelity — the formula must say exactly what the spec says, no more and no less. Say more (a narrower window) and the formula rejects legal sentences the spec allows — false failures. Say less (an unbounded window) and the formula accepts buggy sentences the spec forbids — missed violations. A faithful translation captures the spec's rule precisely; an imprecise one is a mistranslation that either over-rejects or under-rejects. Picture a protocol rule in the spec as a sentence: "after a request, an acknowledge must arrive within one to three cycles." Writing the assertion is translating that sentence, phrase by phrase, into the SVA language. "After a request" becomes the antecedent and the implication — req |->. "Within one to three cycles" becomes the timed delay — ##[1:3]. "An acknowledge" becomes the consequent — ack. The building blocks are the grammar: boolean expressions are the words (req, ack), sequences are the phrases (req ##1 ack), the property is the sentence (the full rule), implication is the if-then, delays are within-N-cycles, repetition is held-for-N. And the quality of the translation is fidelity — the formula must say exactly what the spec says, no more and no less. Say more (a narrower window, ##[1:2]) and the formula rejects legal sentences the spec allows — false failures. Say less (an unbounded window, ##[1:$]) and the formula accepts buggy sentences the spec forbids — missed violations. A faithful translation captures the spec's rule precisely; an imprecise one is a mistranslation that either over-rejects (false alarms) or under-rejects (silent misses).

So writing a protocol assertion is translating a spec sentence into a precise temporal formula: the grammar is boolean (words) → sequence (phrases) → property (sentence) → directive, with implication (if-then), delays (within-N), and repetition (held-for-N) as the temporal vocabulary. The quality bar is fidelity — exactly the spec, no more (too strict → false failures → eroded trust → disabled → missed bugs) and no less (too loose → missed violations → false confidence). Translate the spec phrase by phrase, and make the formula say exactly what the spec says — fidelity is everything.

Visual Explanation — the SVA building-block stack

The defining picture is the stack: boolean → sequence → property → directive — each layer composing the one below into a checkable rule.

The figure shows the SVA building-block stack. Boolean expressions (the brand-colored top — the words) are signal-level conditions evaluated each cycle (req, valid && !ready, grant0). Sequences (the phrases) compose booleans into temporal patterns over cycles using delays and repetition (req ##1 ack, a ##[1:3] b, valid[*2]). Properties (the sentence) compose sequences into checkable rules, usually an implication (req |-> ##[1:3] ack) gating a consequent on an antecedent. A directive (the warning-colored bottom — assert / cover / assume) states what to do with the property: assert (must hold), cover (measure it occurred), assume (constrain, for formal) — all clocked, with disable iff reset. The crucial reading is the composition: each layer builds on the one below, so a property is ultimately sequences of booleans, evaluated cycle-by-cycle under a clock. This layering is how the language scales from simple signal conditions to complex temporal rules: a boolean is one cycle, a sequence adds time (delays, repetition), a property adds logic (implication, the rule), and a directive adds intent (check it, measure it, assume it). Understanding the stack is how you read and write assertions: you recognize the boolean parts (the conditions), the sequence parts (the timing), the property structure (the implication — when X, then Y), and the directive (assert/cover). The brand/success-colored lower layers are the what (the temporal pattern); the warning-colored directive is the intent (warning because choosing assert vs cover vs assume matters — assume constrains rather than checks). The diagram is the language's grammar: boolean (words) → sequence (phrases) → property (sentence) → directive (intent) — the compositional stack you build a protocol rule from. A property is sequences of booleans under a clock, stated by a directive — build the rule up the stack.

RTL / Simulation Perspective — the operators and the protocol patterns

In code, the operators and the protocol patterns are the vocabulary. The example shows implication, delays, repetition, and the standard translations of common protocol rules.

// default clocking + reset disable (apply to all assertions in the checker)
default clocking cb @(posedge clk); endclocking
default disable iff (!rst_n);
 
// === IMPLICATION: |-> overlapping (same cycle) vs |=> non-overlapping (next cycle) ===
a_over:  assert property ( start |->  done );      // done must hold the SAME cycle start does
a_next:  assert property ( start |=>  busy );      // busy must hold the NEXT cycle (|=> == |-> ##1)
 
// === HANDSHAKE: request acked within a window (timing window via ##[m:n]) ===
a_handshake: assert property ( req |-> ##[1:3] ack );   // ack arrives 1 to 3 cycles after req
 
// === STABILITY / HOLD: valid must stay asserted until ready (and data stable) ===
a_valid_hold:  assert property ( valid && !ready |=> valid );        // valid holds while !ready
a_data_stable: assert property ( valid && !ready |=> $stable(data) ); // data unchanged while waiting
 
// === MUTUAL EXCLUSION: two grants must never both be high (a pure boolean property) ===
a_onehot_grant: assert property ( !(grant0 && grant1) );
 
// === ORDERING: every write is eventually followed by a completion ===
a_order: assert property ( wr_start |=> ##[1:$] wr_done );   // wr_done eventually follows wr_start
 
// === REPETITION: a stall must not last more than 4 consecutive cycles ===
a_stall_bound: assert property ( stall |-> stall[*1:4] ##1 !stall );  // at most 4 stall cycles
 
// === SAMPLED-VALUE FUNCTIONS: edges and history ===
a_pulse: assert property ( $rose(start) |-> ##[1:3] $rose(done) );    // rising-edge to rising-edge
 
// ✗ TOO STRICT: ##[1:2] when the spec allows 1..3 → fires on a LEGAL ack at cycle 3 (DebugLab)

The code shows the operators and patterns. The default clocking (@(posedge clk)) and default disable (!rst_n) apply to all assertions — clocking and reset handling once. Implication: |-> overlapping (start |-> done — done the same cycle) vs |=> non-overlapping (start |=> busy — busy the next cycle; |=> ≡ |-> ##1). Handshake: req |-> ##[1:3] ack — ack 1 to 3 cycles after req (a timing window via ##[m:n]). Stability/hold: valid && !ready |=> valid (valid holds while not ready) and ... |=> $stable(data) (data unchanged while waiting). Mutual exclusion: !(grant0 && grant1) (two grants never both — a pure boolean property). Ordering: wr_start |=> ##[1:$] wr_done (completion eventually follows — ##[1:$] = unbounded). Repetition: stall |-> stall[*1:4] ##1 !stall (a stall lasts at most 4 consecutive cycles — [*1:4]). Sampled-value functions: $rose, $fell, $stable, $past for edges and history ($rose(start) |-> ##[1:3] $rose(done)). The closing ✗ flags the too-strict trap (the DebugLab). The shape to carry: the protocol patterns are reusable templates — handshake (|-> ##[m:n]), stability (|=> signal/$stable), mutual exclusion (boolean !(...)), ordering (|=> ##[1:$]), bounded repetition ([*m:n]) — and translating a spec rule is matching it to the right pattern and filling in the exact window and condition. The operators encode the timing precisely: |-> vs |=> is the same-vs-next cycle, ##[1:3] is the exact window, [*1:4] is the exact consecutive count, and $rose/$stable are the exact edge/hold semantics. Match the spec rule to a pattern, and fill in the exact operator, window, and condition.

Verification Perspective — translating spec rules into the right pattern

The skill is translation: reading a spec rule and expressing it with the right operator and the exact window. Seeing the common rules mapped to patterns is the translation table.

The figure shows the translation of common protocol rules into SVA patterns. A handshake (request acked within N cycles) → a windowed implication (req |-> ##[1:N] ack). A stability rule (a signal holds until a condition) → a non-overlapping implication to the held signal or $stable (valid && !ready |=> valid). Mutual exclusion (signals never simultaneously high) → a pure boolean negation of their conjunction (!(g0 && g1)). An ordering rule (one event eventually follows another) → a non-overlapping implication with an unbounded delay (a |=> ##[1:$] b). A timing window (an event within a min-max range) → a bounded delay range (start |-> ##[MIN:MAX] done). The verification insight is that most protocol rules fall into a handful of patterns — and translation is (1) recognizing which pattern the rule is, then (2) filling in the exact operator, window, and condition. The recognition step is reading the spec: "within N cycles" → a bounded window (##[m:n]); "holds until" → a stability implication; "never both" → a boolean mutex; "eventually follows" → an unbounded ordering. The filling-in step is where precision lives: the exact window ([1:3] not [1:2]), the exact qualifier (the precise condition gating the rule), the exact operator (|-> same-cycle vs |=> next-cycle). The brand-colored rules map to the success-colored patterns, and knowing the patterns makes the translation reliable. This is why protocol assertions are a learnable, systematic skill, not ad-hoc: the spec's rules recur (handshakes, holds, ordering, exclusion, windows), and the patterns are their standard SVA forms — so a verifier translates by matching and filling in, precisely. The diagram is the translation table: handshake → windowed implication, stability → non-overlap-to-held, mutex → boolean negation, ordering → unbounded follow, window → bounded range — the recurring rules and their SVA patterns. Recognize the rule's pattern, then fill in the exact operator, window, and condition.

Runtime / Execution Flow — how a property evaluates with implication and delays

At run time, an implication property evaluates in a specific way: the antecedent gates, and the consequent is checked over the following cycles. The flow shows the evaluation.

The flow shows how an implication property evaluates. Check (step 1): every cycle, evaluate whether the antecedent (the if-part) holds on the sampled signals. Vacuous (step 2): if the antecedent doesn't hold, there's nothing to check — the property passes vacuously this attempt. Start (step 3): if it holds, an evaluation attempt starts; the consequent is checked over the following cycles per the delays. Resolve (step 4): if the consequent holds within its window, the attempt passes; if the window elapses without it, the assertion fires. The runtime insight is two-fold. First, the antecedent gates — the property only does real work when the antecedent holds; on every other cycle it passes vacuously (which is why covering the antecedent matters, Module 21.1 — a property whose antecedent never holds passes vacuously forever, checking nothing). Second, many attempts can be in flight at once — a new evaluation attempt can start each cycle the antecedent holds, and each is tracked independently over its window. So a property like req |-> ##[1:3] ack with req high for several cycles starts multiple overlapping attempts, each requiring its own ack within its window. This concurrency of attempts is why SVA can express pipelined protocols (multiple outstanding requests, each independently checked). The vacuous pass (step 2) is correct behavior (you don't want a failure when the antecedent isn't present), but it's why a passing assertion is ambiguous without covering the antecedent. The fire (step 4) is the precise failure — at the exact cycle the window elapses without the consequent. The flow is the implication semantics: antecedent gates (vacuous when false) → attempt starts when true → consequent checked over the window → pass or fire — and understanding it is understanding what your assertion actually checks (and when it vacuously checks nothing). The antecedent gates the check; the consequent is what must then hold within its window — and many attempts run at once.

Waveform Perspective — overlapping versus non-overlapping implication

The one-cycle difference between |-> and |=> is visible on a timeline — and getting it wrong is a classic off-by-one. The waveform shows both operators and a consecutive-repetition hold.

The waveform shows the implication operators and a repetition hold. The antecedent start rises at one cycle. With overlapping implication (|->), the consequent (done) is checked starting the SAME cycle as start (over_window opens at start). With non-overlapping implication (|=>), the consequent (busy) is checked starting the NEXT cycle (next_window opens one cycle later). The crucial reading is the one-cycle shift: |-> evaluates the consequent from the antecedent's cycle, while |=> evaluates it from the next cycle — the whole difference between the operators. Using the wrong one is an off-by-one: if the spec means "the next cycle" but you write |->, the assertion checks the wrong (current) cycle — firing falsely (if the consequent is only true next cycle) or missing a violation; if the spec means "the same cycle" but you write |=>, symmetrically wrong. The operators encode the exact timing, so choosing the right one is part of fidelity (|=> ≡ |-> ##1, so the choice is literally a one-cycle delay). Separately, a stability hold valid[*3] requires valid high for 3 consecutive cycles (cycles 4, 5, 6 → hold_ok at the 3rd), the repetition operator capturing "held-for-N". The picture to carry is that the temporal operators are precise, cycle-level constructs: |-> vs |=> is exactly one cycle, [*3] is exactly three consecutive cycles, and each must match the spec's exact timing. Reading the waveform this way — which cycle does the consequent get checked, and how many cycles must the hold last? — is reading the temporal semantics. The one-cycle shift between over_window and next_window, and the hold_ok at the 3rd consecutive valid, are the signatures of the operators' exact meaning — the cycle-level precision that fidelity demands. The operators encode exact cycle-level timing — |-> is same-cycle, |=> is next-cycle, [*n] is n-consecutive — choose them to match the spec exactly.

DebugLab — the too-strict assertion that got itself disabled

✗ TOO STRICT — window narrower than the spec:
  // spec: "ack must arrive within 1 to 3 cycles of req"
  a_handshake: assert property ( req |-> ##[1:2] ack );   // ← [1:2], but spec allows [1:3]
  // a LEGAL ack at cycle 3 → assertion FIRES → false failure
  // dozens of false failures/night → a week of wasted triage → team DISABLES the assertion
  // 3 weeks later a REAL violation (ack never arrives) → disabled assertion says nothing → SHIPS
 
✓ FAITHFUL — window matches the spec exactly:
  a_handshake: assert property ( req |-> ##[1:3] ack );   // ← [1:3], exactly the spec
  // legal acks at cycles 1, 2, AND 3 all PASS → no false failures → the assertion stays TRUSTED and ON
  // a real violation (no ack within 3) FIRES → caught immediately
  // FIDELITY: translate the spec's exact window; an imprecise assertion is worse than none

Common Mistakes

• Off-by-one window or wrong implication operator. ##[1:2] for a spec of 1–3, or |-> where |=> was meant, fires falsely or misses a violation; match the spec's exact timing.
• Missing disable iff reset. An assertion that evaluates during reset fires on reset-state signals; disable it during reset.
• Too-loose windows. ##[1:$] where the spec bounds the window lets a too-late event pass; use the exact bounded range.
• Disabling an assertion to quiet false failures. A false-firing assertion should be fixed to match the spec, not turned off — a disabled assertion catches nothing.
• Not covering the antecedent. A property whose antecedent never holds passes vacuously, checking nothing; cover the antecedent to confirm it ran.
• Confusing consecutive and goto repetition. [*n] is n consecutive cycles, [->n] is n occurrences not necessarily consecutive; pick the one the rule means.

Senior Design Review Notes

Interview Insights

Exercises

1. Translate the rule. Write the assertion for "after grant, the bus must be driven within 2 cycles and held until release."
2. Pick the operator. For "busy must be high the cycle after start," write the property and justify |-> versus |=>.
3. Fix the window. An assertion fires on a legal response at the spec's maximum latency. Identify the likely cause and fix.
4. Express a hold. Write a property that a stall lasts at most 4 consecutive cycles, using repetition.

Summary

• Protocol assertions are written in the SVA stack: boolean expressions (signal conditions) → sequences (temporal patterns via delays/repetition) → properties (checkable rules, usually implication) → directive (assert / cover / assume), all clocked and sampled with disable iff reset.
• The core operator is implication — |-> (overlapping, consequent the same cycle) and |=> (non-overlapping, the next cycle, ≡ |-> ##1); delays (##N, ##[m:n], ##[1:$]) and repetition ([*n] consecutive, [->n] goto) express timing windows and holds.
• Translating a protocol rule is matching it to a standard pattern — handshake (|-> ##[m:n]), stability (|=> signal/$stable), mutual exclusion (!(a && b)), ordering (|=> ##[1:$]), timing window (##[MIN:MAX]) — and filling in the exact operator, window, and condition.
• Fidelity is the quality bar: too strict (narrower window, wrong operator, missing qualifier) fires on legal behavior, and false failures erode trust until the assertion is disabled and real bugs go uncaught; too loose misses violations — an imprecise assertion is worse than none.
• The durable rule of thumb: write protocol assertions by translating the spec's temporal rules phrase by phrase into the SVA language — boolean to sequence to property to directive — choosing the exact implication operator (same vs next cycle), the exact delay window, and the exact condition, and matching common rules to their standard patterns; fidelity is everything, because a too-strict assertion fires on legal behavior and gets itself disabled while a too-loose one misses violations, and an imprecise checker that cries wolf gets silenced and then catches no wolves.

Next — Assertion-Based Verification: with assertions integrated and written, the next chapter steps back to the methodology — assertion-based verification (ABV) as an approach. Where assertions fit in the verification strategy, who writes them (design versus verification), assertions as executable specification, the trade-offs versus transaction-level checking, and how ABV combines with the constrained-random, coverage-driven flow into a complete checking strategy.