AMBA AXI · Module 16

AXI Assertions (SVA)

Write the core AXI protocol assertions in SystemVerilog Assertions — the handshake rules (VALID stable until READY, VALID not waiting on READY), payload stability ($stable while VALID held), and structural/encoding checks — with the concurrent-assertion idioms, disable-on-reset, and binding pattern that make them reusable across any AXI interface.

The protocol-checker mindset (16.1) produced a categorised rule catalog; this chapter turns the per-cycle rules into executable SystemVerilog Assertions (SVA). We'll write the core checks for the two categories that are naturally cycle-by-cycle — handshake and payload stability — plus the structural/encoding checks, using the concurrent-assertion idioms (property, |->, $stable, $rose, disable iff) that every AXI assertion set relies on. (The ordering/transaction rules that span beats are better handled by monitors and scoreboards in 16.3–16.4.) The goal is a set of assertions you can bind onto any AXI interface and trust — the executable form of the rule catalog, and the engine inside every protocol VIP.

1. The Anatomy of an AXI Assertion

A concurrent SVA assertion has a fixed shape: a clocking event, a disable condition (almost always reset), an antecedent (the trigger), and a consequent (what must then hold). Nearly every AXI rule fits the pattern "when this is observed, that must be true on the relevant cycles."

Azvya Education Pvt. Ltd.VLSI Mentor

Snippet

// Template: every AXI assertion shares this skeleton
property p_example;
  @(posedge aclk) disable iff (!aresetn)
  antecedent |-> consequent;          // |-> same cycle, |=> next cycle
endproperty
a_example: assert property (p_example)
  else $error("AXI violation: <rule> at %0t", $time);

The disable iff (!aresetn) is essential: during reset the bus is not expected to be compliant, so every AXI assertion is disabled while reset is asserted. The |-> (overlapping) and |=> (non-overlapping) implication operators express "in the same cycle" vs. "starting next cycle" — the choice matters for getting the timing of a rule exactly right.

Figure 1 — the anatomy of a concurrent AXI assertion. A clocking event (posedge aclk) samples the signals; disable iff (!aresetn) suppresses the check during reset; the antecedent is the trigger condition; the implication operator (|-> same cycle, |=> next cycle) connects it to the consequent that must hold. Every AXI protocol assertion is an instance of this skeleton.

2. Handshake Assertions

The handshake category produces three canonical checks per channel. Shown for the write-address (AW) channel; the same three apply to W, B, AR, R by signal substitution.

Azvya Education Pvt. Ltd.VLSI Mentor

Snippet

// (H1) VALID must remain asserted, with no change, until READY accepts it.
property p_awvalid_stable;
  @(posedge aclk) disable iff (!aresetn)
  (awvalid && !awready) |=> awvalid;
endproperty
a_awvalid_stable: assert property (p_awvalid_stable)
  else $error("AWVALID deasserted before AWREADY");
 
// (H2) Once asserted, VALID is held — equivalently it may only fall the cycle
//      after a completed handshake (this is the dual of H1).
 
// (H3) VALID must not depend combinationally on READY (no deadlock).
//      Checked structurally / formally: prove awvalid has no comb. path from
//      awready. In simulation, a liveness check guards against the hang:
property p_aw_progress;       // an asserted request is eventually accepted
  @(posedge aclk) disable iff (!aresetn)
  awvalid |-> s_eventually awready;
endproperty
a_aw_progress: assert property (p_aw_progress)
  else $error("AWVALID never accepted — possible deadlock");

H1 (stability of VALID) is the everyday workhorse; the liveness check (H3) guards the deadlock rule that 16.1 flagged as fatal. Note H3's combinational-independence is ideally proven structurally/formally (no logic path awready → awvalid), with the liveness assertion as the simulation backstop.

Figure 2 — the per-channel handshake assertion trio. H1: VALID, once asserted, holds (and its payload is stable) until READY. H2: the dual — VALID only deasserts the cycle after acceptance. H3: VALID is independent of READY (no combinational path) — proven formally, with a liveness/eventually-accepted assertion as the simulation backstop against deadlock. Applied to all five channels by signal substitution.

3. Payload-Stability Assertions

The stability category checks that every payload field stays constant while its VALID is held and not yet accepted — the $stable built-in is exactly the tool. One assertion per payload field per channel (often grouped):

Azvya Education Pvt. Ltd.VLSI Mentor

Snippet

// (S1) All AW payload fields stable while AWVALID held and not yet accepted.
property p_aw_payload_stable;
  @(posedge aclk) disable iff (!aresetn)
  (awvalid && !awready) |=>
      $stable(awaddr) && $stable(awlen)  && $stable(awsize) &&
      $stable(awburst)&& $stable(awid)   && $stable(awprot) &&
      $stable(awcache)&& $stable(awlock);
endproperty
a_aw_payload_stable: assert property (p_aw_payload_stable)
  else $error("AW payload changed while AWVALID held");
 
// (S2) W payload stable while WVALID held.
property p_w_payload_stable;
  @(posedge aclk) disable iff (!aresetn)
  (wvalid && !wready) |=> $stable(wdata) && $stable(wstrb) && $stable(wlast);
