Home › Tutorials › Assertions

SystemVerilog Assertions (SVA)

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.

What are Assertions?

Assertions are statements that describe the expected behavior of your design. They continuously monitor signals during simulation and immediately flag violations. Rather than manually checking waveforms, you let the simulator do the checking for you.

Why Use Assertions?

  • Catch bugs early - Errors are reported immediately when they occur, not when symptoms appear later
  • Self-documenting - Assertions describe design intent clearly
  • Active verification - They check behavior continuously, not just at specific test points
  • Better coverage - Assertion coverage tells you what's been checked
  • Faster debug - Know exactly which protocol rule was violated

Real Example: Without vs With Assertions

Without Assertions - Hard to Debug
// 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!
With Assertions - Immediate Detection
// Assertion fires immediately at cycle 234:
// "ERROR: FIFO overflow! write_en=1 when full=1"
// Bug found in seconds, not hours!

Types of Assertions

SystemVerilog provides two types of assertions:

1. Immediate Assertions

Checked at a single point in time, like an if statement. Used in procedural code (always blocks, tasks, functions).

Immediate Assertion Example
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
end

2. Concurrent Assertions

Checked continuously over time, can span multiple clock cycles. Used for protocol checking and temporal relationships.

Concurrent Assertion Example
// 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 in Detail

Immediate assertions have three forms:

1. Simple Assert

Simple Assert
// Basic form
assert (expression);

// With messages
assert (address[1:0] == 2'b00)
    else $error("Address must be word-aligned!");

2. Assert with Pass/Fail Actions

Assert with Actions
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");

3. Deferred Assertions (SystemVerilog 2012)

Deferred assertions handle glitches by evaluating at the end of the time step:

Deferred Assertions
// #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");

Severity Levels

Severity Functions
// $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
end

Concurrent Assertions in Detail

Concurrent assertions are the heart of SVA. They describe temporal relationships and protocols using sequences and properties.

Basic Structure

Concurrent Assertion Structure
// 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");

Common Temporal Operators

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)

Practical Assertion Examples

1. FIFO Assertions

FIFO Assertions
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);

endmodule

2. AHB Protocol Assertions

AHB Protocol Assertions
module 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");

endmodule

Binding Assertions to Design

You can write assertions in a separate file and bind them to the design. This keeps RTL code clean and makes assertions reusable.

Binding Assertions
// 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!

Topics Covered in This Section

Browse the sidebar to learn more:

  • Immediate Assertions - Simple procedural checks
  • Concurrent Assertions - Multi-cycle temporal checks
  • Sequences - Defining signal patterns
  • Properties - Combining sequences with logic
  • Temporal Operators - ##, |-> , |=>, [*], etc.
  • System Functions - $past, $rose, $fell, $stable
  • Binding - Attaching assertions to design modules
  • Coverage - Measuring assertion coverage

Common Interview Questions

  1. What is the difference between immediate and concurrent assertions?

    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.

  2. What is the difference between |-> and |=> operators?

    |-> 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.

  3. What does "disable iff" do?

    It disables the assertion when the specified condition is true, typically used to disable checking during reset.

  4. What is the difference between [*n], [->n], and [=n]?

    [*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).

Previous Home Next Immediate Assertions