Assertions (SVA) check local temporal properties. For AXI4 outside reset, VALID and its payload must remain stable while stalled. A write-response checker must track acceptance of both AW and the final W beat before allowing BVALID for that transaction. W, including WLAST, may arrive before AW; requiring AW first would reject legal traffic. Beat counts are based on WVALID && WREADY, not elapsed cycles.
For example, assume a slave can buffer early data and initially has no pending writes. A single W beat with WLAST accepted at edge 1, its AW with AWLEN=0 accepted at edge 3, then BVALID asserted after edge 3 is legal. BVALID at edge 2 is illegal because no write address has yet been accepted. If the slave cannot buffer early data, it can hold WREADY low; the master must preserve the stalled W offer. This example follows Arm IHI 0022H A3.3; it is a checker-design walkthrough, not an executable assertion listing.
Scoreboards can correlate transactions across interfaces: a request at one observation point maps to downstream work and an upstream response. Assertions and scoreboards have overlapping capabilities; choose properties, reference models and observation points so wrong data, ordering or missing progress is checked without assuming one mechanism owns an entire bug class.
Assertions: precise sampled properties. Scoreboard: model-based transaction correlation; scopes may overlap.
Formal: exhaustive only for the stated model, assumptions, properties and completed proof bounds; capacity depends on the design and abstraction.
Coverage: did we exercise the scenario? Not: did we prove correctness?
For ordinary AXI4 reads, keep a queue of accepted requests for each observed interface and ARID. Each entry stores the request address, burst shape, expected data and accepted response-beat count. R carries RID, not the request address: match an accepted R beat to the head of that interface's RID queue, validate the beat and RLAST position, then retire the entry only after its final accepted beat. Reusing an ID appends an entry; it must not overwrite an earlier request.
For writes, associate W bursts with AW request order because AXI4 W has no ID. A monitor may need to retain early W data until AW context arrives. Track B responses against the pending write-response queue for BID and check that the corresponding address and data were accepted. Read and write queues are separate; equal numeric IDs do not make them one ordered stream. Across a bridge, record the interface, address translation, ID remapping and any transaction splitting before comparing the two boundaries.
Illustrative read exercise: initially there are no pending requests, and read-only words at 0x1000, 0x2000 and 0x3000 hold 0x11, 0x22 and 0x33. Accept single-beat reads A=(ID 3, 0x1000), B=(ID 3, 0x2000), then C=(ID 7, 0x3000). Queue 3 contains [A, B]; queue 7 contains [C]. A legal completion order is C, A, B. Can a response with RID=3 and data=0x22 satisfy B first? No: it must be checked against A, whose expected data is 0x11. A single map entry for ID 3 would overwrite A and miss the intended association. This assumes ordinary AXI4 reads at one interface with no intervening writes or reset; see Arm IHI 0022H A5–A6 for ordering rules.
Accept only protocol-permitted reordering, not every completion permutation.
Timeout thresholds are system progress assumptions, not a universal AXI response deadline.
Expected data source: memory model, reference model, or golden vector.
Assertions: precise sampled properties. Scoreboard: model-based transaction correlation; scopes may overlap.
Formal: exhaustive only for the stated model, assumptions, properties and completed proof bounds; capacity depends on the design and abstraction.
Coverage: did we exercise the scenario? Not: did we prove correctness?