When AWVALID and AWREADY meet on a rising edge, the address handshake is complete, but verifying every legal AXI4 handshake sequence is far less bounded than the basic rule suggests. VALID must precede READY, yet transaction legality also depends on ordering, response relationships, ID sequencing, and burst lengths. Manually building a complete set for even one AXI slave port quickly reaches dozens of assertions. The invalid state space is larger than the handful of obvious handshake checks, especially when multiple transactions remain outstanding.
The challenge is not reading the AXI specification. Converting its prose into correct SystemVerilog Assertion (SVA) syntax takes time and invites subtle defects: an incorrect temporal operator, a delay shifted by one cycle, or a scope that overlooks the condition under test. A defective assertion can be more harmful than no assertion because it suggests verification is complete when it is not.
AXI Assertion Coverage
Before looking at BigEndian's synthesis method, define what a complete AXI assertion set must check. A partial collection is often mistaken for full protocol coverage. The categories most frequently omitted deserve explicit attention.
Write channel ordering: once AWVALID is asserted, the address handshake must finish before or alongside the write data handshake for the associated IDs. With multiple outstanding transactions, this rule must be tracked independently for each ID. A global ordering check can pass even when a design violates ordering for a particular ID, provided the aggregate channel activity happens to satisfy the broader condition.
Response completeness: each accepted address transaction, where AWVALID and AWREADY are both high on a clock edge, must eventually produce a matching write response, with BVALID and the corresponding BID. This needs a concurrent sequence property that can cover an arbitrary cycle span, not a simple SVA immediate assertion. Bounds require care: a short limit rejects valid long-latency responses, while a loose limit can fail to expose deadlock.
Burst consistency: AWLEN establishes how many data beats the write channel must provide for that transaction. The assertion tracks that length per transaction ID, counts matching data beats, and compares the result on the final beat marked by WLAST.
STROBE validity: on a wide data bus, a narrow transaction's WSTRB must agree with AWSIZE and the beat's position in the burst. Hand coding this check is uncommon because aligned address and beat offset calculations expand into a large truth table.
Generating AXI Assertions from Protocol States
BigEndian starts AXI assertion synthesis with a protocol state machine derived from the AXI specification. It does not parse the specification as free-form prose. Instead, valid and invalid state sequences are represented structurally, then captured in reusable templates that can be instantiated across AXI interfaces in the design.
The synthesis step combines that state machine with the interface definition, including data width, ID width, outstanding transaction count, and master or slave role. It emits SVA properties parameterized for those dimensions. Data width shapes strobe checks, while ID width and outstanding count determine the per-ID tracking registers for ordering and response completeness.
Parameterization is the main advantage over hand-written checks. If an SoC adds an AXI interface that changes only its data width or ID count, engineers otherwise have to inspect every dependent assertion. Regeneration updates the synthesized properties for the new interface parameters.
The output also contains bind statements that connect the assertion module to the interface without changing the DUT. Although binding is standard in assertion-based verification, hierarchy and clock-domain mistakes are common, such as selecting the wrong scope or clocking event. Parameterized generation resolves those details consistently.
Synthesized Assertion Limits
Assertions derived from a protocol model check the rules stated by that model. They do not express implementation-specific micro-architectural behavior. For example, a custom AXI interconnect may prohibit write traffic from master 1 to slave 3 for security reasons. Because that restriction is absent from the AXI specification, synthesized assertions will not include it.
Such properties still need to be written manually. The point is not to remove manual assertions, but to avoid rewriting specification-level checks for every AXI interface. Synthesis supplies that common foundation, allowing the assertion engineer to spend time on design-specific rules that require engineering judgment.
X-propagation creates another practical boundary. Some AXI properties behave poorly around X values in simulation, causing vacuous passes or false failures according to the propagation behavior. Correctly generated assertions add explicit X-filtering to their conditions. We include that filtering by default because diagnosing failures caused by its absence is difficult.
Assertion Coverage Integration
Assertions should be accompanied by cover properties that show whether their trigger conditions were actually reached. A cover property records a specified stimulus pattern, demonstrating that the related assertion had a chance to fail and did not. Without covers, an assertion suite may pass simply because the tests never entered its trigger domain.
Useful AXI cover cases include a transaction using the maximum burst length for the configured AWLEN width, a transaction returning a SLVERR response, multiple outstanding transactions with different IDs active together, and address and data handshakes taking different cycles instead of the same cycle.
BigEndian produces cover properties beside the assertion properties in each synthesized assertion module. Verification engineers can therefore check that stimulus reaches the conditions under test. Verification reports show cover property pass rates next to assertion pass rates, providing a quick view of whether the suite is exercised or merely instantiated.
Protocol assertions are verification infrastructure, not a score. A complete, correctly scoped AXI set finds protocol violations that functional coverage can miss. Synthesizing that infrastructure instead of writing it repeatedly removes subtle assertion defects that might otherwise remain until post-silicon debugging.