SystemVerilog Assertions — A Comprehensive Guide
SystemVerilog
Assertions —
A Comprehensive Guide
From Boolean building blocks to advanced temporal properties — everything you need to write robust formal verification properties for your hardware design, with real waveform intuition for every operator.
01 Why SystemVerilog Assertions?
In hardware design, creating a functionally correct circuit is only half the battle. The other half — proving it works exactly as intended across all possible scenarios — demands a rigorous, mathematically grounded approach. This is the domain of formal verification.
SystemVerilog Assertions (SVAs) are the industry-standard mechanism for encoding design intent as mathematical properties. A formal verification tool can then exhaustively check these properties against your RTL — eliminating entire classes of bugs that simulation might miss even after months of random testing.
Simulation checks specific scenarios you thought to write. Formal verification checks all reachable states — including corner cases you didn't think of. A single well-written assertion can catch bugs that 10 million simulation cycles would never expose.
SVA operates in two contexts: simulation (assertions fire at runtime, flagging failures immediately) and formal property verification (FPV) (a solver mathematically proves or disproves properties without running a testbench). Both use the same syntax — write once, verify everywhere.
02 The Three Statement Types
Every SVA statement is one of three kinds. Understanding the distinction is fundamental — they answer different questions about your design.
Behaviors that must always be true. A failing assertion is a definitive bug. Example: two mutually exclusive grant signals must never be high simultaneously.
Constraints on the input environment. The formal tool restricts its exploration to inputs that satisfy all assumptions — they define the "legal" operating space of your DUT.
Scenarios that must be reachable. A cover failure means the behavior is impossible given your assumptions — often exposing over-constrained environments.
An assertion whose antecedent is never triggered always passes — but trivially. This is called vacuous passing and is one of the most dangerous failure modes in formal verification. Always pair every assert property with a corresponding cover property to confirm the trigger condition is actually reachable.
03 Immediate vs. Concurrent Assertions
| Aspect | Immediate | Concurrent |
|---|---|---|
| Evaluation model | Procedural — like an if statement | Clock-driven — at every specified edge |
| Time span | Single point in time | Can span multiple cycles |
| Clock awareness | None | Explicit clock specification required |
| Used in FPV? | No (simulation only) | Yes — primary FPV tool |
| Placement | Inside procedural blocks | Module, interface, or program scope |
| Reset handling | Manual (wrap in if) | Built-in via disable iff |
Immediate Assertion
always_comb begin
// Fires immediately — no clock, no history
assert (!(grant_a && grant_b))
else $error("[ASSERT] Mutual exclusion violated at time %0t", $time);
endConcurrent Assertion
// Named assertion — label is critical for debug reports
P_req_ack: assert property (
@(posedge clk) disable iff (rst)
req |-> ##[1:4] ack
) else $error("[P_req_ack] ACK not received within 4 cycles of REQ!");04 SVA Syntax: A Layered Architecture
SVA syntax is a four-layer stack. Each layer builds on the one below — more expressive, higher-level constructs are composed from simpler primitives. Understanding this hierarchy makes complex properties much easier to read and write.
assert / assume / cover — instantiate a property and define pass/fail actions|->, |=>), not, disable iff, s_eventually##, [*], [->], and, or// L1: Boolean expressions — req, ack (simple signal references)
// L2: Sequence — req ##[1:4] ack (spans multiple cycles)
// L3: Property — with clock, reset, implication
property p_handshake;
@(posedge clk) disable iff (rst)
req |-> ##[1:4] ack;
endproperty
// L4: Directive — instantiate as assertion
P_handshake: assert property (p_handshake);
C_handshake: cover property (p_handshake); // Vacuity check05 Key Sequence Operators
These operators form the grammar of SVA sequences. Each one has a precise timing meaning — the waveforms below make the behavior concrete.
| Operator | Name | Meaning & Example |
|---|---|---|
| ##n | Fixed Delay | Exactly n clock cycles elapse.
req ##2 ack → ack must be high exactly 2 cycles after req |
| ##[a:b] | Range Delay | Between a and b cycles inclusive. Use $ for unbounded.
req ##[1:4] ack → ack arrives in 1 to 4 cycles |
| [*n] | Consecutive Repetition | Boolean true for exactly n back-to-back cycles.
valid[*3] → valid must be high for 3 consecutive cycles |
| [*a:b] | Variable Repetition | True for a to b consecutive cycles.
busy[*1:8] → busy stays high for 1 to 8 cycles |
| [->n] | Goto Repetition | True exactly n times, not necessarily consecutive; last occurrence ends the sequence.
ack[->2] → ack must be seen 2 times total |
| [=n] | Non-Consecutive Repetition | Like [->n] but the sequence can continue after the last match.
ack[=2] → ack seen 2 times (sequence may continue after) |
| and | Sequence AND | Both sequences must match; they start together but can end at different times.
(a ##1 b) and (c ##2 d) |
| intersect | Sequence Intersect | Like and but both sequences must end at the same cycle.
(a[*3]) intersect (b ##1 c ##1 d) |
| within | Subsequence | First sequence occurs within the window of the second.
a within (b ##[0:$] c) |
06 Implication Operators: Overlapped vs. Non-Overlapped
Implication is the most-used — and most-confused — concept in SVA. Both operators say "if the antecedent matches, then the consequent must also match," but they differ in when the consequent starts.
Overlapped Implication |->
The consequent starts in the same cycle as the last cycle of the antecedent. Think of it as "immediately check."
Non-Overlapped Implication |=>
The consequent starts in the next cycle after the antecedent ends. Equivalent to |-> ##1. Use this for registered outputs — the DUT needs a clock edge to produce a response.
Use |-> for combinatorial outputs (mux selects, arbitration grants that respond in the same cycle). Use |=> for registered outputs (pipeline stages, FIFO flags, FSM state transitions that take a clock cycle to respond).
07 Auxiliary Code & Sampled Value Functions
Complex behaviors are often impossible to capture in a single self-contained property. Auxiliary code — regular SystemVerilog logic that tracks state — bridges this gap. The principle: compute the complex state in an always block, then assert a simple property on the result.
// Auxiliary: count consecutive valid beats
int valid_run;
always @(posedge clk)
valid_run <= valid ? valid_run + 1 : 0;
// Simple property — never hold valid for more than 8 consecutive cycles
P_max_burst: assert property (
@(posedge clk) disable iff (rst)
valid_run <= 8
);Sampled Value Functions
These built-in functions give your properties visibility into signal history across clock cycles:
$past(sig, n)
Value of sig as it was n clock cycles ago. Default n=1.
$rose(sig)
True if sig transitioned 0→1 on the current clock edge.
$fell(sig)
True if sig transitioned 1→0 on the current clock edge.
$changed(sig)
True if sig has a different value than the previous cycle.
$stable(sig)
True if sig has the same value as the previous cycle.
$countones(sig)
Returns number of bits set to 1. Essential for one-hot arbitration checks.
// $past: output must equal input from 2 cycles ago (pipeline latency check)
P_pipe_latency: assert property (
@(posedge clk) disable iff (rst)
out_valid |-> (dout === $past(din, 2))
);
// $rose: on rising edge of valid, data must be stable for 1 more cycle
P_data_stable: assert property (
@(posedge clk) disable iff (rst)
$rose(valid) |=> $stable(data)
);
// $countones: one-hot grant check — exactly one grant at a time
P_one_hot_grant: assert property (
@(posedge clk) disable iff (rst)
|grant |-> ($countones(grant) === 1)
);08 FPV Tool Flow
Writing good SVA properties is only half the job. Understanding how they fit into a real formal verification flow is equally important. Here's the typical FPV flow used in industry:
Always place your property module in a separate file and use a bind statement. This gives the property module full port visibility into the DUT without touching the RTL — a clean design/verification boundary that's essential for tapeout.
09 Common Mistakes & How to Fix Them
Mistake 1: Forgetting disable iff
Without reset handling, assertions fire during reset — filling your log with false failures and masking real ones.
assert property (
@(posedge clk)
req |=> ack
);assert property (
@(posedge clk)
disable iff (rst)
req |=> ack
);Mistake 2: Vacuous Assertions Without Cover
P_arb: assert property (
@(posedge clk)
req |=> grant
);
// If req is never high, always passes!P_arb: assert property (
@(posedge clk)
req |=> grant
);
C_arb: cover property (
@(posedge clk) req
); // Confirms req is reachableMistake 3: Using == Instead of === for X/Z Detection
// X == 1 evaluates to X (not true)
// Assertion doesn't fire on X values
assert property (
@(posedge clk)
state == 2'b00
);// === includes X and Z in comparison
// Fires if state is X or unexpected
assert property (
@(posedge clk)
state !== 2'bxx
);Mistake 4: Over-constraining with Assumptions
If your assume blocks are too tight, the formal tool will "prove" properties that only hold under impossible input conditions — and real silicon will fail. Always check: does every cover property pass? If a cover fails, your assumptions may be excluding the scenario you were trying to cover.
10 Advanced Features & Best Practices
Reset Handling with disable iff
// Asynchronous reset: disable iff checks continuously (not just at clock edges)
P_fifo_no_overflow: assert property (
@(posedge clk) disable iff (rst_n === 1'b0)
fifo_full |-> !wr_en
);
// Synchronous reset: use $rose to catch the exact reset release edge
P_sync_reset_check: assert property (
@(posedge clk)
$rose(rst_n) |=> (state === IDLE)
);Liveness Properties with s_eventually
Safety properties say "bad things never happen." Liveness properties say "good things will always eventually happen." Without liveness, your design could be "safe" by doing nothing.
// Safety: grant is mutually exclusive
P_mutex: assert property (
@(posedge clk) disable iff (rst)
!(grant_a && grant_b)
);
// Liveness: every request must eventually be granted
P_liveness: assert property (
@(posedge clk) disable iff (rst)
req |-> s_eventually grant
);
// Together: safe arbitration that never starvesBest Practice Checklist
- ✓One behavior per assertion. When a property fails, you know exactly what broke. Compound properties make debug exponentially harder.
- ✓Always use auxiliary code for complex state. Keep the property expression itself simple — complexity lives in the helper logic.
- ✓Pair every assert with a cover. No exceptions. Vacuous passes are silent bugs.
- ✓Name every property.
P_req_ack_4cycis infinitely more useful than line 247 in a waveform failure report. - ✓Use
===/!==for safety-critical checks. These include X and Z in the comparison —==does not. - ✓Write both safety and liveness properties. A correct arbiter must grant without deadlock — safety alone doesn't prove that.
- ✓Version your SVA alongside your RTL. Properties that don't track RTL changes become incorrect and misleading.
- ✓Check cover results, not just assert results. All covers must pass before you declare the FPV run complete.
11 Full Working Example
A complete, production-style FPV environment for a 4-bit counter with enable, synchronous reset, and a max_reached output flag. Demonstrates auxiliary code, all sampled functions, both implication operators, liveness, and the bind flow.
module counter #(
parameter WIDTH = 4
) (
input logic clk, rst, en,
output logic [WIDTH-1:0] count,
output logic max_reached
);
always @(posedge clk) begin
if (rst) count <= '0;
else if (en) count <= count + 1;
end
assign max_reached = (count === {WIDTH{1'b1}});
endmodulemodule counter_props #(
parameter WIDTH = 4
) (
input logic clk, rst, en,
input logic [WIDTH-1:0] count,
input logic max_reached
);
// ── Auxiliary Code ──────────────────────────────────────────────────
// Track whether count has been monotonically increasing
logic count_was_incrementing;
always @(posedge clk) begin
if (rst)
count_was_incrementing <= 1'b0;
else
count_was_incrementing <= en && (count < {WIDTH{1'b1}});
end
// ── Input Constraints (Assumptions) ────────────────────────────────
// Assume rst deasserts cleanly (no glitches)
A_rst_stable: assume property (
@(posedge clk)
$fell(rst) |=> $stable(rst)[*4]
);
// ── Safety Properties ───────────────────────────────────────────────
// Reset clears counter in the next cycle (|=> non-overlapped: registered output)
P_reset_clears: assert property (
@(posedge clk)
$rose(rst) |=> (count === '0)
);
// Counter increments by exactly 1 (uses $past for previous value)
P_increment: assert property (
@(posedge clk) disable iff (rst)
en && (count < {WIDTH{1'b1}})
|=> (count === ($past(count) + 1))
);
// Counter holds when not enabled (uses $stable)
P_hold_when_disabled: assert property (
@(posedge clk) disable iff (rst)
!en |=> $stable(count)
);
// max_reached flag is correct (combinatorial: |-> overlapped)
P_max_flag: assert property (
@(posedge clk) disable iff (rst)
max_reached |-> (count === {WIDTH{1'b1}})
);
// No X/Z propagation on outputs
P_no_x_count: assert property (
@(posedge clk) disable iff (rst)
!$isunknown(count)
);
// ── Liveness Properties ─────────────────────────────────────────────
// If enabled, count must eventually reach max
P_reaches_max: assert property (
@(posedge clk) disable iff (rst)
en |-> s_eventually max_reached
);
// ── Cover Properties (vacuity & reachability checks) ───────────────
// Confirm counter reaches mid-range
C_reaches_mid: cover property (
@(posedge clk) disable iff (rst)
(count === {1'b0, {(WIDTH-1){1'b1}}})
);
// Confirm counter wraps (max then zero next cycle)
C_wrap: cover property (
@(posedge clk) disable iff (rst)
(count === {WIDTH{1'b1}}) ##1 (count === '0)
);
// Confirm reset can occur mid-count
C_mid_reset: cover property (
@(posedge clk)
(count > '0) ##1 $rose(rst)
);
endmodule
// ── Bind Statement ──────────────────────────────────────────────────
// Connects property module to DUT without modifying RTL
bind counter counter_props #(.WIDTH(WIDTH)) u_props (
.clk (clk),
.rst (rst),
.en (en),
.count (count),
.max_reached (max_reached)
);Notice how |=> is used for registered outputs (reset effect, increment) and |-> for the combinatorial max_reached flag. This distinction prevents false failures. The cover properties confirm that reset mid-count, the wrap case, and mid-range values are all reachable — ruling out vacuous assertion passes.
Comments