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.
⚡
Formal vs. Simulation
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.
assert
Assertions
Behaviors that must always be true. A failing assertion is a definitive bug. Example: two mutually exclusive grant signals must never be high simultaneously.
assume
Assumptions
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.
cover
Cover Properties
Scenarios that must be reachable. A cover failure means the behavior is impossible given your assumptions — often exposing over-constrained environments.
⚠
The Vacuity Trap
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.
| 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);
end
Concurrent 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.
L4
Assertion Directives
assert / assume / cover — instantiate a property and define pass/fail actions
L3
Properties
Combine sequences with implication (|->, |=>), not, disable iff, s_eventually
L2
Sequences
Ordered Boolean expressions across clock cycles using ##, [*], [->], and, or
L1
Boolean Expressions
Combinatorial conditions that evaluate true/false at a single clock tick — the atomic unit of SVA
// 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 check
05 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.
🎯
Which to use?
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:
01
RTL Freeze
Stable DUT — at least block-level complete
02
Write Properties
assert / assume / cover in bind files
03
Constrain Inputs
assume blocks to limit legal input space
04
Run Formal Tool
JasperGold, Questa Formal, or VC Formal
05
Analyze CEX
Debug counterexamples in waveform viewer
06
Close Coverage
Ensure all covers pass, no vacuous asserts
💡
Bind Files Keep RTL Clean
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 reachable
Mistake 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
✗
The Over-Constraint Trap
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 starves
Best 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_4cyc is 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}});
endmodule
module 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)
);
🔍
Reading the Property Set
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.