AMBA AXI · Module 16

The Protocol-Checker Mindset

How to think like an AXI protocol checker — turning a spec into a catalog of things that could go wrong, classifying rules into handshake/payload-stability/ordering/structural categories, and adopting the adversarial 'what could violate this?' stance that drives every assertion, monitor, scoreboard, and coverage point.

Module 16 is about proving an AXI design correct, and it starts not with a tool but with a way of thinking. A protocol checker is the embodiment of one question asked relentlessly of every signal, every cycle: what would it mean for this to be wrong, and how would I catch it? Before writing a single SystemVerilog assertion, you need the mindset that turns the AXI specification — a document of "shall" statements — into a structured catalog of violations to watch for. This chapter teaches that stance: how to read a spec adversarially, how to classify AXI's rules into a small set of checkable categories, and how that classification becomes the blueprint for the assertions (16.2), monitors (16.3), scoreboards (16.4), and coverage (16.5) that follow. Get the mindset right and the rest of the module is mechanical; get it wrong and you'll write assertions that pass while real bugs slip through.

1. From "Shall" Statements to Watchable Violations

The AXI spec is full of normative rules — "once VALID is asserted it shall remain asserted until the handshake," "the payload shall remain stable," "responses shall be returned in order per ID." The checker mindset inverts each one: for every "shall," ask "what does the violation look like on the wire, and what assertion fires on it?" A rule you can't turn into a concrete, observable failure condition isn't yet a check — it's just prose.

Figure 1 — the checker mindset inverts every spec rule. A normative 'shall' statement is turned into its negation (the violation), then into an observable wire condition, then into a concrete check (assertion/monitor). A rule that can't be reduced to an observable failure isn't yet verifiable — the mindset's job is to make every rule watchable.

2. The Four Categories of AXI Rules

Almost every AXI rule falls into one of four categories, and knowing the categories lets you systematically enumerate what to check rather than hoping you remembered everything:

Handshake rules — the VALID/READY contract on each channel: VALID must not wait for READY; once asserted, VALID stays until the handshake; a transfer occurs only when both are high on a rising edge. Violations: VALID dropped before acceptance, VALID combinationally dependent on READY (deadlock).
Payload-stability rules — once VALID is asserted, the channel's payload (address, data, strobes, resp, last, id, …) must remain constant until the handshake completes. Violation: any payload bit changing while VALID is held and READY is low.
Ordering / transaction rules — relationships across beats and transactions: one B per write burst, WLAST/RLAST on exactly the last beat, responses in order per ID, write data follows its address, no 4 KB-crossing burst, exclusive-access semantics. Violations: wrong beat count, response reordering within an ID, illegal burst shape.
Structural / encoding rules — legal field values and combinations: reserved AxBURST encodings, AxSIZE not exceeding the bus width, aligned wrap bursts, legal AxLOCK/AxCACHE. Violation: an illegal or reserved encoding on the bus.

Figure 2 — the four categories of AXI rules. Handshake rules govern VALID/READY per channel; payload-stability rules govern signal constancy while VALID is held; ordering/transaction rules govern relationships across beats and transactions; structural/encoding rules govern legal field values. Classifying a spec into these four lets you enumerate checks systematically and know your coverage is complete by category.

3. The Adversarial Stance

A protocol checker doesn't assume good behavior — it assumes the design is trying to cheat and asks how. This adversarial framing is what separates a checker that catches bugs from one that rubber-stamps. Concretely: for each rule, imagine the cheapest way a buggy RTL could violate it and make sure a check fires. The mindset also distinguishes what is wrong from who is responsible — a checker pinpoints the violating channel, cycle, and rule, which is what makes a fired assertion immediately actionable.

Figure 3 — a payload-stability violation caught adversarially. The manager asserts AWVALID with an address; while waiting for AWREADY (the subordinate stalls), the address changes — a stability violation. The checker, watching for exactly this, flags the cycle the payload changed under a held VALID. The dashed line is the illegal change the adversarial check is designed to catch.

4. The Mindset Drives the Whole Verification Stack

The four categories and the adversarial stance aren't abstract — they map directly onto the verification components built in the rest of Module 16. Assertions encode the handshake/stability/structural rules as cycle-by-cycle checks; monitors reconstruct transactions so the ordering rules can be checked; scoreboards check data integrity and ordering against a reference; coverage confirms you actually exercised the scenarios where violations would show. The mindset is the spec; the components are the implementation.

Figure 4 — the mindset drives the verification stack. The rule catalog (four categories, adversarially derived) becomes: assertions (handshake/stability/structural, per-cycle), monitors (reconstruct transactions for ordering), scoreboards (data integrity and ordering vs. reference), and coverage (confirm the violation scenarios were exercised). Each later chapter implements one layer of what the mindset specifies.

5. Common Misconceptions

Myths to unlearn

