Assertions
Rules the design must never break, checked automatically
An assertion is a rule you write down that must always hold true. The simulator watches it every cycle and complains the instant it is violated - even if your testbench was looking somewhere else. Assertions are like tripwires placed throughout the design.
Two kinds
| Type | When checked | Example rule |
|---|---|---|
| Immediate | Right now, inside procedural code | "At this point, count must not be zero" |
| Concurrent | Continuously, against the clock | "Whenever request rises, grant must follow within 3 cycles" |
An immediate assertion
// Check a condition at this moment
assert (fifo_count <= FIFO_DEPTH)
else $error("FIFO overflow: count = %0d", fifo_count);A concurrent assertion - rules over time
This is the powerful one. It expresses behavior across clock cycles in a compact line. Read the example as a sentence.
// "Every time req goes high, ack must be high
// within the next 1 to 3 clock cycles."
property req_gets_ack;
@(posedge clk) req |-> ##[1:3] ack;
endproperty
assert property (req_gets_ack)
else $error("req was not acknowledged in time");- @(posedge clk) - check on each clock edge.
- req |-> ... - "if req is true, then the rest must follow."
- ##[1:3] ack - ack must be true somewhere 1 to 3 cycles later.
The building blocks: sequence, property, assert
SVA is built in three layers. A sequence describes a pattern over time (for example req ##[1:3] ack). A property wraps a sequence, usually with an implication, to state a rule: if the antecedent happens, the consequent must follow. And an assertion directive uses the property: assert checks it and fails on a violation, assume constrains the inputs to obey it (used in formal), and cover records whether the scenario was ever actually exercised.
Overlapping vs non-overlapping implication
The two implication operators differ by exactly one cycle. With |-> (overlapping), the consequent is checked starting on the same cycle the antecedent matches. With |=> (non-overlapping), it is checked starting on the next cycle. So req |-> ack means ack in the same cycle as req, while req |=> ack means ack one cycle later. Picking the wrong one is a classic off-by-one assertion bug.
Sampled-value functions
A few built-in functions make edge and history checks readable. $rose(sig) is true when a signal went 0 to 1 this cycle, $fell(sig) when it went 1 to 0, $stable(sig) when it did not change, and $past(sig, n) gives its value n cycles ago. They let you write rules like "if $rose(req) then ack within 3 cycles" without hand-building the edge detection.
Assertions are documentation that checks itself. Writing "req must be acked within 3 cycles" as an assertion captures a spec rule AND enforces it on every test, forever. They often catch the bug at the exact cycle and signal where it happened, instead of as a wrong value a thousand cycles downstream.
Keep assertions in their own place (bound to the design or in the interface), not scattered through RTL. And assert the intent from the specification, not a restatement of the code - an assertion that just repeats the implementation only tells you the code equals itself, which proves nothing.
Finished reading?
Mark it complete to track your progress through the path.
Go further
Preparing for verification interviews? Practice the rounds companies actually run.
Get new lessons by email
New lessons, interview prep and real EDA tool workflows. No spam.