endproperty
a_w_payload_stable: assert property (p_w_payload_stable)
  else $error("W payload changed while WVALID held");
 
// (S3) Read-data payload stable while RVALID held.
property p_r_payload_stable;
  @(posedge aclk) disable iff (!aresetn)
  (rvalid && !rready) |=> $stable(rdata) && $stable(rresp) &&
                          $stable(rlast) && $stable(rid);
endproperty
a_r_payload_stable: assert property (p_r_payload_stable)
  else $error("R payload changed while RVALID held");

$stable(x) is true when x has the same value as the previous clock — so "VALID held last cycle ⇒ payload unchanged this cycle" exactly encodes the stability rule. The |=> (next-cycle) form is correct here because $stable compares against the prior sample.

4. Structural Assertions and Reset Behavior

The structural/encoding category checks legal field values and combinations — immediate, single-cycle conditions on the payload (only meaningful when VALID). Plus a few reset-behavior checks that do apply during/after reset:

Azvya Education Pvt. Ltd.VLSI Mentor

Snippet

// (E1) Burst type is never the reserved encoding (2'b11).
property p_awburst_legal;
  @(posedge aclk) disable iff (!aresetn)
  awvalid |-> (awburst != 2'b11);
endproperty
a_awburst_legal: assert property (p_awburst_legal)
  else $error("Reserved AWBURST encoding");
 
// (E2) Transfer size never exceeds the data bus width.
property p_awsize_legal;
  @(posedge aclk) disable iff (!aresetn)
  awvalid |-> ((1 << awsize) <= (DATA_W/8));
endproperty
a_awsize_legal: assert property (p_awsize_legal)
  else $error("AWSIZE exceeds bus width");
 
// (E3) WRAP bursts have a legal length (2, 4, 8, or 16 beats).
property p_wrap_len_legal;
  @(posedge aclk) disable iff (!aresetn)
  (awvalid && awburst == 2'b10) |-> (awlen inside {1, 3, 7, 15});
endproperty
a_wrap_len_legal: assert property (p_wrap_len_legal)
  else $error("Illegal WRAP burst length");
 
// (R1) RESET behavior: all VALIDs must be low during reset.
property p_reset_valids_low;
  @(posedge aclk) (!aresetn) |-> (!awvalid && !wvalid && !arvalid
                                  && !bvalid && !rvalid);
endproperty
a_reset_valids_low: assert property (p_reset_valids_low)
  else $error("A VALID was high during reset");

Note R1 is not disabled on reset — it specifically checks the reset behavior (all VALIDs low), so it must be active exactly when reset is asserted.

When a structural or handshake assertion fires, the failure is pinned to a cycle and a signal, as the waveform shows:

Payload-stability assertion firing

7 cycles

Figure 3 — an assertion firing on a stability violation. AWVALID is asserted with AWADDR=A while AWREADY stays low (subordinate stalling). On the next cycle AWADDR changes to B with AWVALID still held — the p_aw_payload_stable assertion evaluates $stable(awaddr) as false and fires, marking the exact cycle and signal. The assert-fail marker is the actionable output the checker produces.

The whole set is deployed and trusted via one pattern: write the assertions once in a checker module, bind it to every AXI interface, then prove the set is sound (inject violations → each fires) and non-vacuous (antecedent coverage):

Figure 4 — deploying and self-verifying the assertion set. The catalog-derived properties live in one checker module, bound (bind) to every AXI interface without editing the RTL. The set is then verified itself: injected violations confirm each assertion fires (soundness), and cover property on each antecedent confirms it is actually exercised (non-vacuity). The result is a reusable, trusted protocol checker — the engine inside an assertion VIP.

5. Common Misconceptions

Myths to unlearn

"Assertions don't need disable iff (!aresetn)." They do — during reset the bus isn't expected to be compliant, so almost every AXI assertion must be disabled while reset is asserted. Forgetting it produces a storm of false failures at every reset.
"|-> and |=> are interchangeable." No — |-> checks the consequent in the same cycle as the antecedent; |=> checks it starting the next cycle. Stability rules (which use $stable, a comparison to the prior sample) need |=>; a same-cycle structural check needs |->. Using the wrong one shifts the check by a cycle and either misses violations or fires falsely.
"$stable checks the current cycle." $stable(x) compares x to its value at the previous clock — it's inherently a two-cycle relationship, which is why it pairs with |=> ("VALID was held last cycle ⇒ payload unchanged now").
"VALID-independent-of-READY can be checked with a simple assertion." The combinational-independence rule is a structural property (no logic path), best proven formally; a concurrent assertion can only add a liveness backstop ("eventually accepted") that catches the resulting hang, not the combinational path itself.
"Assertions go inside the RTL module." Reusable AXI assertions live in a separate checker module bound to the interface (bind), so they attach to any instance without editing the design and can be reused across projects — the same pattern a VIP uses.
"More assertions is always better." Redundant or mis-specified assertions add noise and false fails. The value is a complete, correct set derived from the categorised catalog — one good assertion per rule — not a large pile of overlapping ones.

6. Debugging Insight

🔍 Debugging insight — read the fired assertion's category, cycle, and signal

A fired SVA assertion is highly localized; read it methodically:

a_*valid_stable fired. A VALID dropped before its READY. Look at the channel's flow-control FSM — it deasserted VALID without a completed handshake. The $error time-stamps the exact cycle.
a_*_payload_stable fired. A payload field changed while VALID was held. The $stable that failed names the field; look at the register driving it — it's updating on the clock instead of on the handshake.
a_*_progress (liveness) fired. A request was never accepted — a hang/deadlock, often VALID gated by READY or a downstream that never asserts READY. Check the dependency the mindset chapter warned about.
a_*burst_legal / a_*size_legal / a_wrap_len_legal fired. An illegal encoding. The assertion names the field; look at the constant or computation driving it (a reserved BURST, an oversized SIZE, a non-power-of-two WRAP length).
a_reset_valids_low fired. A VALID was high during reset — the reset isn't clearing the channel's valid register. Check the reset path on that flop.
False fails at reset. A missing disable iff (!aresetn) — the assertion is evaluating during reset when it shouldn't.

Because each assertion encodes one catalog rule, the assertion name itself tells you the category and the rule, the $error gives the cycle, and the failing sub-expression (e.g. which $stable) gives the signal — debugging is reading the failure, not hunting for it.

7. Verification Insight

✅ Verification insight — bind a complete, reusable assertion set and verify the assertions themselves

The durable way to deploy AXI assertions is as a bound checker module: write the property/assert set once in a module with the AXI signals as ports, and bind it to every AXI interface in the design. This attaches the full catalog to any instance without touching the RTL, makes the set reusable across projects, and is exactly how commercial AXI assertion VIP is packaged. Three disciplines make the set trustworthy: (1) Completeness from the catalog — derive one assertion per rule per channel from the categorised catalog (16.1), so you can argue coverage by category (handshake/stability/structural) rather than by memory; the ordering/transaction rules that span beats are delegated to monitors/scoreboards (16.3–16.4), not forced into per-cycle SVA. (2) Verify the assertions themselves — an assertion that never fires might be correct or might be mis-written so it can't fail; inject known violations (deliberately drop a VALID, change a payload mid-handshake, emit a reserved BURST) and confirm each assertion fires, and use coverage on the antecedents (cover property) to confirm each assertion is actually being exercised (a VALID-held-with-stall must occur for the stability check to mean anything). (3) Formal where appropriate — the combinational-independence (VALID ⊥ READY) and many structural properties are better proven with formal property checking than sampled in simulation; concurrent assertions provide the simulation backstop. The combination — a complete catalog-derived set, bound for reuse, self-tested with injected violations and antecedent coverage, and backed by formal for the structural/liveness rules — is what turns "we have assertions" into "the interface is assertion-verified." This bound checker is also the natural seam-checker for the composed subsystems of 15.8 and the foundation the monitor (16.3) builds on.

8. Interview Questions

9. Summary

AXI assertions encode the per-cycle rules of the catalog as SystemVerilog Assertions. Every concurrent assertion shares one skeleton — @(posedge aclk) disable iff (!aresetn) antecedent |-> / |=> consequent — where disable iff (!aresetn) suppresses checks during reset and the implication operator selects same-cycle (|->) vs. next-cycle (|=>) timing. The handshake category yields, per channel, the VALID-held-until-READY stability check (the workhorse), its deassert-timing dual, and a liveness backstop for the deadlock rule (with combinational independence proven formally). The payload-stability category uses (valid && !ready) |=> $stable(field) for every payload field — $stable comparing to the prior sample is the exact tool. The structural/encoding category uses same-cycle |-> checks gated on VALID for legal BURST/SIZE/WRAP-length and reserved encodings, plus a reset-behavior check (all VALIDs low) that deliberately stays active during reset.

The cross-beat ordering/transaction rules are not forced into per-cycle SVA — they're delegated to monitors and scoreboards (16.3–16.4) that hold transaction state. Assertions are deployed as a bound checker module (bind) so they attach to any interface without editing RTL and are reusable as VIP. Crucially, the assertion set must itself be verified — injected violations confirm each fires (soundness), antecedent coverage confirms each is exercised (non-vacuity), the catalog mapping confirms completeness, and formal proves the structural/liveness subset. Next, we build the passive monitor that reconstructs transactions so the stateful ordering rules can be checked.

10. What Comes Next

You can now check the signal-local rules; next we reconstruct transactions to check the stateful ones:

16.3 — AXI Monitors (coming next) — a passive monitor that observes the bus and reconstructs complete transactions, the bridge from per-cycle assertions to transaction-level checking.

Previous: 16.1 — The Protocol-Checker Mindset. Related: 3.5 — Handshake Dependency & Deadlock Rules for the handshake rules these assertions encode, 7.4 — WRAP Bursts for the legal WRAP lengths, and 6.8 — RRESP, BRESP & RLAST for the response/last rules.