For the four-outstanding read master, the support matrix fixes ARBURST=INCR, aligned addresses, one ID, bounded length, in-order retirement, and no exclusives. That narrow declaration turns a vague compliance claim into concrete queue and counter requirements.
Enqueue {address, ARLEN+1, destination, accepted_beats=0} only on ARVALID && ARREADY. Reserve capacity before offering AR and hold ARVALID/address/length/ID through acceptance. Outstanding = accepted AR bursts minus retired R bursts, bounded by four; pending AR offers also reserve queue space. Every RVALID && RREADY beat belongs to the head context because same-ID read bursts return in request order. Check RID against the configured ID and RLAST against accepted_beats == expected_beats-1; advance the beat counter only on an accepted beat. A stalled RLAST does not retire the context or return credit. Unexpected RID/length/last is a protocol fault requiring containment, not reassignment to another context.
Illustrative edge | Handshake / offer | Head and credits after edge |
|---|---|---|
E0 | AR A: ID=0, LEN=1 accepted | A(0/2); 3 free |
E1 | AR B: ID=0, LEN=0 accepted | A(0/2), B(0/1); 2 free |
E2 | R ID=0, A beat0, LAST=0 accepted | A(1/2), B; 2 free |
E3 | R ID=0, A beat1, LAST=1; READY=0 | A still head; 2 free |
E4 | Same held A beat1 accepted | A retires, B head; 3 free |
E5 | R ID=0, B beat0, LAST=1 accepted | B retires; 4 free |
Each slot is one clock cycle, and slot k ends at edge Ek. A handshake in slot k changes the free credit count shown from slot k+1.
Slots 0 and 1: two AR handshakes (A with LEN 1, B with LEN 0). Credits fall from 4 to 2.
Slot 3: the last beat of A is offered with rready low. It is not accepted, so A does not retire and credits stay at 2.
Slot 4: the same beat is accepted. A retires and credits rise to 3 in slot 5.
Slot 5: B's only beat is accepted with RLAST, and all four credits are free in slot 6.
The trace above gives these scoreboard rules: the response destination must equal head.destination; accepted beat count never exceeds head.length; credits change by -AR_take + final_R_take, including simultaneous enqueue/retire; after drain, accepted AR count equals retired burst count. Timeouts retain/quarantine contexts until accepted downstream work drains or coordinated reset cancels the epoch.
Supported burst types, sizes, lengths, alignments, and address ranges.
Outstanding limits per channel and per ID.
Ordering matrix for same and different IDs.
AW/W association policy and buffering depth.
Backpressure propagation and deadlock analysis.
Error, timeout, exclusive, and reset behavior.
Performance target with expected channel utilization and queue occupancy.
Invariant | Example assertion intent |
|---|---|
Beat count | Exactly AxLEN+1 accepted data beats per burst |
Last | WLAST/RLAST only on the final accepted beat |
4-KB rule | No burst crosses a 4-KB boundary |
Response | One B per accepted write burst |
Ordering | Same-ID responses preserve required order |
Stability | Every stalled channel holds VALID and payload stable |
If buffering or readiness on one channel waits combinationally for the other while the master makes the opposite dependency, neither handshake progresses. Capture channels independently and pair them from buffered state.
The scoreboard rules and the trace table on this page are written from the stated contract. They have not been run.