PCIe · Module 16

Credit Consumption — Reserved Is Not Spent

Three chapters costed packets and deferred one question: when exactly does a transmitter spend the credit? Answer it wrong by one pipeline stage and two packets buy the same buffer.

Chapters 16.2, 16.3 and 16.4 established what every TLP costs. Each of them gated its send on send_fire and each said the same thing in a footnote: the spend policy belongs here.

Because "what does it cost" is the easy half. The hard half is when the counter moves — and the answer is not "when the packet is ready", not "when the scheduler picks it", and in a pipelined transmitter not even "when it leaves".

Get it wrong by one stage and two packets independently conclude they can afford the same buffer. Both send. The receiver has room for one.

At exactly what ownership event should credit state change, how are several pools committed atomically, and what must exist in a real transmit pipeline so that permission cannot be spent twice?

The mental model this chapter builds

Credit is permission to occupy remote receive capacity. A packet must not spend that permission because it exists, or because a scheduler looked at it — only when the local architecture reaches its declared irrevocable transmission point.

And there are three states, not two. A credit is available (uncommitted), reserved (assigned to a specific packet that has passed the point of no return but has not yet crossed the accounting boundary), or consumed (spent). A shallow transmitter can collapse reservation and consumption into one event. A pipelined one cannot — and calling an early decrement "consumption" when it is really reservation is how designs lose track of where their credits went.

The vocabulary is the engineering. §4's double-spend bug exists entirely because a design had no word — and therefore no state — for "committed but not yet sent".

1. What Is Verified, and What Is a Local Contract

Normative detail, its source, and the tier of each

Source, read directly (as in Chapters 16.1–16.4): Microchip AN2948, DS00002948B (2019–2023), §3.3.7 Flow Control.

The transmitter's obligation, verbatim:

"The transmitter tracks the amount of credits used. If sufficient credits exist or remain, the transmitter may send the TLP. As TLPs are transmitted, the transmitter deducts the amount of credits used. As the receiver empties its buffers, it updates the available credits by sending UpdateFC FCPs."

"The Transaction Layer performs Flow Control accounting functions for received TLPs and 'gates' TLP transmissions based on available credits for transmission."

The atomic multi-pool rule, from a second directly-fetched vendor source — Lattice PCIe X1 IP Core User Guide, FPGA-IPUG-02091-1.2:

"A transaction cannot be transmitted unless there is at least 1 header credit and enough data credits for the packet payload."

That is the whole normative content of this chapter, and it is deliberately small: sufficient credit before sending, deduct as transmitted, all required pools together.

Everything else here is local microarchitectural contract, and this chapter labels it as such rather than dressing it as protocol:

Where in a pipeline the "irrevocable point" sits — a design decision (§3).
Whether reservation state exists — a design decision forced by pipeline depth (§4).
Whether a same-cycle return is usable by a same-cycle consumption — a local contract (§7).
Arbitration between candidate packets — implementation policy.

Not verified, and therefore not published as a rule: the exact normative treatment of credit accounting on a Link-layer replay. §9 explains what this chapter does about that gap instead of guessing.

Deliberately not repeated here. The per-class costs — Chapters 16.2–16.4. The credit units and the six pools — Chapter 16.1. The return protocol — Chapter 16.6. Virtual Channels.

Scope. Conventional non-Flit flow control. The accounting architecture is not mode-specific; the units and encodings are.

2. Four Candidate Moments, and Only One Is Right

A packet passes through several events on its way out. Each is a plausible place to decrement, and three of them are wrong.

Event	Decrement here?	What goes wrong
`pkt_valid` rises — the packet exists	✗	credit drains while nothing is sent; a stalled queue empties the pool
scheduler selects it	✗	selection is revocable; a packet not chosen next cycle has already paid
it enters an irrevocable pipeline stage	reserve	correct — but this is reservation, not consumption (§4)
it crosses the accounting boundary	consume	correct

Why 'valid' is the most tempting and the most wrong

Because pkt_valid is the earliest signal that unambiguously means "there is a packet here", and it is available in the same block that holds the counters.

But valid is a statement about existence, not about progress. A packet can be valid for a thousand cycles — behind a full replay buffer, behind a busy transmit path, behind another packet — and be valid the entire time without ever moving.

Decrementing on it produces a counter that falls monotonically while the Link carries nothing, and that is the signature §15's first debugging scenario describes: a pool draining to zero with an analyzer showing an idle Link.

The general principle, which outlives PCIe: a resource must be charged to an event that happens once per unit of work, not to a level that is asserted while the work waits. valid is a level. valid && ready is an event.

3. The Irrevocable Point

Every transmitter has one, and the design's job is to say where it is.

Azvya Education Pvt. Ltd.VLSI Mentor

Snippet

TLP queue → arbiter → format/pipeline → replay alloc → Link
              ^                              ^
              |                              |
       revocable: a packet          irrevocable: sequence
       looked at here may           number assigned, entry
       not go next cycle            retained, packet gone

In a shallow transmitter, send_fire = tx_valid && tx_ready is that point, and it is the model Chapters 16.2–16.4 used. Nothing downstream can refuse the packet after it, so reservation and consumption coincide and one event suffices.

The condition that makes the simple model legal — and how to check it

send_fire may serve as the consumption point only if nothing after it can refuse, delay-with-cancellation, or re-order the packet.

Check it by asking a single question: after send_fire asserts, is there any sequence of downstream events in which this packet does not reach the Link?

If the answer is no, one event is enough.

If the answer is yes — even rarely — the design has a window, and in that window the credit is in a state the counters cannot express: deducted, but the packet may not go. If the packet is then cancelled, the credit is gone with nothing to show for it; if the design tries to give it back, it needs somewhere to give it back from, which is reservation state under another name.

