Capture values before Active and NBA updates.
Part 1 · Fundamentals
SystemVerilog AssertionsSampling and assertion anatomy
Learn what a property samples, how assertion scheduling avoids races, and how Boolean expressions become sequences, properties, and directives.
Question directory
Questions for Fundamentals
Open a question at its supporting explanation. The complete property reference stays directly above each answer set.
Sampling modelWhat is SVA, and what does it add to SystemVerilog?→Sampling modelHow do immediate and concurrent assertions differ?→Sampling modelWhere does a concurrent assertion sample, evaluate, and run its action block?→Sampling modelHow do $rose, $fell, $stable, and $past use sampled values?→Sampling modelWhich SVA helper functions catch one-hot and unknown-state bugs?→Assertion anatomyWhat is the difference between a sequence, a property, and an assertion directive?→Assertion anatomyWhat does ## mean, and how do delay ranges behave?→Assertion anatomyHow do and, or, intersect, throughout, and within compose sequences?→Assertion anatomyHow does property-level logic differ from sequence composition?→Assertion anatomyWhere can SVA live, and when should you bind a checker?→
Start with the reading method
Read every property as seven explicit decisions.
This is the shortest path from an English requirement to reviewable SVA. If one decision is missing, the property is probably underspecified.Sampling grid
Sample one coherent snapshot at every positive clock edge.
Each waveform column is one posedge of clk. Temporal delays count these sampling events, not simulator time and not arbitrary signal transitions between edges.
Selected clause
@(posedge clk)Complete request-to-acknowledgement contractSystemVerilog
a_req_ack: assert property (
@(posedge clk) disable iff (!rst_n)
$rose(req) |-> ##[1:3] (ack && !$isunknown(ack))
) else $error("ack missing or unknown: ack=%b", $sampled(ack));
c_last_slot: cover property (
@(posedge clk) disable iff (!rst_n)
$rose(req) ##1 !ack[*2] ##1 ack
);
Clock. Sampling grid. All eight columns are sampling events. One ##1 delay moves exactly one column to the right.
Requirement→Sampled trace→Property→Diagnostic + coverage
01 · Sampling modelReason from the sampled clock edge.
Separate simulation updates from assertion sampling, then explain exactly when a concurrent property observes, evaluates, and reports a result.
Concept modelOne clock tick crosses three assertion regions
Run the property using the sampled values.
Execute the concurrent pass or fail action.
disable iff observes current values and can abort between sampled clock events.
Always-visible reference
Learn the mechanism before testing the interview answer.
These notes, tables, examples, and design limits contain the working knowledge for this chapter. The interview questions below are a checkpoint, not the primary explanation.
Why assertions
Use SVA as an executable contract, not as decorative checking.
A useful assertion turns one requirement into an observable, reusable rule. It catches the failure close to its source, documents the intended behavior, and can run in both simulation and formal analysis.
Capture intent precisely
Name the clock, reset policy, trigger, deadline, and required outcome. The property is only as correct as that translation.
Fail near the cause
Internal invariants can expose a corrupt state before the bug propagates to a scoreboard-visible output.
Carry checks with the IP
Interface and block contracts can run in unit simulation, subsystem regression, emulation where supported, and formal harnesses.
Measure exercise separately
Assertion coverage and cover properties show whether attempts and important scenarios occurred. They do not replace data-oriented covergroups.
Two execution models
Choose the assertion form that matches the requirement.
Immediate assertions are procedural checks at one execution point. Concurrent assertions create clocked attempts that can span many samples.
| Form | When it evaluates | Best use | Important caution |
|---|---|---|---|
assert (expr) | When procedural control reaches it | Local combinational or algorithmic invariant | Simple form can observe transient delta-cycle values |
assert #0 / assert final | Deferred within the current time slot | Settled combinational result | Still procedural, not a multi-cycle temporal property |
assert property | On the declared or inherited sampling event | Latency, ordering, stability, pulse, and protocol rules | Uses sampled values and can create overlapping attempts |
Procedural invariant and temporal contractSystemVerilog
always_comb begin
a_grant_shape: assert final ($onehot0(grant))
else $error("grant is not one-hot-or-zero");
end
a_req_ack: assert property (
@(posedge clk) disable iff (!rst_n)
$rose(req) |-> ##[1:3] ack
);
Scheduler model
The sampled value can differ from the waveform value you see later.
At a concurrent assertion clock event, design values are sampled before Active and NBA updates. The property evaluates those samples later in the same time slot, and its action block runs after the result is known.
Sample
Capture the values used by the property before ordinary Active-region logic and nonblocking assignment updates.
Evaluate
Evaluate sequence matches and property truth using the Preponed samples.
Report
Run pass or fail action blocks. Use $sampled(signal) when the message must show the value that the property evaluated.
Abort
disable iff observes its current expression and can terminate an active attempt between sampling events.
Report sampled failure contextSystemVerilog
a_state_known: assert property (
@(posedge clk) disable iff (!rst_n)
!$isunknown(state)
) else $error(
"sampled state=%b current state=%b",
$sampled(state), state
);
Function handbook
Use the sampled-value and four-state helpers deliberately.
Every history function is interpreted on the property's sampling event. Vector edge functions inspect the least significant bit, so write an explicit vector comparison when the requirement is broader.
| Function | Meaning at this sample | Typical contract |
|---|---|---|
$rose(x) | LSB changed from 0/X/Z to 1 | One attempt per rising event |
$fell(x) | LSB changed from 1/X/Z to 0 | Release or completion edge |
$stable(x) | Whole expression equals its prior sample | Payload held under stall |
$changed(x) | Whole expression differs from its prior sample | State or ownership transition |
$past(x, n) | Value sampled n clock events earlier | History and causality |
$sampled(x) | Value captured for this assertion evaluation | Accurate failure message |
$onehot(x) | Exactly one bit is 1 | Exactly one owner |
$onehot0(x) | Zero or one bit is 1 | Idle-capable one-hot grant |
$isunknown(x) | At least one bit is X or Z | Four-state control integrity |
$countones(x) | Number of bits equal to 1 | Population limit |
Deployment
Place each checker where its inputs and ownership are clear.
White-box checks belong near internal state and datapath invariants. Black-box protocol checks belong at interfaces or in bound checkers. System-level ordering may require state outside a pure temporal property.
| Location | Sees | Best for | Ownership risk |
|---|---|---|---|
RTL module | Internal state and datapath | White-box invariants | Tight implementation coupling |
interface | Protocol signals | Reusable interface contract | Clock and modport conventions |
checker + bind | Explicit checker ports | Non-invasive integration | Accidental bind to every module instance |
formal harness | Boundary inputs and state | Assumptions, assertions, covers | Overconstraint |
scoreboard/model | Transactions and history | Identity, ordering, one-to-one accounting | Not a replacement for local assertions |
Interview checkpoint
Explain the rule, then defend its edge cases.
Open a prompt after studying the reference above. A strong answer should name the sampled edge, match endpoint, failure mode, and proof evidence.
Strong answer
SVA stands for SystemVerilog Assertions. It adds executable Boolean and temporal properties that can check design behavior in simulation and formal analysis, and can record that meaningful scenarios occurred.
Why it works
- Immediate assertions check a condition at a procedural execution point. Concurrent assertions describe sampled behavior across one or more clock events.
- Assertions work best as compact contracts near an interface, block, or bound checker, not as a replacement for scoreboards and end-to-end data models.
- A useful assertion names the requirement, states its clock and reset policy, and reports enough sampled context to reproduce a failure.
What the interviewer is testing
Whether you can describe assertions as executable specifications and choose them for temporal control behavior without claiming they replace every verification technique.
Common trap
Do not define SVA as only a simulator feature. The same property language is also central to formal verification and assertion coverage.
Strong answer
A simple immediate assertion executes like a procedural if statement when control reaches it. A concurrent assertion starts attempts on a declared clocking event and evaluates sampled behavior over time.
Why it works
- Use an immediate assertion for a local procedural invariant whose meaning is tied to that execution point.
- Use a concurrent property for clocked protocols, latency, stability, ordering, pulse width, and other temporal contracts.
- A deferred immediate form such as assert final can avoid reporting a transient combinational delta-cycle value.
What the interviewer is testing
Whether you connect assertion type to scheduling semantics instead of treating assert and assert property as interchangeable syntax.
Common trap
A simple immediate assertion does not automatically sample in Preponed or wait for a clock edge.
Procedural and clocked checksSystemVerilog
always_comb begin
a_onehot_grant: assert final ($onehot0(grant))
else $error("grant is not one-hot-or-zero");
end
a_req_ack: assert property (
@(posedge clk) disable iff (!rst_n)
$rose(req) |-> ##[1:3] ack
);
Strong answer
At its clocking event, a concurrent assertion samples referenced design values in Preponed, evaluates the property in Observed, and schedules its pass or fail action block in Reactive.
Why it works
- This region separation prevents the property from racing ordinary Active and NBA updates on the same clock edge.
- The disable iff expression is different: it uses current values and can asynchronously abort an active attempt.
- Inside a Reactive failure action, use $sampled(signal) when the message must report the value that the property actually evaluated.
- Choose $fatal, $error, $warning, or $info in an action block according to the regression policy; the property semantics do not change with the message severity.
What the interviewer is testing
Whether you can explain why a waveform's post-NBA value may differ from the value seen by the concurrent property on that same edge.
Common trap
Printing a raw signal from the action block and calling it the sampled failure value can produce a misleading diagnostic.
Report the sampled failure contextSystemVerilog
a_known_state: assert property (
@(posedge clk) disable iff (!rst_n)
!$isunknown(state)
) else $error(
"sampled state was %b",
$sampled(state)
);
Strong answer
They compare values sampled on the property clock. $rose and $fell detect a 0-to-1 or 1-to-0 transition of the expression's least significant bit, $stable checks that the sampled expression did not change, and $past(expr, n) returns its sampled value n clocking events earlier.
Why it works
- For a vector transition, write the comparison you actually mean instead of assuming $rose(vector) detects any rising bit.
- $stable(payload) is especially useful in a one-step invariant that is retriggered on every stalled ready-valid edge.
- Guard uses of $past near time zero or reset release until enough sampled history exists; otherwise the default historical value can create a misleading pass or failure.
What the interviewer is testing
Whether you connect sampled-value functions to the property clock and can explain their vector and startup edge cases.
Common trap
$past is not a free-running history database, and $rose on a bus does not mean any bit rose.
| Function | Question answered | Common use |
|---|---|---|
$rose(x) | Did sampled bit 0 change to 1? | One attempt per rising edge |
$fell(x) | Did sampled bit 0 change to 0? | Release or completion edge |
$stable(x) | Is x unchanged from the prior sample? | Payload under backpressure |
$past(x, n) | What was x n samples ago? | Bounded history and causality |
Strong answer
$onehot(expr) requires exactly one asserted bit, $onehot0(expr) permits zero or one, $isunknown(expr) detects any X or Z, and $countones(expr) returns the number of one bits. They turn common structural invariants into readable checks.
Why it works
- Use $onehot0 for an idle-capable grant vector and $onehot when one owner must always be selected.
- Check control and state vectors with !$isunknown(...) when X or Z must be a failure rather than an optimistic don't-care.
- $countones(mask) supports bounded-population rules, but state the legal count range explicitly so the intent is visible.
What the interviewer is testing
Whether you know the four-state and population-count helpers well enough to avoid hand-written, error-prone Boolean trees.
Common trap
$onehot0 does not require any bit to be asserted; confusing it with $onehot weakens the contract.
Structural state checksSystemVerilog
a_grant_onehot0: assert property (
@(posedge clk) disable iff (!rst_n)
$onehot0(grant)
);
a_state_known: assert property (
@(posedge clk) disable iff (!rst_n)
!$isunknown({state, valid, ready})
);
02 · Assertion anatomyBuild the temporal sentence in layers.
Start with Boolean expressions, compose sequences across sampled clocks, turn them into properties, and finally choose assert, assume, or cover.
Concept modelSVA grows from values into verification intent
01Boolean
req && readyValue now02Sequence
req ##[1:3] ackMatch across clocks03Property
req |-> responseConditional obligation04Directive
assert property (...)Verification jobDelay
##n · ##[m:n]Repeat
[*] · [=] · [->]Match
and · or · intersectSpan
throughout · withinOutcome
|-> · |=>Always-visible reference
Learn the mechanism before testing the interview answer.
These notes, tables, examples, and design limits contain the working knowledge for this chapter. The interview questions below are a checkpoint, not the primary explanation.
Language model
Identify the language layer before explaining an operator.
The same-looking words can have different semantics at the Boolean, sequence, property, and directive layers. Build the rule from the bottom up.
| Layer | Question it answers | Representative syntax |
|---|---|---|
Boolean expression | What is true on this sample? | req && ready, !$isunknown(state) |
Sequence | What temporal pattern matched? | req ##[1:3] ack, beat[*4] |
Property | What obligation is true or false? | trigger |-> consequent, disable iff |
Directive | What should the tool do? | assert, assume, cover, expect |
Reusable syntax
Name sequences and properties when the timing deserves a name.
A named sequence may have formal arguments, local variables, and an explicit or inherited clock. A property adds implication, reset, and truth-valued composition. Keep the trigger and outcome visible at the call site.
Sequence, property, checker, and bindSystemVerilog
sequence s_req_to_ack;
$rose(req) ##[1:3] $rose(ack);
endsequence
property p_req_to_ack;
@(posedge clk) disable iff (!rst_n)
$rose(req) |-> ##[1:3] $rose(ack);
endproperty
checker req_ack_checker (
input logic clk, rst_n, req, ack
);
a_req_to_ack: assert property (p_req_to_ack);
endchecker
bind request_unit
req_ack_checker i_req_ack_checker (.*);
Operator atlas
Use this table to translate English timing into SVA.
Parenthesize mixed temporal operators even when you know precedence. It makes the intended start point, span, and endpoint reviewable.
| Family | Syntax | Core meaning | Typical mistake |
|---|---|---|---|
Delay | ##0, ##n, ##[m:n] | Concatenate sequence elements by sampled clocks | Counting simulator time instead of samples |
Consecutive repeat | [*n], [*m:n] | Repeat a Boolean or sequence on consecutive samples | Forgetting the implicit ##1 between repeats |
Nonconsecutive repeat | [=n], [=m:n] | Count Boolean hits with gaps and optional trailing slack | Expecting the match to end on the last hit |
Goto repeat | [->n], [->m:n] | Count Boolean hits with gaps and end on the final hit | Applying it to an arbitrary sequence |
Sequence choice | or | Either sequence match is sufficient | Assuming only one candidate endpoint exists |
Sequence conjunction | and | Both start in one compound attempt; later endpoint wins | Treating it like Boolean && |
Endpoint conjunction | intersect | Both sequence matches must share an endpoint | Using it when different endpoints are legal |
Span | expr throughout seq | Expression holds over every sample of the selected match | Forgetting the endpoint is included |
Containment | inner within outer | A complete inner match fits inside outer | Confusing containment with implication |
Implication | |->, |=> | Create a conditional property obligation | Claiming |=> serializes attempts |
Endpoint selection | first_match(seq), seq.ended | Select earliest match or observe a named endpoint | Confusing endpoint selection with transaction ownership |
Outcome control | disable iff, accept_on, reject_on | Abort or force an attempt outcome | Treating all three as reset |
Per-attempt state
A property-local variable belongs to one attempt.
Capture a sampled value in a sequence match item. Every overlapping attempt receives its own copy, which makes local variables useful for correlation but not for global event consumption.
- The comma introduces a sequence match item and captures the value when the trigger matches.
- Do not use a standalone assignment as if it were a sequence expression.
- One response can still satisfy multiple overlapping attempts. Use outstanding-ID state or a scoreboard for one-to-one accounting.
- Functions called from assertion expressions should be side-effect-free. Verify tool support for complex dynamic, class, handle, or real-valued constructs.
Capture an ID legallySystemVerilog
property p_tagged_response;
logic [ID_W-1:0] saved_id;
@(posedge clk) disable iff (!rst_n)
($rose(req), saved_id = req_id)
|-> ##[1:8] (rsp && rsp_id == saved_id);
endproperty
Interview checkpoint
Explain the rule, then defend its edge cases.
Open a prompt after studying the reference above. A strong answer should name the sampled edge, match endpoint, failure mode, and proof evidence.
Strong answer
A sequence describes a temporal match. A property turns that match into a Boolean obligation, often with implication, reset, or logical composition. A directive such as assert, assume, or cover tells a tool what to do with the property.
Why it works
- Named sequences improve reuse, but a bare sequence used as a property fails whenever it does not match from a sampled start point.
- Implication is the usual way to say that a consequent matters only after an antecedent match.
- The same property can be asserted in one context, assumed at a formal boundary, or covered to measure reachability.
What the interviewer is testing
Whether you understand the semantic layers and avoid writing a bare temporal sequence when the intended requirement is conditional.
Common trap
The expression err[*2] ##1 alert alone is not a conditional checker. It fails on every start cycle where that complete sequence does not match.
Layer a conditional temporal checkSystemVerilog
sequence s_two_err;
$rose(err) ##1 err;
endsequence
property p_alert_after_two_err;
@(posedge clk) disable iff (!rst_n)
s_two_err |=> alert;
endproperty
a_alert_after_two_err:
assert property (p_alert_after_two_err);
Strong answer
The ## operator concatenates sampled sequence elements by clock ticks, not simulator time units. ##n selects an exact sampled delay, while ##[m:n] permits a match at any sampled delay in the inclusive range.
Why it works
- ##0 starts the next sequence element at the current sequence endpoint. ##1 advances one sampling event.
- A range can create several possible match endpoints. Draw those endpoints before composing it with and, intersect, throughout, or implication.
- Use a finite range when the specification has a deadline. An unbounded upper limit may need strong semantics or a separate fairness assumption in formal analysis.
What the interviewer is testing
Whether you count sampled clock events from the antecedent endpoint instead of counting visual spaces or simulation time.
Common trap
Do not read ##2 as two nanoseconds unless the property clock itself advances every nanosecond.
| Form | Meaning | Typical use |
|---|---|---|
##0 | Same sampled endpoint | Sequence composition |
##1 | Next sampling event | Next-cycle response |
##[1:3] | Any of the next one to three samples | Bounded latency |
##[1:$] | Some later sample | Unbounded eventual response |
Strong answer
or accepts a match from either operand. Sequence and starts both operands together and may finish when the later one ends. intersect also requires both operands to start together, but it requires the same endpoint. throughout and within constrain one sequence across another sequence's span.
Why it works
- Use intersect when identical endpoints are part of the requirement, not merely because two conditions must both happen.
- expr throughout seq requires expr on every sampled tick occupied by a selected match of seq.
- inner within outer requires a complete inner match to fit inside an outer match.
What the interviewer is testing
Whether you reason about start and end points rather than treating temporal and as ordinary Boolean conjunction.
Common trap
Two sequences can both match and still fail intersect because their endpoints differ.
Strong answer
Sequence operators such as and, or, and intersect combine temporal matches and therefore have start and endpoint semantics. Property-level not, and, or, and if...else combine truth-valued property expressions. The spelling can look similar, but the object being combined is different.
Why it works
- Sequence and permits different endpoints, while sequence intersect requires a common endpoint; property and simply requires both property expressions to succeed.
- A property if...else selects one property branch from a sampled Boolean condition, which is useful when operating modes have different legal behavior.
- Named properties can be reused and may be recursive, but recursive properties are an advanced feature with progress and operator restrictions; use a positive time advance and verify tool support.
What the interviewer is testing
Whether you can identify the language layer before explaining an operator and avoid applying Boolean intuition to temporal endpoints.
Common trap
Do not assume that sequence and, property and, and Boolean && have identical timing or completion semantics.
| Layer | Examples | Primary concern |
|---|---|---|
Boolean | &&, ||, ! | Value on one sampled edge |
Sequence | and, or, intersect | Temporal match and endpoint |
Property | not, and, or, if...else | Truth of an obligation |
Strong answer
Sequences and properties can be declared in modules, interfaces, programs, clocking blocks, packages, or compilation-unit scope where the language permits them. A bound checker attaches verification logic to a module type or instance without editing the RTL, which keeps reusable interface contracts separate from implementation code.
Why it works
- Place white-box assertions near internal invariants when design ownership allows it; place black-box protocol assertions at interfaces or in reusable checker modules.
- Binding a module type applies the checker to every matching instance, while an instance-specific bind targets one hierarchy location.
- Pass signals through explicit checker ports when possible. Uncontrolled hierarchical references make reuse and integration fragile.
What the interviewer is testing
Whether you can choose an ownership and deployment model for assertions instead of treating their file location as an afterthought.
Common trap
bind changes where the checker is instantiated, not the timing semantics of its properties.
Attach a checker without editing RTLSystemVerilog
checker req_ack_checker (
input logic clk, rst_n, req, ack
);
a_req_ack: assert property (
@(posedge clk) disable iff (!rst_n)
$rose(req) |-> ##[1:3] ack
);
endchecker
bind request_unit
req_ack_checker i_req_ack_checker (.*);