PCIe · Module 14
Replay Buffer — Where Reading Is Not Dequeuing
A replay buffer looks like a FIFO and behaves like nothing of the sort: a packet is read for transmission without being removed, may be read again, and leaves only when acknowledged. Three independent pointers, a captured replay boundary, and the wrap bug that only appears at depth five.
Chapter 14.2 retired entries from a window it did not fill. Chapter 14.3 walked entries by logical position and said explicitly that it did not own them.
Both were describing this.
How do we build finite hardware that retains every unresolved transmitted TLP, retires acknowledged history, replays the correct retained suffix after a retry event, handles wrap and simultaneous operations safely, and never exposes replay as duplicate Transaction Layer traffic?
1. Why a FIFO Is Not Enough
A FIFO has one lifecycle, and it is the wrong one.
FIFO: push → pop the data is gone
Replay buffer: allocate → send → retain → maybe send again
→ maybe again → ACK → retire| FIFO | Replay buffer | |
|---|---|---|
| Reading an entry | removes it | leaves it in place |
| Entries leave | on read | on acknowledgement |
| An entry may be read | once | any number of times |
| Pointers | read, write | retire, allocate, transmit — three |
| Occupancy means | data waiting to be consumed | reliability responsibility not yet discharged |
2. The Verified Behaviour
3. Three Pointers
A FIFO has two. This needs three, and they move for three unrelated reasons.
| Pointer | Points at | Moves when | Driven by |
|---|---|---|---|
| head — retire | the oldest unresolved entry | an acknowledgement retires a prefix | the receiver, via ACK/NAK |
| tail — allocate | where the next new packet is stored | the Transaction Layer hands one down | the layer above |
| replay — transmit | which retained entry is currently being sent | a transmit handshake completes | the Link |
And a fourth quantity that is not a pointer: occupancy, kept as a counter for the reason §13 develops.
4. Entry Lifetime
FREE
│ allocation — reliability responsibility begins
▼
ALLOCATED / not yet sent
│ transmit handshake
▼
SENT / UNACKED ◄─────────┐
│ │ replay: sent again, entry untouched
│ │
├───────────────────────┘
│ acknowledgement covers it
▼
RETIRED → FREETwo transitions must be impossible, and they are the chapter's core invariants:
| Forbidden | Why |
|---|---|
| SENT → FREE without acknowledgement | the packet may still be needed (Chapter 14.1 §2) |
| allocation over an unresolved entry | it overwrites a packet the design promised to deliver |
Note that the diagram has no separate REPLAYED state. A replay is a second read of an entry in SENT/UNACKED — it does not change the entry's state at all, which is exactly §1's point expressed as a state machine. §6's model keeps no per-entry sent flag for this reason: the pointers already say everything the design needs.
5. The Structure
The separation is deliberate and it is what makes both blocks readable. The core answers what is retained and where is it; the scheduler answers what do I send next. Neither can corrupt the other: the scheduler holds no storage and never writes, and the core has no opinion about transmission order.
6. RTL — Replay Buffer Core
// SYNTHESIZABLE. The retained-packet store: allocate, hold immutably,
// look up by logical position, retire a prefix on acknowledgement.
// Retention-until-acknowledged and cumulative prefix retirement: NORMATIVE
// (section 2). The register-array storage, the match search and the error
// outputs: ILLUSTRATIVE teaching representation.
//
// This module does NOT decide what to transmit. That is replay_tx_scheduler.
module replay_buffer_core #(
parameter int DEPTH = 8,
parameter int PKT_W = 128,
parameter int SEQ_W = 8 // internal identity, NOT PCIe
) (
input logic clk,
input logic rst_n,
// ---- Allocation, from the Transaction Layer --------------------------
input logic alloc_valid,
output logic alloc_ready,
input logic [PKT_W-1:0] alloc_packet,
input logic [SEQ_W-1:0] alloc_seq,
// ---- Lookup by LOGICAL position (0 = oldest retained) ----------------
// Positions, not memory indices. The caller never sees the ring.
// TWO independent read ports, because there are two independent readers:
// the transmit scheduler (which entry to send) and the retry controller's
// search (Chapter 14.3 section 11). A register array supports both cheaply;
// a RAM-based store would need arbitration, and section 6a says so.
input logic [$clog2(DEPTH+1)-1:0] lookup_pos, // scheduler port
output logic lookup_valid,
output logic [PKT_W-1:0] lookup_packet,
output logic [SEQ_W-1:0] lookup_seq,
input logic [$clog2(DEPTH+1)-1:0] search_pos, // search port
output logic search_valid,
output logic [SEQ_W-1:0] search_seq,
// ---- Retirement --------------------------------------------------
// A COUNT, not an identity. The retry controller already searched for the
// named identity (Chapter 14.3 section 11) and knows the prefix length —
// searching again here would be the same decode in two places, which is
// the anti-pattern Chapter 11.7 section 8 is about.
input logic retire_req,
input logic [$clog2(DEPTH+1)-1:0] retire_req_count,
output logic retire_done,
output logic [$clog2(DEPTH+1)-1:0] retire_count,
output logic retire_illegal,
// ---- State -----------------------------------------------------------
output logic [$clog2(DEPTH+1)-1:0] occupancy,
output logic full,
output logic empty
);
generate
if (DEPTH < 1) $error("DEPTH must be at least 1");
if (PKT_W < 1) $error("PKT_W must be at least 1");
endgenerate
// Width-safe at DEPTH == 1, where $clog2(1) is 0 and a zero-width index is
// illegal. CNT_W is one wider than IDX_W so DEPTH itself is representable —
// a same-width occupancy counter cannot express `full` (section 13).
localparam int IDX_W = (DEPTH <= 1) ? 1 : $clog2(DEPTH);
localparam int CNT_W = $clog2(DEPTH + 1);
typedef struct packed {
logic valid;
logic [SEQ_W-1:0] seq;
logic [PKT_W-1:0] packet;
} replay_entry_t;
replay_entry_t mem_q [DEPTH];
logic [IDX_W-1:0] head_q, tail_q;
logic [CNT_W-1:0] cnt_q;
assign occupancy = cnt_q;
assign full = (cnt_q == CNT_W'(DEPTH));
assign empty = (cnt_q == '0);
// `full` reflects UNRESOLVED RELIABILITY OWNERSHIP, not Link busy-ness
// (section 12). A transmitted-but-unacknowledged packet still occupies.
assign alloc_ready = !full;
// EXPLICIT WRAP at DEPTH-1. Natural rollover wraps at 2^IDX_W, which
// equals DEPTH only at powers of two — section 10's DEPTH=5 bug.
function automatic logic [IDX_W-1:0] next_idx (input logic [IDX_W-1:0] i);
next_idx = (i == IDX_W'(DEPTH - 1)) ? '0 : (i + IDX_W'(1));
endfunction
// Logical position -> physical index, wrapped at DEPTH.
function automatic int unsigned phys_of (input int unsigned pos);
phys_of = (int'(head_q) + pos) % DEPTH;
endfunction
// ---- Lookup ----------------------------------------------------------
// RANGE SAFETY: lookup_pos is CNT_W wide and can express DEPTH itself, so
// it is bounds-checked before any array access (the class of bug fixed in
// Chapters 12.1 and 12.3).
wire lookup_in_range = (lookup_pos < cnt_q);
wire [IDX_W-1:0] lookup_phys = IDX_W'(phys_of(int'(lookup_pos)));
always_comb begin
lookup_valid = 1'b0;
lookup_packet = '0;
lookup_seq = '0;
if (lookup_in_range) begin
lookup_valid = mem_q[lookup_phys].valid;
lookup_packet = mem_q[lookup_phys].packet;
lookup_seq = mem_q[lookup_phys].seq;
end
end
// ---- Search read port -------------------------------------------------
// Same range discipline as the scheduler port. This is what Chapter 14.3's
// sequential search reads, one position per cycle.
wire search_in_range = (search_pos < cnt_q);
wire [IDX_W-1:0] search_phys = IDX_W'(phys_of(int'(search_pos)));
always_comb begin
search_valid = 1'b0;
search_seq = '0;
if (search_in_range) begin
search_valid = mem_q[search_phys].valid;
search_seq = mem_q[search_phys].seq;
end
end
// ---- Retirement -------------------------------------------------------
// The count arrives already computed. The core's only job is to REFUSE an
// impossible one: retiring more entries than are retained would clear
// storage that was never allocated and would corrupt the head.
wire count_legal = (retire_req_count != '0) && (retire_req_count <= cnt_q);
wire do_retire = retire_req && count_legal;
assign retire_done = do_retire;
assign retire_count = do_retire ? retire_req_count : '0;
assign retire_illegal = retire_req && !count_legal;
wire [CNT_W-1:0] covered = retire_req_count;
wire push = alloc_valid && alloc_ready;
always_ff @(posedge clk or negedge rst_n) begin
if (!rst_n) begin
head_q <= '0; tail_q <= '0; cnt_q <= '0;
for (int i = 0; i < DEPTH; i++) mem_q[i] <= '0;
end else begin
// ---- Retirement: clear exactly `covered` entries from the head ----
if (do_retire)
for (int k = 0; k < DEPTH; k++)
if (CNT_W'(k) < covered)
mem_q[phys_of(k)].valid <= 1'b0;
// ---- Allocation --------------------------------------------------
// The packet is written ONCE, here, and never again. Immutability is
// structural: there is no other write to .packet in the module, which
// is what makes "a replay sends the same bits" a fact rather than a
// hope (section 10, P5).
if (push) begin
mem_q[tail_q].valid <= 1'b1;
mem_q[tail_q].seq <= alloc_seq;
mem_q[tail_q].packet <= alloc_packet;
tail_q <= next_idx(tail_q);
end
// ---- Head advance: by exactly the retired count -------------------
if (do_retire)
head_q <= IDX_W'((int'(head_q) + int'(covered)) % DEPTH);
// ---- Occupancy ---------------------------------------------------
// SAME-CYCLE CONTRACT in one expression, so retirement and allocation
// in the same cycle cannot be resolved by statement order. `covered`
// is bounded by cnt_q by construction, so this cannot underflow.
cnt_q <= cnt_q
- (do_retire ? covered : CNT_W'(0))
+ (push ? CNT_W'(1) : CNT_W'(0));
end
end
endmoduleClassification: synthesizable.
Architecture. A ring of immutable entries with three independent index sources: head_q (retirement), tail_q (allocation), and — externally — a logical position for lookup. The core never decides what to send.
State. The entry array, head and tail, and an occupancy counter.
Why alloc_ready is !full and full is about ownership. A packet that has been transmitted and not acknowledged still occupies a slot (§12). full therefore means no safe slot exists for new reliability ownership — not that the Link is busy.
Why lookup is by logical position. The scheduler and Chapter 14.3's controller reason about "the oldest survivor" and "the next one", not about memory indices. Keeping the ring inside the core means the wrap arithmetic exists in exactly one place — and §10 shows why that matters.
Why there are two read ports, and why retirement takes a count. §6a is that argument in full; briefly: there are two independent readers — the scheduler choosing what to transmit and the controller's search walking for an identity — and one searcher, which is the controller. Having the core search again for the same identity would be the same decode in two places (Chapter 11.7 §8's anti-pattern), so the core accepts the prefix length and only validates it.
Failure — seven, and §15 maps each to a check. Clearing an entry on lookup makes it a FIFO and empties the buffer on the first replay. Writing .packet anywhere but the allocation arm breaks immutability. Advancing the head by one per retirement leaks storage (Chapter 14.2 §5). Inferring full from head_q == tail_q reads a full buffer as empty (§9). Natural rollover breaks at any non-power-of-two DEPTH (§10). Omitting either range check lets a CNT_W-wide position index outside the array. And accepting a retirement count larger than the occupancy clears storage that was never allocated and leaves the head pointing at nothing.
Deliberately simplified: a register array rather than RAM; a match search rather than sequence arithmetic (Chapter 14.5); no per-entry sent flag (§4); no replay timer.
6a. How the Three Blocks Compose
Module 14 has produced three blocks that must actually fit together, and the interfaces are where that is decided.
| Block | Owns | Reads | Writes |
|---|---|---|---|
| retry controller (14.3 §11) | one reliability event at a time; the search | the search port, one position per cycle | nothing — it emits a count and an arming pulse |
| buffer core (§6) | the storage, the three pointers | its own memory | entries, on allocation and retirement |
| transmit scheduler (§7) | what to send next; the walk | the scheduler port | nothing — it emits a position |
7. RTL — Transmit Scheduler
// SYNTHESIZABLE. Decide what the Link transmits next: the next new packet,
// or an entry from an active replay walk.
// The captured replay boundary and the strict replay priority are
// ILLUSTRATIVE IMPLEMENTATION POLICY (Chapter 14.3 sections 9 and 10).
// That a replay must not create a Transaction Layer acceptance is a
// NORMATIVE consequence of the identity distinction (Chapter 14.3 section 6).
module replay_tx_scheduler #(
parameter int DEPTH = 8,
parameter int PKT_W = 128,
parameter int SEQ_W = 8
) (
input logic clk,
input logic rst_n,
// ---- Core view -------------------------------------------------------
input logic [$clog2(DEPTH+1)-1:0] occupancy,
output logic [$clog2(DEPTH+1)-1:0] lookup_pos,
input logic lookup_valid,
input logic [PKT_W-1:0] lookup_packet,
input logic [SEQ_W-1:0] lookup_seq,
// How many entries the core just retired, and whether it did. Used to
// rebase the walk when a retirement renumbers the survivors.
input logic retire_done,
input logic [$clog2(DEPTH+1)-1:0] retire_count,
// ---- Replay arming, from the retry controller ------------------------
input logic arm_replay,
input logic [$clog2(DEPTH+1)-1:0] arm_survivors, // walk length
// ---- Normal send stream ----------------------------------------------
// Position of the oldest entry that has never been transmitted. Tracked
// here because it is a transmission concern, not a storage one.
input logic new_pending, // something unsent exists
// ---- Link transmit ---------------------------------------------------
output logic tx_valid,
input logic tx_ready,
output logic [PKT_W-1:0] tx_packet,
output logic [SEQ_W-1:0] tx_seq,
output logic tx_is_replay, // telemetry, not a wire
output logic replay_active,
output logic walk_overrun_error
);
localparam int CNT_W = $clog2(DEPTH + 1);
logic active_q;
logic [CNT_W-1:0] walk_pos_q; // logical position within the walk
logic [CNT_W-1:0] walk_stop_q; // CAPTURED exclusive bound
logic [CNT_W-1:0] send_pos_q; // logical position of next unsent entry
logic ovr_q;
assign replay_active = active_q;
assign walk_overrun_error = ovr_q;
// The scheduler asks the core for ONE position per cycle. During a walk
// that is the walk pointer; otherwise it is the next unsent entry.
assign lookup_pos = active_q ? walk_pos_q : send_pos_q;
// STRICT REPLAY PRIORITY while active (Chapter 14.3 section 10).
wire want_send = active_q ? (walk_pos_q < walk_stop_q)
: new_pending;
assign tx_valid = want_send && lookup_valid;
assign tx_packet = lookup_packet;
assign tx_seq = lookup_seq;
assign tx_is_replay = active_q;
wire fire = tx_valid && tx_ready;
always_ff @(posedge clk or negedge rst_n) begin
if (!rst_n) begin
active_q <= 1'b0; walk_pos_q <= '0; walk_stop_q <= '0;
send_pos_q <= '0; ovr_q <= 1'b0;
end else begin
// ---- Rebase on retirement -----------------------------------------
// A retirement renumbers logical positions: what was position k
// becomes k - retire_count. Every position this block holds must be
// rebased, or it silently points at the wrong entry afterwards.
// This is the subtlest interaction in the chapter (section 11).
if (retire_done) begin
send_pos_q <= (send_pos_q >= retire_count)
? (send_pos_q - retire_count) : CNT_W'(0);
if (active_q) begin
walk_pos_q <= (walk_pos_q >= retire_count)
? (walk_pos_q - retire_count) : CNT_W'(0);
walk_stop_q <= (walk_stop_q >= retire_count)
? (walk_stop_q - retire_count) : CNT_W'(0);
end
end
// ---- Arm a walk ---------------------------------------------------
// arm has priority over the rebase above for the walk registers: the
// controller computes `arm_survivors` from the POST-retirement view,
// so it is already rebased.
if (arm_replay && !active_q) begin
active_q <= 1'b1;
walk_pos_q <= '0; // oldest survivor
walk_stop_q <= arm_survivors; // CAPTURED, cannot move
end else if (active_q && fire) begin
if ((walk_pos_q + CNT_W'(1)) >= walk_stop_q) begin
active_q <= 1'b0; // walk complete
walk_pos_q <= '0;
end else begin
// ADVANCE ONLY ON THE HANDSHAKE.
walk_pos_q <= walk_pos_q + CNT_W'(1);
end
end
// ---- Normal send advance ------------------------------------------
// A new send moves the unsent frontier forward. During a walk no new
// sends occur, so this cannot race the walk.
if (!active_q && fire)
send_pos_q <= send_pos_q + CNT_W'(1);
// A walk pointer that has passed its bound, or points outside the
// occupancy, is reported rather than allowed to index anything.
if (active_q && ((walk_pos_q > walk_stop_q) || (walk_stop_q > occupancy)))
ovr_q <= 1'b1;
end
end
endmoduleClassification: synthesizable.
Architecture. A mode machine over three logical positions, holding no storage and performing no writes to the core. It selects; the core stores.
State. active_q, the walk pointer and its captured bound, the unsent frontier, and a sticky overrun report.
Same-cycle contract, stated explicitly:
| Event pair | Resolution |
|---|---|
| retirement + walk advance | rebase first, then advance — both apply, in that order within the cycle |
| arm + retirement | arm_survivors is computed post-retirement, so the arm arm wins for the walk registers |
| arm while already active | ignored here; Chapter 14.3 §11 reports it |
| walk completes + new send | the walk clears active_q; the new send begins the following cycle |
| transmit stalled | nothing advances — fire is the only thing that moves a pointer |
Failure — four. Advancing on tx_valid rather than fire skips an entry the first time the Link stalls. Omitting the rebase leaves every held position pointing one or more entries too late after a retirement — §11 is that bug in full. Using live occupancy as the walk bound lets it chase a moving tail (Chapter 14.3 §9). And asserting tx_valid without lookup_valid offers an entry the core says does not exist.
8. The Rebase Problem
The subtlest interaction in the chapter, and it exists only because lookup is by logical position.
Positions are relative to the head. When a retirement advances the head, every logical position renumbers.
before retirement: pos: 0 1 2 3 4
seq: 10 11 12 13 14
^
walk is here (pos 2, seq 12)
ACK retires 10, 11 → two entries released, head advances by 2
after retirement: pos: 0 1 2
seq: 12 13 14
^
seq 12 is NOW pos 0 — the walk must rebase to 09. Occupancy Is Not Pointer Equality
A classic ring-buffer bug, and it is worth showing rather than asserting.
DEPTH = 4
empty: head_q = 2, tail_q = 2 cnt_q = 0
full: head_q = 2, tail_q = 2 cnt_q = 4Identical pointers. Opposite states.
A design inferring emptiness from head_q == tail_q reads a full buffer as empty, asserts alloc_ready, and allocates over an unresolved entry — overwriting a packet it has promised to deliver, which is §4's forbidden transition.
The occupancy counter is one bit wider than the index for the same reason. IDX_W reaches DEPTH−1; CNT_W must reach DEPTH, or the counter cannot represent a full buffer and wraps to zero — which produces the identical failure through a different route.
10. Non-Power-of-Two Depth
DEPTH = 5 is where a design that looked correct at 8 falls over.
DEPTH = 5 → IDX_W = $clog2(5) = 3 → the index reaches 7
natural rollover: 0 1 2 3 4 5 6 7 0 1 ... ← wraps at 8
required: 0 1 2 3 4 0 1 2 3 4 ... ← wraps at 5Indices 5, 6 and 7 address nothing. Entries alias, allocation writes outside the intended range, and lookups return whatever the synthesis tool put there.
§6's next_idx wraps at DEPTH−1 explicitly, and phys_of uses a modulo — so both are correct at every depth.
11. Full Means Ownership, Not Busy
fullmeans no safe slot exists for new reliability ownership. It does not mean the Link is busy.
A packet may have been transmitted — possibly several times — and still occupy a slot. Its delivery is unresolved, so the design still owes it (Chapter 14.1 §2).
Which produces a state that looks wrong and is not:
| Observation | Interpretation |
|---|---|
| buffer full, Link idle, every packet transmitted | correct — waiting for acknowledgement |
buffer full, alloc_ready low, Transaction Layer stalled | correct — the layer refusing work is the contract working |
| buffer full and acknowledgements arriving with no retirement | a bug — §18's first scenario |
And the confusion §17 has to prevent: this is not flow control. Replay-buffer occupancy is transmit-side reliability storage; flow-control credits are a separate mechanism describing the receiver's ability to accept, owned by Module 16.
12. Allocation and Retirement in the Same Cycle
The case that decides whether the design can run at full rate.
At full, a retirement releases slots and a new packet arrives. May it be accepted the same cycle?
13. A Full Trace
Internal teaching signals, not PCIe wire signals. DEPTH = 4.
step 1 2 3 4 5 6 7 8 9 10
alloc_valid 1 1 1 1 0 0 0 0 1 0
alloc_ready 1 1 1 1 0 0 1 1 1 1
alloc_seq 10 11 12 13 - - - - 14 -
tx_valid 1 1 1 1 0 1 1 1 0 1
tx_ready 1 1 1 1 0 0 1 1 0 1
tx_seq 10 11 12 13 - 12 12 13 - 14
tx_is_replay 0 0 0 0 - 1 1 1 - 0
nak_valid 0 0 0 0 1 0 0 0 0 0
nak_seq - - - - 11 - - - - -
head (seq) 10 10 10 10 10 12 12 12 12 12
occupancy 1 2 3 4 4 2 2 2 2 3
replay_active 0 0 0 0 0 1 1 1 0 0
walk_pos - - - - - 0 0 1 - -
walk_stop - - - - - 2 2 2 - -Step 4 → 5: the buffer is full. Four entries, all transmitted, none acknowledged. alloc_ready is low and the Link is idle — §11's "correct" row.
Step 5: a NAK naming 11 retires 10 and 11 (occupancy 4 → 2), and arms a walk of length 2 over the survivors 12 and 13.
Steps 6–7: tx_ready is low at step 6, so walk_pos does not move — the same entry is offered twice. That is P7.
Step 8: 13 is replayed, the walk reaches its bound, and replay_active drops.
Step 9: a new packet is allocated. Note it went to the tail while the head sat at 12 — three pointers, three independent motions (§3).
And read tx_seq across the whole trace. 12 and 13 each appear twice; alloc_seq shows each once. Two sends, one acceptance (Chapter 14.3 §6).
14. Assertions
// SVA over replay_buffer_core and replay_tx_scheduler. These assert the
// NORMATIVE retention and retirement rules of section 2 and the LOCAL
// ownership contracts. They assert nothing about sequence arithmetic
// (Chapter 14.5), DLLP format (Module 15), or flow control (Module 16).
// ---- ENVIRONMENT ASSUMPTIONS ----------------------------------------
// A1: the retirement count the controller supplies was derived from a
// genuine match in this window (Chapter 14.3's search). The core validates
// the RANGE but cannot re-derive the identity — that is the point of not
// searching twice (section 6a).
assume property (@(posedge clk) disable iff (!rst_n)
(retire_req && count_legal) |-> (retire_req_count <= occupancy));
// A2: the Link eventually accepts a continuously offered packet. PCIe does
// not guarantee it — it depends on the Physical Layer and Link state.
assume property (@(posedge clk) disable iff (!rst_n)
tx_valid |-> s_eventually tx_ready);
// ---- STORAGE OWNERSHIP ----------------------------------------------
// P1: THE CHAPTER'S CENTRAL PROPERTY. A send does NOT clear an entry.
// Catches the FIFO instinct in one line.
property p_send_does_not_retire;
@(posedge clk) disable iff (!rst_n)
(fire && !retire_done) |=> (occupancy == $past(occupancy)
+ ($past(push) ? CNT_W'(1) : CNT_W'(0)));
endproperty
a_send_not_pop : assert property (p_send_does_not_retire);
// P2: NEVER OVERWRITE A VALID UNRESOLVED ENTRY. Per entry, so a write to the
// wrong slot cannot hide in an aggregate count.
generate for (genvar g = 0; g < DEPTH; g++) begin : g_no_overwrite
a_no_overwrite : assert property (@(posedge clk) disable iff (!rst_n)
(push && (tail_q == IDX_W'(g))) |-> !mem_q[g].valid);
end endgenerate
// P3: PACKET IMMUTABILITY. A stored packet does not change while valid. The
// property that makes "a replay sends the same bits" a fact.
generate for (genvar g = 0; g < DEPTH; g++) begin : g_immutable
a_immutable : assert property (@(posedge clk) disable iff (!rst_n)
(mem_q[g].valid && !(push && (tail_q == IDX_W'(g))))
|=> ($stable(mem_q[g].packet) && $stable(mem_q[g].seq)));
end endgenerate
// P4: an entry becomes valid ONLY by allocation.
generate for (genvar g = 0; g < DEPTH; g++) begin : g_alloc_only
a_alloc_only : assert property (@(posedge clk) disable iff (!rst_n)
$rose(mem_q[g].valid) |-> ($past(push) && ($past(tail_q) == IDX_W'(g))));
end endgenerate
// P5: an entry is cleared ONLY by a retirement covering it.
generate for (genvar g = 0; g < DEPTH; g++) begin : g_retire_only
a_retire_only : assert property (@(posedge clk) disable iff (!rst_n)
$fell(mem_q[g].valid) |-> ($past(do_retire) || $past(!rst_n)));
end endgenerate
// ---- RETIREMENT ------------------------------------------------------
// P6: retirement is a bounded prefix; an ILLEGAL count retires nothing and
// is reported. The core's whole retirement responsibility, in one property.
property p_retire_prefix_bounded;
@(posedge clk) disable iff (!rst_n)
retire_req |-> (count_legal ? ((retire_count >= CNT_W'(1))
&& (retire_count <= occupancy))
: ((retire_count == '0) && retire_illegal));
endproperty
a_prefix : assert property (p_retire_prefix_bounded);
// P6a: INTEGRATION. The two read ports are independent — a search never
// disturbs what the scheduler is reading, and vice versa (section 6a).
property p_ports_independent;
@(posedge clk) disable iff (!rst_n)
($stable(lookup_pos) && $stable(mem_q)) |=> $stable({lookup_valid, lookup_packet, lookup_seq});
endproperty
a_ports_indep : assert property (p_ports_independent);
// P6b: INTEGRATION. Both ports are range-safe independently.
property p_search_range_safe;
@(posedge clk) disable iff (!rst_n)
(search_pos >= occupancy) |-> !search_valid;
endproperty
a_search_safe : assert property (p_search_range_safe);
// P7: OCCUPANCY CONSERVATION across every event combination.
property p_occupancy_exact;
@(posedge clk) disable iff (!rst_n)
1'b1 |=> (occupancy == $past(occupancy)
- $past(retire_done ? retire_count : CNT_W'(0))
+ $past(push ? CNT_W'(1) : CNT_W'(0)));
endproperty
a_occ_exact : assert property (p_occupancy_exact);
// P8: occupancy is bounded, and full/empty agree with it — never inferred
// from pointer equality (section 9).
property p_occ_flags_consistent;
@(posedge clk) disable iff (!rst_n)
(occupancy <= CNT_W'(DEPTH))
&& (full == (occupancy == CNT_W'(DEPTH)))
&& (empty == (occupancy == '0));
endproperty
a_flags : assert property (p_occ_flags_consistent);
// ---- REPLAY WALK -----------------------------------------------------
// P9: THE REBASE PROPERTY (section 8). After a retirement during an active
// walk, the walk still addresses the same logical entry.
property p_walk_rebased_on_retire;
@(posedge clk) disable iff (!rst_n)
(active_q && retire_done && (walk_pos_q >= retire_count))
|=> (walk_pos_q == $past(walk_pos_q) - $past(retire_count));
endproperty
a_rebase : assert property (p_walk_rebased_on_retire);
// P10: the walk pointer advances ONLY on a completed handshake.
property p_walk_advances_on_handshake;
@(posedge clk) disable iff (!rst_n)
(active_q && !$stable(walk_pos_q))
|-> ($past(fire) || $past(arm_replay) || $past(retire_done));
endproperty
a_walk_handshake : assert property (p_walk_advances_on_handshake);
// P11: the walk never offers a position past its captured bound.
property p_walk_within_bound;
@(posedge clk) disable iff (!rst_n)
(active_q && tx_valid) |-> (walk_pos_q < walk_stop_q);
endproperty
a_walk_bound : assert property (p_walk_within_bound);
// P12: a replayed packet equals the retained original.
// (exp_packet is a testbench map keyed by seq — section 15.)
property p_replay_bits_identical;
@(posedge clk) disable iff (!rst_n)
(fire && tx_is_replay) |-> (tx_packet == exp_packet[tx_seq]);
endproperty
a_replay_same : assert property (p_replay_bits_identical);
// P13: a replay never creates a Transaction Layer acceptance.
property p_replay_not_acceptance;
@(posedge clk) disable iff (!rst_n)
(fire && tx_is_replay) |-> !push;
endproperty
a_no_new_accept : assert property (p_replay_not_acceptance);
// P14: a retired entry can never be replayed. Catches a walk addressing
// history the head has already passed.
property p_no_stale_replay;
@(posedge clk) disable iff (!rst_n)
(fire && tx_is_replay) |-> lookup_valid;
endproperty
a_no_stale : assert property (p_no_stale_replay);
// ---- RANGE AND WRAP ---------------------------------------------------
// P15: pointers stay in range at EVERY depth, including non-powers of two.
property p_pointers_in_range;
@(posedge clk) disable iff (!rst_n)
(head_q < IDX_W'(DEPTH)) && (tail_q < IDX_W'(DEPTH));
endproperty
a_ptr_range : assert property (p_pointers_in_range);
// P16: a lookup outside the occupancy is refused rather than indexed.
property p_lookup_range_safe;
@(posedge clk) disable iff (!rst_n)
(lookup_pos >= occupancy) |-> !lookup_valid;
endproperty
a_lookup_safe : assert property (p_lookup_range_safe);
// P17: reset clears the LOCAL ownership state, per entry.
generate for (genvar g = 0; g < DEPTH; g++) begin : g_reset
a_reset : assert property (@(posedge clk) !rst_n |=> !mem_q[g].valid);
end endgenerate
// ---- LIVENESS, with its assumption ----------------------------------
// L1: under A2, an armed walk completes.
property p_walk_completes;
@(posedge clk) disable iff (!rst_n)
arm_replay |-> s_eventually !replay_active;
endproperty
a_liveness : assert property (p_walk_completes);Formal — ghost identities
// VERIFICATION-ONLY. Ghost packet identities for formal proof.
// GHOST ID IS VERIFICATION METADATA, NOT PCIe STATE and not design state.
int ghost_next_id;
int ghost_of_seq [int]; // seq -> ghost id, assigned at TL acceptance
bit ghost_accepted [int];
bit ghost_retired [int];
// On TL acceptance: ghost_of_seq[alloc_seq] = ghost_next_id++;
// ghost_accepted[id] = 1;
// On retirement: ghost_retired[id] = 1;
// G1: every send carries an identity that was previously accepted.
property g_send_was_accepted;
@(posedge clk) disable iff (!rst_n)
fire |-> ghost_accepted[ghost_of_seq[tx_seq]];
endproperty
// G2: a retired identity is never sent again. The strongest statement of
// the lifetime rule — stronger than P14, because it is about the identity
// rather than about the slot the identity used to occupy.
property g_retired_never_resent;
@(posedge clk) disable iff (!rst_n)
fire |-> !ghost_retired[ghost_of_seq[tx_seq]];
endproperty
// G3: one acceptance per ghost identity, regardless of send count.
property g_one_acceptance_per_id;
@(posedge clk) disable iff (!rst_n)
push |-> !ghost_accepted[ghost_next_id];
endproperty
// G4: no accepted identity is lost — every one is eventually retired or
// still retained. Bound as an end-of-test check rather than a property.P1 is the chapter in one property. A send must not change occupancy. It is the FIFO instinct, made checkable, and it fires on the very first transmission of a design that pops on read.
P2 through P5 are per-entry, and that is deliberate. An aggregate occupancy check passes a design that writes the wrong slot as long as the count is right. Per-entry properties say which entry changed and why it was allowed to, which is what turns a failure into a diagnosis.
P9 is the rebase property and it is the one worth having most. §8's bug leaves every register individually correct and the relationship wrong. No property about a single block finds it — only one that ties the walk pointer to the retirement count.
G2 is stronger than P14 and the difference matters. P14 says a replay offers a slot the core considers valid. G2 says the identity has not been retired — which also catches the case where a slot was retired, reallocated to a new packet, and the walk is now happily replaying that new packet under the old walk's bound. The slot is valid; the packet is wrong.
The ghost identities are testbench metadata, assigned at acceptance and carried in the verification environment only. Nothing in the design sees them.
15. Verification
Monitors observe: the allocation interface, the transmit interface with tx_is_replay, the retirement request and its count, the walk state, and occupancy.
The scoreboard is a logical list, not a ring
Mandatory. The reference model must not mirror the pointers.
// VERIFICATION-ONLY. A logical list, deliberately NOT a ring buffer.
// Mirroring head/tail/replay pointers would verify only that the DUT agrees
// with itself — and every pointer bug in section 15's table keeps the DUT
// internally consistent.
typedef struct {
int ghost_id;
int seq_id;
bit [127:0] packet;
int send_count; // may be ANY value >= 1
} sb_entry_t;
sb_entry_t retained [$]; // index 0 is the oldest
// allocate : retained.push_back(...)
// send : find by seq_id; send_count++; ASSERT packet unchanged
// retire(seq) : find the index of seq; ASSERT the DUT's retire_count
// equals index+1; delete the prefix independently
// arm walk : construct the expected replay suffix from `retained`
// AFTER applying the retirement — never from walk_stop_qThe retirement check is the important one. The scoreboard finds the identity in its own list and computes the prefix length. A DUT that retires one per event keeps retire_count and its occupancy mutually consistent — only an independent count disagrees.
Basic
- One packet: allocate, send, ACK. Occupancy 0 → 1 → 1 → 0. Verify occupancy does not fall on the send (P1).
- Several packets, then one cumulative ACK. Verify the prefix retires in one event.
- Fill to
DEPTH. Verifyalloc_readydrops and the Link may still be transmitting. - Drain to empty. Verify
emptyand thathead_q == tail_qwith occupancy 0 (§9). - Fill, then drain, then fill again across the physical wrap.
Retirement
- ACK naming the head, the middle, and the newest. Retire counts 1, k, and
occupancy. - A retirement count of zero, and one larger than the occupancy. Verify nothing retires and
retire_illegalsets (P6) — the core refusing a count it cannot honour. - A search read and a scheduler read of different positions in the same cycle. Verify both answer correctly and independently (P6a, P6b) — the two-port contract of §6a.
- ACK on an empty buffer.
- ACK and allocation in the same cycle at every occupancy below
DEPTH(P7). - Full + ACK + allocation offered. Verify the allocation is accepted the next cycle (§12) and that occupancy never exceeds
DEPTH.
Replay
- Retry the oldest survivor. Walk length equals occupancy after retirement.
- Retry the middle. Verify the retired prefix and the walk suffix are disjoint and together cover the old occupancy.
- A walk that crosses the physical wrap — head near
DEPTH−1. Verify every entry is offered exactly once. tx_readylow for the entire walk, then released. Verifywalk_pos_qnever moves while stalled (P10) and the packet is stable.tx_readytoggling every cycle during a walk.- An ACK arriving mid-walk. Verify the walk still replays the same logical packets (P9) — the required test for §8's rebase, and the one a natural test plan omits.
- An ACK mid-walk that retires past the walk's start. Verify the walk rebases to 0 and does not replay retired entries (G2).
- A second arm during an active walk. Per Chapter 14.3 §11's contract.
- Reset mid-walk.
Parameter corners
DEPTH = 1. The index-width guard; allocate, send, retire, replay a single entry.DEPTH = 3, 5, 7. Required — fill past the wrap, retire across it, replay across it, and verify pointer range (P15). Natural rollover passes every power-of-two depth (§10).DEPTH = 8. The control case: verify everything still works where the bug would be invisible.
Mutations and what kills each
| # | Mutation | Caught by |
|---|---|---|
| 1 | clear the entry on send (pop-on-read) | P1, on the first send; and the first replay finds nothing |
| 2 | allocate over a valid entry when full | P2, per entry; and the scoreboard's packet comparison |
| 3 | head advances one extra on retirement | P7 occupancy mismatch; P5 clears an uncovered entry |
| 4 | an unknown identity retires the head | P6 |
| 5 | replay begins one entry late | scoreboard suffix mismatch; the first replayed seq is wrong |
| 6 | the walk bound is one entry short | scoreboard suffix mismatch; the last survivor is never resent |
| 7 | walk_pos_q advances on tx_valid | P10, with tx_ready low |
| 8 | a stored packet is modified after a send | P3, per entry; and P12 |
| 9 | full + retire + allocate corrupts a slot | P2; and the scoreboard's packet comparison on that entry |
| 10 | pointers wrap at 2^IDX_W | P15, at DEPTH = 5 |
| 11 | a replay creates a TL acceptance | P13, and the scoreboard sees two entries for one packet |
| 12 | a retired packet remains replayable | G2 — the ghost property; P14 only if the slot is also invalid |
| 13 | the walk is not rebased after a retirement | P9, and the mid-walk-ACK test |
| 14 | full inferred from head_q == tail_q | P8, and the fill-then-drain test |
Coverage should include: occupancy at 0, 1, DEPTH−1, DEPTH; retirement counts from 1 to DEPTH; walks of length 1 to DEPTH; walks crossing the physical wrap; retirement during a walk at each walk position; allocation and retirement together at each occupancy; and DEPTH at 1, 3, 5, 7 and 8.
16. Resource and Performance Reasoning
Replay storage is finite hardware, and its depth is a throughput parameter — the Link-layer analogue of Chapter 12.5 §5.
And the connection back to §11: when this storage is exhausted, the Data Link Layer refuses work from the Transaction Layer. That is the contract working (Chapter 14.1 §2), not a failure — but it is also a throughput ceiling, and a design that hits it constantly is under-provisioned rather than broken.
17. Replay Storage Is Not Flow Control
A confusion worth killing explicitly, because both are "buffers with occupancy" in the Data Link neighbourhood.
| Replay buffer | Flow control | |
|---|---|---|
| Lives at | the transmitter | describes the receiver's capacity |
| Holds | packets already sent, awaiting acknowledgement | nothing — it is an accounting mechanism |
| Full means | I cannot take reliability ownership of more | the receiver cannot accept more |
| Released by | an acknowledgement | a credit update |
| Owned by | this module | Module 16 |
They can be exhausted independently and for unrelated reasons. A transmitter can have plenty of credits and a full replay buffer — acknowledgements are slow — or plenty of replay storage and no credits, because the receiver is not draining.
Diagnosing one as the other sends the investigation to the wrong side of the Link entirely.
18. Debugging
The replay buffer is full although the Link is active
Retirement is not keeping up with allocation, and there are three distinguishable causes.
Acknowledgements are arriving and not retiring. Check Chapter 14.3's event_unknown — if it is set, the controller's search found nothing, which is an identity-mapping problem upstream rather than a buffer problem. If instead retire_illegal is set here, the controller produced a count this window cannot honour, and the fault is in the search.
Acknowledgements are retiring too little. Compare retire_count against the position of the acknowledged identity. One per event, against identities several positions in, is the cumulative bug (Chapter 14.2 §5).
Acknowledgements are not arriving at all. Then the buffer is behaving correctly and the question is why the receiver is silent — a Link problem, not a storage one.
And rule out the non-bug first: buffer full with everything transmitted and no acknowledgements yet is correct (§11).
The replayed packets have the right identities but the wrong payload
Immutability is broken, or the storage was reallocated underneath the walk.
Check whether the slot was retired and reallocated. If an ACK retired the entry and a new packet took the slot, the walk is replaying the new packet under an old bound — the slot is valid, the identity even looks plausible, and the data is entirely wrong. G2 is the property, because it tracks the identity rather than the slot.
Otherwise it is a write to .packet outside the allocation arm (P3). Check for anything that updates storage during transmission — a design that "refreshes" an entry before replaying it is the usual form.
The bug appears at DEPTH = 5 and never at DEPTH = 8
Pointer wrap (§10). $clog2(5) is 3, so a naturally-rolling index counts to 7 and addresses three slots that do not exist.
Check head_q and tail_q against DEPTH — P15 asserts they stay below it. If either reaches DEPTH or beyond, the wrap is natural rather than explicit.
And the tell that saves time: the failure is depth-dependent, not traffic-dependent. Re-run the identical stimulus at DEPTH = 8; if it passes, stop looking at the traffic.
The same TL packet reaches the receiver twice as two accepted packets
This is probably not a replay-buffer bug at all.
A replay is expected to put the packet on the wire twice. The receiver is supposed to recognise the second as a duplicate and deliver it upward once (Chapter 14.1 §9).
Check the transmitting side's acceptance count first. One TL acceptance with two sends → the transmitter is correct and the receiver duplicated it. Two acceptances → the replay created a new packet (P13), and that is this side's bug.
A new packet disappears during a replay
Allocation and the walk collided.
Under §7's strict-priority policy this should be impossible — tx_valid comes from the walk while active, and the normal send frontier does not advance. So check whether the policy is actually being enforced: if a new packet was accepted into storage and the unsent frontier was not updated, it is retained but will never be transmitted.
The signature: occupancy includes it, tx_seq never shows it. Dump the retained identities against the transmitted ones.
Occupancy becomes DEPTH + 1 after a full + retire + allocate cycle
The same-cycle count is wrong (§12).
Occupancy must be computed over both events in one expression. A design that decrements on retirement and increments on allocation in separate statements can produce an intermediate value, and if alloc_ready was derived from the intermediate rather than from the start-of-cycle occupancy, it accepts a packet it had no room for.
P7 catches it directly, and §15's full-plus-ACK-plus-allocation test is the stimulus.
19. Common Misconceptions
- "A replay buffer is just a FIFO." Reading for transmission does not remove the entry. Entries leave on acknowledgement, not on read (§1).
- "A packet leaves the buffer when it is first transmitted." It leaves when acknowledged. A transmitted packet still occupies storage (§1, §11).
- "The send pointer and the retire pointer are the same." Three pointers, three agents, three independent motions (§3).
- "Every replayed packet is reallocated." A replay reads a retained entry. Reallocating would create a new packet (Chapter 14.3 §6).
- "An ACK frees one entry." It is cumulative — it frees a prefix (Chapter 14.2 §5).
- "A slot can be overwritten once its packet has been transmitted." Not until it is acknowledged. That is §4's forbidden transition.
- "
head == tailalways means empty." It also means full. Use an occupancy counter (§9). - "Power-of-two pointer wrap works for any depth." It works for powers of two. At
DEPTH = 5a$clog2-width index reaches 7 and aliases (§10). - "A replayed packet can be regenerated from current Transaction Layer signals." It is owned immutable state from acceptance (Chapter 14.1 §8, P3).
- "Retry count equals the number of Transaction Layer Requests." One packet may have many attempts (Chapter 14.3 §6).
- "The replay buffer stores Completions only." It stores every TLP it transmits, including posted writes.
- "The replay buffer is shared end to end through Switches." It is per-Link, per-transmitter. A Switch has its own on each Link (Chapter 3.2 §2).
- "An ACK or NAK DLLP is stored as a buffer entry." The buffer holds TLPs. DLLPs are the mechanism that retires them, not things retained.
- "New traffic and replay can share one pointer." They address different entries for different reasons, and merging them makes the walk unrepresentable (§3).
- "Replay-buffer occupancy is flow-control credits." Different mechanism, different side of the Link, different owner (§17).
20. Understanding Check
21. What's Next
Module 14's transmit side is now complete. Chapter 14.1 set the contract, 14.2 retired retained state on a cumulative frontier, 14.3 turned a NAK into a retirement and a bounded walk, and this chapter built the storage all three were describing — an ordered structure where reading is not dequeuing, with three pointers moving for three unrelated reasons.
One abstraction has been carrying the whole module. Every chapter used seq_id: a locally assigned identity, matched by searching rather than compared arithmetically, with no wrap, no modulus, and no comparison rule (Chapter 14.2 §3).
Chapter 14.5 replaces it with PCIe's actual Sequence Number mechanism: the real field, its wrap, the arithmetic for deciding whether one identity precedes another, and the receive-side gap and duplicate detection that this module's abstract "is this a duplicate" verdict stood in for. The match searches in §6 and in 14.2 §8 exist because that arithmetic had not been taught — 14.5 is where they become unnecessary.
Module 15 then covers the packets that carry these events. Chapter 15.3 owns the ACK DLLP's format and timing and 15.4 the NAK DLLP's — the wire-level material every chapter in Module 14 has deliberately left alone.
The idea to carry forward: a replay buffer is where a packet lives between being sent and being known to have arrived — and the only event that ends that is the acknowledgement, never the transmission.