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.

Region	What happens	Why it matters here
Preponed	Assertion sampling point defined by the SystemVerilog language model	The ideal place to observe handshake intent before sequential updates react to the same edge
Active	Procedural blocks and combinational logic evaluate using values visible at the clock edge	This is where an AXI handshake is conceptually decided from VALID && READY
NBA	Non-blocking assignments (<=) from always_ff take effect	FIFO full flags, counters, and registered READY signals may update because the beat was just accepted
Post-NBA	The design is observed after those sequential updates have settled	A checker can see TREADY=0 on the same edge where the transfer was actually accepted

Table (1): Simulation regions relevant to the Verilator assertion caveat

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.

It helps to picture one clock edge as a sequence of simulation regions rather than a single instant. In the active region, the current values of VALID and READY determine whether a handshake happened. In the non-blocking assignment (NBA) region, the flops update: FIFOs may become full, internal state advances, and READY may drop as a consequence of the just-accepted beat. In the post-NBA observation point, the checker sees those updated values. So a transfer can legally complete in the active region, yet by the time the assertion samples the same edge, READY already looks low because the design has reacted to that transfer.

For this discussion, the most useful mental model is not the full scheduler diagram but a short sequence of steps:

1. Preponed — concurrent assertions conceptually sample signals for this time slot before design updates react to the edge.
2. Active — procedural code runs; blocking assignments take effect immediately; non-blocking assignments are evaluated and scheduled; an AXI handshake is logically determined from the values visible at the edge.
3. NBA — updates from <= take effect; FIFO full flags, counters, and registered READY signals may change because a beat was just accepted.
4. Observed / post-NBA view — the checker sees the design after those sequential updates have landed.

That distinction between "what happened at the edge" and "what the design looks like after reacting to the edge" is the whole heart of the caveat. Assertions want to reason about the first view. In this Verilator-specific corner case, the checker effectively sees more of the second view.

That is exactly the corner case in the verilaxi stream checker. Imagine a FIFO that was not full before the edge, so the final free slot is accepted with TVALID=1 and TREADY=1. The handshake is therefore valid. Then the FIFO full flag updates in the NBA region, which drives TREADY low. A post-NBA checker now sees TVALID=1 and TREADY=0 on that same edge and may incorrectly conclude that the channel was stalled, even though the beat was just accepted.

Step	Signal view	Interpretation
At the clock edge	TVALID=1, TREADY=1	The transfer is accepted
After NBA updates	FIFO becomes full, TREADY drops to 0	The design reacts to the accepted beat
Checker sees the edge	TVALID=1, TREADY=0	A naive stalled-channel property may misclassify the edge
Next cycle	The master may legally deassert TVALID	The beat was already consumed on the previous edge

Table (2): Why a completed handshake can look like a stall to a post-NBA observer

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.

In other words, the fix is not "turn the rule off when Verilator gets confused." The fix is to ask a slightly more precise question: was the channel truly stalled for a whole cycle, or did READY only appear low because the design consumed a beat and updated its state immediately afterwards? The !$fell(tready) term removes that ambiguous edge, and the || tready term allows VALID or payload to change on the next cycle if the previous cycle actually completed a handshake.

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 is not the same issue as the post-NBA assertion caveat. 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. The assertion caveat, by contrast, is about which simulation region the checker observes for the same clock edge. Both affect what a human sees during debug, but only the latter changes whether a naive SVA can produce a false positive.

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, think about preponed versus post-NBA observation of the same edge.

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

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