Assertions are powerful statements that automatically check your design's behavior during simulation. They catch bugs immediately when they happen, not hours later when you're debugging waveforms. This is your complete guide to mastering SVA.
SystemVerilog Assertions (SVA) are statements embedded in the design or testbench that validate specific behaviors or temporal rules.
Think of them as "Active Comments":
SVA solves the "Needle in a Haystack" problem. In traditional verification, a "Test Failed" message at simulation time 1,000,000ns might be caused by a bug that happened at 200ns. Assertions fire the exact cycle the violation occurs, pointing you directly to the source of the error.
// Your FIFO verification
// Test runs for 10000 cycles
// At cycle 9532, read data is wrong
// You spend 4 hours debugging waveforms...
// Finally discover: overflow happened at cycle 234!// Assertion fires immediately at cycle 234:
// "ERROR: FIFO overflow! write_en=1 when full=1"
// Bug found in seconds, not hours!SystemVerilog provides two types of assertions:
Checked at a single point in time, like an if statement. Used in procedural code (always blocks, tasks, functions).
always @(posedge clk) begin
// Simple immediate assertion
assert (data != 'x)
else $error("Data is unknown!");
// With pass action
assert (valid && ready)
$display("Handshake successful!")
else
$error("Handshake failed: valid=%b, ready=%b", valid, ready);
// Assert with severity levels
assert (count <= MAX_COUNT)
else begin
$fatal(1, "Counter overflow! count=%0d, max=%0d", count, MAX_COUNT);
end
endChecked continuously over time, can span multiple clock cycles. Used for protocol checking and temporal relationships.
// Property: After req goes high, ack must follow within 1-5 cycles
property req_ack_protocol;
@(posedge clk) disable iff (rst)
req |-> ##[1:5] ack;
endproperty
// Assert the property
assert property (req_ack_protocol)
else $error("Protocol violation: ack not received within 5 cycles of req");
// Cover the property (for verification)
cover property (req_ack_protocol)
$display("req->ack handshake observed");Immediate assertions have three forms:
// Basic form
assert (expression);
// With messages
assert (address[1:0] == 2'b00)
else $error("Address must be word-aligned!");assert (expression) pass_action else fail_action;
// Example
assert (fifo_full && write_en == 0)
$display("PASS: No write when full")
else
$error("FAIL: Attempted write to full FIFO");Deferred assertions handle glitches by evaluating at the end of the time step:
// #0 - Observed region (after all NBA updates)
assert #0 (data === expected_data)
else $error("Data mismatch in observed region");
// final - Final region (very end of time step)
assert final (done || (count < MAX))
else $error("Failed at end of time step");// $info - Informational message (lowest severity)
// $warning - Warning, simulation continues
// $error - Error, simulation continues (default)
// $fatal - Fatal error, simulation stops immediately
assert (condition)
else begin
case (severity_level)
0: $info("Just FYI: condition failed");
1: $warning("Watch out! condition failed");
2: $error("Error! condition failed");
3: $fatal(1, "Fatal! condition failed, stopping simulation");
endcase
endConcurrent assertions are the heart of SVA. They describe temporal relationships and protocols using sequences and properties.
// Level 1: SEQUENCE - Defines a pattern of events
sequence burst_start;
valid && ready && burst_type != 0;
endsequence
// Level 2: PROPERTY - Adds temporal logic
property burst_completes;
@(posedge clk) disable iff (reset)
burst_start |-> ##[1:10] burst_done;
endproperty
// Level 3: ASSERTION - Checks the property
assert property (burst_completes)
else $error("Burst did not complete within 10 cycles");| Operator | Meaning | Example |
|---|---|---|
##N
|
Delay by N cycles |
req ##2 ack (ack 2 cycles after req)
|
##[m:n]
|
Delay by m to n cycles |
req ##[1:5] ack (ack within 1-5 cycles)
|
|->
|
Overlapping implication |
a |-> b (if a, then b same cycle)
|
|=>
|
Non-overlapping implication |
a |=> b (if a, then b next cycle)
|
[*N]
|
Consecutive repetition |
valid[*3] (valid for 3 cycles)
|
[->N]
|
Goto repetition |
ack[->3] (wait for 3rd ack)
|
[=N]
|
Non-consecutive repetition |
valid[=3] (3 valids, not necessarily consecutive)
|
module fifo_assertions (
input logic clk, rst_n,
input logic push, pop,
input logic full, empty,
input logic [7:0] wdata, rdata,
input logic [4:0] count
);
// Never write to a full FIFO
property no_write_when_full;
@(posedge clk) disable iff (!rst_n)
full |-> !push;
endproperty
assert property (no_write_when_full)
else $error("FIFO OVERFLOW: push while full!");
// Never read from an empty FIFO
property no_read_when_empty;
@(posedge clk) disable iff (!rst_n)
empty |-> !pop;
endproperty
assert property (no_read_when_empty)
else $error("FIFO UNDERFLOW: pop while empty!");
// Count should increment on push only
property count_inc_on_push;
@(posedge clk) disable iff (!rst_n)
(push && !pop && !full) |=> (count == $past(count) + 1);
endproperty
assert property (count_inc_on_push);
// Count should decrement on pop only
property count_dec_on_pop;
@(posedge clk) disable iff (!rst_n)
(pop && !push && !empty) |=> (count == $past(count) - 1);
endproperty
assert property (count_dec_on_pop);
// Count should stay same on simultaneous push and pop
property count_stable_on_both;
@(posedge clk) disable iff (!rst_n)
(push && pop && !full && !empty) |=> (count == $past(count));
endproperty
assert property (count_stable_on_both);
// Full flag correctness
property full_check;
@(posedge clk) disable iff (!rst_n)
(count == 16) |-> full;
endproperty
assert property (full_check);
// Empty flag correctness
property empty_check;
@(posedge clk) disable iff (!rst_n)
(count == 0) |-> empty;
endproperty
assert property (empty_check);
endmodulemodule ahb_assertions (
input logic HCLK,
input logic HRESETn,
input logic [31:0] HADDR,
input logic [1:0] HTRANS,
input logic HWRITE,
input logic [2:0] HSIZE,
input logic [2:0] HBURST,
input logic [31:0] HWDATA,
input logic [31:0] HRDATA,
input logic HREADY,
input logic [1:0] HRESP,
input logic HSEL
);
// HTRANS encoding
localparam IDLE = 2'b00;
localparam BUSY = 2'b01;
localparam NONSEQ = 2'b10;
localparam SEQ = 2'b11;
// 1. Address must be aligned based on HSIZE
property addr_aligned;
@(posedge HCLK) disable iff (!HRESETn)
(HTRANS inside {NONSEQ, SEQ}) |->
case (HSIZE)
3'b001: (HADDR[0] == 0); // Halfword
3'b010: (HADDR[1:0] == 0); // Word
3'b011: (HADDR[2:0] == 0); // Doubleword
default: 1'b1;
endcase;
endproperty
assert property (addr_aligned)
else $error("AHB: Address not aligned for transfer size");
// 2. BUSY transfer only allowed within a burst
property busy_only_in_burst;
@(posedge HCLK) disable iff (!HRESETn)
(HTRANS == BUSY) |-> (HBURST != 3'b000); // Not SINGLE
endproperty
assert property (busy_only_in_burst)
else $error("AHB: BUSY transfer outside burst");
// 3. Control signals stable during wait states
property control_stable_during_wait;
@(posedge HCLK) disable iff (!HRESETn)
(!HREADY && HTRANS != IDLE) |=>
($stable(HADDR) && $stable(HTRANS) &&
$stable(HWRITE) && $stable(HSIZE) && $stable(HBURST));
endproperty
assert property (control_stable_during_wait)
else $error("AHB: Control signals changed during wait state");
// 4. Two-cycle error response
property two_cycle_error;
@(posedge HCLK) disable iff (!HRESETn)
(HRESP == 2'b01 && !HREADY) |=> (HRESP == 2'b01 && HREADY);
endproperty
assert property (two_cycle_error)
else $error("AHB: ERROR response not two cycles");
// 5. First transfer of burst must be NONSEQ
sequence burst_start;
(HTRANS == NONSEQ) && (HBURST != 3'b000);
endsequence
property first_transfer_nonseq;
@(posedge HCLK) disable iff (!HRESETn)
$rose(HSEL && HTRANS != IDLE) |-> (HTRANS == NONSEQ);
endproperty
assert property (first_transfer_nonseq)
else $error("AHB: First transfer must be NONSEQ");
// 6. No unknown values on active transfers
property no_x_on_active;
@(posedge HCLK) disable iff (!HRESETn)
(HTRANS inside {NONSEQ, SEQ}) |->
!$isunknown(HADDR) && !$isunknown(HWRITE) &&
!$isunknown(HSIZE) && !$isunknown(HBURST);
endproperty
assert property (no_x_on_active)
else $error("AHB: Unknown values on control signals");
endmoduleYou can write assertions in a separate file and bind them to the design. This keeps RTL code clean and makes assertions reusable.
// Assertions file: ahb_sva.sv
module ahb_sva (
input logic HCLK, HRESETn,
input logic [31:0] HADDR,
input logic [1:0] HTRANS,
// ... other signals
);
// All assertions here
property addr_aligned;
@(posedge HCLK) disable iff (!HRESETn)
(HTRANS != 2'b00) |-> (HADDR[1:0] == 2'b00);
endproperty
assert property (addr_aligned);
endmodule
// Bind file: bind_ahb.sv
bind ahb_master ahb_sva ahb_sva_inst (
.HCLK (HCLK),
.HRESETn (HRESETn),
.HADDR (HADDR),
.HTRANS (HTRANS)
// ... connect all signals
);
// Now assertions are automatically attached to ahb_master!Browse the sidebar to learn more:
Immediate assertions check conditions at a single point in simulation time (like if statements). Concurrent assertions check conditions continuously over multiple clock cycles and can express temporal relationships.
|-> is overlapping implication: if antecedent is true, consequent must be true in the same cycle. |=> is non-overlapping: consequent must be true in the next cycle.
It disables the assertion when the specified condition is true, typically used to disable checking during reset.
[*n] is consecutive repetition (signal must be true for n consecutive cycles). [->n] is goto (wait for nth occurrence). [=n] is non-consecutive (n occurrences with gaps allowed).