SystemVerilog Assertions (SVA): A Practical Guide

An assertion is a small, executable statement of something that must always be true about your design. When the design breaks the rule, the assertion fires and points straight at the cycle and signal that went wrong. SystemVerilog assertions (SVA) turn the invariants you already have in your head (“we never write a full FIFO”, “every request is eventually acknowledged”) into checks the simulator enforces on every run. This guide builds the whole topic from first principles with code you can run yourself.

The two families: immediate vs concurrent

Every assertion in SystemVerilog belongs to one of two families, and the single most common beginner mistake is mixing them up. The difference is when the condition is evaluated.

Immediate assertions are just procedural if statements with a built-in failure report. Concurrent assertions describe behaviour across clock cycles and are the reason SVA exists as a language. We start with immediate, because it is the family you can run in any simulator today.

Immediate assertions: checking logic right now

The form is assert (expression) pass_block else fail_block;. If the expression is true the optional pass block runs; if false, the else block runs (typically $error). Here is a self-contained adder check. The testbench module is named tb, drives a few vectors, and asserts the sum after each.

// ex1_immediate.sv  --  immediate assertions check logic right now
module tb;
  logic [3:0] a, b;
  logic [4:0] sum;

  // A tiny combinational "DUT": a 4-bit adder
  assign sum = a + b;

  initial begin
    // Drive a few vectors and check each result immediately.
    a = 4'd3;  b = 4'd4;  #1;
    assert (sum == 5'd7)
      else $error("add failed: %0d + %0d = %0d", a, b, sum);

    a = 4'd15; b = 4'd1;  #1;
    assert (sum == 5'd16)   // carry out into bit 4
      $display("PASS: 15 + 1 = %0d", sum);   // pass action block is optional

    a = 4'd9;  b = 4'd9;  #1;
    assert (sum == 5'd18)
      else $error("add failed: %0d + %0d = %0d", a, b, sum);

    $display("All immediate assertions passed.");
    $finish;
  end
endmodule

PASS: 15 + 1 = 16
All immediate assertions passed.
/var/folders/l0/gs5hnkm56g54bmxg32r6nnwr0000gn/T/tmpekfwa7zf/ex1_immediate.sv:24: $finish called at 3 (1s)

Two things to notice. First, the pass and fail blocks are both optional – the middle assertion uses only a pass block, the others only an else. Second, because this is procedural, each assert sees the value of sum at the exact moment it executes, after the #1 lets the combinational result settle.

Immediate assertions across clock cycles

Immediate assertions are not limited to combinational checks. Placed inside a clocked loop, they become a classic self-checking testbench: run a reference model alongside the DUT and assert they agree every cycle. Below, a modulo-16 counter is compared against an independent reference counter.

// ex2_counter.sv  --  immediate assertions inside a clocked checker
module tb;
  logic clk = 0, rst_n;
  logic [3:0] count;

  always #5 clk = ~clk;   // 10 ns clock

  // DUT: a modulo-16 up counter with active-low reset
  always_ff @(posedge clk or negedge rst_n)
    if (!rst_n) count <= 4'd0;
    else        count <= count + 4'd1;

  // Reference model kept in the testbench
  logic [3:0] expect_count;
  always_ff @(posedge clk or negedge rst_n)
    if (!rst_n) expect_count <= 4'd0;
    else        expect_count <= expect_count + 4'd1;

  initial begin
    rst_n = 0;
    repeat (2) @(posedge clk);
    rst_n = 1;

    // Check the invariant once per cycle, just after the clock edge settles.
    repeat (20) begin
      @(posedge clk);
      #1;  // let non-blocking updates settle before sampling
      assert (count == expect_count)
        else $error("mismatch @%0t: count=%0d expected=%0d",
                    $time, count, expect_count);
    end

    $display("Counter matched reference for 20 cycles. count=%0d", count);
    $finish;
  end
endmodule

Counter matched reference for 20 cycles. count=4
/var/folders/l0/gs5hnkm56g54bmxg32r6nnwr0000gn/T/tmplrqt3j6x/ex2_counter.sv:34: $finish called at 216 (1s)

The #1 after the edge matters: non-blocking assignments (<=) update in the NBA region, after the clock edge, so sampling immediately at the edge would read stale values. Concurrent assertions solve this sampling problem for you automatically – which is exactly where we are headed.

Implication, by hand first

Many design rules have an “if-then” shape: if some condition holds, then something else must be true. A handshake rule is typical: whenever ack is high, req must also be high. You can express this with an ordinary if wrapped around an immediate assertion, which makes the idea concrete before we meet the SVA operator for it.

// ex3_handshake.sv  --  an "if-then" invariant, the idea behind |->
module tb;
  logic clk = 0;
  logic req, ack;

  always #5 clk = ~clk;

  // Stimulus: ack is only ever raised while req is high (legal protocol).
  initial begin
    req = 0; ack = 0;
    for (int i = 0; i < 12; i++) begin
      @(negedge clk);
      req = $urandom_range(0, 1);
      ack = req ? $urandom_range(0, 1) : 1'b0;  // ack implies req
    end
  end

  // Checker: sample after each rising edge and assert the implication by hand.
  int checks = 0;
  initial begin
    repeat (12) begin
      @(posedge clk);
      #1;
      // "ack high -> req high": only meaningful when ack is high.
      if (ack)
        assert (req)
          else $error("protocol violation @%0t: ack without req", $time);
      checks++;
    end
    $display("Handshake invariant held on %0d sampled cycles.", checks);
    $finish;
  end
endmodule

Handshake invariant held on 12 sampled cycles.
/var/folders/l0/gs5hnkm56g54bmxg32r6nnwr0000gn/T/tmpw5ijf1r0/ex3_handshake.sv:31: $finish called at 116 (1s)

Notice the structure: when ack is low the rule is vacuously satisfied, so we only assert when ack is high. That “antecedent gates the consequent” pattern is precisely what the concurrent implication operators give you natively, with far less boilerplate and with correct cross-cycle timing.

Concurrent assertions: property and sequence

Concurrent assertions are written as assert property (...) and are built from two reusable pieces:

• Sequence – a pattern of events over time, e.g. “req this cycle, then !req the next”. Delays between cycles are written with ##n (fixed) or ##[m:n] (a window).
• Property – a statement built from sequences and operators (including implication) that is true or false. You assert, assume, or cover a property.

The two implication operators are the heart of temporal checking:

• |-> overlapping: when the antecedent matches, the consequent is checked on the same cycle.
• |=> non-overlapping: the consequent is checked on the next cycle. It is exact shorthand for |-> ##1.

The following checker is standard IEEE 1800 SVA. It is shown as a reference (it needs a driven clock and a simulator run with assertions enabled), not as a runnable snippet here.

// req_ack.sv  --  concurrent SVA (needs a clock; run in a full simulator)
module req_ack_sva (input logic clk, req, ack);
  // Named property: once req is high, ack must follow within 1 to 3 cycles.
  property p_ack_follows;
    @(posedge clk) req |-> ##[1:3] ack;
  endproperty

  // |->  overlapping: consequent is checked on the SAME cycle req holds.
  // |=>  non-overlapping: shorthand for  |-> ##1  (checked NEXT cycle).
  a_ack_follows: assert property (p_ack_follows)
    else $error("ack did not follow req");

  // A sequence names a temporal pattern you can reuse and compose.
  sequence s_single_pulse;
    req ##1 !req;      // high this cycle, low the next
  endsequence
  a_pulse: assert property (@(posedge clk) $rose(req) |=> s_single_pulse);
endmodule

Read req |-> ##[1:3] ack as: on any cycle where req is sampled high, ack must be high on at least one of the next one-to-three cycles. The label before each assertion (a_ack_follows:) names it in reports and waveforms – always label your assertions.

Sampled-value functions: $rose, $fell, $stable, $past

Concurrent assertions sample signals in the preponed region, just before the clock edge, so they never see glitches or mid-cycle values. Four functions let you talk about change over time using those clean samples:

• $rose(x) – true when x was 0 last cycle and 1 now (a rising edge).
• $fell(x) – true on a 1-to-0 edge.
• $stable(x) – true when x is unchanged since the previous cycle.
• $past(x) – the value x held one cycle ago (optionally $past(x, n) for n cycles back).

// sampled.sv  --  sampled-value functions in concurrent SVA
module edges (input logic clk, rst_n, load, input logic [7:0] data, q);
  default clocking cb @(posedge clk); endclocking
  default disable iff (!rst_n);

  // $rose(x): x was 0 last cycle and 1 now.   $fell(x): 1 to 0 edge.
  // $stable(x): value unchanged since last cycle.
  // $past(x):  the value x held one cycle ago.

  // If we did NOT load this cycle, the register must hold its value.
  a_hold: assert property (!load |=> $stable(q));

  // One cycle after a load, q must equal the data sampled at the load.
  a_load: assert property (load |=> q == $past(data));
endmodule

Two conveniences appear here. default clocking sets one clock for every property in the module so you need not repeat @(posedge clk). default disable iff (!rst_n) switches off all checks during reset, since invariants should not be enforced while the design is being initialised.

Binding assertions to a design

You rarely want assertion code tangled inside synthesizable RTL. The bind construct keeps checkers in a separate module and wires them into the DUT from the outside – the design source is never edited, so RTL and synthesis stay clean while verification gets full visibility.

// bind_example.sv  --  attach a checker to a DUT without editing the DUT
module fifo (input logic clk, wr, rd, full, empty);
  // ... real FIFO logic lives here ...
endmodule

// A standalone checker module with the same ports we want to watch:
module fifo_sva (input logic clk, wr, rd, full, empty);
  // Rule: never present a write while the FIFO is full unless a read drains it.
  a_no_overflow: assert property (@(posedge clk) (full && wr) |-> rd)
    else $error("overflow: wrote while full");
endmodule

// 'bind' wires the checker into every fifo instance. The DUT source is
// never touched, so synthesis and RTL stay clean.
bind fifo fifo_sva u_chk (.clk(clk), .wr(wr), .rd(rd),
                          .full(full), .empty(empty));

One bind line attaches the checker to every instance of fifo in the whole design at once. This is how teams layer protocol checkers (AXI, APB, custom handshakes) onto designs they are not allowed to modify.

How to choose

Reach for immediate assertions for testbench self-checking and combinational sanity checks where you already have the values in hand. Reach for concurrent assertions for anything that spans clock cycles – handshakes, pipeline latency, “eventually” and “within N cycles” rules – and bind them in from the side so your RTL stays pure. Start every assertion with a label and a clear $error message; a good message turns a failing run into an instant diagnosis.