Flow Control Updates — A Counter, Not a Delta

Chapter 15.1 named the Flow Control category and handed it forward. This is that chapter — and it is narrower than it first appears, because Module 16 owns the credit system: the pools, what a transmitter spends, and how it decides it may send.

What this chapter owns is the packet and its decode, and that turns out to contain the single most dangerous misreading in the Data Link Layer.

What does a Flow Control update DLLP actually carry, and how does a receiver of that update turn it into newly-available capacity without inventing space that does not exist?

1. What This Chapter Owns

The curriculum splits flow control across two modules, and the split is worth stating before anything else.

So this chapter builds the update receiver and the arithmetic it needs, and its output is one thing: a decoded credit-return event — this pool just gained this many credits. Module 16 consumes that event and owns everything downstream of it. §8 holds no availability counter, no consumption input and no eligibility logic, and §10's P11 asserts that boundary rather than merely stating it.

2. The Verified Mechanism

3. Credits Are Not a Ready Signal

The first thing to unlearn, because the intuition is a valid/ready handshake and this is not one.

4. Header Credits and Data Credits Count Different Things

One data credit is 16 bytes. One header credit is one header. That asymmetry is not an inconsistency — it reflects what the receive buffer actually holds.

A receiver's storage for a packet has two parts. Header information goes into a structure sized by the number of packets it can hold; payload goes into a data buffer sized in bytes. So the two are counted in their natural units: packets and 16-byte quantities.

5. Cumulative, Not Incremental

The chapter's central fact, and the source of its worst bug.

An update carries the total number of credits issued since initialisation, modulo the field width. It does not carry "how many I am adding now."

update #1:  DataFC = 511      ← total issued so far
receiver frees 64 DW  =  16 credits
update #2:  DataFC = 527      ← 511 + 16, still a TOTAL

The newly-returned capacity is the difference:

returned = (new_value − last_seen_value)  mod  M

6. The Counter Wraps

HdrFC is 8 bits and DataFC is 12. Both wrap — and the difference must be taken modularly, for exactly the reason Chapter 14.5 gave.

DataFC, mod 4096
 
last seen:   4090
new value:      6
 
returned = (6 − 4090) mod 4096 = 12          ← correct
naive:    6 − 4090            = −4084        ← nonsense

In fixed-width unsigned logic the subtraction wraps for free — new - old on a 12-bit value is the modular difference. Widening the operands first destroys it, exactly as it did for sequence numbers (Chapter 14.5 §8).

7. RTL — Modular Update Decode

// SYNTHESIZABLE. Decode one credit update into newly-returned capacity.
// The cumulative representation and the modular difference: NORMATIVE for
// the conventional representation (section 2). The field widths are
// parameters because the mechanism is architectural and the widths are not.
package fc_pkg;
 
  // Which accounting a given update refers to. NORMALIZED INTERNAL
  // METADATA — not a wire encoding; Chapter 15.1 declined those and this
  // chapter does not add them.
  typedef enum logic [1:0] {
    FC_POSTED   = 2'd0,
    FC_NONPOST  = 2'd1,
    FC_COMPL    = 2'd2,
    FC_INVALID  = 2'd3
  } fc_class_e;
 
  typedef enum logic {
    FC_HEADER = 1'b0,
    FC_DATA   = 1'b1
  } fc_kind_e;
 
endpackage

import fc_pkg::*;
 
// COMBINATIONAL. The newly-returned amount between two cumulative values.
// Fixed-width unsigned subtraction IS modular subtraction (Chapter 14.5
// section 8). Widening the operands first would destroy the wrap.
function automatic logic [FC_W-1:0] fc_returned
    (input logic [FC_W-1:0] new_total, input logic [FC_W-1:0] last_total);
  fc_returned = new_total - last_total;
endfunction

Classification: synthesizable (function; package: compile-time).

What it is. One subtractor, and nothing else. What it is not: a validity test. The result is always representable and always looks plausible — checking whether it is believable needs the pool's capacity, which is §8's.

The mistake it prevents is the one §6 names: widening before subtracting, or reaching for %. Both produce a value that is correct away from the wrap and wrong at it, which is the hardest failure profile there is.

8. RTL — Per-Pool Baseline Tracker

