In short: systemverilog assertions (SVA) let verification engineers describe what a design must and must not do as formal, time-aware rules that simulators and formal tools check automatically. They come in two flavours — immediate assertions that fire inside procedural code, and concurrent assertions that watch signals across clock edges using sequences, properties and implication operators.
SystemVerilog Assertions, almost always written as systemverilog assertions (SVA), are a declarative sub-language built into the SystemVerilog standard (IEEE 1800) for specifying the expected temporal behaviour of a hardware design. Instead of writing yet more procedural checker code, you state a property — "every request is eventually granted", "FIFO full and write-enable are never high together" — and the tool continuously evaluates it. When the property is violated, the assertion fails, pinpoints the exact clock cycle and signals involved, and (optionally) stops or counts the error.
Assertions serve three jobs at once. They act as executable documentation of designer intent, as active checkers during dynamic simulation, and as the proof targets that formal property-verification engines try to exhaustively prove or disprove. A single, well-written assertion can therefore be reused across directed tests, constrained-random UVM environments, and formal sign-off.
SVA has exactly two assertion kinds, and understanding the split is the single most tested concept in interviews.
An immediate assertion is a procedural statement that behaves like an if check. It evaluates the moment execution reaches it, using the current simulation values, and has no notion of a clock. It is written inside an always or initial block:
assert (a && b) else $error("a and b must both be high");assert final and assert #0 were added to avoid false fails on transient values.A concurrent assertion is clocked and samples its operands in the preponed region, just before the clock edge, so it always sees stable values. It describes behaviour that unfolds over multiple cycles and is typically placed in module scope:
assert property (@(posedge clk) req |=> gnt);Concurrent assertions are built from two layers. A sequence describes a series of events across cycles; a property wraps sequences with directionality and operators, and is what you actually assert.
The core operator is the cycle delay ##n, meaning "n clock ticks later". A range ##[1:3] allows a window, and ##[1:$] means "eventually". Repetition operators compress common patterns:
a ##1 b ##2 c — a, then b one cycle later, then c two cycles after that.a[*3] — a holds for three consecutive cycles (consecutive repetition).a[=2] and a[->2] — non-consecutive and goto repetition, matching the 2nd occurrence of a.A property adds operators sequences cannot express alone: not (must never happen), and/or, throughout (a condition holds for the whole span of a sequence), within, and the implication operators described next. You name reusable properties and sequences so a verification plan reads like a specification:
property p_handshake; @(posedge clk) disable iff (!rst_n) req |-> ##[1:4] ack; endpropertydisable iff (!rst_n) is the standard way to suppress assertions during reset so you do not drown in spurious failures.Implication is the heart of most real assertions. It splits a property into an antecedent (the trigger) and a consequent (what must then be true). The consequent is only checked when the antecedent matches — this is called vacuous success when it does not.
|->: the consequent is evaluated in the same cycle the antecedent completes. wr_en |-> !full means "on any cycle wr_en is high, full must be low that same cycle".|=>: the consequent starts one cycle after the antecedent matches. It is exactly equivalent to |-> ##1. req |=> gnt means "the cycle after req, gnt must be high".Choosing the wrong operator is a classic bug: using |-> where the protocol has a one-cycle latency produces failures on every valid transaction, while |=> on a combinational relationship misses the real cycle.
In practice SVA lives in three places: inline in RTL for designer-authored "white-box" checks, in bind files that attach assertions to a DUT without touching its source (bind dut_module assert_checker chk(.*);), and inside UVM interfaces and scoreboards. The cover property directive is the under-used companion to assert — it reports whether a scenario was ever exercised, turning assertions into functional-coverage points.
Every major simulator (Synopsys VCS, Cadence Xcelium, Siemens Questa) compiles concurrent assertions natively and reports pass, fail and vacuous counts. Formal tools (Cadence JasperGold, Synopsys VC Formal, Questa PropCheck) consume the same SVA and attempt a mathematical proof over all legal input sequences, which is why a reusable assertion library pays for itself: write once, run in both simulation and formal. Assertion density and the ratio of proven-to-covered properties are now standard metrics in sign-off reviews.
Real projects and industry tool flows, with certification.
Explore CourseTron Courses →The overlapping operator |-> checks the consequent in the same cycle the antecedent succeeds; the non-overlapping operator |=> checks it one cycle later. a |=> b is identical to a |-> ##1 b. Use overlapping for same-cycle relationships and non-overlapping when there is a one-cycle protocol latency.
When the antecedent of an implication never matches on a given evaluation attempt, the property passes trivially without checking the consequent — that is a vacuous pass. Tools count vacuous and non-vacuous passes separately; a property that only ever passes vacuously means your stimulus never triggered it, so add a cover property to confirm real coverage.
Concurrent assertions are clocked and sample operands in the preponed region, giving glitch-free, race-free values and the ability to span multiple cycles with sequences and implication. Immediate assertions are unclocked, single-point procedural checks that read active-region values, so they are best for simple in-block sanity checks, not temporal protocols.
disable iff (expr) asynchronously aborts assertion evaluation whenever the expression is true, most commonly during reset. Without it, every in-flight property would report failures while the design is held in reset, flooding the log with false errors and masking real bugs.
Related: UVM scoreboards · the VLSI Glossary · all courses.