This is why the vocabulary matters. A design with no word for "committed but not gone" cannot reason about the window, and will usually resolve it by picking whichever decrement point makes the current testcase pass.

4. The Double-Spend, Concretely

This is the argument for reservation, and it is best seen as a trace rather than a principle.

Setup. One pool. PH = 1, PD = 4. Two packets waiting:

Azvya Education Pvt. Ltd.VLSI Mentor

Snippet

A : needs PH=1, PD=2
B : needs PH=1, PD=2

A two-stage transmitter with no reservation state:

Azvya Education Pvt. Ltd.VLSI Mentor

Snippet

cycle   1                       2                       3
        arbiter examines A      A is in the pipeline     A sends
        PH=1 PD=4 → A fits      arbiter examines B       PH → 0, PD → 2
        A admitted              PH=1 PD=4 → B fits
                                B admitted
                                                        4
                                                        B sends
                                                        PH → -1  ✗

Both packets read a true value and reached a false conclusion

Neither arbiter decision was wrong when it was made. At cycle 1, PH = 1 and A fits. At cycle 2, PH is still 1 — because A has not sent yet — and B fits.

The counter was accurate. The inference was not, because "available" silently meant two different things: "not yet spent" and "not yet promised". With one packet in flight those are the same number. With two they are not.