// SYNTHESIZABLE. Per-pool cumulative-baseline tracking: turn a stream of
// cumulative FC update totals into discrete "this much was returned" events.
// The cumulative representation and the modular difference: NORMATIVE
// (section 2). The pool indexing, the plausibility bound and the error
// outputs: ILLUSTRATIVE.
//
// THERE IS NO AVAILABLE-CREDIT COUNTER HERE, and no consumption input.
// Those are Module 16's.
module fc_update_tracker #(
  parameter int FC_W  = 12,     // 8 for header, 12 for data (section 2)
  parameter int POOLS = 6,      // P/NP/Cpl x header/data
  // POOL INDEX WIDTH, guarded at the minimum. $clog2(1) is 0, and a
  // zero-width port is not a legal index -- so the one-pool configuration
  // must be special-cased HERE, in the parameter, rather than everywhere a
  // pool index appears. Do not write $clog2(POOLS) in a port declaration.
  parameter int POOL_W = (POOLS <= 1) ? 1 : $clog2(POOLS),
  // The largest single return this model will believe. A receiver cannot
  // free more than its buffer holds; anything larger indicates a decode
  // fault rather than capacity. Module 16 owns the real bound.
  parameter int MAX_RETURN = 512
) (
  input  logic clk,
  input  logic rst_n,
 
  // ---- Initialisation, from InitFC (section 2) -------------------------
  input  logic                       init_valid,
  input  logic [POOL_W-1:0]          init_pool,
  input  logic [FC_W-1:0]            init_total,
 
  // ---- Credit update in ------------------------------------------------
  // A CUMULATIVE total, not a delta (section 5).
  input  logic                       upd_valid,
  output logic                       upd_ready,
  input  logic [POOL_W-1:0]          upd_pool,
  input  logic [FC_W-1:0]            upd_total,
 
  // ---- Decoded return event out, to Module 16's credit management ------
  output logic                       ret_valid,
  input  logic                       ret_ready,
  output logic [POOL_W-1:0]          ret_pool,
  output logic [FC_W-1:0]            ret_count,
 
  // ---- Reported conditions ---------------------------------------------
  output logic                       err_uninit,
  output logic                       err_implausible,
  output logic                       err_bad_pool
);
 
  localparam int PW = POOL_W;
 
  generate
    if (FC_W  < 2)       $error("FC_W must be at least 2");
    if (POOLS < 1)       $error("POOLS must be at least 1");
    // An integrator who overrides POOL_W too narrowly would silently alias
    // pool indices. Caught at elaboration rather than in simulation.
    if (POOL_W < 1)      $error("POOL_W must be at least 1");
    if ((POOLS > 1) && ((1 << POOL_W) < POOLS))
      $error("POOL_W too narrow to index POOLS");
  endgenerate
 
  // The ONLY per-pool state this chapter owns: what total we last accepted.
  logic [FC_W-1:0]  last_q [POOLS];
  logic [POOLS-1:0] init_q;
 
  // RANGE SAFETY: a PW-wide index can express values >= POOLS whenever
  // POOLS is not a power of two (the class of bug fixed in Chapters 12.1,
  // 12.3 and 14.4). Checked one bit wider, before any array access.
  localparam int CHK = PW + 1;
  wire upd_pool_legal  = (CHK'(upd_pool)  < CHK'(POOLS));
  wire init_pool_legal = (CHK'(init_pool) < CHK'(POOLS));
 
  logic [FC_W-1:0] last_sel;
  logic            init_sel;
  always_comb begin
    last_sel = '0; init_sel = 1'b0;
    if (upd_pool_legal) begin
      last_sel = last_q[upd_pool];
      init_sel = init_q[upd_pool];
    end
  end
 
  // MODULAR DIFFERENCE against the last accepted total (section 6).
  wire [FC_W-1:0] returned = fc_returned(upd_total, last_sel);
 
  // Plausibility. A difference is always representable, so it always looks
  // valid — the bound is what makes it believable (section 6).
  wire plausible = init_sel && (returned <= FC_W'(MAX_RETURN));
 
  // ---- Output holding stage --------------------------------------------
  // Module 16 may be busy. A decoded return event must NOT be dropped: the
  // cumulative representation makes a lost UPDATE harmless (section 9), but
  // a lost decoded EVENT is capacity that was measured and thrown away.
  logic                  ret_v_q;
  logic [PW-1:0]         ret_p_q;
  logic [FC_W-1:0]       ret_c_q;
 
  wire ret_fire = ret_v_q && ret_ready;
 
  // Accept an update when the output stage is empty or draining this cycle.
  assign upd_ready = !ret_v_q || ret_ready;
 
  wire accept = upd_valid && upd_ready;
  // A zero-valued return is a legitimate no-op (a duplicate update,
  // section 5) and is consumed WITHOUT producing an event.
  wire emit   = accept && upd_pool_legal && plausible && (returned != '0);
 
  assign ret_valid = ret_v_q;
  assign ret_pool  = ret_p_q;
  assign ret_count = ret_c_q;
 
  logic uni_q, imp_q, bad_q;
  assign err_uninit      = uni_q;
  assign err_implausible = imp_q;
  assign err_bad_pool    = bad_q;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      for (int i = 0; i < POOLS; i++) last_q[i] <= '0;
      init_q <= '0;
      ret_v_q <= 1'b0; ret_p_q <= '0; ret_c_q <= '0;
      uni_q <= 1'b0; imp_q <= 1'b0; bad_q <= 1'b0;
    end else begin
      if (init_valid && init_pool_legal && !init_q[init_pool]) begin
        last_q[init_pool] <= init_total;
        init_q[init_pool] <= 1'b1;
      end
 
      // The baseline advances ONLY on an update this block ACCEPTED and
      // believed. Advancing it on a rejected one would measure the next
      // difference from a total the sender never sent, losing that capacity
      // permanently (section 9).
      if (accept && upd_pool_legal && plausible)
        last_q[upd_pool] <= upd_total;
 
      // Output stage: emit has priority over drain, so a same-cycle
      // accept-and-consume leaves the new event held rather than lost.
      if (emit) begin
        ret_v_q <= 1'b1;
        ret_p_q <= upd_pool;
        ret_c_q <= returned;
      end else if (ret_fire) begin
        ret_v_q <= 1'b0;
      end
 
      if (upd_valid && !upd_pool_legal)                bad_q <= 1'b1;
      if (upd_valid &&  upd_pool_legal && !init_sel)   uni_q <= 1'b1;
      if (upd_valid &&  upd_pool_legal &&  init_sel
                    && (returned > FC_W'(MAX_RETURN))) imp_q <= 1'b1;
    end
  end
 
endmodule

Classification: synthesizable.

Architecture. One baseline register per pool and one output holding stage. That is the entire state — there is no availability counter anywhere in the module, because availability is Module 16's.

Cycle behaviour.

Contract. The producer holds an update stable while upd_valid is asserted and upd_ready is low. Module 16 consumes ret_* on a valid/ready handshake and is responsible for everything downstream of "this pool gained this many."

Failure — five, and §11 maps each. Adding upd_total rather than the modular difference treats a total as a delta (§5). Widening the operands before subtracting destroys the wrap (§6). Advancing the baseline on a rejected update loses the next update's capacity permanently. Dropping a decoded event under backpressure throws away capacity that was correctly measured — and unlike a lost update, that is not recoverable by the next one. And indexing last_q before the pool bounds check breaks at any non-power-of-two POOLS.

Deliberately simplified: no availability, no consumption, no eligibility, no per-class cost — all Module 16's; a single plausibility constant rather than a per-pool capacity; one update per cycle.

9. The Update Interface Contract

Credit updates arrive as decoded DLLP events (Chapter 15.1 §5), and that raises the same ownership question Chapter 14.2 §8 had.

This model accepts at most one update per pool per cycle, and the update input is not backpressurable.

10. Assertions

// SVA over fc_update_tracker. These assert the NORMATIVE cumulative decode
// of section 2 and the LOCAL tracker contract. There is deliberately NO
// property here about credit availability, consumption cost, or packet
// eligibility — Module 16 owns those, and asserting them here would mean
// this chapter had implemented them.
 
// ---- ENVIRONMENT -----------------------------------------------------
// A1: the producer holds an offered update stable until accepted.
assume property (@(posedge clk) disable iff (!rst_n)
  (upd_valid && !upd_ready)
    |=> (upd_valid && $stable({upd_pool, upd_total})));
 
// ---- SAFETY ----------------------------------------------------------
 
// P1: THE CENTRAL PROPERTY. The emitted return count is the MODULAR
// DIFFERENCE from the last accepted total — never the total itself. The one
// a delta-interpreting design fails on its first update.
property p_return_is_modular_difference;
  @(posedge clk) disable iff (!rst_n)
  emit |=> (ret_count == $past(upd_total) - $past(last_sel));
endproperty
a_modular : assert property (p_return_is_modular_difference);
 
// P2: A DUPLICATE UPDATE EMITS NOTHING. The idempotence of section 5,
// stated directly — and what catches `ret_count = upd_total`.
property p_duplicate_emits_nothing;
  @(posedge clk) disable iff (!rst_n)
  (accept && upd_pool_legal && plausible && (upd_total == last_sel))
    |-> !emit;
endproperty
a_duplicate_noop : assert property (p_duplicate_emits_nothing);
 
// P3: THE WRAP PROPERTY. Checked against an independent reference
// (section 11), so a design that widened its operands cannot pass by
// agreeing with itself.
property p_wrap_difference_correct;
  @(posedge clk) disable iff (!rst_n)
  emit |-> (ret_count == ref_returned(upd_total, last_sel, FC_W));
endproperty
a_wrap : assert property (p_wrap_difference_correct);
 
// P4: the baseline advances ONLY on an accepted, believed update.
// Advancing on a rejected one measures the next difference from a total the
// sender never sent, losing that capacity permanently (section 9).
generate for (genvar g = 0; g < POOLS; g++) begin : g_baseline
  a_baseline : assert property (@(posedge clk) disable iff (!rst_n)
    !$stable(last_q[g])
      |-> ($past(accept && upd_pool_legal && plausible
                && (upd_pool == PW'(g)))
        || $past(init_valid && init_pool_legal && (init_pool == PW'(g)))
        || $past(!rst_n)));
end endgenerate
 
// P5: POOL ISOLATION. An update for one pool never disturbs another's
// baseline. Per-pool, so a write to the wrong index cannot hide.
generate for (genvar g = 0; g < POOLS; g++) begin : g_isolation
  a_isolation : assert property (@(posedge clk) disable iff (!rst_n)
    (accept && upd_pool_legal && (upd_pool != PW'(g))) |=> $stable(last_q[g]));
end endgenerate
 
// P6: NO DECODED EVENT IS LOST. A measured return that the consumer has not
// taken is still offered next cycle. Unlike a lost UPDATE (section 9), a
// lost decoded EVENT is unrecoverable.
property p_no_event_lost;
  @(posedge clk) disable iff (!rst_n)
  (ret_valid && !ret_ready) |=> (ret_valid && $stable({ret_pool, ret_count}));
endproperty
a_no_loss : assert property (p_no_event_lost);
 
// P7: SAME-CYCLE emit and consume — the new event is HELD, not lost.
property p_emit_wins_over_drain;
  @(posedge clk) disable iff (!rst_n)
  (emit && ret_fire) |=> (ret_valid && (ret_count == $past(returned)));
endproperty
a_emit_priority : assert property (p_emit_wins_over_drain);
 
// P8: an implausible update is REPORTED and NOT APPLIED — no event, and the
// baseline does not move.
property p_implausible_rejected;
  @(posedge clk) disable iff (!rst_n)
  (upd_valid && upd_pool_legal && init_sel && (returned > FC_W'(MAX_RETURN)))
    |-> !emit ##1 err_implausible;
endproperty
a_implausible : assert property (p_implausible_rejected);
 
// P9: an out-of-range pool index touches nothing. The range-safety class of
// bug fixed in Chapters 12.1, 12.3 and 14.4, reappearing here.
property p_bad_pool_inert;
  @(posedge clk) disable iff (!rst_n)
  (upd_valid && !upd_pool_legal) |-> (!emit ##1 err_bad_pool);
endproperty
a_bad_pool : assert property (p_bad_pool_inert);
 
// P10: nothing is decoded before that pool is initialised.
property p_uninit_inert;
  @(posedge clk) disable iff (!rst_n)
  (upd_valid && upd_pool_legal && !init_sel) |-> (!emit ##1 err_uninit);
endproperty
a_uninit : assert property (p_uninit_inert);
 
// P11: SCOPE. This chapter emits credit-return events and nothing else —
// no availability, no eligibility. Asserted so the boundary with Module 16
// is checkable rather than merely stated (section 1).
property p_no_eligibility_output;
  @(posedge clk) disable iff (!rst_n)
  ret_valid |-> (ret_count != '0);
endproperty
a_scope : assert property (p_no_eligibility_output);
 
// P12: reset clears the local decode state.
property p_reset_defined;
  @(posedge clk)
  !rst_n |=> (!ret_valid && (init_q == '0));
endproperty
a_reset : assert property (p_reset_defined);

P1 and P3 are a pair and P3 is the one that survives a plausible-looking mistake. P1 checks the difference against the module's own operands; P3 checks it against an independent integer-modulo reference, so a design that widened its operands — producing a correct value away from the wrap — fails at the boundary rather than passing by self-agreement.

P4 and P5 are per-pool, deliberately. An aggregate check passes a design that writes the wrong baseline as long as some baseline moved. Per-pool properties say which one changed and why it was allowed to, which is what turns a failure into a diagnosis.

P6 names an asymmetry worth remembering. §9 explains that a lost update is harmless — the next cumulative total recovers it. A lost decoded event is not: the baseline has already advanced past it, so the capacity was measured and then discarded, and no later update will mention it again. The holding stage exists for exactly that difference.

P11 is a scope property rather than a correctness one, and it is here because §1's boundary is easy to erode. A future edit that added an availability counter would have to add properties about it — and their absence is what keeps this chapter from becoming Chapter 16.1.

11. Verification

Monitors observe: the initialisation and update inputs, the consume interface, the available count, the baseline, and every reported condition.

The scoreboard maintains an independent model with its own modular subtraction:

// VERIFICATION-ONLY. Reference difference in integer arithmetic.
// Deliberately NOT the DUT's expression — a mirror of `new - old` would
// agree with a design that widened its operands and destroyed the wrap.
function automatic int ref_returned(int new_total, int old_total, int w);
  int m = 1 << w;
  return ((new_total - old_total) % m + m) % m;
endfunction

And it tracks available capacity itself, from the updates and consumptions it observed — never by reading avail_q. A mirrored scoreboard agrees with a delta-interpreting design at every step, because both would add the same wrong number.

Update decode

• Initialisation, then one update. Verify the emitted count is the difference, not the total.
• A duplicate update — the same total twice. Verify the second emits nothing (P2).
• A stale update — an older total. Verify the modular difference and, if implausibly large, rejection (P8).
• A sequence of increasing totals. Verify each emitted count against the reference model.
• An update across the wrap — last accepted 4090, new value 6. Verify 12 (§6), not a negative number and not 4012.
• FC_W = 8 — the header width. Verify wrap at 256.
• An update implying more than MAX_RETURN. Verify no event, err_implausible, and the baseline unchanged (P4, P8).

Pool isolation and range

• Updates to each pool in turn. Verify only that pool's baseline moves (P5).
• Interleaved updates to two pools. Verify independent baselines and correct per-pool differences.
• An out-of-range pool index. Verify nothing touched and err_bad_pool (P9).
• A non-power-of-two POOLS — 6 is the natural value, and $clog2(6) is 3, so indices 6 and 7 are presentable. Required test.
• POOLS = 1. The width corner: $clog2(1) is zero, so a design that put $clog2(POOLS) in the port list does not elaborate at all. Verify the instance builds, that pool 0 works, and that pool index 1 is rejected (err_bad_pool). Required test.
• POOLS = 3 and 8. 3 is a second non-power-of-two; 8 is the exact-power case where the bounds check becomes a no-op and must still not misbehave. These four values are the claimed configuration set — nothing wider is asserted.
• An update before that pool is initialised. Verify err_uninit (P10), and that another pool that is initialised still works.

Output ownership

• ret_ready low for a long run with an event held. Verify stability (P6).
• Emit and consume in the same cycle. Verify the new event is held, not lost (P7).
• Back-to-back updates faster than the consumer drains. Verify upd_ready backpressures and no update is silently consumed without emitting.
• A zero-difference update while an event is pending. Verify it is consumed without disturbing the held event.
• Reset with an event pending (P12).

Which mutation which check kills

12. Performance and Debugging

Update rate is a throughput parameter

The transmitter's view is always as fresh as the last update it received, and no fresher (§3).

sustainable in-flight capacity  ≈  consumption rate  ×  update interval

Derived systems reasoning, not a PCIe requirement — and the same relation as Chapter 12.5 §5's, at a different layer. If updates arrive rarely relative to the transmit rate, the transmitter stalls holding stale information while the receiver has room.

No numbers appear here, because the update interval is an implementation and configuration property, and Chapter 16.6 owns the credit-return system's behaviour.

Three resources, three different stalls

A transmitter can be stopped for three unrelated reasons, and they are distinguishable in one reading.

They are not the same and confusing them sends the investigation to the wrong side of the Link. Chapter 14.4 §17 makes the first two distinction explicit; this table adds the third.

Available credits grow beyond what the receiver advertised

The delta interpretation (§5), and it is the most damaging bug in the chapter.

Check whether available ever exceeds CAPACITY — P5 asserts it cannot, so if the design has no such bound, that is the first thing to add. Then check whether a duplicate update changes anything: it must not (P2).

And the consequence is worth stating plainly. The transmitter is now sending into a buffer with no room. Nothing downstream reports it — the packets are well-formed and delivered — so the symptom surfaces as corrupted or lost traffic that looks like a physical-layer problem.

It works until the credit counter wraps

Modular arithmetic (§6), and the diagnosis is the same as Chapter 14.5 §13's.

Look for widened operands or a % with signed intermediates. Both are correct away from the wrap. And check the field width: an 8-bit header counter wraps sixteen times more often than a 12-bit data counter, so the header pool will show it first — which is a useful signature in itself.

Only Memory Writes stall; Completions keep flowing

Not a Link failure — a single pool is exhausted.

Memory Writes are posted, so they consume the Posted accounting; Completions consume their own. One pool draining while others do not is exactly what separate pools are for, and it points at either the posted traffic pattern or a missing update for that category.

The observation: read the three pools' available counts. One at zero and the others healthy is a category problem, not a Link problem — and Chapters 16.2–16.4 own what each pool is for.

13. Common Misconceptions

• "PCIe flow control is ready/valid across the Link." It is accounting: the receiver advertises totals asynchronously and the transmitter decides locally (§3).
• "An FC Update says 'add this many credits'." It carries a cumulative total. The returned amount is a modular difference from the last value seen (§5).
• "A duplicate update is harmless because the numbers are the same." With the correct cumulative reading, yes — it returns zero. With a delta reading it manufactures capacity that does not exist (§5, P2).
• "Replay-buffer space and receive credits are the same resource." One is transmit-side reliability storage; the other describes the remote receive buffer. Either can be exhausted while the other is free (Chapter 14.4 §17).
• "All TLPs use one credit pool." Posted, Non-Posted and Completion are accounted separately, each with header and data (§2).
• "One credit always means one byte." One data credit is 16 bytes; one header credit is one header (§2, §4).
• "A payload-free packet still consumes a data credit." It does not — and charging one drains the data pool with traffic that never needed it (§4).
• "Payload cost can round down." It rounds up: a partial 16-byte unit still occupies a whole one, and rounding down under-charges and overruns the receiver (§4).
• "Ordinary integer comparison is safe for wrapping credit counters." It is correct away from the wrap and wrong at it — the same failure as Chapter 14.5 §6.
• "Credits are consumed when a packet becomes valid." They are consumed on an actual send. Consuming on an offer leaks credits that are never returned (§8).
• "Enough Link bandwidth means credits cannot be the bottleneck." Credit starvation stalls a transmitter with a completely idle Link (§12).
• "Credit updates are Transaction Layer Completions." They are DLLPs — Link-local, unrouted, and they never enter the Transaction Layer (Chapter 15.1 §6).
• "An ACK returns flow-control credits." Different mechanism, different category, different engine. An ACK retires replay storage (Chapter 14.2); a credit update returns receive-buffer capacity.
• "Credits guarantee the destination resource is ready." They describe buffer space at the far end of one Link — not the target Function, not memory, and not software (Chapter 14.2 §4's scope argument, applied to capacity).

14. Understanding Check

15. What's Next

This chapter took one packet category and found the arithmetic inside it: a credit update carries a running total, not an increment, and turning it into usable capacity is a modular subtraction bounded by a plausibility check. Read as a delta, it manufactures room that does not exist — and the receiver overruns with nothing anywhere reporting it.

That is the second wrapping counter in three chapters. Chapter 14.5 compared sequence identities within a half-range window; this one compares credit totals against a capacity bound. Same arithmetic, different constants, and in both cases the bound is a separate rule the comparison silently depends on.

Chapters 15.3 and 15.4 own the acknowledgement and retry packets' formats and timing; 15.5 the power-management packets — completing the DLLP module.

And Module 16 takes the credit system properly. 16.1 covers what a credit is and how the architecture fits together; 16.2–16.4 the Posted, Non-Posted and Completion pools individually; 16.5 what a transmitter spends and how it decides it may send; and 16.6 the credit-return mechanism as a system. §8's single pool is deliberately not any of that — it exists so this chapter's decode has somewhere to land.

The idea to carry forward: a cumulative counter is robust to loss and duplication by design — and a design that reads it as a delta turns that robustness into the failure mode.