SVA Protocol Checkers for AXI

A testbench that drives stimulus and checks data values is necessary but not sufficient. A DUT can produce correct output values while simultaneously violating the AXI protocol — for example, by dropping VALID between beats without a handshake, or by issuing a burst that crosses a 4KB page boundary. These violations will cause failures in a real system but may go undetected in a functional simulation unless protocol rules are explicitly checked. SystemVerilog Assertions (SVA) are the right tool for this. This post explains the four checker modules in verilaxi and how they work with Verilator.

SVA in one minute

Before diving into AXI-specific properties, it helps to decode the basic SVA syntax. A property is a statement about signal behaviour over time. In practice, most protocol checks answer questions such as: "if this happened on one clock edge, what must still be true on the next edge?" or "if this handshake occurred, what condition must hold immediately?".

property p_example;
    @(posedge clk) disable iff (!rst_n)
    antecedent |=> consequent;
endproperty

Skeleton of a clocked SVA property

In that form:

• @(posedge clk) means the property is sampled on every rising clock edge.
• disable iff (!rst_n) turns the property off during reset.
• the antecedent is the condition being watched.
• |=> means "if the antecedent is true now, the consequent must be true on the next sampled cycle".
• the consequent is the rule that must hold.

For AXI, that maps naturally onto handshake rules. A property such as

tvalid && !tready |=> tvalid;

simply says: if VALID is high and READY is low on this clock edge, then VALID must still be high on the next clock edge. In other words, once the master has offered a transfer, it must keep offering it until the handshake completes.

Another common operator is |->, which is used for same-cycle implications. In protocol checkers it is useful for statements like "if a beat is accepted with WLAST high, the internal beat counter must already be at the last beat." The key point is that SVA is not magic syntax to memorise in isolation; it is a compact way of writing temporal protocol rules that designers already describe informally.

One important caveat: Verilator post-NBA evaluation

Before showing the properties, there is one Verilator-specific behaviour worth understanding upfront, because it affects how every VALID stability property must be written.

Verilator evaluates assert property consequents in the post-NBA region — after always_ff blocks have settled — rather than in the preponed region mandated by the SystemVerilog specification. This means the checker sees signal values that have already been updated by the current clock edge. If a master correctly deasserts VALID one cycle after a handshake completes, the naive property sees valid=0 at that edge and fires a false positive — even though the behaviour is correct.

Two guards are applied consistently across all properties in verilaxi to handle this:

• || tready in the consequent — allows the master to deassert VALID if READY is high at the next cycle, meaning the handshake completed
• !$fell(tready) in the antecedent — excludes the cycle where READY transitions from 1 to 0, which can happen when a FIFO fills on the same edge as a handshake

All properties shown below include both guards. A spurious deassert — VALID going low while READY is already low — is still caught.

The four checkers

Verilaxi includes four SVA checker modules, each focused on a specific aspect of the AXI protocol:

• axis_checker.sv — AXI4-Stream: TVALID stability, payload stability, no-X checks
• axil_checker.sv — AXI4-Lite: per-channel VALID stability, payload stability, error response detection
• axi_mm_checker.sv — AXI4-Full: write and read channel rules, WLAST and RLAST alignment
• axi_4k_checker.sv — 4KB boundary: no AW or AR burst may cross a 4KB page boundary

Each checker is a standalone module instantiated inside the test, alongside the DUT. It receives the same interface signals and runs continuously throughout the simulation. A failing assertion stops the simulation immediately and reports the time, hierarchy path, and property name.

VALID stability

The AXI specification requires that once a master asserts VALID it must not deassert it until the handshake completes (READY goes high). This is the most commonly violated rule when an FSM or driver has a bug. The assertion is straightforward:

Read the property directly in AXI terms: "if the channel is stalled this cycle (VALID=1, READY=0), then the offer must still be present next cycle." That is exactly the English-language rule from the AXI specification, expressed as a one-line temporal check.

// Once TVALID is asserted it must remain high until TREADY goes high
property p_tvalid_stable;
    @(posedge clk) disable iff (!rst_n)
    tvalid && !tready |=> tvalid;
endproperty

assert property (p_tvalid_stable)
    else $error("TVALID deasserted without a handshake");

Basic TVALID stability property

In Verilator, however, this property fires a false positive at the handshake cycle — for the reason explained at the top of this post. The fix applies the two guards:

// Corrected for Verilator post-NBA evaluation
property p_tvalid_stable;
    @(posedge clk) disable iff (!rst_n)
    tvalid && !tready && !$fell(tready) |=> tvalid || tready;
endproperty

VALID stability property corrected for Verilator's post-NBA evaluation

Payload stability

While VALID is asserted and READY is low (no handshake yet), all payload signals — address, data, WLAST, burst parameters — must remain stable. A driver that updates these signals before the handshake completes is presenting incoherent data to the slave.

This is where the combination of AXI and SVA becomes especially natural. Once the handshake is stalled, the channel payload is logically frozen. The property is therefore the same shape as the VALID rule, but with $stable(...) in the consequent instead of the signal itself.

