DOC SVC.POSTREV 2026.07
PAGE 06 / 08● LIVE
← All insights

SystemVerilog assertions that scale beyond block level.

Write properties around sampled intent, explicit reset semantics, reusable interfaces, and actionable failures.

CLKREQACKreq |-> ##[1:3] ackSAMPLED INTENT / WINDOW

SystemVerilog Assertions describe sampled temporal behavior. They scale when they express interface and state invariants in a consistent clocking model, and when a failure tells an engineer what obligation was violated. They become fragile when they encode an entire test scenario or depend on implicit sampling assumptions.

State the sampling contract

Every property needs a deliberate clock and reset policy. Use a default clocking event only when the containing scope has one unambiguous domain. For multi-clock logic, keep properties close to the interface or domain they observe. Decide whether reset disables the obligation, forms part of the antecedent, or must itself be checked.

Concurrent assertions sample values according to SystemVerilog scheduling semantics. A waveform viewed after updates can look different from values sampled by a property. When an assertion surprises you, inspect the clocking event, sampled-value functions, and reset expression before changing the temporal operator.

Express one obligation at a time

A useful property has a recognizable antecedent and consequence: when a defined condition occurs, a defined response must follow within a defined window. Split unrelated obligations. Separate legal-request checks, response timing, data stability, and cancellation behavior so a failure identifies the broken contract.

  1. Safety: something invalid never occurs.
  2. Response: a request receives an allowed response within a stated bound.
  3. Stability: payload remains stable while a transfer is stalled.
  4. Mutual exclusion: incompatible grants or states never overlap.
  5. Accounting: accepted work is neither duplicated nor lost.

Place properties at stable boundaries

Interface-level properties survive implementation changes better than assertions tied to temporary internal signals. Package reusable sequences and properties around protocol concepts, and bind implementation-specific assertions where editing RTL is undesirable. Parameterization should reflect real protocol variation, not create a property generator that nobody can review.

An assertion message should identify the interface instance, obligation, relevant identifiers, and sampled context. The property name should describe the rule rather than the expected outcome. Failure action blocks can add context, but checking semantics should remain in the property.

Measure assertion activity

A passing assertion may never have been activated. Track antecedent activity and add cover properties for meaningful scenarios, especially for properties used in formal analysis. Review disabled properties, vacuous results, and reset behavior. A zero-failure count alone is not evidence that the checker participated.

A scalable assertion library makes intent visible at the same boundaries where integration fails.

Prefer a small library of reviewed properties over many generated checks with unclear ownership. Run them in simulation, formal analysis where appropriate, and regression triage. Shared semantics turn assertions into executable interface documentation rather than isolated tool syntax.

Primary references

Need help applying these methods to a verification programme? Start a technical conversation.

▌ Engage with us

Bring us your hardest verification problem.

A focused specialist or a defined work package — scope, responsibilities, milestones, and evidence are agreed for each engagement.