"If the testbench runs without errors, the protocol is verified." No — absence of errors only means no check fired. If you didn't write the check (or didn't exercise the scenario), the bug passes silently. Verification is about the checks you wrote and the scenarios you covered, not a clean run.
"A protocol checker proves the design is functionally correct." It proves the design is protocol-compliant (legal AXI traffic) — not that it does the right thing. A slave that returns legal but wrong data passes the protocol checker; functional correctness needs a scoreboard against a reference (16.4).
"You can write assertions ad hoc as you think of them." Ad hoc assertions have gaps. The categorisation (handshake / stability / ordering / structural) is what makes coverage of the rule space systematic and lets you argue completeness by category rather than by memory.
"Checking VALID/READY is enough." Handshake checks are one of four categories. Payload stability, ordering/transaction rules, and structural encodings are equally part of compliance — a design can handshake perfectly while reordering responses or emitting illegal burst encodings.
"The checker tells you the design is good." A checker tells you what's wrong (and where). Silence from a checker is only as strong as the checks behind it — which is why the adversarial mindset (imagine the violation first) matters more than the tool.
"Coverage and checking are the same thing." Checks catch violations when a scenario occurs; coverage measures whether the scenario occurred. You need both — a perfect assertion never tested by the right stimulus protects nothing.

6. Debugging Insight

🔍 Debugging insight — a fired protocol assertion already localizes the bug by category

The categorisation pays off at debug time: which category fired tells you where to look:

A handshake assertion fires (VALID dropped / deadlock). Look at the channel's flow-control logic — a VALID gated by READY, or a state machine that deasserts VALID before acceptance. The fired cycle is the exact violation point.
A payload-stability assertion fires. Look for a register feeding the payload that updates while VALID is held — often a datapath that advances on the clock instead of on the handshake. The changed bit and cycle are reported.
An ordering/transaction assertion fires (wrong beat count, response reorder). Look at the engine's counters and ID tracking — WLAST/RLAST mis-timed, or a response path that doesn't preserve per-ID order. This needs the monitor's reconstructed transaction, not just one signal.
A structural/encoding assertion fires. Look at how the offending field is driven — a reserved AxBURST, an AxSIZE exceeding the bus, a misaligned wrap. Usually a constant or a miscomputed field.

Because each assertion is tied to a specific rule and category, a fired check is self-localizing: it names the channel, the cycle, the rule, and (by category) the kind of logic to suspect. This is the practical reason to write assertions from a categorised catalog rather than ad hoc — the catalog structure becomes the debug taxonomy.

7. Verification Insight

✅ Verification insight — the mindset makes completeness arguable and reuse possible

The protocol-checker mindset turns "did we check everything?" from a hope into an argument. Because every AXI rule maps to one of four categories, you can enumerate the rules per category, confirm an assertion exists for each, and argue completeness by category — handshake rules covered, stability rules covered, ordering rules covered, structural rules covered — rather than trusting memory. This is also why protocol checking is reusable: the rule catalog is a property of AXI, not of your design, so a well-built assertion set (or a standard VIP that embodies it) attaches to any AXI interface and checks compliance for free — which is exactly the leverage a VIP provides (16.8). Two disciplines make it real: (1) separate compliance from correctness — the protocol checker proves legal traffic, while a scoreboard against a reference proves the design does the right thing; conflating them leaves one or the other unchecked; and (2) pair every check with coverage — an assertion only protects you on cycles where the violating scenario is actually exercised, so coverage (16.5) must confirm those scenarios occurred (a VALID-held-with-stall must happen for the stability assertion to mean anything). The mindset's deliverable is the rule catalog: a categorised list of every compliance rule with, for each, the violation condition, the assertion that catches it, and the coverage that exercises it. That catalog is the specification the entire rest of Module 16 implements — and the thing that lets you claim, with evidence, that an interface is protocol-verified.

8. Interview Questions

9. Summary

The protocol-checker mindset is the foundation of AXI verification: it inverts every normative spec rule into an observable violation and a concrete check, and it adopts an adversarial stance — assume the design might cheat, imagine the cheapest violation, and make sure a check fires. Almost every AXI rule falls into one of four categories — handshake (the VALID/READY contract), payload stability (constancy while VALID is held), ordering/transaction (relationships across beats and transactions), and structural/encoding (legal field values) — and that classification is what lets you enumerate checks systematically and argue completeness by category rather than from memory.

The mindset's deliverable is a rule catalog: every compliance rule, with its violation condition, the assertion that catches it, and the coverage that exercises it. That catalog is the specification the rest of Module 16 implements — assertions (16.2) encode the per-cycle rules, monitors (16.3) reconstruct transactions for the ordering rules, scoreboards (16.4) check correctness against a reference, and coverage (16.5) confirms the scenarios occurred. Two disciplines are non-negotiable: separate compliance from correctness (a checker proves legal traffic, a scoreboard proves right behavior), and pair every check with coverage (an unexercised assertion protects nothing). A clean run is not verification; the checks you wrote and the scenarios you covered are. Next, we turn the handshake/stability/structural rules into concrete SystemVerilog assertions.

10. What Comes Next

You have the mindset and the rule catalog; next we encode it in executable assertions:

16.2 — AXI Assertions (SVA) (coming next) — writing the core AXI protocol assertions in SystemVerilog Assertions: the handshake, stability, and structural rules as concrete, cycle-by-cycle checks.

Previous: 15.8 — Reusable AXI RTL Templates. Related: 3.5 — Handshake Dependency & Deadlock Rules for the handshake rules to check, 6.8 — RRESP, BRESP & RLAST for response/last rules, and 10.5 — AXI4-Lite Verification Checklist for a worked compliance checklist.