// Payload must not change while TVALID is high and TREADY is low
property p_tdata_stable;
    @(posedge clk) disable iff (!rst_n)
    tvalid && !tready && !$fell(tready) |=> $stable(tdata) || tready;
endproperty

assert property (p_tdata_stable)
    else $error("TDATA changed while TVALID high and TREADY low");

Payload stability property for AXI-Stream TDATA

WLAST alignment

For AXI4-Full write bursts, WLAST must be asserted on exactly the last beat of the burst — the beat numbered AWLEN. A DUT that asserts WLAST early (truncating the burst) or late (extending it) will confuse the interconnect. The axi_mm_checker counts W-channel beats after each AW handshake and checks that WLAST arrives exactly at beat AWLEN+1.

Here the property is paired with a small amount of supporting state. SVA is excellent at expressing time relationships, but it often works best when simple helper logic captures context such as the expected burst length. In other words, the checker is not "only assertions"; it is a small monitor plus assertions over that monitor state.

// WLAST must be asserted on beat number awlen+1 and not before
int unsigned beat_count;

always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n)
        beat_count <= 0;
    else if (wvalid && wready) begin
        if (wlast) beat_count <= 0;
        else       beat_count <= beat_count + 1;
    end
end

property p_wlast_correct;
    @(posedge clk) disable iff (!rst_n)
    wvalid && wready && wlast |-> (beat_count == captured_awlen);
endproperty

assert property (p_wlast_correct)
    else $error("WLAST asserted at beat %0d, expected beat %0d",
                beat_count, captured_awlen);

WLAST alignment check (simplified from tb/assertions/axi_mm_checker.sv)

The 4KB boundary rule

The AXI4 specification forbids a burst from crossing a 4KB address boundary. This rule exists because many interconnect fabrics map 4KB pages to different slaves; a burst crossing the boundary would require the interconnect to split it, which most implementations do not support. The rule is subtle: it depends on the burst base address, beat size, and burst length together.

The check computes the address of the last byte in the burst and verifies it falls within the same 4KB page as the first byte:

This is a good example of why protocol assertions matter even when the RTL appears straightforward. A burst can have the correct AWLEN, correct AWSIZE, and correct VALID/READY behaviour, yet still be illegal if the resulting address range crosses a page boundary. SVA lets that derived rule be checked continuously instead of relying on a human to infer it from the waveform.

// No AW burst may cross a 4KB boundary
property p_aw_no_4k_cross;
    logic [ADDR_WIDTH-1:0] last_byte_addr;
    @(posedge clk) disable iff (!rst_n)
    (awvalid && awready,
        last_byte_addr = awaddr + ((awlen + 1) << awsize) - 1)
    |->
        (awaddr[11:0] + ((awlen + 1) << awsize)) <= 12'hFFF + 1;
endproperty

assert property (p_aw_no_4k_cross)
    else $error("AW burst crosses 4KB boundary: addr=0x%0h len=%0d size=%0d",
                awaddr, awlen, awsize);

4KB boundary checker for the AW channel (from tb/assertions/axi_4k_checker.sv)

This is the check that verilaxi's S2MM and MM2S engines are specifically designed to satisfy. Both engines include a two-stage PREP pipeline that clips burst length at 4KB boundaries before issuing the AW or AR address. The assertion fires immediately if that logic has a bug.

Enabling assertions in Verilator

Assertions are compiled but silently ignored unless the --assert flag is passed to Verilator. Without it, all assert property and cover property statements are no-ops. In verilaxi this flag is always enabled in mk/config.mk:

VERILATOR_FLAGS += --assert

When an assertion fires, Verilator prints the simulation time, the full hierarchical path of the failing property, and the message from the else $error(...) clause, then terminates the simulation. The FST waveform written up to that point can be opened in Surfer or GTKWave to inspect the signals at and before the failure time.

Summary

SVA protocol checkers are a lightweight and highly effective addition to any AXI testbench. VALID stability and payload stability catch the most common driver and FSM bugs. WLAST and RLAST alignment checkers catch burst-count errors. The 4KB boundary checker is essential for any engine that issues multi-beat bursts near page boundaries. All four checks in verilaxi are Verilator-compatible, with the post-NBA sampling caveat handled by the !$fell(tready) guard and the || tready consequent. The full checker source is available in verilaxi.

Read next:
Building SystemVerilog AXI VIP for Fast Bring-Up for the task-based environment that these assertions watch.
AXI DMA — Moving Data Without the CPU for a concrete example where WLAST and 4KB checks matter in practice.
Implementation pointers in verilaxi: tb/assertions/axis_checker.sv, tb/assertions/axil_checker.sv, tb/assertions/axi_mm_checker.sv, and tb/assertions/axi_4k_checker.sv.

References:
[1] ARM. AMBA AXI and ACE Protocol Specification. 2011
[2] IEEE Std 1800-2017. SystemVerilog Language Reference Manual.
[3] Building SystemVerilog AXI VIP for Fast Bring-Up — sistenix.com

---

Also available in GitHub.