UCIe · Module 12
End-to-End Data-Flow Examples
Three complete transaction classes traced cycle by cycle through the whole UCIe stack — a memory read with a transport retry, a multi-beat memory write with a stall and a partial final beat, and a coherent ownership change with a retry mid-flow — each with initial state, RTL exercised, injected failure, assertions, scoreboard snapshots, and retirement.
Module 12 has built four mechanisms in isolation. Chapter 12.1 built request ownership, Chapter 12.2 built the response obligation, Chapter 12.3 built payload movement, and Chapter 12.4 built the transaction's lifetime.
This chapter removes the scaffolding. It takes three real transaction classes — a memory read, a memory write, and a coherent ownership change — and follows each one through the complete stack, cycle by cycle, with a genuine failure injected into each. No new abstractions are introduced. Every mechanism used here has already been built; the work is seeing them operate together, which is where the interactions live.
The three classes are chosen because they fail differently. A read's hazard is a duplicated request. A write's hazard is a duplicated side effect. A coherence transaction's hazard is a duplicated ownership action — and only the last of those has no address you can inspect afterwards.
1. What This Chapter Is For
Transport correctness and semantic correctness are different properties, and the only way to see the difference is to follow one transaction all the way through while something goes wrong.
Each example therefore has the same seven parts: initial state, the transaction's representation, a cycle trace, the RTL actually exercised, an injected failure, the assertions that catch it, and the scoreboard state at retirement.
2. Sourcing, and What Is Symbolic
3. One System Model, Used by All Three Examples
// ILLUSTRATIVE system parameters, used consistently by all three examples so
// the traces can be compared. NOT UCIe values — every one is symbolic.
localparam int PROTO_BEAT_B = 8; // bytes per Protocol-side beat
localparam int ADAPTER_BEAT_B = 4; // bytes per Adapter-internal beat
localparam int CONV_RATIO = PROTO_BEAT_B / ADAPTER_BEAT_B; // 2
localparam int MAX_TXNS = 8; // transaction table entries
localparam int MAX_IDS = 8; // identity space
localparam int BOUNDARY_DEPTH = 2; // FDI-side skid (Ch 12.1 §8)
localparam int REPLAY_DEPTH = 4; // Adapter replay entries
localparam int RSP_DEPTH = 2; // local response queue (Ch 12.2 §11)The topology, unchanged across the three examples:
Initiator Protocol Layer → local D2D Adapter (framing, CRC, replay) → local PHY → package → remote PHY → remote D2D Adapter → remote Protocol Layer / memory / coherence agent.
And the reference identities used in the traces: transaction identities are drawn from the eight-entry space; monitor tags are the testbench's verification-only identities (Chapter 12.3 §5), unique for the whole run.
4. Example 1 — Memory Read
The simplest class, and the one whose duplication hazard is easiest to underestimate.
The operation. The initiator reads address A. The remote memory returns data D.
Initial state, stated explicitly because every trace row is a delta from it:
| Structure | State at cycle 0 |
|---|---|
| Transaction table | empty; txn_count_q = 0 |
| Identity space | all eight free; no quarantine; all generations at 0 |
| FDI boundary skid | empty |
| Replay store | empty, 4 entries available |
| Credits | non-zero — the far side has receive space |
| Local response queue | empty |
| Link | operational; format epoch stable |
| Remote memory | ready; address A holds D |
4.1 The transaction's representation
// Illustrative — the read's state at the moment of allocation. Fields as
// defined in Chapter 12.4 §6; values are this example's.
txn_q[3] = '{
valid : 1'b1,
id : 8'd5, // identity claimed from the free pool
gen : 4'd1, // first attempt on identity 5
state : TXN_DISPATCHED,
meta : pack_meta(ADDR_A, DIR_READ, LEN_8B),
payload_done : 1'b1, // a READ carries no request payload
age : '0,
retry_count : '0,
fail_valid : 1'b0,
fail_cause : '0,
mon_id : MON_R1 // verification-only
};Note payload_done is set at allocation. A read has no request-side payload, so Chapter 12.3 §4's data lifetime is empty on the forward path and begins only when the response returns. That single field is the difference between this example and the next.
4.2 Cycle trace — with a transport retry on the request
Illustrative latencies. The retry is injected at cycle 9.
| Cyc | Txn state | Table | Skid | Replay | PHY | Remote | Rsp queue | Note |
|---|---|---|---|---|---|---|---|---|
| 1 | — | 0 | — | — | — | — | — | request presented at FDI |
| 2 | DISPATCHED | 1 | req | — | — | — | — | allocated; id 5 gen 1 |
| 3 | QUEUED | 1 | req | — | — | — | — | skid holds it |
| 4 | IN_TRANSPORT | 1 | — | obj | — | — | — | framed: header + CRC; replay retained |
| 6 | IN_TRANSPORT | 1 | — | obj | in flight | — | — | on the lanes |
| 8 | IN_TRANSPORT | 1 | — | obj | — | CRC fails | — | flit corrupt; nothing accepted |
| 9 | IN_TRANSPORT | 1 | — | obj re-sent | replay | — | — | retry: no re-allocation |
| 11 | REMOTE_OWNED | 1 | — | obj | — | accepted ONCE | — | duplicate suppressed |
| 12 | WAIT_RESP | 1 | — | obj | — | reading A | — | — |
| 13 | WAIT_RESP | 1 | — | — | — | reading | — | confirmed → replay retires |
| 16 | WAIT_RESP | 1 | — | — | — | returns D | in flight | response on the link |
| 18 | RESP_PENDING | 1 | — | — | — | — | D, id 5 gen 1 | matched; entry still live |
| 19 | RESP_PENDING | 1 | — | — | — | — | held | consumer not ready |
| 20 | COMPLETE | 1 | — | — | — | — | — | consumer accepted D |
| 21 | FREE | 0 | — | — | — | — | — | retired; id 5 released |
Six things to read off it.
Cycle 2 is the only allocation — cycle 9's retry does not allocate, which is Chapter 12.4 §8's rule doing its work. A design allocating on adapter_accept would now have two live entries on identity 5.
Cycle 9 re-sends without changing replay occupancy. The send pointer rewound; nothing was allocated (Chapter 9.4 §8).
Cycle 11 accepts once despite two transmissions. The delivery fence (Chapter 11.4 §16) suppressed the first arrival's duplicate — and note the retry here was a corruption, so the first copy never arrived at all. The dangerous case is a lost confirmation, where both copies arrive intact; §4.5's assertion is written for that.
Cycle 13 retires the replay entry with eight cycles of transaction life remaining. Transport finishes early. That is normal.
Cycle 19 is the row Chapter 12.2 §18's bug destroys. One cycle of consumer stall, and a design retiring at cycle 18 has released identity 5 with D still in the queue.
And cycle 21 releases the identity as a consequence of the state transition, not of any transport event.
4.3 The RTL actually exercised
// Illustrative — the four blocks this trace touches, kept focused rather than
// assembled into one module.
// (a) ALLOCATION — cycle 2. One semantic event; no transport event appears.
wire alloc_fire = fdi_req_valid && fdi_req_ready;
// (b) ADMISSION — cycle 2's `ready`. Chapter 12.1 §10's four vetoes, and note
// that transaction-table space and identity availability are among them.
assign fdi_req_ready = skid_space
&& replay_space
&& (tx_credit_q != '0)
&& link_operational
&& txn_space // Ch 12.4 §21
&& id_available; // Ch 12.4 §12
// (c) RESPONSE MATCH — cycle 18. Four conjuncts, not one (Ch 12.2 §6).
always_comb begin
for (int t = 0; t < MAX_TXNS; t++)
rsp_match[t] = txn_q[t].valid
&& (txn_q[t].id == rsp_in.id)
&& (txn_q[t].gen == rsp_in.gen) // generation, Ch 12.2 §24
&& (txn_q[t].state == TXN_WAIT_RESP);
end
// (d) RETIREMENT — cycle 21. A state transition, and the identity release is
// its consequence (Ch 12.4 §13).
assign retire_normal = (txn_q[t].state == TXN_COMPLETE) && ev.retire;On the state term in the match. Requiring TXN_WAIT_RESP means a response arriving while the transaction is still QUEUED — impossible in a correct system — does not match. That is a cheap extra conjunct that converts an impossible situation into a reported orphan rather than a silent acceptance.
4.4 What the injected failure proves
The retry at cycle 9 is not decoration. It exercises the four independent mechanisms that must all hold for a read to survive transport unreliability:
| Mechanism | Where | Proved by |
|---|---|---|
| Replay retained the object | cycles 4–13 | it was available to re-send at cycle 9 |
| Retry did not re-allocate | cycle 9 | replay occupancy unchanged; table still 1 |
| Remote accepted once | cycle 11 | the delivery fence |
| Transaction survived it all | cycles 4–21 | one entry, one identity, one retirement |
And the mechanism the trace does not exercise, which must be injected separately: a lost confirmation. That is the only fault that makes both copies arrive intact (Chapter 9.4 §12), and therefore the only one that tests duplicate suppression rather than merely retransmission. §16's coverage lists it for that reason.
4.5 Assertions
// Illustrative — the read's four invariants. Monitor tags are verification-only.
// The far side accepts the request at most once, however many times it crossed.
property p_read_remote_accept_once;
@(posedge clk) disable iff (!rst_n)
remote_semantic_accept |-> !accepted_mon[remote_mon_id];
endproperty
a_read_remote_accept_once: assert property (p_read_remote_accept_once);
// A response requires a live outstanding transaction in the right phase.
property p_read_response_requires_live_txn;
@(posedge clk) disable iff (!rst_n)
rsp_valid |-> (rsp_match != '0);
endproperty
a_read_response_requires_live_txn:
assert property (p_read_response_requires_live_txn);
// Exactly one match — a corrupted table or a duplicate identity fires this.
property p_read_match_onehot;
@(posedge clk) disable iff (!rst_n)
(rsp_valid && (rsp_match != '0)) |-> $onehot(rsp_match);
endproperty
a_read_match_onehot: assert property (p_read_match_onehot);
// The transaction completes at most once, and only after the consumer has D.
property p_read_completion_once;
@(posedge clk) disable iff (!rst_n)
txn_complete_fire |-> (!completed_mon[txn_mon_id] && consumer_accepted);
endproperty
a_read_completion_once: assert property (p_read_completion_once);4.6 Scoreboard at retirement
TRANSPORT MODEL
object O1: framed@4, transmitted@6, crc_fail@8, retransmitted@9,
confirmed@13, retired@13, transmissions = 2
TRANSACTION MODEL (by monitor tag)
MON_R1: allocated@2 (count = 1)
phase_history = DISPATCHED@2, QUEUED@3, IN_TRANSPORT@4,
REMOTE_OWNED@11, WAIT_RESP@12,
RESP_PENDING@18, COMPLETE@20, FREE@21
id_used = 5, gen_used = 1
remote_accepts = 1
responses_received = 1
completions = 1
retired_at = 21
SEMANTIC MEMORY MODEL
address A: value D (unchanged — a read has no side effect)
observed_read_value = D ✓ matchesThe row that matters is transmissions = 2 beside remote_accepts = 1. That combination is duplicate suppression visibly working, and a regression in which it never appears has not tested the mechanism (Chapter 12.2 §21).
5. Memory Read, Diagrammed
6. Example 2 — Memory Write
The same lifecycle with a fundamentally different hazard: a write has a side effect, so a duplicate is not merely untidy.
The operation. The initiator writes 10 bytes to address B. With PROTO_BEAT_B = 8, that is two Protocol-side beats — one full, one carrying 2 valid bytes. With ADAPTER_BEAT_B = 4, the Adapter sees five internal beats, the last of which is partial.
What is different from Example 1, stated before the trace because it is the whole point:
| Read | Write | |
|---|---|---|
| Request-side payload | none | 10 bytes, multi-beat |
payload_done at allocation | already true | false until the last beat is sent |
| Width conversion involved | on the response only | on the request path (12.3 §8) |
| Partial final beat | no | yes — mask matters (12.3 §12) |
| Duplication hazard | a redundant read | the write applied twice |
| Association hazard | response to wrong request | payload to wrong address |
6.1 The write-context table
// ILLUSTRATIVE write-context state. This is the structure that keeps a
// multi-beat payload attached to its metadata — Chapter 12.3 §18's
// reassociation, specialised for writes. NOT a UCIe structure.
typedef struct packed {
logic valid;
logic [TXN_ID_W-1:0] id;
logic [ADDR_W-1:0] addr;
logic [LEN_W-1:0] bytes_expected; // from the request's length
logic [LEN_W-1:0] bytes_seen; // accumulated across beats
logic [MON_ID_W-1:0] mon_id; // VERIFICATION ONLY
} write_ctx_t;
write_ctx_t wctx_q [MAX_TXNS];
// Beat acceptance updates bytes_seen — on the HANDSHAKE only (Ch 12.3 §15).
always_ff @(posedge clk or negedge rst_n) begin
if (!rst_n) begin
for (int c = 0; c < MAX_TXNS; c++) wctx_q[c].valid <= 1'b0;
end else begin
if (wctx_alloc_fire) begin
wctx_q[wctx_idx] <= '{ valid : 1'b1,
id : alloc_id,
addr : req_addr,
bytes_expected : req_len_bytes,
bytes_seen : '0,
mon_id : req_mon_id };
end
if (wbeat_valid && wbeat_ready) begin
wctx_q[wbeat_ctx].bytes_seen
<= wctx_q[wbeat_ctx].bytes_seen + LEN_W'($countones(wbeat_strb));
end
if (wctx_retire_fire) wctx_q[wctx_idx].valid <= 1'b0;
end
end
// The payload is complete when the accumulated byte count matches EXACTLY.
// `>=` would accept an over-long payload, meaning a length mismatch went
// undetected (Ch 11.4 §16's argument, applied to bytes).
assign wctx_complete = wctx_q[c].valid
&& (wctx_q[c].bytes_seen == wctx_q[c].bytes_expected);Architecture. It answers a question the transaction table cannot: how much of this write's payload has actually been accepted? The transaction table knows the operation exists; this knows how far the bytes have got.
State. One entry per in-flight write with per-payload lifetime — allocated with the request, freed when the payload is fully accepted and transmitted. Not freed at transaction retirement, which would hold it for the whole round trip.
Cycle behaviour. bytes_seen advances by the population count of the beat's strobe, on the handshake only. Using the strobe rather than a fixed beat width is what makes a partial final beat count correctly.
Contract. The framing stage relies on wctx_complete before declaring the object whole. The far side relies on receiving exactly bytes_expected bytes.
Failure. Counting a fixed width per beat instead of the strobe population makes the final partial beat over-count, so bytes_seen exceeds bytes_expected and — with a >= completion test — the write completes having sent bytes nobody asked for. With the exact == test it never completes, which is the better failure: a hang rather than corruption.
DV. Payload lengths of one byte, one full beat, and one-full-beat-plus-one; a stall on every beat index; and a beat arriving for a context that is not valid, which must be reported (§6.5).
6.2 Cycle trace — with a stall mid-payload
Illustrative latencies. The stall is injected at cycles 7–9, in the middle of the payload.
| Cyc | Txn state | bytes_seen | Converter | Replay | PHY | Remote | Note |
|---|---|---|---|---|---|---|---|
| 1 | — | — | — | — | — | — | write request presented |
| 2 | DISPATCHED | 0 / 10 | — | — | — | — | txn + write context allocated, id 6 |
| 3 | QUEUED | 0 | — | — | — | — | metadata queued |
| 4 | IN_TRANSPORT | 4 | capture beat 0, slice 0 out | — | — | — | first 4 bytes |
| 5 | IN_TRANSPORT | 8 | slice 1 out; capture beat 1 | — | — | — | 8 of 10 bytes |
| 6 | IN_TRANSPORT | 8 | slice 0 of beat 1, mask = 0x3 | — | — | — | partial: 2 valid bytes |
| 7 | IN_TRANSPORT | 8 | stalled | — | not ready | — | nothing advances |
| 8 | IN_TRANSPORT | 8 | stalled, data stable | — | not ready | — | bytes_seen frozen |
| 9 | IN_TRANSPORT | 8 | stalled, data stable | — | not ready | — | mask still 0x3 |
| 10 | IN_TRANSPORT | 10 | final slice accepted | obj | resumes | — | payload complete |
| 11 | IN_TRANSPORT | 10 | — | obj | in flight | — | framed and sent |
| 14 | REMOTE_OWNED | 10 | — | obj | — | 10 bytes received | mask honoured |
| 15 | WAIT_RESP | 10 | — | obj | — | write applied ONCE | side effect happens here |
| 16 | WAIT_RESP | 10 | — | — | — | — | confirmed → replay retires |
| 19 | RESP_PENDING | 10 | — | — | — | — | completion matched |
| 20 | COMPLETE | 10 | — | — | — | — | consumer accepted |
| 21 | FREE | — | — | — | — | — | retired; id 6 released; context freed |
Five things to read off it.
Cycles 7–9 are the rows Chapter 12.3 §15's bug destroys. bytes_seen stays at 8, the slice pointer does not move, the data and the mask hold. A design advancing on valid alone would count 10 at cycle 8 and declare the payload complete having sent 8 bytes — a two-byte hole at the end of the write.
Cycle 6's mask is 0x3. Two valid bytes of four. Chapter 12.3 §13's bug would send 0xF and the far side would commit two bytes of garbage past the payload's end, into whatever lives there.
Cycle 10 is where bytes_seen reaches bytes_expected exactly. Not >=.
Cycle 15 is where the side effect happens, and it happens once. This is the row that makes a write's duplication hazard concrete: two semantic deliveries here would apply the write twice.
And the write context is freed at cycle 21 in this trace, but it could have been freed at cycle 11 — as soon as the payload was fully transmitted and retained. Holding it to retirement is simpler and costs storage for the round trip; freeing it early is the Chapter 12.3 §28 discipline. Either is defensible; the design must know which it chose.
6.3 Wrong write association
The write-specific version of Chapter 12.3 §16, and it is worth spelling out because the mechanism differs.
How it happens. The request metadata — address B, length 10 — travels through the control path. The payload travels through the wide datapath. If they are rejoined by identity and two writes are in flight with the same identity (Chapter 12.3 §19), or if the identity pipeline and the data pipeline have different depths, write A's payload is committed to write B's address.
Why it is worse than the read equivalent. A misassociated read delivers wrong data to a requester, which may notice. A misassociated write modifies the wrong memory location, and:
- both writes report success;
- the completion for each returns and matches correctly;
- conservation balances — two writes accepted, two completed;
- and two memory locations are now wrong, each holding the other's data.
Nothing in the transport or the transaction layer sees it. The only check that does is one comparing the committed bytes at each address against what that specific write was asked to write, which is §6.7's semantic model.
6.4 The exactly-once side effect
The write's central invariant, and the reason its retry story differs from the read's.
A read applied twice returns the same value twice — wasteful and, in most systems, harmless. A write applied twice is not. If the write is not idempotent — an increment, a doorbell, a queue push, or a byte-enabled partial write over a value that has since changed — the memory state is now wrong, permanently, with no error anywhere.
So the delivery fence (Chapter 11.4 §16) is not an optimisation for writes; it is the mechanism that makes them safe:
// Illustrative — the write's side effect is gated on transport RESOLUTION plus
// duplicate suppression, never on arrival.
assign apply_write = obj_reconstructed
&& (bytes_received == bytes_expected) // exact, §6.1
&& !obj_is_duplicate // Ch 9.4 §12
&& write_order_ok;And the corollary for timeouts, which is Chapter 12.4 §16 applied to this class: a write that times out from REMOTE_OWNED must not be reissued, because the far side certainly applied it. That is the single most consequential phase-dependent decision in the module.
6.5 Assertions
// Illustrative — the write's five invariants.
// Write data only ever arrives against a live context.
property p_write_beat_requires_context;
@(posedge clk) disable iff (!rst_n)
(wbeat_valid && wbeat_ready) |-> wctx_q[wbeat_ctx].valid;
endproperty
a_write_beat_requires_context: assert property (p_write_beat_requires_context);
// The payload never over-runs its declared extent. Catches a fixed-width byte
// count on a partial final beat (§6.1).
property p_write_no_overrun;
@(posedge clk) disable iff (!rst_n)
wctx_q[c].valid |-> (wctx_q[c].bytes_seen <= wctx_q[c].bytes_expected);
endproperty
a_write_no_overrun: assert property (p_write_no_overrun);
// The object is declared complete only on an EXACT byte match.
property p_write_complete_exact;
@(posedge clk) disable iff (!rst_n)
write_object_complete
|-> (wctx_q[c].bytes_seen == wctx_q[c].bytes_expected);
endproperty
a_write_complete_exact: assert property (p_write_complete_exact);
// Nothing advances during a stall — the property cycles 7-9 depend on.
property p_write_no_progress_under_stall;
@(posedge clk) disable iff (!rst_n)
(wbeat_valid && !wbeat_ready)
|=> ($stable(wctx_q[wbeat_ctx].bytes_seen) && $stable(wbeat_data)
&& $stable(wbeat_strb));
endproperty
a_write_no_progress_under_stall:
assert property (p_write_no_progress_under_stall);
// The side effect happens at most once per semantic write.
property p_write_effect_once;
@(posedge clk) disable iff (!rst_n)
apply_write |-> !write_applied_mon[write_mon_id];
endproperty
a_write_effect_once: assert property (p_write_effect_once);6.6 Second injection — a link recovery before the final beat
The stall in §6.2 was benign: the datapath waited and resumed. This injection is not, and it is the one that exercises every lifetime in Module 12 at once.
The scenario. Replay Example 2, and at cycle 8 — with bytes_seen = 8 of 10, one partial beat still to send — the UCIe link enters recovery.
What must survive, and what must not:
| State | Survives recovery? | Why | From |
|---|---|---|---|
Transaction entry, phase IN_TRANSPORT | yes | not link state; the operation is still owed | 12.4 §24 |
| Identity 6 and its generation | yes | the identity's lifetime is the transaction's | 12.4 §13 |
Write context: bytes_seen = 8 | yes | per-payload state, and the 8 bytes were genuinely accepted | §6.1 |
| The two remaining payload bytes in the source buffer | yes | not yet transmitted; still owed | 12.3 §28 |
| Converter capture and slice pointer | local reset is acceptable | per-beat state, reconstructible from bytes_seen | 12.3 §28 |
| Credits | no — re-advertised | link-epoch state, correctly re-established | 9.5 §13 |
| Replay entries | no — re-baselined with the peer | link-epoch state | 9.4 |
| Format epoch | no — re-established, both ends must agree | link-epoch, and distributed | 11.4 §23 |
| Remote partial reconstruction | discarded | the object never completed; must not be mistaken for a short payload | 11.4 §16 |
The three ways designs get this wrong, and each is a bug already named in this module.
Sweeping the transaction table with the link. The write is forgotten while software still waits, and if the link recovers and the far side retained anything, a completion arrives matching nothing — or matching a transaction that reused identity 6 (Chapter 12.4 §25's reset-scope error).
Clearing bytes_seen. The write context restarts at zero while the far side has already reconstructed 8 bytes. On resumption the payload is sent from the beginning, so the far side receives 18 bytes for a 10-byte write — and the exact-match completion test (Chapter 12.3 §28, §6.1) is what turns that into a detected fault rather than a silent over-write.
Treating the remote partial reconstruction as a completed short payload. Eight bytes arrived and the object never completed. A receiver that reclaims the buffer by delivering what it has commits a truncated write. The exact-extent match is the guard, and it must be == rather than >=.
And the decision this injection forces, which no earlier chapter had to make. The write is in IN_TRANSPORT, so Chapter 12.4 §16's table says the outcome is unknown — the far side may or may not have received enough to act. For a write that means:
- if the transport can resume and the remaining bytes complete the object, the write proceeds normally and nothing above ever learns of the recovery — the good case, and the reason retention matters;
- if it cannot, the transaction must move to
FAILEDwith an ambiguous outcome and its identity quarantined, because a partially-received write may or may not have been applied and a reissue could double it.
A partial write interrupted by a recovery is the clearest case in Module 12 where the phase, the payload state, and the reset scope must all be consulted together. Any one of them alone gives the wrong answer.
// Illustrative — the three survival properties this injection needs.
// The transaction table is untouched by a link recovery.
property p_write_txn_survives_recovery;
@(posedge clk) disable iff (!rst_n)
ucie_recovery_event |=> ($stable(txn_valid_vec) && $stable(txn_count_q));
endproperty
a_write_txn_survives_recovery: assert property (p_write_txn_survives_recovery);
// The payload's accepted-byte count is not rolled back.
property p_write_bytes_seen_survives_recovery;
@(posedge clk) disable iff (!rst_n)
(ucie_recovery_event && wctx_q[c].valid)
|=> (wctx_q[c].bytes_seen == $past(wctx_q[c].bytes_seen));
endproperty
a_write_bytes_seen_survives_recovery:
assert property (p_write_bytes_seen_survives_recovery);
// And credits ARE re-advertised — the direction people forget to assert.
property p_credits_readvertised_after_recovery;
@(posedge clk) disable iff (!rst_n)
ucie_recovery_complete |-> credits_readvertised;
endproperty6.7 Scoreboard at retirement
TRANSPORT MODEL
object O2: framed@11, transmitted@11, confirmed@16, retired@16,
transmissions = 1, retries = 0
TRANSACTION MODEL
MON_W1: allocated@2 (count = 1), id 6 gen 1
phase_history = DISPATCHED@2 … COMPLETE@20, FREE@21
completions = 1, retired_at = 21
PAYLOAD MODEL (Ch 12.3 §30)
MON_W1: expected_length = 10 bytes
expected_bytes[] = the exact 10 bytes presented at FDI
expected_final_mask = 0x3 (derived from the length, independently)
observed_bytes[] = 10 bytes reassembled remotely ✓ byte-for-byte
beat_counts = { FDI: 2, adapter: 3 } ✓ per width
SEMANTIC MEMORY MODEL
address B: value = the 10 expected bytes ✓
writes_applied_to_B = 1 ✓ exactly once
bytes_beyond_extent_modified = 0 ✓ mask honouredThe last line is the one §6.5's p_write_no_overrun protects and the mask assertion proves. A model that only checked the 10 requested bytes would pass on Chapter 12.3 §13's bug — the requested bytes would be right and two extra bytes would have been silently committed. Checking what was not modified is as important as checking what was.
7. Example 3 — A Coherent Ownership Change
The class where a duplicate has no address to inspect afterwards.
The operation. An accelerator on the remote die holds line X readable and wants write ownership. Another agent also holds it readable and must be invalidated first.
Initial state:
| Structure | State at cycle 0 |
|---|---|
Line X, accelerator's view | C_SHARED, clean, probe_pending = 0, txn_pending = 0 |
Line X, reference model | value V0; owner none; sharers {host, accel}; pending none |
| Coherence transaction table | empty — no transaction open on X |
| Transaction table | empty |
| Link | operational |
7.1 Cycle trace — with a retry mid-flow
Illustrative latencies. The retry is injected at cycle 8, on the object carrying the ownership request.
| Cyc | Accel line state | Coh txn | Txn state | Replay | Host / other agent | Note |
|---|---|---|---|---|---|---|
| 1 | C_SHARED | — | — | — | sharer | accelerator needs to write X |
| 2 | C_S_TO_X | 1 entry | DISPATCHED | — | sharer | transient state; one txn per line |
| 3 | C_S_TO_X | 1 | QUEUED | — | sharer | on the cache-class queue |
| 4 | C_S_TO_X | 1 | IN_TRANSPORT | obj | sharer | framed; replay retained |
| 6 | C_S_TO_X | 1 | IN_TRANSPORT | obj | sharer | in flight |
| 8 | C_S_TO_X | 1 | IN_TRANSPORT | obj | sharer | CRC fails — discarded |
| 9 | C_S_TO_X | 1 | IN_TRANSPORT | obj re-sent | sharer | retry: no re-allocation |
| 11 | C_S_TO_X | 1 | REMOTE_OWNED | obj | Home Agent accepts ONCE | duplicate suppressed |
| 12 | C_S_TO_X | 1 | WAIT_RESP | obj | probes the other agent | one probe for X |
| 13 | C_S_TO_X | 1 | WAIT_RESP | — | probe outstanding | confirmed → replay retires |
| 15 | C_S_TO_X | 1 | WAIT_RESP | — | probe response: invalidated | clean copy, no data owed |
| 16 | C_S_TO_X | 1 | WAIT_RESP | — | ownership resolved | Home Agent serialised it |
| 18 | C_S_TO_X | 1 | RESP_PENDING | — | grant returning | matched to the transaction |
| 19 | C_EXCLUSIVE | 1 | COMPLETE | — | — | transient state left, once |
| 20 | C_MODIFIED | 0 | FREE | — | — | local write; txn retired |
Seven things to read off it.
Cycle 2 opens exactly one coherence transaction for line X. Chapter 11.3 §15's published restriction — multiple evictions to one line are not allowed, and one snoop per line per device — is the reason a second concurrent ownership attempt on X would be non-conformant.
Cycles 2–18 are all transient. The line is neither C_SHARED nor C_EXCLUSIVE, and during this whole window a local access must be refused (Chapter 11.3 §8). Seventeen cycles of a state that a stable-state-only design cannot represent.
Cycle 9's retry does not open a second transaction. If it did, two ownership transitions would be in flight for one line — Chapter 11.3 §16's failure, where both may believe they won.
Cycle 11 accepts once. This is where the duplicate-suppression stakes are highest: a second semantic acceptance would make the Home Agent process the ownership request twice, and it would probe the other agent twice — for a line on which only one snoop may be outstanding.
Cycle 15's probe response carries no data, because the other agent's copy was clean. Had it been dirty, the specification requires the data be returned to the Host — and the trace would have a data transfer here.
Cycle 19 leaves the transient state exactly once. A design with two independent writers of the line state (Chapter 11.3 §13) could have a probe and this grant collide and produce two write owners.
And cycle 20 is the local write — the point at which memory becomes stale relative to the accelerator's copy, which is a correct state of the system (Chapter 11.3 §20).
7.2 Assertions
// Illustrative — the coherence flow's four invariants. Coherence state names
// are Chapter 11.3 §11's teaching enum, not CXL encodings.
// One semantic coherence allocation per operation, retries notwithstanding.
property p_coh_one_allocation;
@(posedge clk) disable iff (!rst_n)
coh_txn_alloc_fire |-> !coh_allocated_mon[coh_mon_id];
endproperty
a_coh_one_allocation: assert property (p_coh_one_allocation);
// At most one ownership-changing transaction per line — Ch 11.3 §15's
// published restriction, enforced locally.
property p_coh_one_txn_per_line;
@(posedge clk) disable iff (!rst_n)
coh_txn_alloc_fire |-> $onehot0(same_line_vec);
endproperty
a_coh_one_txn_per_line: assert property (p_coh_one_txn_per_line);
// A local access is served only from a permitted stable state — never from a
// transient one, which is cycles 2 through 18 of the trace.
property p_coh_access_only_when_permitted;
@(posedge clk) disable iff (!rst_n)
local_access_served |-> (read_allowed(line_state_q) && !probe_pending_q);
endproperty
a_coh_access_only_when_permitted:
assert property (p_coh_access_only_when_permitted);
// The ownership transition happens at most once per transaction.
property p_coh_ownership_change_once;
@(posedge clk) disable iff (!rst_n)
ownership_transition_fire |-> !ownership_changed_mon[coh_mon_id];
endproperty
a_coh_ownership_change_once: assert property (p_coh_ownership_change_once);
// The transaction retires only after ownership is actually resolved.
property p_coh_retire_after_resolution;
@(posedge clk) disable iff (!rst_n)
coh_txn_retire_fire |-> (line_state_q inside {C_EXCLUSIVE, C_MODIFIED});
endproperty7.3 Scoreboard — before, during, and after
LINE X, reference model
BEFORE (cycle 1)
latest_value = V0
owner = none
sharers = { host, accel }
pending = none
accel_state = C_SHARED
DURING (cycle 12 — request accepted remotely, probe outstanding)
latest_value = V0
owner = none (transferring)
sharers = { host, accel }
pending = { ownership txn T1 for accel, probe P1 to host }
accel_state = C_S_TO_X ← transient, and REPRESENTED
AFTER (cycle 20)
latest_value = V1 (accelerator's local write)
owner = accel
sharers = { } (host invalidated at cycle 15)
pending = none
accel_state = C_MODIFIED
dirty_at = accel ← memory is now STALE, correctly
INVARIANTS CHECKED
ownership_transitions(T1) = 1 ✓ despite 2 transmissions
probes_issued_for_X = 1 ✓ one snoop per line
concurrent_txns_on_X = 1 ✓ never 2
accesses_from_transient = 0 ✓ cycles 2-18 refused
write_owners_simultaneous = 1 ✓ never 2The dirty_at = accel line is the one that closes Module 11's argument. Memory holds V0 and the true value is V1, held only by the accelerator. That is not a bug — it is the normal condition whenever any agent holds modified data, and coherence exists so that nobody reads memory in that state without asking (Chapter 11.3 §20).
7.4 Diagrammed
8. The Three Classes Compared
| Aspect | Memory read | Memory write | Coherent ownership |
|---|---|---|---|
| Request-side payload | none | the data | none (metadata only) |
| Response-side payload | the data | completion only, where the protocol defines one | a grant; data if the probed agent was dirty |
| Outstanding state | required | required | required, plus per-line transient state |
| Width conversion path | response | request | neither, typically — the object is small |
| Partial final beat | possible on the response | likely on the request | not applicable |
| Duplicate hazard | a redundant read | the side effect applied twice | the ownership action performed twice |
| Is a duplicate detectable afterwards? | usually harmless | inspect the address | no address to inspect |
Timeout from REMOTE_OWNED | reissue often safe (idempotent) | reissue unsafe | reissue unsafe and unrecoverable |
| Final completion | the response is consumed | semantic completion, protocol-defined | ownership resolved and the transient state left |
| What a packet scoreboard misses | wrong data to the right request | wrong bytes, or bytes past the extent | everything that matters |
The row worth dwelling on is the seventh. A duplicated read wastes bandwidth. A duplicated write corrupts a location you can go and look at. A duplicated ownership action corrupts distributed state that has no location — the system's belief about who may write a line — and the only way to see it is a model that tracks owners and sharers.
And the eighth row is the module's most consequential design rule. Whether a timeout may be followed by a reissue depends on the transaction class and the phase (Chapter 12.4 §16), and for two of the three classes the answer from REMOTE_OWNED is no.
9. The Common Lifetime Pattern
Despite those differences, all three examples traced the same seven steps:
- Semantic accept — the operation is admitted, and admission includes table space, identity availability, replay capacity, and credit.
- State allocation — exactly once, at the semantic boundary, with the identity claimed and its generation bumped.
- Mapping — classification, framing, header and CRC.
- Transport — one or more physical attempts, with the object retained until confirmed.
- Remote semantic action — accepted once, and the effect applied once.
- Return — a response or a grant, matched against a still-live entry.
- Retirement — after the consumer accepts, releasing the entry and the identity.
That sequence is the durable model, and it is what makes the three classes comparable at all. What varies between them is what happens at step 5 and what a duplicate at step 5 costs.
10. The Master Conservation Model
One equation for the whole module, and its clause is what ties the four chapters together.
accepted_semantic_ops = completed + outstanding + failedTransport replays do not increase
accepted_semantic_ops. A retransmission is another physical attempt at a transport object; it is not an operation. Every trace in this chapter transmitted at least one object twice and incrementedaccepted_semantic_opsexactly once.
Three companion equations, one per chapter, and they must all hold simultaneously:
| Level | Equation | From |
|---|---|---|
| Request path | accepted = remote_accepted + in_path + aborted | 12.1 §29 |
| Response path | requests_accepted = completed + in_flight + abandoned | 12.2 §32 |
| Payload | bytes_accepted = bytes_delivered + bytes_in_flight + bytes_aborted | 12.3 §29 |
| Lifecycle | allocated = retired + live + failed_not_yet_retired | 12.4 §23 |
Why four equations and not one. Each is counted in different units at different boundaries, and a bug can satisfy three while violating the fourth. A dropped beat balances the transaction equations and violates the byte equation. A double allocation balances the byte equation and violates the lifecycle equation. Checking all four is what makes the set complete, and it is cheap: each is a handful of counters compared each cycle.
And what none of the four proves: that any operation was paired correctly. Every mispairing bug in Module 12 — Chapter 12.3 §16's identity misalignment, Chapter 12.2 §16's FIFO assumption, Chapter 12.2 §25's stale alias, §6.3's write misassociation — produces perfectly balanced counts. Balance is necessary and never sufficient, which is why §13's third scoreboard layer exists.
11. The Failure Matrix
The practical table, organised by where the fault is rather than by what it looks like.
| Stage | Symptom | Likely bug | Best evidence |
|---|---|---|---|
| Request queue | request never leaves; source stalls | which admission veto is low | 12.1 §10; per-veto counters |
| Request queue | request accepted then vanishes | occupancy drift from two count updates | 12.1 §29's equation, per cycle |
| Mapping | valid object, wrong contents | metadata/payload misalignment | 12.3 §16; the header/payload source-tag property |
| Mapping | corruption after a config event | flit-format or lane-map epoch | 11.4 §11; 12.3 §26 |
| Datapath | wrong bytes past the payload's end | byte-mask width or full-mask default | 12.3 §12, §13; final-mask assertion |
| Datapath | corruption only under stalls | progress without a handshake | 12.3 §15's no-progress property |
| Datapath | bytes permuted, none missing | lane-map committed mid-beat | 12.3 §26; map-stability property |
| Replay | unrecoverable after one CRC error | accepted without replay capacity or contents | 12.1 §11; 12.3 §27 |
| Replay | transaction table fills over time | allocation on a transport event | 12.4 §8; one-allocation property |
| PHY | CRC errors, retries succeed | physical margin | Module 7 — not a datapath bug |
| Remote execution | request never answered | remote or return path; check the phase | 12.4 §31's phase table |
| Remote execution | side effect applied twice | semantic delivery keyed on arrival | §6.5's effect-once property; look for a lost confirmation |
| Response match | response matches nothing | entry retired early, or a late response | 12.2 §8, §25 |
| Response match | wrong data to the right request | FIFO assumption, or response bundling | 12.2 §13, §16 |
| Response match | intermittent corruption after timeouts | identity reused before quarantine | 12.2 §25; stale-rejection counter non-zero |
| Coherence | stale data, link entirely clean | ownership or data-obligation bug | 11.3 §33; per-line semantic model |
| Coherence | two agents behave as owners | two state writers, or two txns per line | 11.3 §13, §16 |
| Coherence | requests hang, nothing times out | channel dependency cycle | 11.3 §28 — all safety assertions pass |
12. Four Worked Failures
Each of these is one row of §11, developed enough to be recognisable.
12.1 A lost write beat
Symptom. The final memory value at address B is wrong — specifically, a contiguous run of bytes in the middle is stale.
The trace. Replaying Example 2 with the stall at cycles 7–9 and a beat counter that advances on valid: bytes_seen reaches 10 at cycle 8 while only 8 bytes were transferred. The object is declared complete and framed with 8 bytes of payload.
Root cause. Progress advanced without a handshake (Chapter 12.3 §15).
Why it is stall-dependent. On an unstalled link the counter and the transfers agree, so the write is correct. The same test passes in isolation and fails under congestion, and the position of the missing bytes tracks where the stall occurred.
The evidence. p_write_no_progress_under_stall fires in the cycle it happens. Without it, the byte-level payload model catches it at the sink, and the offset of the first diverging byte names the beat that was skipped.
12.2 A duplicated memory read
Symptom. Two responses return for one request identity. The second matches nothing, or matches a later transaction.
The trace. A lost confirmation — not a corruption. The request arrived intact; its acknowledgement did not; the Adapter retransmitted; the far side saw the same object twice. With semantic acceptance keyed on arrival, the remote memory read twice and returned two responses.
Root cause. Delivery keyed on transport arrival rather than resolution (Chapter 11.4 §17).
Why "harmless for a read" is wrong. The read itself is idempotent, so the data is fine. But the second response arrives at a transaction that has already retired, so it either is dropped — losing the evidence — or matches a transaction that reused identity 5, delivering the old read's data to a new requester. The accounting breaks even when the operation does not.
The evidence. p_read_remote_accept_once fires at the second acceptance. And the transport model's transmissions = 2 beside remote_accepts = 2 is the signature: the correct pairing is 2 and 1.
12.3 A stale response aliasing a new transaction
Symptom. Intermittent wrong data, beginning after a period of link stress and continuing, uncorrelated with the transaction that reports it.
The trace. A read on identity 5 is delivered and executed; its response is delayed; the local side times out from WAIT_RESP and reports a failure; identity 5 is released rather than quarantined; a new transaction takes identity 5; the old response arrives and matches it cleanly.
Root cause. Identity reuse before the ambiguity was resolved (Chapter 12.2 §25; Chapter 12.4 §12).
Why every check passes. The match is one-hot. Conservation balances — the same number of completions as requests. The CRC was clean both times. The pairing is wrong and nothing about the failing transaction is anomalous, so an engineer examining it finds it flawless.
The evidence. The generation check rejects it and logs it. And the diagnostic tell is temporal: correlate with earlier timeouts, not with the corrupted transaction.
12.4 Coherence stale data with a perfect link
Symptom. The accelerator computes on a value the host has since changed. Zero CRC errors, zero retries, zero credit violations, zero protocol errors.
The trace. Replaying Example 3 with a probe handler that computes its data obligation from C_MODIFIED alone: a line in C_X_TO_I — being given up, still holding modified data — is probed and answers with no data, because the state is not literally modified. The Home Agent then reads memory, which is stale.
Root cause. A probe response computed from stable states only (Chapter 11.3 §18).
Why it is the module's most important failure. Every transport mechanism worked perfectly. The request was delivered once, the probe was delivered once, the response was well formed and legal, and the answer was a lie about the state of the world. This is the concrete form of the claim Module 11 kept making: a clean transport scoreboard is entirely consistent with total semantic failure.
The evidence. Only the per-line semantic model — value, owner, sharers, dirty-holder — sees it, by noticing that a read returned a value the model says was superseded.
13. The Three-Layer Scoreboard
The architecture all three examples used, and what each layer uniquely catches.
JOIN KEY — the verification-only monitor tag. Required at all three layers,
because the protocol identity is reused across attempts and generations, and
the transport identity is invisible above the mapping layer.
LAYER 1 — TRANSPORT MODEL
per object: framed_at, transmissions[], crc_events[], confirmed_at, retired_at
per link: retry_count, credit_history, format_epoch
INVARIANT: every object delivered at least once and eventually retired
LAYER 2 — TRANSACTION MODEL
per operation (by tag): allocated_at (== 1), phase_history[], id, gen,
remote_accepts (== 1), responses, completions (== 1),
retired_at (== 1), first_fail_cause
INVARIANT: exactly once, legal phases, retired only after resolution
LAYER 3 — SEMANTIC MODEL
memory: value per address; writes_applied per address; bytes_beyond_extent
coherence: per line — value, owner, sharers[], dirty_at, pending[]
INVARIANT: every observed value was one the agent was permitted to observe| Layer | Catches | Blind to |
|---|---|---|
| Transport | CRC storms, lost objects, replay-occupancy bugs, format-epoch violations | every duplicate semantic action — from its view, retransmitting is correct |
| Transaction | double allocation, illegal phase transitions, early retirement, identity reuse | wrong data with correct bookkeeping — mispairing balances perfectly |
| Semantic | stale reads, duplicated side effects, wrong-address writes, bytes past the extent, ownership violations | why — it says a value was wrong, not which stage did it |
The pairing is what makes a diagnosis possible. The semantic layer says that something is wrong; the transaction layer says which operation; the transport layer says what happened to it. Any two of the three leaves a question unanswerable, and the most common gap is having layers 1 and 2 and calling it verification — which passes on §12.4.
14. Coverage Strategy
The temptation with five chapters of mechanisms is a Cartesian product. Resist it: cover combinations that interact, not every pair.
| Cross | Why it interacts |
|---|---|
| transaction class × stall location | a stall on a read's response and on a write's payload exercise different state (12.3 §15 versus 12.2 §11) |
| transaction class × retry | the duplicate hazard differs per class (§8's sixth row) |
| transaction class × lost confirmation | the only fault producing a genuine duplicate, and the consequence is class-specific |
| payload length class × conversion ratio | the partial final beat interacts with the converter's flush (12.3 §10, §12) |
| response ordering × outstanding depth | the FIFO assumption is invisible at depth 1 (12.2 §16) |
| timeout phase × transaction class | reissue safety depends on both (12.4 §16; §8's eighth row) |
| identity reuse × delayed response | the stale alias needs both, in order (12.2 §25) |
| coherence state × retry | a retry while a line is transient is the module's hardest case |
| recovery × lifecycle phase | six phases with six different safe actions (12.4 §24) |
Three bins that must be non-zero rather than zero, because their value is proof that a defence ran: duplicate-suppressed count, stale-response-rejected count, and late-response-logged count. A regression reporting zero for any of them has either never injected the fault or has a broken defence, and those are indistinguishable from outside.
And three that must stay at zero: two concurrent transactions on one cache line; two write owners; an identity reallocated from quarantine. Writing them down converts assumptions into checked facts.
15. The Full Debug Methodology
For any failed transaction, in this order. The ordering is the method.
- Identify the semantic operation and its monitor tag. Not the packet, not the flit — the operation.
- Confirm the source accepted it, and exactly once.
- Read the lifecycle phase. Chapter 12.4 §31 — six of ten signatures are distinguished by this alone.
- Inspect the transaction entry: identity, generation, age, retry count, first failure cause.
- Inspect the payload state: bytes expected, bytes seen, the final mask, and whether progress advanced only on handshakes.
- Inspect the mapping entry: class, format epoch, and whether metadata and payload came from the same source object.
- Inspect the replay state: allocated once, retained, immutable, and not re-allocated on retry.
- Inspect the physical transfer: CRC events, retries, and whether the lane map moved.
- Confirm the remote semantic acceptance count is one.
- Inspect the remote action: was the effect applied, and once?
- Inspect the return transport: did a response leave, and did it arrive?
- Inspect the response match: one-hot, right generation, right phase.
- Confirm the final consumer accepted before anything retired.
- Compare the transport model. Objects, transmissions, confirmations.
- Compare the semantic model. Values, owners, sharers, bytes committed.
- Identify the first divergence, not the last symptom.
Step 16 is the whole method and step 3 is what makes it fast. The four worked failures in §12 all present far from their causes — a stall-dependent write hole, a read duplicated by a lost acknowledgement, corruption correlated with an earlier timeout, and a stale coherent read with a flawless link. In every one, the last symptom points at the wrong stage, and the first divergence in the layered models points at the right one.
16. Common Misconceptions
"Request, payload, and transaction are the same lifetime." Four lifetimes: the semantic transaction, the transport object inside it, each physical attempt inside that, and the payload — which for a read does not exist on the forward path at all, and for a write can be entirely confirmed with the transaction still open (12.3 §4, 12.4 §3).
"A transport replay creates another semantic transaction." It is another physical attempt at the same object. Every trace in this chapter transmitted an object twice and allocated once; allocating on a transport event leaves orphaned entries that leak identities until the table fills (12.4 §8).
"A clean CRC means end-to-end correctness." CRC proves the bytes that arrived are the bytes that were sent. Misassociation, misalignment, duplicate delivery, stale responses, and every coherence failure pass it, because they are failures of association or of state rather than of transmission (§12.4).
"Memory reads are always harmless to replay." The data is idempotent; the accounting is not. A second response arrives at a retired transaction and is either dropped — destroying the evidence — or matched against a transaction that reused the identity (§12.2).
"Writes can be retried blindly." A write that timed out from REMOTE_OWNED certainly executed. Reissuing a non-idempotent write applies it twice, permanently, with no error anywhere — and the reissue enters as a new semantic operation, so transport-level duplicate suppression does not apply (§6.4).
"A response identity alone prevents a stale alias." It does not, once the identity has been reused. A generation carried with the request and reflected in the response is what closes the window, and a quarantine narrows it (12.2 §24; §12.3).
"Coherence correctness can be verified with a packet scoreboard." Example 3's failure delivers every message exactly once, correctly framed and correctly matched, and returns a stale value — because a probe response was computed from stable states only. Only a per-line model of value, owner, sharers, and dirty-holder sees it (§12.4).
"Once the remote side accepts, local state can be cleared." REMOTE_OWNED is three phases short of retirement. The far side owes a response, and clearing the entry leaves it nowhere to match (12.4 §14).
"If all FIFOs are in range, transaction flow is correct." Two independent count updates keep every count a small legal number while drifting until an entry is overwritten. And every mispairing bug in Module 12 balances all four conservation equations perfectly (§10).
"The last visible failure is the root cause." Failures cascade, and a write-once first-cause field is the cheapest diagnostic in the module. Across many transactions, an unguarded field also destroys the distribution of causes, which is the information that would identify the broken mechanism (12.4 §20).
17. Understanding Check
18. Module 12 Complete
Five chapters, from one interface handshake to three complete transaction classes.
12.1 Request Flow — a request is passed through ownership boundaries, not copied through layers; and a timeout is an absence of information.
12.2 Response Flow — a response closes an obligation created earlier, so it cannot be understood without the retained request state; and a reused identity turns a late response into silent corruption.
12.3 Data Flow — control says what the transaction means, data flow says where the bytes are; a payload has one beat count per interface, so conservation is counted in bytes.
12.4 Transaction Lifecycle — a transaction is an obligation with a lifetime, and physical transmission is one event inside it rather than either end of it.
12.5 End-to-End Examples — three classes, three duplication hazards, one lifetime pattern, and four conservation equations that must all hold at once.
The through-line: every mechanism in this module exists to keep a semantic operation happening exactly once, in an order the protocol permits, with its bytes and its identity intact — across a transport that is free to retransmit whenever reliability requires it. Module 12's real contribution is the habit of asking, for any observed failure, which layer's model diverged first, and knowing that the answer is almost never the layer that reported the symptom.
19. What's Next
We can now follow every transaction and every byte through the link, and prove that nothing was lost, duplicated, reordered, or retired early.
What has been assumed throughout is that the resources those transactions consume were available. Every trace in this chapter had a credit when it needed one, a replay entry when it needed one, and queue space when it needed one — and Module 12 treated each of those as a precondition to check rather than a mechanism to build.
That mechanism is the next module's subject: how a UCIe link prevents perfectly tracked transactions from overrunning finite buffers when traffic becomes sustained rather than occasional:
- 13.1 — Credit-Based Flow Control — L-credit accounting at each layer.
Browse the full path on the UCIe tutorials index.