SVA Protocol Checkers for AXI

Catching protocol violations early with SystemVerilog Assertions

Posted by Nelson Campos on March 21, 2026

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.

Strict sampling and race-free BFMs

Verilaxi is validated with Verilator 5.048 and uses the strict SystemVerilog interpretation of AXI stability. Concurrent assertions sample the channel at the clock edge. If VALID=1 and READY=0 are sampled, no handshake occurred on that edge; the source must keep VALID asserted and hold the payload unchanged through the next edge.

The original Verilator 5.046 environment used $fell(ready) antecedent guards and || ready consequent escapes to work around observed coroutine and active-edge scheduling behaviour. Those guards explain the older checker implementation, but they also weaken the AXI rule. After moving the BFMs to race-free edge timing, Verilator 5.048 runs the strict properties without the 5.046 workarounds.

This remains true if READY becomes high on the next edge. That next edge is the eventual handshake, so VALID and the payload must still describe the stalled transfer at that sampling point. Consequently, the checker does not add !$fell(ready) to the antecedent and does not add || ready to the consequent. Either escape can hide a real protocol violation.

False failures that appear after removing those escapes usually indicate a testbench race. A procedural BFM must not change READY, VALID, or payload in the same active-region edge where the DUT and assertions sample them. Verilaxi drivers set up controls on the falling edge and count transfers only when VALID && READY is observed at the following rising edge. This makes the intended handshake unambiguous across simulators.

Waveforms and sampled interfaces

There is a related but separate source of confusion when reading waveforms in verilaxi. Some tests use helper modules such as sample_axis_if to copy one interface into another on the clock edge before dumping waveforms. These sampled interfaces are useful because they make the captured traffic cleaner to inspect, especially when the original activity is driven through virtual interfaces and class-based BFMs.

That waveform convenience does not change assertion semantics. A sampled interface is simply a registered mirror of another interface, so it may lag or clean up what you see in the wave dump. Assertions should be connected to the actual protocol interface and BFMs should establish their outputs before the active sampling edge.

So the practical debugging advice is:

  • If a waveform looks one cycle "cleaner" or more delayed than expected, check whether you are looking at a sampled interface used for observability.
  • If an assertion seems to complain even though the handshake looks legal, check whether a BFM drives READY, VALID, or payload in the same active-region edge where the DUT samples it.

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.

These checkers are designed to sit next to the task-based drivers described in Building SystemVerilog AXI VIP for Fast Bring-Up. The VIP generates realistic AXI traffic; the SVA modules continuously verify that the traffic obeys the protocol. Together they form a lightweight verification stack: procedural stimulus on one side, protocol rules on the other.

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

No READY escape is required. If this strict property fails, inspect the source or BFM for an edge-ordering race before weakening the assertion.

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 |=> $stable(tdata);
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/build.mk: 

verilator -Wall --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 use strict stability properties without $fell(ready) guards or || ready escapes and are validated with Verilator 5.048. 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.
Writing a CSR Block Using AXI-Lite for a simple register interface where AXI-Lite VALID and payload checks are immediately useful.
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.