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 manager must preserve the stalled W offer. Arm IHI 0022H A3.3 defines the channel dependency; the executable teaching observer below implements a bounded subset of these sampled obligations.
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?
Read first: AXI channel independence and acceptance
For sampled rising edges outside reset: if WVALID && !WREADY held at the preceding edge, this edge must still show WVALID and the same WDATA, WSTRB and WLAST. Check the entire offered payload, not only accepted beats. A change on the accepting edge is still a failure. For BVALID, check saved history before adding this edge's handshakes: AW and final W acceptance must already have occurred.
The executable listing has a clocked observer and a separate self-checking testbench. It implements assertion obligations procedurally, using sticky violation bits and fatal testbench checks, so no concurrent-SVA engine or UVM package is required. Scope: one single-beat write outstanding, 64-bit WDATA, eight strobes, and reset clearing the observer. It does not check AW/B payload stability, BID, arbitrary bursts or every AXI rule.
Classify offers before running a checker
Observed sequence outside reset | Expected result | Reason |
|---|---|---|
Final W accepted; AW accepted later; B offered afterwards | Legal dependency | W-before-AW is allowed when buffered. |
W stalls with value A; next edge accepts value B | Retention violation | Acceptance does not excuse changing the outstanding offer. |
W stalls; next edge withdraws WVALID | Retention violation | The offered beat was not accepted or cancelled by reset. |
AW and final W first accepted at this edge; BVALID already high | Response dependency violation | Same-edge acceptance is not prior completed history. |
The bench sweeps AW-first, W-first and simultaneous arrival with varied gaps/data, checks stalled B operation, isolates eight negative stimuli including WDATA/WSTRB/WLAST retention and each missing response prerequisite, and replays a clean case. PASS means this teaching harness verified its expected outcomes, not full AXI compliance.
// Self-checking teaching observer, not a complete AXI4 checker.
// Scope: one single-beat write outstanding, 64-bit WDATA, no reset overlap.
module sampled_write_observer (
input wire clk, reset,
input wire awvalid, awready,
input wire wvalid, wready, wlast,
input wire [63:0] wdata,
input wire [7:0] wstrb,
input wire bvalid, bready,
output reg [2:0] violations
);
reg aw_seen, last_w_seen, stalled;
reg [72:0] held_payload;
always @(posedge clk) begin
if (reset) begin
aw_seen <= 0;
last_w_seen <= 0;
stalled <= 0;
held_payload <= 0;
violations <= 0;
end else begin
// Check against the preceding sampled stalled offer, even on acceptance.
if (stalled && (!wvalid || {wlast, wstrb, wdata} !== held_payload))
violations[0] <= 1;
// Pre-edge history: handshakes on this edge cannot justify BVALID here.
if (bvalid && !(aw_seen && last_w_seen)) violations[1] <= 1;
if (wvalid && wready && !wlast) violations[2] <= 1;
stalled <= wvalid && !wready;
held_payload <= {wlast, wstrb, wdata};
if (awvalid && awready) aw_seen <= 1;
if (wvalid && wready && wlast) last_w_seen <= 1;
if (bvalid && bready) begin
aw_seen <= 0;
last_w_seen <= 0;
end
end
end
endmodule
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.
Use the shared SRAM0 range: initialise read-only 64-bit words at 0x2000_0000, 0x2000_0008 and 0x2000_0010 to 0x11, 0x22 and 0x33. This explicitly overrides zero initial data for this exercise. Accept DMA0 single-beat reads A=(ID 3, first address), B=(ID 3, second address), C=(ID 7, third address). Queue 3 is [A,B]; queue 7 is [C]. C,A,B is a legal return order. RID=3/data=0x22 must be checked against A's expected 0x11, not used to search for B and declare success. See Arm IHI 0022H A5–A6 for the ordinary AXI4 ordering scope.
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.
The executable event observer below receives accepted AR/R events. It is not a pin-level AXI implementation. For each of two observation ports and sixteen IDs, it stores up to four accepted request contexts. R carries no address: the observer checks its data, status and single-beat RLAST against the oldest expected entry. The memory oracle is read-only here, so concurrent-write visibility is outside scope.
The bench tests legal cross-ID and cross-port return permutations, wrong same-ID association, port collision, orphan response, missing RLAST, unexpected status and observer-capacity exhaustion. A final varied replay fills and drains every port/ID queue. Queue overflow is reported as lost observation capacity, not labelled an AXI violation. A mismatched single-beat response is retired for subsequent diagnostics but remains an error; this is not multi-beat recovery logic.
Per-port queues after three accepted reads
A=(port 0, ID 3, 0x2000_0000→0x11), B=(port 0, ID 3, 0x2000_0008→0x22), D=(port 1, ID 3, 0x2000_0018→0x44). No reset or intervening writes.
Response event | Expected head | Remaining queues if correct |
|---|---|---|
Port 1: RID 3, data 0x44 | D | Port 0/3=[A,B]; port 1/3=[] |
Port 0: RID 3, data 0x11 | A | Port 0/3=[B] |
Port 0: RID 3, data 0x22 | B | Both queues empty |
The two ports are independent observation contexts, not an invented extra field on AXI R. The self-contained listing checks the shown queue operations; it is not a complete AXI implementation.
// Executable transaction-observer exercise, not an AXI endpoint or UVM package.
// Two observation ports, 4-bit IDs, depth four per ID, aligned one-beat reads.
// Expected words are independently obtained from a read-only memory oracle.
module read_scoreboard_tb;
reg [63:0] expected [0:1][0:15][0:3];
reg [31:0] address [0:1][0:15][0:3];
integer count [0:1][0:15];
integer requests, responses, comparisons, errors, capacity_errors, checks = 0;
function [63:0] word_at(input [31:0] addr);
begin
case (addr)
32'h2000_0000: word_at = 64'h11;
32'h2000_0008: word_at = 64'h22;
32'h2000_0010: word_at = 64'h33;
32'h2000_0018: word_at = 64'h44;
default: word_at = 0;
endcase
end
endfunction
task require(input bit ok, input [511:0] why);
begin
checks = checks + 1;
if (!ok) $fatal(1, "FAIL: %0s", why);
end
endtask
task fresh;
begin
requests=0; responses=0; comparisons=0; errors=0; capacity_errors=0;
for (integer p=0; p<2; p=p+1)
for (integer id=0; id<16; id=id+1) begin
count[p][id]=0;
for (integer n=0; n<4; n=n+1) begin
expected[p][id][n]=0; address[p][id][n]=0;
end
end
end
endtask
// Called only when ARVALID && ARREADY was observed at this port.
task accept_ar(input integer port, input [3:0] id, input [31:0] addr);
integer n;
begin
n=count[port][id];
if (n==4) capacity_errors=capacity_errors+1;
else begin
address[port][id][n]=addr;
expected[port][id][n]=word_at(addr);
count[port][id]=n+1;
requests=requests+1;
end
end
endtask
// R contains no address. RID selects the *oldest* queued request at this port.
task accept_r(input integer port, input [3:0] rid,
input [63:0] data, input bit last, input [1:0] status);
begin
responses=responses+1;
if (count[port][rid]==0) errors=errors+1;
else begin
comparisons=comparisons+1;
if (data !== expected[port][rid][0] || !last || status !== 2'b00)
errors=errors+1;
// Retire this single-beat response even on mismatch to keep diagnostics
// aligned with observed traffic; this does not make the mismatch pass.
for (integer n=0; n<3; n=n+1) begin
expected[port][rid][n]=expected[port][rid][n+1];
address[port][rid][n]=address[port][rid][n+1];
end
count[port][rid]=count[port][rid]-1;
end
end
endtask
task require_drained;
begin
for (integer p=0; p<2; p=p+1)
for (integer id=0; id<16; id=id+1)
require(count[p][id]==0, "all admitted reads retired");
require(requests>0 && responses==requests && comparisons==requests,
"nonzero complete observed work");
end
endtask
initial begin
// Same numeric ID on both ports is independent; different IDs may reorder.
fresh();
accept_ar(0,3,32'h2000_0000); accept_ar(0,3,32'h2000_0008);
accept_ar(0,7,32'h2000_0010); accept_ar(1,3,32'h2000_0018);
accept_r(1,3,64'h44,1,0); accept_r(0,7,64'h33,1,0);
accept_r(0,3,64'h11,1,0); accept_r(0,3,64'h22,1,0);
require(errors==0 && capacity_errors==0, "legal per-port/per-ID ordering");
require_drained();
// Fault: newest entry would look right to an overwritten one-entry map.
fresh(); accept_ar(0,3,32'h2000_0000); accept_ar(0,3,32'h2000_0008);
accept_r(0,3,64'h22,1,0);
require(errors==1 && count[0][3]==1, "wrong same-ID head detected");
// Fault: correct data from another port cannot satisfy this port's head.
fresh(); accept_ar(0,3,32'h2000_0000); accept_ar(1,3,32'h2000_0018);
accept_r(0,3,64'h44,1,0);
require(errors==1, "source-port collision detected");
fresh(); accept_r(0,3,64'h11,1,0);
require(errors==1 && comparisons==0, "orphan response detected");
fresh(); accept_ar(0,3,32'h2000_0000); accept_r(0,3,64'h11,0,0);
require(errors==1, "single-beat response requires RLAST");
fresh(); accept_ar(0,3,32'h2000_0000); accept_r(0,3,64'h11,1,2'b10);
require(errors==1, "unexpected response status detected");
fresh();
for (integer n=0; n<5; n=n+1) accept_ar(0,3,32'h2000_0000);
require(capacity_errors==1 && count[0][3]==4 && errors==0,
"observer capacity is separate from protocol violations");
// Varied IDs/ports and clean post-fix replay; memory remains read-only.
fresh();
for (integer p=0; p<2; p=p+1)
for (integer id=0; id<16; id=id+1)
for (integer n=0; n<4; n=n+1)
accept_ar(p,id,32'h2000_0000+8*n);
for (integer p=1; p>=0; p=p-1)
for (integer id=15; id>=0; id=id-1)
for (integer n=0; n<4; n=n+1)
accept_r(p,id,word_at(32'h2000_0000+8*n),1,0);
require(errors==0 && capacity_errors==0 && requests==128, "varied legal replay");
require_drained();
require(checks>70, "assertion work is non-vacuous");
$display("PASS: per-port per-ID queues, negative cases and clean replay");
$finish;
end
endmoduleCompare a stalled offer with the previous sampled offer, including the edge on which acceptance occurs.
BVALID needs previously accepted AW and final W; BREADY cannot excuse a premature offer.
A response ID selects a per-port queue head, not the newest request or an invented response address.