Chapter 1 · Fundamentals

Sampling and assertion anatomy

Q: How do and, or, intersect, throughout, and within compose sequences?

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. 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. Interview focus: 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.

Try the experiment ↓

Learn what a property samples, how assertion scheduling avoids races, and how Boolean expressions become sequences, properties, and directives.

Curated and reviewed by industry engineersUpdated July 2026IEEE 1800 SystemVerilog reference

Watercolor of a verification workstation with waveform traces and a development board. — Turn timing contracts into checks.

The language bench / assertions

Give the response a deadline.

Sampled clock 0RESET RELEASED

Sampled values by clock cycle
Cycle	req	ack	reset
0	0	0	0

No rising request has been exercised. There is no response evidence yet.

REQ at next clock

ACK at next clock

Controls stage the next sample. Reset acts between clocks. This scratch trace holds 24 clocks; Reset starts again.

pending0

passed0

failed0

aborted0

assert property (@(posedge clk) disable iff (!rst_n)
  $rose(req) |-> ##[1:3] ack);
// ACK must be sampled 1, 2, or 3 cycles after REQ rises.

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?

Sampling reference

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)

Each row is one sampled positive clock edge. Highlighted rows belong to the selected obligation.

Sample	rst_n	req	ack	outcome	cover hit
t0	0	0	0	0	0
t1	1	0	0	0	0
t2	1	1	0	0	0
t3	1	0	0	0	0
t4	1	0	0	0	0
t5	1	0	1	1	1
t6	1	0	0	0	0
t7	1	0	0	0	0

All eight columns are sampling events. One ##1 delay moves exactly one column to the right.

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.

RequirementSampled tracePropertyDiagnostic + coverage

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

01SamplePreponed

Capture values before Active and NBA updates.

02EvaluateObserved

Run the property using the sampled values.

03ReportReactive

Execute the concurrent pass or fail action.

disable iff observes current values and can abort between sampled clock events.

Concurrent properties sample design values in Preponed, evaluate those samples in Observed, and schedule pass or fail action blocks in Reactive.

Reference, examples and proof details

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.

Specification

Capture intent precisely

Name the clock, reset policy, trigger, deadline, and required outcome. The property is only as correct as that translation.

Observability

Fail near the cause

Internal invariants can expose a corrupt state before the bug propagates to a scoreboard-visible output.

Reuse

Carry checks with the IP

Interface and block contracts can run in unit simulation, subsystem regression, emulation where supported, and formal harnesses.

Evidence

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.

Preponed

Sample

Capture the values used by the property before ordinary Active-region logic and nonblocking assignment updates.

Observed

Evaluate

Evaluate sequence matches and property truth using the Preponed samples.

Reactive

Report

Run pass or fail action blocks. Use $sampled(signal) when the message must show the value that the property evaluated.

Asynchronous control

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.

SVA
assertions
simulation
formal

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
);

immediate assertion
concurrent assertion
assert final

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)
);

Preponed
Observed
Reactive
$sampled

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

$rose
$fell
$stable
$past
sampling

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})
);

$onehot
$onehot0
$isunknown
$countones

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

01Booleanreq && readyValue now

02Sequencereq ##[1:3] ackMatch across clocks

03Propertyreq |-> responseConditional obligation

04Directiveassert property (...)Verification job

Delay##n · ##[m:n]

Repeat[*] · [=] · [->]

Matchand · or · intersect

Spanthroughout · within

Outcome|-> · |=>

Each layer adds one kind of meaning. A directive gives a property a job; it does not change the property's timing semantics.

Reference, examples and proof details

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);

sequence
property
assert property
antecedent

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

##
cycle delay
range
clocking event

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

property logic
if...else
recursive property
sequence

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 (.*);

bind
checker
interface
white-box
black-box

Sampled values by clock cycle

Cycle

req

ack

reset

Sample

rst_n

req

ack

outcome

cover hit

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 );

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

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 );

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

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

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

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 (.*);

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

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