What the hardware does next depends on how carefully it was written. If the pool underflows, availability wraps to a huge value and the transmitter sends freely into a receiver that has no room (Chapter 16.1 §8's widening exists for this). If it is clamped and reported, the design has an error flag and one packet that must be un-sent — which is not possible, because it has already gone.

And the failure needs two packets in flight, so it appears when the pipeline is busy and disappears when you add debug that slows it down. It is a Heisenbug by construction.

The fix is a third state. Once A is admitted, its credit is reserved: no longer available to B, not yet consumed. B's arbiter sees PH available = 0 and waits. §8 builds it, and P8 asserts that two packets can never reserve the same unit.

5. Available, Reserved, Consumed

Three words for three different things, and using them interchangeably is the bug in §4.

State	Meaning	Who owns it
Available	permission held locally, promised to nobody	the pool
Reserved	promised to one specific packet that has passed the irrevocable point	that packet
Consumed	spent — the packet crossed the accounting boundary	the remote receiver's buffer

The invariant that ties them together, for a transmitter that has not yet had anything returned:

Azvya Education Pvt. Ltd.VLSI Mentor

Snippet

advertised = available + reserved + consumed-and-not-yet-returned

Nothing leaves this equation except through a return. §12's conservation property is exactly this identity, checked continuously.

6. The Cost Vector

Every TLP normalizes to six numbers, most of them zero.

Packet	PH	PD	NPH	NPD	CPLH	CPLD
Memory Write, 64 B	1	4	0	0	0	0
Message without data	1	0	0	0	0	0
Memory Read	0	0	1	0	0	0
I/O Write	0	0	1	1	0	0
`CplD`, 64 B	0	0	0	0	1	4
`Cpl`	0	0	0	0	1	0

Costs from Chapters 16.2–16.4; this chapter only carries them.

Two properties of this table do all the work in §7's RTL. Every packet touches at most two pools — a header pool and its matching data pool — and no packet ever touches two different classes. So the eligibility test is a loop over six entries in which four are trivially satisfied, and the atomicity requirement reduces to committing a vector rather than a pair.

Representing it as a vector rather than as a class-plus-payload is the design decision, and it pays off twice: the consumption engine becomes class-agnostic, and the conservation property (§12) is one loop instead of six special cases.

7. RTL — Cost Vector and Atomic Consumption

Azvya Education Pvt. Ltd.VLSI Mentor

Snippet

// SYNTHESIZABLE. Normalized credit cost vector and the multi-pool
// eligibility test.
// The six pools and their units are NORMATIVE (Chapter 16.1 section 1);
// the per-class costs are NORMATIVE (Chapters 16.2-16.4). The VECTOR
// REPRESENTATION and the pool ordering are internal teaching metadata.
package credit_vec_pkg;
 
  localparam int NPOOL  = 6;
  localparam int CW     = 12;      // credit / cost width
 
  // Pool ordering is arbitrary but FIXED. Header pools are even, data
  // pools odd, so a header/data pair is (2k, 2k+1) -- which lets the
  // pairing be checked structurally rather than by convention.
  localparam int P_PH   = 0, P_PD   = 1;
  localparam int P_NPH  = 2, P_NPD  = 3;
  localparam int P_CPLH = 4, P_CPLD = 5;
 
  typedef logic [CW-1:0] credit_cost_t [NPOOL];
 
  // WIDENED ACCUMULATOR. Two bits above the credit width, so
  // available + returned cannot wrap and effective - cost is evaluated
  // where a negative result is REPRESENTABLE rather than wrapped to a
  // huge positive one (Chapter 16.1 section 8).
  localparam int ACC_W = CW + 2;
 
endpackage

Azvya Education Pvt. Ltd.VLSI Mentor

Snippet

import credit_vec_pkg::*;
 
// SYNTHESIZABLE. Atomic multi-pool eligibility and consumption.
// "A transaction cannot be transmitted unless there is at least 1 header
// credit and enough data credits for the packet payload" -- vendor-stated
// (section 1). The same-cycle return contract is a LOCAL CONTRACT,
// declared below rather than left implicit.
module credit_consume_engine (
  input  logic clk,
  input  logic rst_n,
 
  // ---- Pool state, one entry per pool -----------------------------------
  input  logic [CW-1:0]   available   [NPOOL],
  input  logic [CW-1:0]   capacity    [NPOOL],
  input  logic            pool_infinite [NPOOL],
  input  logic            pool_init     [NPOOL],
 
  // ---- Normalized returns for this cycle (Chapter 16.6) ------------------
  input  logic            return_valid  [NPOOL],
  input  logic [CW-1:0]   return_count  [NPOOL],
 
  // ---- The candidate packet ----------------------------------------------
  input  logic            pkt_valid,
  input  credit_cost_t    pkt_cost,
 
  // ---- The irrevocable transmission event (section 3) --------------------
  input  logic            send_fire,
 
  // ---- Outputs ------------------------------------------------------------
  output logic            eligible,
  output logic [CW-1:0]   next_available [NPOOL],
  output logic            consume_valid  [NPOOL],
  output logic [CW-1:0]   consume_cost   [NPOOL],
  output logic [NPOOL-1:0] blocked_pool,
  output logic            range_error
);
 
  // =====================================================================
  // THE SAME-CYCLE CONTRACT -- declared, because leaving it implicit is
  // how two blocks come to disagree about one cycle.
  //
  //   effective[p]   = available[p] + returned-this-cycle[p]
  //   eligible       = for every pool: effective[p] >= cost[p]
  //   next[p]        = effective[p] - consumed-this-cycle[p]
  //
  // A return arriving THIS cycle IS usable by a consumption THIS cycle.
  // The alternative -- returns visible only next cycle -- is equally
  // defensible and costs one cycle of latency per return.
  //
  // What is NOT defensible is deciding eligibility from the stale value
  // and then applying both events: that consumes capacity that was never
  // available. Both the decision and the next state below are derived
  // from the SAME `effective` array, so they cannot disagree.
  // =====================================================================
 
  logic [ACC_W-1:0] effective [NPOOL];
  logic [ACC_W-1:0] next_x    [NPOOL];
  logic             pool_ok   [NPOOL];
 
  always_comb begin
    for (int p = 0; p < NPOOL; p++) begin
      effective[p] = ACC_W'(available[p])
                   + ((return_valid[p] && pool_init[p] && !pool_infinite[p])
                        ? ACC_W'(return_count[p]) : '0);
 
      // A pool the packet does not use is trivially satisfied -- it must be
      // neither consulted nor charged. An infinite pool is always satisfied
      // (Chapter 16.1 section 6); it is the absence of a limit, not a
      // large number.
      pool_ok[p] = (pkt_cost[p] == '0)
                 || (pool_init[p]
                     && (pool_infinite[p]
                         || (effective[p] >= ACC_W'(pkt_cost[p]))));
    end
  end
 
  // ALL REQUIRED POOLS, OR NONE. There is no arm of this design in which
  // one pool is charged and another is not (section 4's leak, generalized
  // from a pair to a vector).
  always_comb begin
    eligible = pkt_valid;
    for (int p = 0; p < NPOOL; p++) eligible = eligible && pool_ok[p];
  end
 
  always_comb
    for (int p = 0; p < NPOOL; p++)
      blocked_pool[p] = pkt_valid && (pkt_cost[p] != '0) && !pool_ok[p];
 
  // ONE COMMIT DRIVES EVERY POOL. Not six decisions -- one, distributed.
  wire commit = pkt_valid && eligible && send_fire;
 
  always_comb begin
    for (int p = 0; p < NPOOL; p++) begin
      consume_valid[p] = commit && (pkt_cost[p] != '0) && !pool_infinite[p];
      consume_cost[p]  = pkt_cost[p];
 
      next_x[p] = effective[p]
                - (consume_valid[p] ? ACC_W'(pkt_cost[p]) : '0);
 
      // An infinite pool never moves. Otherwise clamp the POST-CONSUMPTION
      // value at the ceiling: clamping on the return alone would discard a
      // same-cycle consumption and leave the pool at full capacity
      // (Chapter 16.1 section 8).
      next_available[p] = pool_infinite[p]
                        ? available[p]
                        : ((next_x[p] > ACC_W'(capacity[p]))
                             ? capacity[p] : CW'(next_x[p]));
    end
  end
 
  // Any next-state that left the legal range. With ACC_W two bits wider
  // than CW this cannot happen silently -- it is detected, not wrapped.
  always_comb begin
    range_error = 1'b0;
    for (int p = 0; p < NPOOL; p++)
      if (!pool_infinite[p] && (next_x[p] > ACC_W'(capacity[p])))
        range_error = 1'b1;
  end
 
endmodule

Classification: synthesizable (combinational) plus a compile-time package.

Architecture. One loop computes effective, one computes eligibility, one commit wire drives all six consume strobes. There is deliberately no per-pool sequencing — Chapter 16.1 §9's argument, generalised: the leak requires an ordering, and this structure has none.

Cycle behaviour.

Situation	Result
any required pool short	`eligible` low; no pool changes; `blocked_pool` names which
all required pools sufficient, no `send_fire`	`eligible` high; no pool changes
all sufficient and `send_fire`	every non-zero cost committed in the same cycle
return and consume together	both applied, from one `effective` value
infinite pool	always satisfied, never decremented
uninitialised pool with a non-zero cost	not eligible — no information means no permission

Failure — six. Per-pool sequencing leaks the first pool when a later one is short. Deciding eligibility from available and applying both events spends capacity that never existed. Consulting or charging a zero-cost pool blocks a Memory Read on the data pool it does not use. Narrow arithmetic wraps below zero and reports vast availability. Treating infinite as a large number eventually decrements it to something finite. And a single blocked flag cannot say which of six pools is the constraint, which is the difference between a debug session and a guess.

Deliberately simplified: one candidate packet per cycle — §8 adds the second; no arbitration policy; return_count already normalized by Chapter 16.6.

8. RTL — Reservation Engine

Azvya Education Pvt. Ltd.VLSI Mentor

Snippet

import credit_vec_pkg::*;
 
// SYNTHESIZABLE. Per-pool account with an explicit RESERVED state.
// The three-state model (available / reserved / consumed) is a LOCAL
// MICROARCHITECTURAL CONTRACT, not PCIe wire state (section 5). What it
// implements is the normative rule that sufficient credit must exist
// before sending (section 1) -- in a pipeline where "before" spans more
// than one cycle.
module credit_reservation #(
  parameter int CW_P = CW
) (
  input  logic clk,
  input  logic rst_n,
 
  input  logic [CW_P-1:0] init_capacity,
  input  logic            init_valid,
  input  logic            init_infinite,
 
  // ---- Return, normalized by Chapter 16.6 --------------------------------
  input  logic            return_valid,
  input  logic [CW_P-1:0] return_count,
 
  // ---- Stage 1: the arbiter admits a packet ------------------------------
  // Asserted when a packet passes the irrevocable point (section 3).
  input  logic            reserve_valid,
  input  logic [CW_P-1:0] reserve_cost,
 
  // ---- Stage 2: that packet crosses the accounting boundary --------------
  input  logic            consume_valid,
  input  logic [CW_P-1:0] consume_cost,
 
  // ---- Outputs ------------------------------------------------------------
  // THE ARBITER MUST TEST THIS, NOT `available_total`. It is what remains
  // unpromised, which is the only question the arbiter is actually asking
  // (section 5).
  output logic [CW_P-1:0] unreserved,
  output logic [CW_P-1:0] reserved,
  output logic            can_reserve,     // for reserve_cost
  output logic            infinite,
  output logic            account_error
);
 
  localparam int AW = CW_P + 2;            // widened, as everywhere
 
  logic [CW_P-1:0] avail_q, resv_q, cap_q;
  logic            init_q, inf_q, err_q;
 
  assign unreserved    = avail_q;
  assign reserved      = resv_q;
  assign infinite      = inf_q;
  assign account_error = err_q;
 
  wire [AW-1:0] avail_x = AW'(avail_q);
  wire [AW-1:0] ret_x   = (return_valid && init_q && !inf_q)
                            ? AW'(return_count) : '0;
  wire [AW-1:0] cap_x   = AW'(cap_q);
 
  // Effective UNRESERVED capacity for this cycle's admission decision.
  wire [AW-1:0] effective = avail_x + ret_x;
 
  assign can_reserve = init_q
                    && (inf_q || (effective >= AW'(reserve_cost)));
 
  wire do_reserve = reserve_valid && can_reserve && !inf_q;
  wire do_consume = consume_valid && !inf_q;
 
  // available: falls on RESERVE, rises on RETURN.  It does NOT fall again
  // on consume -- that would charge the packet twice.
  wire [AW-1:0] next_avail = effective - (do_reserve ? AW'(reserve_cost) : '0);
 
  // reserved: rises on RESERVE, falls on CONSUME. The credit moves from
  // one bucket to the other; it is not created or destroyed here.
  wire [AW-1:0] next_resv  = AW'(resv_q)
                           + (do_reserve ? AW'(reserve_cost) : '0)
                           - (do_consume ? AW'(consume_cost) : '0);
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      avail_q <= '0; resv_q <= '0; cap_q <= '0;
      init_q  <= 1'b0; inf_q <= 1'b0; err_q <= 1'b0;
    end else begin
      if (init_valid && !init_q) begin
        init_q  <= 1'b1;
        inf_q   <= init_infinite;
        cap_q   <= init_infinite ? '0 : init_capacity;
        avail_q <= init_infinite ? '0 : init_capacity;
        resv_q  <= '0;
      end else if (init_q && !inf_q) begin
        avail_q <= (next_avail > cap_x) ? cap_q : CW_P'(next_avail);
        resv_q  <= CW_P'(next_resv);
      end
 
      // A consume larger than what is reserved, or a reserve accepted
      // without capacity, is a CONTRACT VIOLATION by the caller. Reported
      // rather than silently wrapped -- with AW two bits wider than CW_P,
      // the wrap is detectable rather than invisible.
      if (consume_valid && (AW'(consume_cost) > AW'(resv_q)))  err_q <= 1'b1;
      if (reserve_valid && !can_reserve)                       err_q <= 1'b1;
      if (next_resv > cap_x)                                   err_q <= 1'b1;
    end
  end
 
endmodule

Classification: synthesizable.

Architecture. Two counters and a widened accumulator. The credit moves between them; it is neither created nor destroyed by a reservation. That is what makes §12's conservation identity checkable.

Cycle behaviour, and the table is the design.

Event	`unreserved`	`reserved`
reserve (admitted)	− cost	+ cost
consume (packet crosses)	unchanged	− cost
return	+ count, clamped	unchanged
reserve refused	unchanged	unchanged
reserve and consume together	− reserve cost	+ reserve − consume
infinite pool	never moves	never moves

Read the second row carefully: consumption does not touch unreserved. The packet already paid, at reservation. A design that decremented in both places would charge every packet twice — §14's mutation 8, and it presents as a pool draining at exactly double the send rate.

can_reserve tests unreserved, not total availability. That single choice is what kills §4's double-spend: B's arbiter sees A's promise reflected in the number it reads.

Failure — six. Arbitrating against avail + resv reintroduces the double-spend exactly. Decrementing unreserved on consume as well as reserve double-charges. Consuming more than is reserved underflows the reserved bucket — caught, because the caller's contract was violated. Never consuming a reservation leaks it permanently, and the pool shrinks with no packets to account for it. Recomputing the cost at consume time rather than using the reserved value lets the two disagree (§10). And omitting the widening turns each of these from a reported error into a wrapped counter.

Deliberately simplified: no cancellation — stated above; one reserve and one consume per cycle; a single pool per instance, with the vector composed by instantiating six.

9. Replay and Credit — What This Chapter Will Not Claim

The normative gate applied to a question this chapter cannot answer

A Link-layer replay retransmits a TLP that was already sent (Chapter 14.3). Does that retransmission consume flow-control credit again?

No source available to this chapter states the rule. The vendor documentation read directly for Module 16 covers consumption at transmission and return at buffer-free, and says nothing about replay-time accounting. Searching did not produce a specification-grade statement either.

So this chapter does not publish a rule, and a design must take it from the Base Specification.

What can be said, clearly labelled as derived reasoning rather than a quoted rule: a credit represents space in the receiver's buffer for a particular TLP. A replayed TLP is the same TLP. Either the receiver got it the first time — in which case the buffer was occupied and will be freed and returned normally — or it did not, in which case the buffer was never occupied at all. In neither case does a second, independent allocation exist to be paid for. Charging twice would mean a Link with errors consumes credit faster than a Link without, in proportion to its error rate.

What this chapter therefore does is state a local contract and enforce it:

§8's consume_valid is asserted once per TLP, on its first crossing of the accounting boundary. A replay does not assert it again.

P13 asserts that contract, and it is labelled as the design's declared behaviour rather than as a published PCIe rule — which is the honest form for a claim at this evidence level.

And a design review should ask for the revision it was taken from, because the consequence of getting it wrong is asymmetric: charging twice exhausts credit under exactly the conditions where recovery matters most, and §14's mutation 8 shows what that looks like.

10. Cost Travels With the Packet

A short section for a rule that prevents a whole class of bug.

When a packet is reserved, its cost vector is captured with it. At consume time, the engine spends the stored vector, never a freshly-derived one.

Azvya Education Pvt. Ltd.VLSI Mentor

Snippet

reserve : capture { identity, cost_vector }
consume : spend the CAPTURED vector

Why re-deriving at consume time fails, and why it fails intermittently

Because the inputs the cost was derived from may have moved on.

The cost came from the packet's class and payload length (Chapters 16.2–16.4). If the consume stage recomputes from live queue outputs, and the queue head has advanced to the next packet, it spends packet B's cost against packet A's reservation.

The two are usually similar, which is what makes it intermittent: both might be 64-byte writes costing 1 PH and 4 PD, and nothing goes wrong. It breaks when consecutive packets differ — a 64-byte write followed by a Cpl, or a write followed by a read — and then the reserved and consumed vectors disagree and §8's account_error fires, or worse, does not.

This is Chapter 11.6 §7's rule — decoded metadata is owned, not re-derived — applied to credit. A reservation is a promise about a specific packet, and it must carry the packet's identity with it or it is a promise about nothing.

11. The Full Loop

Figure 1 — one packet's journey through the credit accounting. The left half is local and fast: cost derivation, the eligibility test against unreserved capacity, reservation, then consumption at the irrevocable point. The right half is remote and slow: the packet occupies the receiver's buffer until the receiver drains it, and only then does an update return the capacity. Note that the reservation and the return are separated by a full Link round trip plus the receiver's own processing.

Three things to read out of the figure.

The two self-messages on the engine are different events. reserve moves credit from available to reserved; consume moves it from reserved to spent. A design with one self-message has collapsed them, which is correct only for a shallow transmitter (§3).

The gap between consume and return is not a design parameter. It is a Link round trip plus the far side's processing — nanoseconds to microseconds, entirely outside the transmitter's control. That gap is why credit exists, and why Chapter 16.1 §2's advertised-capacity scheme replaces a ready signal.

And the return is unsolicited. Nothing in the left half asks for it. The engine adds capacity when it arrives and waits when it does not.

12. A Trace

Internal teaching signals, not PCIe wire signals. One pool pair. PH capacity 2, PD capacity 8. Two-stage pipeline with reservation.

Azvya Education Pvt. Ltd.VLSI Mentor

Snippet

step             1     2     3     4     5     6     7     8
pkt_valid        1     1     1     1     0     0     0     0
ph_cost          1     1     1     1     -     -     -     -
pd_cost          4     4     4     4     -     -     -     -
 
ph_unreserved    2     1     0     0     0     0     1     1
ph_reserved      0     1     1     1     0     0     0     0
pd_unreserved    8     4     0     0     0     0     4     4
pd_reserved      0     4     4     4     0     0     0     0
 
can_reserve      1     1     0     0     0     0     1     -
reserve_fire     1     1     0     0     0     0     0     0
send_fire        0     1     0     0     1     0     0     0
 
pd_return        0     0     0     0     0     0     1     0

Read step 1. Packet A is admitted. ph_unreserved falls to 1 and ph_reserved rises to 1 — the credit moved buckets; nothing was spent.

Read step 2 — the whole point of the chapter. Packet B is examined. ph_unreserved is 1, not 2, because A's promise is visible. B fits, is admitted, and A sends in the same cycle. Note ph_reserved stays at 1: A's reservation was consumed and B's was created.

Read step 3. A third packet arrives and ph_unreserved is 0. can_reserve is low and nothing happens — this is §4's double-spend refused, in one signal.

Read steps 3–4. The pool is not exhausted in absolute terms — B still holds a reservation. It is exhausted in the only sense that matters to an arbiter: nothing is unpromised.

Read step 5. B sends. ph_reserved falls to 0. ph_unreserved does not change — B paid at step 2.

Read step 7. A PD return of 4 arrives and pd_unreserved rises. can_reserve goes high again.

And note what never happens: ph_unreserved never falls on a send_fire, and ph_reserved never falls on a reserve_fire.

13. Assertions

Azvya Education Pvt. Ltd.VLSI Mentor

Snippet

// SVA over credit_consume_engine and credit_reservation. These assert the
// LOCAL accounting contract and the declared same-cycle and reservation
// policies. They assert NOTHING about credit-return timing or transmit
// readiness (environment properties -- Chapter 16.1 section 15), nothing
// about per-class costs (Chapters 16.2-16.4), and nothing about the update
// protocol (16.6).
 
// ---- ENVIRONMENT ------------------------------------------------------
// A1: returns are normalized DIFFERENCES from Chapter 16.6, not totals.
assume property (@(posedge clk) disable iff (!rst_n)
  return_valid |-> (return_count != '0));
// A2: send_fire is the IRREVOCABLE point -- nothing downstream refuses.
assume property (@(posedge clk) disable iff (!rst_n)
  send_fire |-> pkt_valid);
// A3: a consume always corresponds to a packet previously reserved.
assume property (@(posedge clk) disable iff (!rst_n)
  consume_valid |-> (reserved != '0));
 
// ---- OWNERSHIP: WHEN CREDIT MAY CHANGE --------------------------------
 
// P1: NO POOL CHANGES WITHOUT A DECLARED EVENT. The chapter's foundational
// property -- credit moves on reserve, consume, return or init, and on
// nothing else. A design decrementing on `valid` fails here immediately.
property p_no_change_without_event;
  @(posedge clk) disable iff (!rst_n)
  (!reserve_valid && !consume_valid && !return_valid && !init_valid)
    |=> ($stable(unreserved) && $stable(reserved));
endproperty
a_ownership : assert property (p_no_change_without_event);
 
// P2: A STALLED PACKET CONSUMES NOTHING. Valid is a level, not an event.
property p_stall_consumes_nothing;
  @(posedge clk) disable iff (!rst_n)
  (pkt_valid && !send_fire && !reserve_valid)
    |=> ($stable(unreserved) && $stable(reserved));
endproperty
a_stall : assert property (p_stall_consumes_nothing);
 
// P3: consumption does NOT touch unreserved -- the packet paid at reserve.
// Catches the double-charge (section 8).
property p_consume_leaves_unreserved;
  @(posedge clk) disable iff (!rst_n)
  (consume_valid && !reserve_valid && !return_valid && !infinite)
    |=> $stable(unreserved);
endproperty
a_no_double_charge : assert property (p_consume_leaves_unreserved);
 
// ---- ELIGIBILITY AND ATOMICITY ----------------------------------------
 
// P4: a send implies EVERY required pool had sufficient effective credit.
property p_send_implies_all_pools;
  @(posedge clk) disable iff (!rst_n)
  commit |-> eligible;
endproperty
a_all_pools : assert property (p_send_implies_all_pools);
 
// P5: FAILED ELIGIBILITY CHANGES NO POOL. Not one, not partially.
property p_failed_eligibility_is_free;
  @(posedge clk) disable iff (!rst_n)
  (pkt_valid && !eligible)
    |=> (next_available == $past(available));
endproperty
a_atomic : assert property (p_failed_eligibility_is_free);
 
// P6: ALL REQUIRED POOLS COMMIT TOGETHER -- every non-zero cost, one cycle.
property p_atomic_commit;
  @(posedge clk) disable iff (!rst_n)
  commit |-> (foreach_pool_nonzero_cost_implies_consume_valid);
endproperty
a_together : assert property (p_atomic_commit);
 
// P7: A ZERO-COST POOL IS NEITHER CONSULTED NOR CHARGED. A Memory Read
// must not be blocked by, or billed to, the data pool.
generate for (genvar p = 0; p < NPOOL; p++) begin : g_unused
  property p_unused_pool_untouched;
    @(posedge clk) disable iff (!rst_n)
    (commit && (pkt_cost[p] == '0))
      |-> (!consume_valid[p] && (next_available[p] == available[p]));
  endproperty
  a_unused : assert property (p_unused_pool_untouched);
end endgenerate
 
// ---- RESERVATION ------------------------------------------------------
 
// P8: THE DOUBLE-SPEND PROPERTY (section 4). A reservation is only granted
// against UNRESERVED capacity, so two packets can never hold the same unit.
property p_reserve_from_unreserved_only;
  @(posedge clk) disable iff (!rst_n)
  (reserve_valid && can_reserve && !infinite)
    |-> (unreserved >= reserve_cost);
endproperty
a_no_double_spend : assert property (p_reserve_from_unreserved_only);
 
// P9: CONSERVATION. Nothing leaves the accounting except through a return.
// Ghost counters are TESTBENCH state -- this is a VERIFICATION ACCOUNTING
// IDENTITY, not PCIe wire state.
property p_conservation;
  @(posedge clk) disable iff (!rst_n)
  (init_q && !infinite)
    |-> ((g_initial + g_returned)
         == (unreserved + reserved + g_consumed_not_yet_returned));
endproperty
a_conserve : assert property (p_conservation);
 
// P10: a consume never exceeds what is reserved.
property p_consume_within_reserved;
  @(posedge clk) disable iff (!rst_n)
  (consume_valid && !infinite) |-> (consume_cost <= reserved);
endproperty
a_within : assert property (p_consume_within_reserved);
 
// P11: neither counter underflows, and neither exceeds capacity.
property p_range;
  @(posedge clk) disable iff (!rst_n)
  (init_q && !infinite)
    |-> ((unreserved <= cap_q) && (reserved <= cap_q)
      && ((unreserved + reserved) <= cap_q));
endproperty
a_range : assert property (p_range);
 
// P12: THE COST TRAVELS WITH THE PACKET (section 10). What is consumed
// equals what was reserved for THAT packet -- not a freshly derived value.
property p_reserved_cost_is_consumed;
  @(posedge clk) disable iff (!rst_n)
  consume_valid |-> (consume_cost == resv_cost_of_current_packet);
endproperty
a_cost_owned : assert property (p_reserved_cost_is_consumed);
 
// ---- REPLAY -----------------------------------------------------------
 
// P13: THIS DESIGN'S DECLARED CONTRACT, NOT A PUBLISHED PCIe RULE
// (section 9). A replayed TLP does not consume flow-control credit a
// second time: consume_valid is asserted once per TLP, on its first
// crossing of the accounting boundary.
property p_replay_does_not_reconsume;
  @(posedge clk) disable iff (!rst_n)
  dut_replay.replaying |-> !consume_valid;
endproperty
a_replay : assert property (p_replay_does_not_reconsume);
 
// P14: nor does a replay alter reservation state.
property p_replay_leaves_reservation;
  @(posedge clk) disable iff (!rst_n)
  dut_replay.replaying |=> ($stable(unreserved) && $stable(reserved));
endproperty
a_replay_state : assert property (p_replay_leaves_reservation);
 
// ---- CROSS-RESOURCE ---------------------------------------------------
 
// P15: an ACK returns replay storage, never credit (Chapter 14.2).
property p_ack_returns_no_credit;
  @(posedge clk) disable iff (!rst_n)
  (dut_retire_window.retire_valid && !return_valid)
    |=> ($stable(unreserved) && $stable(reserved));
endproperty
a_ack : assert property (p_ack_returns_no_credit);
 
// P16: pools do not borrow from one another.
generate for (genvar p = 0; p < NPOOL; p++) begin : g_iso
  property p_pool_isolated;
    @(posedge clk) disable iff (!rst_n)
    (return_valid[p] && !consume_valid[p])
      |=> (next_available[p] != available[p]);
  endproperty
  a_iso : assert property (p_pool_isolated);
end endgenerate
 
// P17: reset and init are explicit.
property p_reset;
  @(posedge clk)
  !rst_n |=> ((unreserved == '0) && (reserved == '0) && !can_reserve);
endproperty
a_reset : assert property (p_reset);

P1 is the property the whole chapter exists to make true. It says credit changes on declared events and nothing else — and a design that decrements on pkt_valid, or on scheduler selection, or on a replay, fails it without any further reasoning about costs or pools.

P8 is the double-spend property, and its precision matters: it asserts the reservation is granted against unreserved, not against total availability. A design arbitrating on unreserved + reserved satisfies every other property here and fails this one.

P9 is the conservation identity, and it is labelled a verification accounting identity deliberately — the ghost counters exist only in the testbench, and PCIe has no such state. What it catches is any credit that appeared or vanished without an event, which is every leak and every double-charge in one property.

P13 and P14 are labelled as this design's contract, not as protocol (§9). That labelling is the honest form for a claim at that evidence level, and it tells an integrator exactly what to re-check against the specification.

14. Verification and Fault Injection

The scoreboard maintains its own six-pool model — capacity, unreserved, reserved, cumulative consumed, cumulative returned — from observed reserve, send and update events. It never reads available, unreserved, can_reserve or eligible, and never calls the DUT's cost derivers.

Ownership

A packet valid and stalled for 100 cycles. Verify nothing moves (P2) — the required test, and the one a valid-triggered design fails on cycle 1.
The scheduler examining a packet it does not admit. Verify nothing moves.
Reserve, then a long gap, then consume. Verify the two counters move at the two events and not in between.
Consume without a prior reserve. Verify account_error (A3's contract violated deliberately).

Eligibility and atomicity

One-pool packet (Memory Read: NPH only). Verify PD, PH, CPLH, CPLD are all untouched (P7).
Two-pool packet (Memory Write). Verify both commit together (P6).
Exactly enough credit in every required pool — the exact-fit case.
One short in one required pool, the others plentiful. Verify no pool changes (P5), and blocked_pool names the right one.
Each of the six pools short in turn, holding the rest full.

The reservation race — the required set

§4's exact trace. PH = 1, two packets each needing 1 PH, a two-stage pipeline. Verify the second is refused (P8). This is the chapter's headline test, and a design without reservation sends both.
Reserve and consume in the same cycle (trace step 2).
Reserve and return in the same cycle.
Consume and return in the same cycle.
All three in one cycle.
Back-to-back sends with reservations overlapping.

Same-cycle contract

Return and consume together, where the packet is affordable only with the return counted. The declared-contract test.
Return and consume together, unaffordable even with it. Verify refusal and that the return still applies.
A return that would exceed capacity, coinciding with a send. Verify the consumption is still deducted and the pool does not sit at the ceiling (Chapter 16.1 §8).

Replay and reset

A replay of a TLP whose credit was already consumed. Verify no second consumption (P13) and no reservation change (P14).
An ACK with no UpdateFC. Verify no credit moves (P15).
Reset mid-reservation — verify both counters clear (P17).

Mutations

#	Mutation	Caught by	Silicon symptom
1	consume on `pkt_valid`	P1, P2	pool drains to zero with an idle Link
2	consume on scheduler select	P1	credit lost for packets never sent
3	header pool charged despite a short data pool	P5	slow leak; one class dies after minutes
4	cost recomputed at consume from the live queue	P12	intermittent mis-charge when consecutive packets differ
5	reservation not subtracted from `unreserved`	P8	§4's double-spend — receiver overflow
6	arbiter tests `unreserved + reserved`	P8	the same double-spend, one expression later
7	reservation never consumed	P9, P10	reserved grows without bound; pool starves
8	replay decrements credit again	P13	credit exhaustion proportional to the error rate
9	return applied twice	P9	capacity invented; intermittent overflow
10	same-cycle return ignored by eligibility	P4	unnecessary stalls; throughput loss only
11	unsigned underflow wraps	P11	availability appears enormous; overflow
12	one pool's return credited to another	P16	one class over-sends while another starves
13	zero-cost pool consulted	P7	Memory Reads blocked by the data pool
14	reserved packet's cost overwritten under stall	P12	the wrong amount is released at consume

The counterexample: the double-spend, and why adding debug hides it

Remove the reservation subtraction so unreserved falls only at consume.

PH = 1. Two 64-byte Memory Writes, A and B, in a two-stage transmitter.

Cycle	Arbiter sees	Action	Truth
1	`PH = 1`	admit A	A owns the only PH
2	`PH = 1` — A has not sent	admit B	B owns nothing
3	—	A sends, `PH → 0`	correct
4	—	B sends, `PH → −1`	receiver overflow

Both arbiter decisions read a true number. The counter was never wrong; it answered "how much is unspent" when the arbiter was asking "how much is unpromised".

Now the property that makes this hard to find. It requires two packets in flight simultaneously. Add a debug probe that costs a cycle, or run with a slower transmit path, or single-step the pipeline in simulation — and the second packet is never examined before the first sends. The bug vanishes under observation and returns at full rate.

And the failure surfaces at the receiver, as a buffer overflow with no error at the transmitter: every packet was well-formed, every LCRC passed, every credit check returned true.

P8 fails at cycle 2, deterministically, without needing the overflow to occur — because it checks the reason for the admission rather than the consequence. §14's PH = 1 two-packet test provokes it in four cycles.

15. Debugging

Credits disappear while the Link is stalled

Consumption is tied to a level rather than an event (§2).

Check whether the decrement correlates with pkt_valid or with send_fire. One waveform separates them: if the pool falls while the analyzer shows no traffic, the counter is being driven by the packet's existence.

The signature is a monotonic drain with an idle Link — and it terminates in a transmitter that has spent all its credit on packets that never left.

Two packets launch with only one header credit

No reservation state, or the arbiter is testing the wrong number (§4).

Check what can_reserve compares against. If it is total availability rather than unreserved capacity, that is mutation 6 — and note it satisfies every other check, because the arithmetic is right and only the question is wrong.

The tell in the lab: it only happens when the pipeline is busy, and it stops when you slow anything down.

Credit exhaustion appears after errors

Almost certainly a replay re-consuming credit (§9, mutation 8).

The signature is diagnostic on its own: credit consumption exceeds the number of distinct TLPs sent, by exactly the number of replays. Compare a count of unique sequence numbers transmitted against a count of consume events — on a clean Link they match, and on an erroring Link they diverge by the replay count.

And it is worst exactly when it hurts most, since replays cluster during error bursts.

Credit counters exceed the original capacity after returns

Either a duplicate update was applied twice, or a cumulative total was treated as a delta — Chapter 16.6 §5 and §8 own both.

Check account_error and range_error first. If either fired, the engine caught it at the boundary and the fault is upstream in the update path. If neither did and the counter still grew, the range check is missing.

Available credit exists but the packet stays blocked

Read blocked_pool — six bits, and the one that is set names the constraint.

If none is set, credit is not the blocker: check replay_space and the transmit path (Chapter 16.1 §10).

And if the packet needs a pool that was never initialised, it is permanently ineligible — no information means no permission, and that is correct behaviour rather than a fault.

16. Common Misconceptions

"Credit is consumed when the packet becomes valid." On the declared irrevocable ownership event — valid is a level, not an event (§2, P1).
"Scheduler selection means consumption." Selection is revocable; consumption is not (§2, §5).
"Header and data pools may be consumed separately." Every required pool commits atomically, or none does (§7, P5).
"Reservation and consumption are the same thing." Three states, not two — and a design with no word for "reserved" cannot express §4's problem (§5).
"Reservation is unnecessary in a pipelined transmitter." It is only necessary in a pipelined transmitter, and §4 is why.
"A retransmission is a new credit-consuming transaction." This design's contract says it is not — and the normative rule is not published here (§9).
"Stale packet metadata may be used to compute the cost at consume time." The cost travels with the packet (§10, P12).
"Returned credit can always be used in the same cycle." That is a local contract, and it must be declared. Both answers are valid designs (§7).
"Credit counters may wrap internally without checks." Widened arithmetic and an explicit range check, or availability appears enormous (§7, P11).
"FC credit consumption is the same as replay-buffer allocation." Remote receive capacity versus local storage (Chapter 16.1 §3, P15).
"One pool can borrow from another." Six independent pools; isolation is the mechanism (P16).
"A successful ACK restores credit." An ACK retires replay storage; UpdateFC returns credit (P15).
"If the arithmetic is right, the accounting is right." §4's counters were arithmetically perfect and the design still double-spent. The question the arbiter asks is as important as the number it reads.

17. Understanding Check

18. What's Next

The three cost chapters asked what; this one answered when. Credit changes on a declared irrevocable event and on nothing else — not on valid, not on selection. Every required pool commits together or none does. And in any transmitter deep enough to hold a packet in flight, there is a third state: reserved, which is what lets an arbiter ask "how much is unpromised" instead of "how much is unspent".

The vocabulary was the engineering. §4's double-spend exists entirely because a design had no word for "committed but not gone", and therefore no state for it, and therefore no way to answer the only question that mattered.

Chapter 16.6 — Credit Updates closes Module 16 from the far end. Everything here spent credit; nothing here explained where it comes back from. When does receive storage actually become reusable, how is that progress carried in a cumulative counter that wraps, and how does a transmitter turn a wrapping total back into live credit exactly once — never twice on a duplicate, and never lost when one update goes missing.

The idea to carry forward: the number you read is only as good as the question you asked it.