SystemVerilog Assertions (SVA) — Complete Beginner Guide

Introduction to Assertions

Assertions are statements used to validate the behavior of a design during simulation.
They help catch protocol violations, timing errors, and unexpected signal interactions early in the verification cycle.

In simple terms —

“Assertions are design checkers that continuously monitor whether design behavior meets the expected protocol.”

Why Assertions Are Important

Assertions improve:

• Debug efficiency — detect bugs close to the source.
• Verification completeness — ensure all timing and handshake rules are met.
• Reusability — can be reused across testbenches or integrated in RTL.
• Formal verification — assertions become constraints or properties.

Types of Assertions

(a) Immediate Assertions

Evaluated instantly when simulation executes that line.
Used in procedural blocks like always or initial.

(b) Concurrent Assertions

Evaluated over time, based on clock events.
Used to check temporal behaviors like request → acknowledge relationship.

Immediate Assertion Example

module immediate_assertion;
  bit clk, data;

  initial begin
    data = 1;
    assert (data == 1)
      $display("PASS: Data is 1");
    else
      $error("FAIL: Data is not 1");
  end
endmodule

Output:

PASS: Data is 1

Immediate assertions work just like runtime “if-checks”, but they are more powerful for verification intent.

Concurrent Assertions Overview

Concurrent assertions check temporal relationships (events over multiple clock cycles).
They are declared using:

• sequence
• property
• assert property

Example structure:

property p_example;
  @(posedge clk) req |-> ##1 ack;
endproperty

assert property (p_example)
  else $error("Request not followed by ack in next cycle");

This checks that if req occurs, then ack must occur 1 cycle later.

Sequences and Properties

Sequence

Defines a pattern of signal events.

sequence seq_req_ack;
  req ##1 ack;
endsequence

Property

Wraps the sequence with verification intent.

property p_req_ack;
  @(posedge clk) seq_req_ack;
endproperty

assert property(p_req_ack);

Implication Operators

Example:

property overlapped;
  @(posedge clk) a |-> b;
endproperty

property non_overlapped;
  @(posedge clk) a |=> b;
endproperty

Disable Condition (disable iff)

Used to turn off assertions during reset or invalid states.

property p_req_ack_disable;
  @(posedge clk) disable iff (!rst_n)
  req |-> ##1 ack;
endproperty

assert property (p_req_ack_disable);

During reset (rst_n = 0), the assertion is disabled.

Repetition Operators

Example:

sequence s_three_highs;
  sig[*3];
endsequence

Assert, Assume, and Cover Properties

Example:

cover property (@(posedge clk) req |-> ##1 ack);

Complete Assertion Example

module req_ack_assertion;
  bit clk, rst_n, req, ack;

  // Clock
  always #5 clk = ~clk;

  // DUT behavior simulation
  initial begin
    clk = 0; rst_n = 0; req = 0; ack = 0;
    #10 rst_n = 1;
    #10 req = 1;  // Request
    #10 req = 0; ack = 1;  // Ack one cycle later
    #10 ack = 0;
    #20 $finish;
  end

  // Property: Ack should come 1 cycle after Req
  property p_req_ack;
    @(posedge clk) disable iff (!rst_n)
    req |=> ack;
  endproperty

  assert property(p_req_ack)
    else $error("ACK not received after REQ");
endmodule

Simulation Log Output

# PASS: All assertions successful
# Simulation completed without errors

If ack fails to come next cycle, you’d see:

# ** Error: ACK not received after REQ