Flow-Control Logic

Chapter 19.4 gave every buffer a depth, a threshold and a lifetime. What decides whether an object may enter one of them at all is a number this side holds about storage it cannot see. This chapter builds the machine that maintains that number.

1. The One-Sentence Model

A credit is not permission to send. It is a claim this side holds on storage that exists on the other side of the link — so the only property that matters is that the sum of all outstanding claims never exceeds the storage those claims describe. Every bug below is a moment when a claim was created without storage, destroyed without release, duplicated, or survived the storage it described.

That framing decides the RTL. A counter is not the thing being designed; it is a replica, maintained locally, of a fact that lives on the far die. A replica can be wrong in exactly four ways — too large, too small, updated at the wrong moment, or updated by an event belonging to a fact that no longer exists — and §§13–31 are those four ways, in RTL.

2. What This Chapter Owns

13.1 owns the accounting model. This chapter owns the machine that implements it — and the distinction is not a formality, because everything below is a failure of implementation on top of an accounting model that was already correct on paper:

Three numbers that get collapsed into one (§4–§7). Physical capacity, allocatable capacity and advertised credit are different, and §§38–39 are the design that advertises the wrong one.

Arithmetic that is wrong before it is wrong (§10–§16). A counter one bit too narrow boots the link with zero credits; an unsigned subtraction evaluated in the wrong order converts a two-unit consumption into a maximum-value credit grant.

Events chosen at the wrong instant (§17–§23). Consume on valid, consume on a grant, return when the read begins — three lines that each look like the correct line.

A return that arrives twice, or from a link that no longer exists (§24–§31).

A batching threshold that deadlocks a link with free capacity and no correctness failure anywhere (§40–§44) — the chapter's flagship liveness bug.

And a conservation law strong enough to catch all of them (§53–§56), with the reason a scoreboard built from the design's own consume signal catches none of them.

3. Sourcing

4. Three Different Numbers

The single most common flow-control defect is not an arithmetic error. It is using one number where the design needs three.

Three properties follow, and each one is a bug when it is forgotten.

Physical capacity is the only one that is constant, which is why it is the only one safe to bake into an assertion bound.

Allocatable capacity can be far below physical free space — 13.2 §8 established that free is not allocatable; §38 below is the RTL that ignores it.

And advertised credit is always stale. It describes the receiver's state as of the last advertisement that has propagated, and the link's flight time means the sender is always acting on old information. That staleness is not a defect to remove — it is the reason a conservative advertisement is a correctness requirement rather than a performance choice.

The rule. Advertise from allocatable, bound assertions with physical, and never let the sender's replica be derived from anything but the messages it actually received.

5. The Fourth Number Nobody Writes Down

There is a fourth quantity, and it has no register anywhere in the design: capacity that has been promised and is neither free nor yet occupied.

The instant a sender consumes a credit, the receiver's entry is not yet occupied — the object is still in flight, in the transmit queue, in the PHY, on the wire. The entry is not free either, because the sender has already committed it. That capacity exists only as an implication of two counters on two dies, and it is the reason conservation must be stated over the whole loop rather than at either end.

physical_capacity
  =  occupied                 // an object is sitting in the entry
   +  reserved                // held back locally: safety, progress, repair
   +  allocatable             // free and offerable
   +  promised_not_yet_arrived // consumed by the sender, not yet landed

The last term is exactly the sender's spent credits that have not yet become occupancy, and no single register holds it. Two consequences:

The receiver must never re-offer promised capacity. It cannot see the promise directly — it sees only that it has advertised n and had m arrivals. §38's design forgets this and offers physical free space, which double-counts the promised term.

And the verification model must hold it explicitly (§55). A scoreboard that tracks only "sender credit" and "receiver occupancy" has a gap exactly the size of the flight time, and every over-advertisement bug lives in that gap.

6. The Machine, End to End

Read the loop, not the blocks. Every arrow is a place where information about capacity is converted into a different representation, and every conversion is lossy in one direction: allocatable loses the reason for the reservation, the advertisement loses the instant it was computed, the replica loses everything except a count.

Two crossings of the die boundary appear, and they have different latencies in general. The advertisement path and the return path are not symmetric, which is why §44's liveness argument needs the return path stated separately.

And notice what is absent. There is no arrow from the receiver's occupancy directly to the sender's replica. The sender can never observe the receiver's state; it can only observe messages about it, and every bug below is a moment when the design forgot that.

7. The Credit Domain Descriptor

// ILLUSTRATIVE. A verification-and-design view of one credit domain. This is
// NOT a UCIe structure and no field here is claimed to exist on any interface
// (Section 3). Widths are symbolic.
typedef struct packed {
  logic [CAP_W-1:0]   physical_capacity;   // elaboration constant, per domain
  logic [CAP_W-1:0]   occupied;            // receiver-side, observed
  logic [CAP_W-1:0]   reserved;            // safety + progress + repair
  logic [CAP_W-1:0]   advertised;          // what the peer has been told
  logic [CAP_W-1:0]   returned_pending;    // released, not yet advertised
  logic [EPOCH_W-1:0] epoch;               // which synchronisation this belongs to
} credit_domain_t;

Architecture. One descriptor per domain, per direction. The receiver owns the first five fields; the sender owns a replica of advertised only — and drawing the struct with all six fields together is a modelling convenience, not a suggestion that one block holds them all.

State. physical_capacity has elaboration lifetime; occupied and reserved have cycle lifetime; advertised and returned_pending have epoch lifetime; epoch has link-synchronisation lifetime.

Cycle behaviour. In one cycle the receiver may take an arrival, release an entry, change a reservation and emit an advertisement — so all five mutable fields can move together, and any RTL that updates them in separate always_ff blocks with separate qualifications will eventually let them disagree.

Contract. The invariant that binds them is §53's conservation equation, not any individual bound.

Failure. The descriptor's real value is that it makes an omission visible. A design whose credit block has no reserved field cannot implement §45's progress reserve, and a design with no epoch field cannot implement §30's stale-return rejection — the missing fields are the missing mechanisms.

DV. The scoreboard of §55 holds exactly this structure, derived independently — that is the whole point of §56.

8. Credit State Is Indexed, Not Scalar

Credit state must be indexed by whatever partitions the storage it describes. Candidates, in rough order of how often they matter:

• resource class — the receive structures are physically separate, so their capacities are separate;
• protocol — where per-protocol paths have their own storage;
• virtual or resource channel — where the architecture defines one;
• direction — transmit and receive credit are unrelated quantities (19.1 §41);
• link, in a multi-link package (18.4);
• destination, where a shared fabric fans out.

The test is physical, not logical. Two flows share a credit counter if and only if they draw from one physical pool of entries at the receiver. If they draw from different structures, one counter cannot describe both — and this is a fact about the receiver's floorplan, not about how the protocol groups traffic.

No class or pool count is claimed for UCIe (§3). NUM_CLASSES below is a parameter, and choosing it is an architecture decision informed by your revision.

9. Wrong RTL — One Global Credit Pool

// WRONG — one counter for storage that is physically several structures.
logic [CREDIT_W-1:0] credit_q;
assign may_send = (credit_q != '0);

19.3 §39 showed this at the Adapter's admission term. Here is why it fails in both directions, with the arithmetic:

Direction one — overflow. Control storage holds 4 entries, bulk holds 28, total 32. Bulk traffic has consumed 20; the global counter reads 12. A control object arrives, the counter is non-zero, it is admitted. But control's own 4 entries are full. The global sum was made of the wrong entries. The receiver's control structure overflows, and from the sender's accounting nothing was exceeded — no assertion on credit_q can fire, because credit_q was never wrong about the thing it was counting. It was counting the wrong thing.

Direction two — a false stall. Bulk exhausts the global counter to zero. A control object now cannot be admitted even though all 4 control entries are free. Throughput is lost with no error anywhere.

Three properties make this hard to catch.

The two failures have opposite symptoms — a data-corrupting overflow and a benign-looking stall — from one line of RTL, so a team that fixes the stall by increasing the global initial value makes the overflow more likely.

The diagnostic signature is misleading. Aggregate credit is comfortably non-zero right up to the moment it is zero, so the stall looks like a cliff rather than one class draining. Per-class counters make the same event look like exactly what it is.

And it survives directed testing. Any test that exercises one class at a time passes. The bug needs two classes with asymmetric depths and asymmetric load — which is the steady state in production and rarely the state in a directed test.

10. The Counter Width

A counter that must represent every legal credit value for a depth of DEPTH must hold DEPTH + 1 distinct values — zero through DEPTH inclusive.

// ILLUSTRATIVE. The +1 is the whole point: DEPTH+1 values, 0..DEPTH.
localparam int CREDIT_W = $clog2(DEPTH + 1);
 
// Pointer width, for contrast — this indexes DEPTH entries, so it is different.
localparam int PTR_W    = (DEPTH <= 1) ? 1 : $clog2(DEPTH);

Architecture. Two widths that look interchangeable and are not. A pointer selects one of DEPTH entries; a credit counts from 0 to DEPTH. Those are different cardinalities — DEPTH versus DEPTH + 1 — and they coincide only when DEPTH is not a power of two, which is exactly why the bug hides.

State. Elaboration constants.

Cycle behaviour. None — but the value chosen here determines whether the very first advertisement is representable.

Contract. Every register, port and comparison that carries a credit quantity must be CREDIT_W wide. A single PTR_W-wide port in the middle of the chain reintroduces the defect at that point and nowhere else, which makes it a genuinely difficult bug to localise.

Failure. §11.

DV. §12's elaboration assertion, plus a parameter sweep that includes DEPTH values of 1, 2, 3, 15, 16, 17 — the powers of two and their neighbours, because only the powers of two fail.

11. Wrong Width — $clog2(DEPTH)

// WRONG — DEPTH values, not DEPTH+1. Fails only when DEPTH is a power of two.
localparam int CREDIT_W = $clog2(DEPTH);
logic [CREDIT_W-1:0] credit_q;

Worked, with DEPTH = 16. $clog2(16) is 4. A 4-bit register represents 0 through 15. The initial advertisement is 16. 4'(16) is 4'b0000.

The link boots reporting zero credits and never sends anything.

Four properties make this the classic parameterisation bug.

It is silent. No overflow, no assertion, no X. The counter holds a perfectly legal value that happens to be wrong.

The symptom is maximally misleading. A link that trains successfully, reports healthy, and transmits nothing looks like a training bug, a clocking bug, or a far-end bug. It is an arithmetic bug in a localparam.

It passes on the depth the team debugged with. A depth of 12 or 20 works perfectly — 4-bit and 5-bit counters respectively both represent the value. The bug appears when a product picks a round number, and round numbers are what products pick.

And the mirror case is worse. If the truncation happens on a maximum rather than an initial value — for example a re-advertisement of DEPTH after recovery — the link runs correctly for hours, recovers once, and then stops. The failure is now separated from its cause by the entire uptime of the link.

The related trap. $clog2(DEPTH) also returns 0 for DEPTH = 1, producing a zero-width or negative-width declaration depending on the tool. §10's pointer expression guards it; the credit expression does not need the guard because $clog2(2) is 1, but a design that copies the guard onto the credit width and forgets the +1 has now written the bug deliberately.

12. SVA — The Advertisement Fits the Counter

// MANDATORY, and an ELABORATION check, not a runtime one — a runtime assertion
// on a truncated value cannot fire, because the truncated value is legal.
initial begin
  assert (CREDIT_W >= $clog2(DEPTH + 1))
    else $fatal(1, "CREDIT_W=%0d cannot represent DEPTH=%0d", CREDIT_W, DEPTH);
  assert (DEPTH >= 1)
    else $fatal(1, "DEPTH must be at least 1");
end
 
// MANDATORY, runtime — an advertisement never exceeds what this side can hold.
property p_advert_fits_capacity;
  @(posedge clk) disable iff (!rst_n)
    advert_valid |-> (advert_value <= CAP_W'(PHYSICAL_CAPACITY));
endproperty
a_advert_fits_capacity: assert property (p_advert_fits_capacity);
 
// MANDATORY — after an advertisement is applied, the replica equals it exactly.
// Not "at least", not "approximately": exactly, or a straggler was absorbed.
property p_advert_sets_exact;
  @(posedge clk) disable iff (!rst_n)
    advert_apply |=> (credit_q == CREDIT_W'($past(advert_value)));
endproperty
a_advert_sets_exact: assert property (p_advert_sets_exact);

Architecture. One elaboration check and two runtime checks, and the elaboration check is the one that catches §11. This is the general principle: a width defect produces a legal value, so it must be caught where widths are known — at elaboration — and not where values are observed.

Why p_advert_sets_exact uses equality. An inequality would pass while a stale return (§29) added to the freshly applied advertisement in the same or the following cycle. Equality turns "a straggler was absorbed into the new epoch" into an immediate failure at the exact cycle it happened, rather than an overflow several thousand cycles later. This is the strongest single property in the chapter for the cost of one line.

DV. Sweep DEPTH across 1, 2, 3, 4, 7, 8, 9, 15, 16, 17, 31, 32, 33 and confirm the elaboration assertion is the thing that fails when the width expression is deliberately broken.

13. Consume and Return in the Same Cycle

At the operating point the design was built for, the producer and the consumer are both active. A consume and a return in the same cycle is therefore not a corner case — it is the common case, and any RTL that treats it as an exception is wrong at full load and right when idle.

// ILLUSTRATIVE. Single-unit form. One owner, all four arms enumerated, and the
// both-arm written explicitly rather than left to a default.
always_ff @(posedge clk or negedge rst_n) begin
  if (!rst_n) begin
    credit_q <= '0;                      // NOT full — see Section 35
  end else if (advert_apply) begin
    credit_q <= CREDIT_W'(advert_value); // atomic re-baseline, Section 12
  end else begin
    unique case ({credit_consume, credit_return})
      2'b10  : credit_q <= credit_q - CREDIT_W'(1);
      2'b01  : credit_q <= credit_q + CREDIT_W'(1);
      2'b11  : credit_q <= credit_q;       // spent and regained — net zero
      default: credit_q <= credit_q;       // idle
    endcase
  end
end

Chapter 9.5 §6 established the four-case discipline and 13.1 §9 established it per domain. What this chapter adds starts at §14, because the form above is only correct while both events carry exactly one unit.

Three things in the block above are load-bearing and easy to lose in a refactor.

The advertisement branch is above the case, not inside it. An advertisement is a re-baseline, not a delta, so it must not be combined with a consume or a return in the same cycle — it replaces the value those events were modifying. §29 is what happens when a delta is allowed to reach a freshly baselined counter.

The 2'b11 arm is written out. Folding it into default produces identical behaviour today and is one refactor away from a bug, because a later engineer adding a fifth condition to the default arm silently changes the simultaneous case.

And there is exactly one always_ff writing credit_q. Two blocks — one handling consumption, one handling returns — is the shape of the defect in 19.1 §13, and here it loses a return on every simultaneous cycle, which is to say on most cycles at full load.

14. Multi-Unit Delta Arithmetic

Real credit paths are not one-unit-at-a-time. A batched return (§41) carries several units; a large object may consume several; an advertisement update may deliver a delta rather than an absolute. The moment either side can carry more than one unit, the case statement of §13 is insufficient and must become arithmetic — and the arithmetic must be signed and wider than the counter before anything is truncated.

// ILLUSTRATIVE. The delta is computed at CREDIT_W+1 bits, SIGNED, so that both
// an over-return and an over-consume are representable rather than wrapped.
logic signed [CREDIT_W:0] delta;
logic signed [CREDIT_W:0] next_credit_ext;
 
assign delta = $signed({1'b0, return_count})     // zero-extend, then treat as signed
             - $signed({1'b0, consume_count});
 
assign next_credit_ext = $signed({1'b0, credit_q}) + delta;
 
// The range check happens on the EXTENDED value, before any truncation.
assign credit_underflow = (next_credit_ext < 0);
assign credit_overflow  = (next_credit_ext > $signed({1'b0, active_capacity}));
assign credit_fault     = credit_underflow || credit_overflow;
 
always_ff @(posedge clk or negedge rst_n) begin
  if (!rst_n)                credit_q <= '0;
  else if (advert_apply)     credit_q <= CREDIT_W'(advert_value);
  else if (credit_fault)     credit_q <= credit_q;          // hold and raise
  else                       credit_q <= CREDIT_W'(next_credit_ext);
end

Architecture. Compute wide and signed, check the range, then truncate. The extra bit is not paranoia — it is the only place an illegal result can be represented long enough to be detected. Once the value is truncated into CREDIT_W bits, an out-of-range result has become an in-range lie.

State. delta and next_credit_ext are combinational; credit_q is the only register.

Cycle behaviour. All three of return_count, consume_count and advert_apply may be active in one cycle. The priority chain settles that: an advertisement wins, because it is a statement about the whole quantity rather than a change to it. Whether stragglers in the same cycle should be counted into the new epoch is exactly §29's question, and the answer here is that they must not be.

Contract. active_capacity is the current upper bound (§36), not the elaboration parameter — a repaired or degraded link may be operating below its structural maximum, and bounding against the structural maximum would let a real over-return pass.

Failure. credit_fault holds the counter and raises a fault rather than saturating. Saturation is the wrong response: it converts a detected accounting failure into a plausible-looking number and lets the link continue with a corrupted replica. Holding preserves the last known-good value and makes the event visible.

DV. Drive every combination of consume_count in 0..N and return_count in 0..M, including both at maximum in the same cycle, and separately force each of credit_underflow and credit_overflow and confirm the counter holds rather than moves.

15. Wrong RTL — Unsigned Subtraction First

// WRONG — unsigned arithmetic, left to right, truncated at CREDIT_W.
credit_q <= credit_q + return_count - consume_count;

Worked, with CREDIT_W = 5 and a capacity of 16. credit_q is 1, return_count is 0, consume_count is 2.

SystemVerilog evaluates left to right in a 5-bit context: 1 + 0 = 1, then 1 - 2 = 5'b11111 = 31.

The counter now reads 31 against a capacity of 16. The sender believes it has nearly twice the far end's total storage available, admits objects freely, and the receiver overflows — the catastrophic direction, arrived at from a single-unit deficit.

Four properties make this worse than it first looks.

The expression is the natural one to write. It reads exactly like the equation it implements. Nothing about it looks dangerous, and it is what a reviewer expects to see.

It is order-dependent, so it can be "fixed" by luck. Writing credit_q - consume_count + return_count fails in a different pattern; writing credit_q + return_count - consume_count fails only when the running total dips below zero mid-expression. A team that reorders the terms to fix an observed failure has made the bug rarer, not absent.

The bound assertion of §16 does catch it — one cycle later. By then the wrong value is already gating admission combinationally, so a same-cycle admission decision was made on 31. This is why the range check belongs on the extended value before the register, not on the register afterwards.

And it is a load-correlated bug. The dip below zero requires a consumption larger than the current credit, which requires the credit to already be low, which requires the link to be busy. It cannot happen in a quiet test.

16. SVA — The Counter Stays in Range

// MANDATORY. Two-sided, and bounded by ACTIVE capacity (Section 36), not by the
// structural parameter — a degraded link has a smaller legal maximum.
property p_credit_in_range;
  @(posedge clk) disable iff (!rst_n)
    (credit_q <= active_capacity);
endproperty
a_credit_in_range: assert property (p_credit_in_range);
 
// MANDATORY — the pre-truncation value never leaves the range either. This is
// the one that fires in the SAME cycle as Section 15's wrap, not after it.
property p_next_credit_in_range;
  @(posedge clk) disable iff (!rst_n)
    !advert_apply |-> (!credit_underflow && !credit_overflow);
endproperty
a_next_credit_in_range: assert property (p_next_credit_in_range);
 
// MANDATORY — no consumption without sufficient credit, checked on the CURRENT
// value, before the decrement. Multi-unit form.
property p_no_consume_without_credit;
  @(posedge clk) disable iff (!rst_n)
    (consume_count != '0) |-> (fc_state == FC_ACTIVE)
                           && (consume_count <= credit_q);
endproperty
a_no_consume_without_credit: assert property (p_no_consume_without_credit);

Architecture. A bound on the register, a bound on the intermediate, and the flow-control guarantee itself.

Why the second property is not redundant. The first one is evaluated on credit_q, which is the truncated result — and §15's wrap produces a truncated result of 31 against a capacity of 16, so the first property does catch that particular case one cycle late. But a wrap that happens to land inside the legal range is invisible to the first property and visible to the second. With CREDIT_W = 5, a credit of 2 and a consume of 20 wraps to 18, which fails; a credit of 2, a return of 30 and a consume of 16 lands at 16, which passes the bound and is completely wrong. Only the pre-truncation check sees it.

Why the third names FC_ACTIVE. Consumption before synchronisation is complete is consumption against capacity that was never confirmed (§35). Folding the state term into the credit property is cheaper than a separate assertion and makes the sequencing requirement explicit at the point it matters.

DV. Directed injection of each violation; then a long random run with the properties bound, because the interesting failures are the ones that require a specific ratio of counts to current value.

17. The Consume Event

A credit is consumed at the instant remote capacity becomes committed, and at no other instant. Everything in this section is the work of deciding which cycle that is.

The candidates, and why three of them are wrong:

// ILLUSTRATIVE. Two terms, and both are necessary. The first is an actual
// transfer; the second excludes transfers that do not create a NEW remote
// allocation. What falls into the second category is architecture-defined and,
// for retransmission specifically, is Section 51's sourcing question.
assign credit_consume_fire = object_commit_fire
                          && requires_new_remote_allocation;
 
assign consume_count = credit_consume_fire ? object_credit_units : '0;

Architecture. A handshake-qualified event, further qualified by whether the object needs storage the far end has not already set aside for it.

State. None — it is a pulse, and it must be a pulse. A level here is §18.

Cycle behaviour. One assertion per committed object, regardless of how many cycles the object's data takes to cross the link. A multi-beat object consumes on one of its beats, not on each — and which beat is an architecture choice that must be consistent between the consume event and the receiver's occupancy accounting, or the two ends count different things.

Contract. object_credit_units must be computed from the same object description the receiver will use to charge its own storage. If the sender charges by object and the receiver allocates by beat, conservation cannot close — and the mismatch appears only for objects whose beat count differs from the common case.

Failure. §18 and §19, which are the same failure reached two ways: a credit charged for something that did not commit remote capacity.

DV. Count credit_consume_fire assertions and compare against the number of distinct objects the receive-side monitor observes arriving. Those two numbers must be equal over any interval that starts and ends with an empty link — and any difference is a leak or an inflation, with the sign telling you which.

18. Wrong Consume — on valid

// WRONG — a level, not an event.
assign credit_consume_fire = tx_valid;

Worked. The source asserts tx_valid and holds it while the downstream path is stalled for 8 cycles. The credit counter decrements 8 times for one object.

Seven credits are destroyed. They describe storage that is genuinely free at the far end and that this side will now never use.

Four properties.

The direction is the survivable one, which is why it lives. The link becomes slow, then stops. It does not corrupt data and it does not overflow the far end. A team under schedule pressure raises the initial credit value, throughput returns, and the leak continues at the same rate — now with a longer time-to-symptom.

The rate is proportional to congestion. At light load valid and ready coincide and the bug is invisible; the leak rate scales with exactly the backpressure the credit system exists to manage. The bug is quietest when the link is idle and fastest when it matters.

No bound assertion fires. The counter descends through entirely legal values and stops at zero, which is a legal value. §16's properties all pass forever.

And the far end looks healthy, because it is. Its occupancy returns to baseline, its buffers drain, and every check it runs passes. The asymmetry — sender at zero credit, receiver empty — is the diagnostic signature of §63, and it is the only thing that identifies this bug quickly.

The correction is one conjunction: tx_valid && tx_ready, further qualified by §17's allocation term. That is the entire fix, and the assertion of §20 is what stops it being reintroduced.

19. Wrong Consume — on a Grant

// WRONG — a grant is a selection, not a transfer.
assign credit_consume_fire = arb_grant[c];

This is §18 wearing a disguise, and it is harder to spot because a grant genuinely is an event rather than a level, so the usual review question — "is that a pulse?" — returns the wrong answer.

Worked. The arbiter grants class c. The downstream stage is not ready. Depending on the arbiter, the grant either persists until the transfer happens, or is withdrawn and re-issued next cycle when the requester is re-evaluated. Both variants charge a credit for a transfer that has not occurred, and the re-issuing variant charges once per cycle of stall, which is §18's leak rate exactly.

The general rule, now seen at enough layers to name.

Advance state only on an actual transfer, never on a grant. A grant is a statement about arbitration; a transfer is a statement about the world. This curriculum has now hit the distinction in the transmit queue, the replay ring, the semantic table, the buffer pointers and here — and the credit counter is the instance where the consequence is a distributed one, because the state being advanced describes storage on the other die.

The subtle sub-case. Where the arbiter is bound — where a grant guarantees a transfer in the same cycle because the ready term was part of the request qualification — consuming on the grant is arithmetically correct today. It is still the wrong line to write, because it makes the credit machine depend on an internal property of the arbiter, and the first arbiter change that decouples grant from transfer breaks flow control silently. Qualify on the transfer even when the grant is currently equivalent.

20. SVA — One Consume Per Allocation

// MANDATORY. A consume must coincide with an actual commit — never with a
// bare valid, a bare grant, or a stalled cycle.
property p_consume_on_commit_only;
  @(posedge clk) disable iff (!rst_n)
    credit_consume_fire |-> (object_commit_fire && requires_new_remote_allocation);
endproperty
a_consume_on_commit_only: assert property (p_consume_on_commit_only);
 
// MANDATORY — no second consume for the same object identity. Identity comes
// from the verification monitor's tag (Section 55), NOT from a protocol field.
property p_consume_once_per_object(int unsigned tag);
  @(posedge clk) disable iff (!rst_n)
    (credit_consume_fire && (commit_tag == tag))
      |=> always !(credit_consume_fire && (commit_tag == tag));
endproperty
 
// MANDATORY — a stalled transfer does not consume. This is Section 18 directly.
property p_no_consume_while_stalled;
  @(posedge clk) disable iff (!rst_n)
    (tx_valid && !tx_ready) |-> (consume_count == '0);
endproperty
a_no_consume_while_stalled: assert property (p_no_consume_while_stalled);

Architecture. Three properties covering the event's cause, its multiplicity and its most common false trigger.

Why the multiplicity property needs a monitor tag. 19.2 §21 established that a protocol identity can legitimately be reused after retirement, so a property keyed on a protocol field would fire falsely on a legitimate reuse. The verification-only tag is unique for the life of the simulation, which is what makes "never again" a checkable statement. This is the same tag 13.1 §17's scoreboard uses as its join key, and for the same reason.

Why p_no_consume_while_stalled is worth writing separately even though p_consume_on_commit_only implies it: it names the failure. When it fires, the message says "a stalled cycle consumed credit" rather than "the commit qualification is wrong", and the first message is the one that gets the bug fixed in an afternoon.

DV. Force multi-cycle stalls at every point in the transmit path, with valid held; the third property must remain quiet. Then break the qualification deliberately and confirm all three fire.

21. The Return Event

A credit returns when the remote storage it describes becomes genuinely reusable, and not one cycle earlier.

The candidates, and why four of them are wrong:

// ILLUSTRATIVE. The release event, guarded so one entry can return at most once
// (Section 25). The guard is what makes this different from a bare pulse.
assign entry_release_fire = rx_entry_pop_fire;           // an actual pop, not a read
 
assign credit_return_fire = entry_release_fire
                         && rx_entry_q[pop_idx].valid
                         && !rx_entry_q[pop_idx].credit_returned;

Architecture. A handshake-qualified pop, guarded by a per-entry bit.

State. The credit_returned bit is per entry with entry lifetime — it is set when the return is generated and cleared when the entry is next allocated, and clearing it anywhere else is a bug.

Cycle behaviour. One release may produce one return; several structures may release in one cycle, which is why §48's arbitration exists.

Contract. "Reusable" must mean the same thing to the allocation logic and the return logic. If allocation can hand out an entry that a downstream stage is still reading, the return was correct and the allocation is the bug — and the two are easy to get out of step when a pipeline stage is added later.

Failure. §22 for the timing, §24 for the multiplicity.

DV. Compare the total returns emitted against the total pops observed by an independent receive-side monitor over a long run; they must be equal, and any surplus is §24.

22. Wrong Early Return — Distributed Use-After-Free

// WRONG — returning when the read starts rather than when the entry is freed.
assign credit_return_fire = rx_entry_read_start;

Worked. The receive entry holds an object. A downstream stage begins reading it — a multi-beat read taking 6 cycles. The credit returns immediately.

The sender sees the credit, admits a replacement object, and it arrives 4 cycles later. The allocator, believing the entry is free, writes the new object over the old one while the downstream stage is still reading beats 5 and 6.

This is a use-after-free with the free and the use on different dies.

Five properties make it one of the worst failures in the chapter.

It corrupts data rather than stalling. Unlike every leak in this chapter, this one produces wrong values delivered as correct ones.

No transport check catches it. The old object crossed the link perfectly and its CRC was fine. The new object crossed the link perfectly and its CRC was fine. The corruption is a local ownership failure at the receiver, invisible to every integrity mechanism the Adapter has — the same blind spot 19.4 §36's ping-pong bug lives in.

It is partial. Only the beats the consumer had not yet read are wrong. The object is nearly right, which for numerical or streaming payloads can pass a tolerance check and be attributed to something else entirely.

It is timing-dependent in the direction that hides it. If the round-trip is longer than the read, the replacement always arrives after the read completes and nothing goes wrong. The bug appears only when the link is fast relative to the consumer — which is the regime the whole system was optimised toward.

And every credit assertion passes. The counter never leaves its range, the conservation equation closes, no consume is unmatched. The accounting is perfect; the meaning of one event is wrong.

The rule. A return is a statement about storage, not about data movement. If the design cannot point at the exact cycle after which the entry may be overwritten, it cannot correctly generate a return.

23. SVA — A Return Means Released Storage

// MANDATORY. A return implies the entry is actually free THIS cycle.
property p_return_implies_released;
  @(posedge clk) disable iff (!rst_n)
    credit_return_fire |-> (entry_release_fire && !rx_entry_q[pop_idx].valid_d);
endproperty
a_return_implies_released: assert property (p_return_implies_released);
 
// MANDATORY — the effect check, which catches Section 22 even if the cause
// check is written against the same wrong signal. An entry that has had its
// credit returned is never subsequently read.
property p_no_read_after_return(int idx);
  @(posedge clk) disable iff (!rst_n)
    (credit_return_fire && (pop_idx == idx))
      |=> !(rx_entry_read_fire && (read_idx == idx))
          until (rx_entry_alloc_fire && (alloc_idx == idx));
endproperty
 
// MANDATORY — an entry allocated while its previous occupant is still being
// read. The direct statement of the hazard.
property p_no_alloc_over_live_read(int idx);
  @(posedge clk) disable iff (!rst_n)
    (rx_entry_alloc_fire && (alloc_idx == idx)) |-> !read_in_progress_q[idx];
endproperty

Architecture. A cause check, an effect check and a hazard check.

Why the effect check exists. This is the most important verification lesson in the section. If the designer returns on rx_entry_read_start and the verification engineer writes the cause property against rx_entry_read_start because that is what the RTL does, the property passes and the bug ships. The effect property is written against a different observable — a read occurring after a return — and therefore cannot be satisfied by the same misconception. It is the assertion-level version of §56's argument about scoreboards.

Why the hazard check is stated at the allocator. §22's failure is symmetrical: the return may be early, or the allocation may be careless. Checking only the return leaves the other half unverified, and a design that fixes the return timing and later adds a pipeline stage to the read path reintroduces the same corruption from the allocator's side.

DV. Constrain the read latency long and the round-trip short — the opposite of the natural configuration — because §22 requires exactly that ratio to be observable.

24. The Duplicate Return

A duplicated release event manufactures capacity out of nothing. This is the most dangerous single class of credit bug, because its direction is the overflow direction and its onset is gradual.

How duplicates arise, and none of these is exotic:

• a release event that is a level rather than a pulse, sampled twice;
• a release path crossing a clock domain as a pulse, which 19.1 §40 established will be seen zero, one or two times;
• a retransmitted release message, where the return path itself has a reliability mechanism;
• an entry released once by a normal pop and once by a flush during recovery;
• two structures sharing an entry index and both reporting the release.

The arithmetic of the failure. Each duplicate inflates the sender's replica by one. The counter stays comfortably inside its legal range — a capacity of 16 with 5 spurious credits reads 16 at most, because the sender has also been spending. No bound assertion can fire, because no bound has been exceeded. What has been exceeded is the relationship between the count and the storage, and only conservation (§53) states that relationship.

The onset. The link works. Then, under a load that keeps the receiver near full, the sender's inflated credit lets it admit n more objects than exist entries. The receiver overflows. The overflow happens the first time the receiver is genuinely full, which may be hours or days after the duplicates accumulated — and at that moment the credit counter, the occupancy counter and every bound assertion all look correct.

25. The Per-Entry Return Bit

// ILLUSTRATIVE. The guard that makes a duplicate release harmless. Note where
// the bit is CLEARED — at allocation, and nowhere else.
typedef struct packed {
  logic                valid;
  logic                credit_returned;   // this entry's credit is already back
  logic [EPOCH_W-1:0]  alloc_epoch;       // which epoch allocated it (Section 28)
  logic [PAYLOAD_W-1:0] payload;
} rx_entry_t;
 
rx_entry_t rx_entry_q [DEPTH];
 
always_ff @(posedge clk or negedge rst_n) begin
  if (!rst_n) begin
    for (int i = 0; i < DEPTH; i++) begin
      rx_entry_q[i].valid           <= 1'b0;
      rx_entry_q[i].credit_returned <= 1'b0;
    end
  end else begin
    // Allocation is the ONLY place the guard is cleared.
    if (rx_entry_alloc_fire) begin
      rx_entry_q[alloc_idx].valid           <= 1'b1;
      rx_entry_q[alloc_idx].credit_returned <= 1'b0;
      rx_entry_q[alloc_idx].alloc_epoch     <= credit_epoch_q;
      rx_entry_q[alloc_idx].payload         <= alloc_payload;
    end
    // Release sets the guard, and the guard qualifies the return.
    if (entry_release_fire && !rx_entry_q[pop_idx].credit_returned) begin
      rx_entry_q[pop_idx].valid           <= 1'b0;
      rx_entry_q[pop_idx].credit_returned <= 1'b1;
    end
  end
end

Architecture. Per-entry state converting a rate problem into a set problem. A counter can be incremented twice for one release; a bit can only be set once.

State. One bit per entry, entry lifetime, cleared exclusively at allocation.

Cycle behaviour. Allocation and release of different entries in the same cycle is normal and the two if statements are independent because they index differently. Allocation and release of the same entry in the same cycle must be examined: with the code as written the allocation branch runs first in source order and the release branch would then clear a just-allocated entry. Whether that combination is reachable is an architecture question, and if it is, the release must be qualified with (pop_idx != alloc_idx) || !rx_entry_alloc_fire — and an assertion should state which of the two the design believes.

Contract. The bit is meaningful only if allocation is the sole clear point. A recovery handler that clears credit_returned across all entries "to start clean" has re-armed every entry to return a second time — which is §29's family of bug reached from a different direction.

Failure. §26.

DV. Inject a duplicated release on the same index in consecutive cycles and confirm exactly one return; then inject one across a re-allocation boundary and confirm exactly two, because that is two genuine releases of two genuine occupancies.

26. Wrong RTL — A Scalar Release Counter

// WRONG — no identity, so a duplicate is indistinguishable from a second release.
always_ff @(posedge clk)
  if (entry_release_fire) pending_return_q <= pending_return_q + 1'b1;

Architecture. A counter where the design needs a set. The counter cannot answer the question "have I already returned this entry?" because it does not retain which entries it counted.

Failure. A duplicated release increments twice. There is no cycle at which the design can detect this, now or later, because the information needed to detect it — which entry each increment referred to — was discarded at the moment of the increment.

Three consequences.

Recovery is impossible even after detection. Suppose conservation eventually fires and reports a surplus of 3 credits. The design cannot tell which 3 to withdraw, because it does not know which returns were spurious. The only safe response is a full resynchronisation of the domain (§28), which is a heavier hammer than the bug deserved.

It composes badly with batching. §41's accumulator is also a counter — and it must be, because a batch is a quantity. The guard therefore has to live at the entry, upstream of the accumulator, which is exactly why §25 puts it there. A design that tries to deduplicate inside the accumulator has already lost the identity.

And it cannot express the epoch. §28's stale-return rejection needs to know which synchronisation a released entry belonged to. alloc_epoch in §25's struct carries that; a scalar counter has nowhere to put it.

The general form. This is the seventh appearance in this curriculum of bitmap, not counter — a counter is correct only when the events it counts are indistinguishable and independently generated, and a release event is neither.

27. Return Identity and What It Must Be Tied To

A return carries, at minimum, a quantity. What it must additionally be tied to — and this is a design obligation regardless of how the tie is expressed on the wire — is the answer to two questions:

Does this return refer to capacity that was actually consumed? Does it refer to the link synchronisation that is currently in force?

The two questions are independent. A return can refer to real consumed capacity and to a dead epoch (§29). It can refer to the live epoch and to capacity that was never consumed (§24's duplicate). A design that guards only one of them is exposed to the other, and the guards live in different places: the per-entry bit of §25 answers the first, the epoch comparison of §30 answers the second.

28. The Flow-Control Epoch

Chapter 13.1 §15 established the epoch as a concept: different flow-control state has different recovery lifetimes, and the unsafe outcome is a mixture. This section builds it as a machine and ties it to the FSM of §32, which is what makes the mixture structurally impossible rather than merely checked.

// ILLUSTRATIVE. A LOCAL control-and-verification construct. No claim is made
// that UCIe transports an epoch field (Section 27).
logic [EPOCH_W-1:0] credit_epoch_q;
 
always_ff @(posedge clk or negedge rst_n) begin
  if (!rst_n)                       credit_epoch_q <= '0;
  else if (fc_epoch_advance)        credit_epoch_q <= credit_epoch_q + EPOCH_W'(1);
end
 
// The advance is an FSM output (Section 34), not a raw event. That is the whole
// design: the epoch changes exactly when the machine says the old agreement is
// void, and no earlier — so there is no window in which the counter has been
// re-baselined but the epoch has not.

Architecture. A monotonic tag on the agreement, not on the traffic. It exists to make "this return belongs to a link agreement that no longer exists" a decidable question in one comparison.

State. Link-synchronisation lifetime. It must not be reset by anything narrower than the event that voids the agreement — in particular not by a datapath reset, a counter clear, or a diagnostic reset (19.6 §27).

Cycle behaviour. Advanced once per resynchronisation, on the same cycle the counter is re-baselined, from the same FSM output. Advancing it in a separate always_ff from a separately derived condition reintroduces the window it exists to close.

Width. EPOCH_W must be wide enough that the tag cannot wrap within the maximum lifetime of an in-flight return. Two bits is almost certainly too few — a link that recovers four times while a return is stuck behind a congested path will alias a stale return into acceptance. The cost of extra bits here is trivial and the failure they prevent is §29's.

Contract. Every piece of state whose meaning depends on the agreement must be re-baselined together with the epoch: the counter, the pending-return accumulator, and the receiver's advertised value. A pending-return accumulator that survives an epoch change reports old-epoch releases into the new one, which is §24's inflation arriving by a different route.

Failure. §29.

DV. Force a resynchronisation with returns in flight and confirm the counter equals the new advertisement exactly (§12), not the advertisement plus stragglers.

29. Wrong Recovery — Re-Baseline the Counter, Accept the Stragglers

This is the chapter's flagship correctness bug. It requires no arithmetic error, no width error and no event-qualification error. Every line is individually correct.

// WRONG — the counter is re-baselined on recovery, and returns are applied
// unconditionally. Both halves look right; together they over-advertise.
always_ff @(posedge clk) begin
  if (fc_resync_done)        credit_q <= CREDIT_W'(negotiated_capacity);
  else if (return_valid)     credit_q <= credit_q + CREDIT_W'(return_count);
  else if (consume_fire)     credit_q <= credit_q - CREDIT_W'(consume_count);
end

Worked, cycle by cycle.

The counter now claims 19 against a physical capacity of 16.

Five properties make this the bug to remember.

Both halves are correct in isolation. Re-baselining on resynchronisation is exactly right. Applying returns is exactly right. The defect is that the second has no way to know the first happened, and no code review of either branch finds anything wrong.

The window is small and the consequence is permanent. The straggler must land after the re-baseline — a window of a few cycles to a few hundred, depending on the return path's depth and whether it crosses a clock domain. Miss the window and everything is fine; hit it and the replica is corrupt until the next resynchronisation, which may be never.

It requires a recovery to reproduce, and recoveries are the thing most functional tests are configured not to have. The bug lives in the intersection of two features — reliability and flow control — that are usually verified separately.

The bound assertion of §16 does fire here, because 19 exceeds 16. That is the good news, and it is why §12's exact-equality property matters more: it fires at t+31, at the exact cycle the straggler was absorbed, naming the cause. The bound property fires at the same cycle but says only "too large", and a team can spend a week deciding whether the capacity constant is wrong.

And the mirror failure is silent. If the re-baseline happens after a straggler rather than before, the straggler is simply overwritten and lost. No assertion fires anywhere, no bound is exceeded, and the link runs permanently short by 3 credits. That direction has no symptom at all except reduced throughput — which is why the epoch guard must reject stale returns rather than merely ordering the updates.

The fix is §30, and it is three lines.

30. Stale-Return Rejection

// ILLUSTRATIVE. A return is applied only if it belongs to the current epoch.
// The epoch tie is a LOCAL construct (Section 27).
assign return_accept = return_valid
                    && (return_epoch == credit_epoch_q)
                    && (fc_state == FC_ACTIVE);
 
assign return_count  = return_accept ? return_units : '0;
assign stale_return  = return_valid && (return_epoch != credit_epoch_q);

Architecture. A comparison, an acceptance term and — importantly — a named stale_return signal that is counted rather than silently dropped (§62). A stale return is a normal, expected event during recovery and an alarming one during steady state, and only a counter distinguishes those two cases.

State. None; it is a qualification.

Cycle behaviour. Evaluated per return. The fc_state term prevents returns being applied during the resynchronisation itself, when the counter is mid-transition and the epoch may be about to advance.

Contract. Requires that the epoch is advanced atomically with the re-baseline (§28), or there is a cycle where a same-epoch return is applied to an already-re-baselined counter — the same failure with an extra step.

31. SVA — A Stale Epoch Cannot Move Credit State

// MANDATORY. A stale return changes nothing.
property p_stale_return_inert;
  @(posedge clk) disable iff (!rst_n)
    (return_valid && (return_epoch != credit_epoch_q))
      |=> (credit_q == $past(credit_q)) || $past(advert_apply);
endproperty
a_stale_return_inert: assert property (p_stale_return_inert);
 
// MANDATORY — the epoch advances only with the re-baseline, in the same cycle.
property p_epoch_atomic_with_rebaseline;
  @(posedge clk) disable iff (!rst_n)
    fc_epoch_advance |-> advert_apply;
endproperty
a_epoch_atomic_with_rebaseline: assert property (p_epoch_atomic_with_rebaseline);
 
// MANDATORY — the epoch is monotonic. Catches a reset reaching it from a scope
// that should not touch it (Section 28, and 19.6 Section 27's reset matrix).
property p_epoch_monotonic;
  @(posedge clk) disable iff (!rst_n)
    (credit_epoch_q != $past(credit_epoch_q))
      |-> (credit_epoch_q == EPOCH_W'($past(credit_epoch_q) + 1));
endproperty
a_epoch_monotonic: assert property (p_epoch_monotonic);
 
// MANDATORY — the pending-return accumulator is cleared by a resynchronisation.
// Without this, Section 28's contract is unchecked and old-epoch releases are
// reported into the new epoch.
property p_pending_cleared_on_resync;
  @(posedge clk) disable iff (!rst_n)
    fc_epoch_advance |=> (pending_return_q == '0);
endproperty
a_pending_cleared_on_resync: assert property (p_pending_cleared_on_resync);

Architecture. Four properties: the rejection itself, the atomicity it depends on, the monotonicity that detects an out-of-scope reset, and the accumulator clear that is the easiest half of the contract to forget.

Why the monotonicity property earns its place. An epoch that jumps by more than one, or backwards, means something other than the flow-control FSM wrote it. The most likely culprit is a reset domain that should not have reached it — and that is a bug found at integration by this property, or found in silicon by an overflow. Chapter 19.6 §27 makes the reset matrix that prevents it a deliverable of the IP.

Why the accumulator property is separate from the rest. It checks the receiver's side of the epoch contract while the others check the sender's. They fail independently, and a design that implements stale-return rejection perfectly while carrying an old accumulator forward has moved the inflation from the sender's replica to the receiver's next advertisement — the same overflow, one hop upstream.

DV. Recovery with returns in flight at every distance from the re-baseline: one cycle before, the same cycle, one after, and at the far edge of the quarantine window if §30's fallback is in use.

32. The Flow-Control State Machine

Everything so far has been arithmetic and event qualification. What sequences them — what decides when a counter may be trusted, when a return may be applied, and when the epoch advances — is a small state machine, and giving it explicit states is what removes the ambiguous windows the previous sections kept running into.

The states, and what each one asserts about the world:

Two design decisions in that table are worth stating explicitly.

FC_SYNC and FC_RESYNC are separate states even though their permissions are identical. They differ in what precedes them and in what the epoch does: the first entry establishes epoch zero and has no stale returns to reject; a resynchronisation advances the epoch and does. Merging them makes the epoch-advance condition a side condition inside one state, which is exactly the ambiguity §28 exists to remove.

FC_FAULT holds rather than recovers automatically. A detected conservation violation means the replica and the storage have disagreed, and the design cannot know by how much or in which direction. Automatic re-entry to FC_SYNC would repair the symptom and discard the evidence — 19.1 §35's first-fault record is the pattern, and the exit from FC_FAULT should be a deliberate, externally commanded resynchronisation.

33. The Flow-Control States, Drawn

Read the transition into FC_ACTIVE from FC_RESYNC. The label carries two actions on one edge deliberately — the epoch advance and the re-baseline are the same event, which is §31's p_epoch_atomic_with_rebaseline drawn rather than asserted.

And read what is missing. There is no edge from FC_FAULT to FC_ACTIVE. A fault cannot be cleared by resuming; it can only be cleared by re-establishing the agreement from scratch.

34. The Flow-Control FSM in RTL

// ILLUSTRATIVE. One next-state owner; every output is state-derived or
// registered, never combinational from a raw event.
typedef enum logic [2:0] {
  FC_RESET  = 3'd0,
  FC_SYNC   = 3'd1,
  FC_ACTIVE = 3'd2,
  FC_RESYNC = 3'd3,
  FC_FAULT  = 3'd4
} fc_state_e;
 
fc_state_e fc_state_q, fc_state_d;
 
always_comb begin
  fc_state_d = fc_state_q;                       // default: hold
  unique case (fc_state_q)
    FC_RESET  : if (cfg_valid)          fc_state_d = FC_SYNC;
    FC_SYNC   : if (sync_timeout)       fc_state_d = FC_FAULT;
                else if (cap_confirmed) fc_state_d = FC_ACTIVE;
    FC_ACTIVE : if (credit_fault)       fc_state_d = FC_FAULT;
                else if (resync_req)    fc_state_d = FC_RESYNC;
    FC_RESYNC : if (resync_timeout)     fc_state_d = FC_FAULT;
                else if (cap_confirmed) fc_state_d = FC_ACTIVE;
    FC_FAULT  : if (sw_resync_cmd)      fc_state_d = FC_RESYNC;
    default   :                         fc_state_d = FC_FAULT;
  endcase
end
 
always_ff @(posedge clk or negedge rst_n)
  if (!rst_n) fc_state_q <= FC_RESET;
  else        fc_state_q <= fc_state_d;
 
// Outputs, all derived from the state — this is the block's whole interface
// to the arithmetic of Sections 13-31.
assign allow_consume    = (fc_state_q == FC_ACTIVE);
assign accept_return    = (fc_state_q == FC_ACTIVE);
assign send_advert      = (fc_state_q == FC_ACTIVE) || (fc_state_q == FC_RESYNC);
assign fc_epoch_advance = (fc_state_q == FC_RESYNC) && cap_confirmed;
assign advert_apply     =  fc_epoch_advance;      // the SAME cycle (Section 31)
assign fc_fault         = (fc_state_q == FC_FAULT);

Architecture. A next-state function with one writer and outputs that are pure functions of the state. The credit arithmetic never inspects a raw event such as resync_req or credit_fault directly — it inspects allow_consume and accept_return, which is what makes the sequencing auditable in one place.

State. One register, FC_RESET at reset.

Cycle behaviour. fc_epoch_advance and advert_apply are the same expression, so §31's atomicity property is true by construction rather than by review. Assigning them separately from separately derived conditions is the single most likely way to reintroduce §29 — and it is the kind of change a refactor makes for readability.

Contract. cap_confirmed must mean the peer has agreed, not that this side has asked. §35 is the design that confuses those.

Failure. A default arm that holds rather than faulting would let an illegal encoding — from an SEU, or from an incomplete reset — persist as a working state. Faulting on the default is the conservative choice and costs nothing.

DV. Every arc, including both timeouts and the commanded exit from FC_FAULT. Then a state-coverage bin per state and a transition-coverage bin per arc, because the arcs that are never exercised are the ones that carry the epoch.

35. Wrong Initialisation — Starting Full Locally

// WRONG — the local side assumes the configured depth is available before the
// peer has confirmed anything.
always_ff @(posedge clk or negedge rst_n)
  if (!rst_n) credit_q <= CREDIT_W'(CFG_RX_DEPTH);   // "we know what we built"

The reasoning behind this line is seductive. Both dies are built from the same IP, both are configured with the same depth parameter, so the sender already knows the answer and waiting for the peer to say it is a formality.

Four ways that is false, in increasing order of how badly they hurt.

The peer may be a different implementation. The entire point of a die-to-die standard is that the two dies need not come from the same design team, the same company, or the same generation. A depth this side compiled with is a fact about this side only.

The peer may be operating below its structural capacity. §36's distinction: a repaired, degraded or partially-configured receiver has an active capacity below its physical one. Its parameter is unchanged; its usable storage is not.

The peer may not have drained. After a recovery, the receiver may legitimately still hold entries. A sender that assumes full capacity over-allocates by exactly the number of entries the receiver was holding — 13.1 §16's failure, and the same one arrived at here from initialisation rather than recovery.

And the failure is immediate, at the worst possible moment. Over-allocation at bring-up means the very first burst of traffic overflows the receiver — during initial silicon bring-up, when every other subsystem is also unproven, and when a data-corrupting overflow will be attributed to almost anything before flow control.

The rule. The counter resets to zero and is populated only by an advertisement that came from the peer. FC_SYNC exists so that "we have not been told yet" is a state rather than an assumption — and the reset value of zero is what makes a missing advertisement a stall rather than an overflow.

36. Requested Capacity Is Not Active Capacity

The receiver has two capacity numbers that a naive design collapses into one:

• requested — what configuration asked for, or what the parameter says was built;
• active — what is currently usable, after repair, degradation, partial power-down, or a feature that reserves entries.

// ILLUSTRATIVE. The commit discipline this curriculum has now used at five
// layers: a requested value is staged, validated, and committed atomically.
logic [CAP_W-1:0] cap_requested_q;     // written by configuration
logic [CAP_W-1:0] cap_active_q;        // what the machine actually uses
logic             cap_commit;          // one-cycle atomic commit
 
always_ff @(posedge clk or negedge rst_n) begin
  if (!rst_n) begin
    cap_active_q <= '0;
  end else if (cap_commit) begin
    cap_active_q <= cap_requested_q;   // atomic: one register, one cycle
  end
end
 
// The commit is gated on validation AND on quiescence, never on the write alone.
assign cap_commit = cap_req_pending_q
                 && cap_legal(cap_requested_q)
                 && (fc_state_q == FC_RESYNC)
                 && (occupancy_q == '0);

Architecture. Staged requested value, atomic commit, quiesce guard. This is the sixth appearance of the requested-versus-active pattern in this curriculum — it appeared at the link manager, the Adapter's configuration epoch, the protocol engine's enable mask, and the buffer's thresholds — and the reason it keeps appearing is that every one of those is a number the datapath reads every cycle.

State. cap_requested_q has configuration lifetime; cap_active_q has epoch lifetime, and the two are deliberately different so a configuration write cannot move the datapath's number.

Cycle behaviour. The commit is one register write, so no cycle exists in which part of the capacity has changed.

Contract. Advertise cap_active_q, bound assertions with cap_active_q, and never advertise cap_requested_q — §16's range property already does this, and §37's advertisement engine is where the mistake would be made.

Failure. Advertising the requested value before validation promises storage that may not exist. The quiesce term matters just as much: committing a reduced capacity while entries are occupied means occupied can exceed active_capacity, and every downstream subtraction underflows.

DV. Request a capacity change with traffic in flight and confirm the commit waits; request an illegal capacity and confirm cap_active_q does not move; and check cap_active_q against the advertisement on every advertisement cycle.

37. The Advertisement Engine

// ILLUSTRATIVE. Allocatable is computed once, in one place, from all five terms
// — and the advertisement is a function of allocatable, never of free space.
logic [CAP_W:0] committed_ext;      // one extra bit: the sum can exceed CAP_W
logic [CAP_W:0] allocatable_ext;
 
assign committed_ext = {1'b0, occupancy_q}
                     + {1'b0, reserved_q}          // repair / safety
                     + {1'b0, progress_reserve_q}  // Section 45
                     + {1'b0, promised_q};         // advertised-not-yet-arrived
 
assign allocatable_ext = (committed_ext >= {1'b0, cap_active_q})
                       ? '0                                        // saturate at zero
                       : ({1'b0, cap_active_q} - committed_ext);
 
assign allocatable = CAP_W'(allocatable_ext);
 
// The advertised value is the allocatable number, never the free number.
assign advert_value = allocatable;
assign advert_fire  = send_advert && (advert_value != last_advertised_q);

Architecture. One expression, four subtrahends, an explicit saturation, and an advertisement gated on change rather than emitted every cycle.

State. last_advertised_q exists so the engine does not consume control bandwidth restating an unchanged number — and it must be cleared on an epoch advance, or the first advertisement of a new epoch is suppressed as a duplicate of the last one from the old epoch. That is a genuine and easily-missed bug: the link resynchronises, the allocatable number happens to be the same as before, no advertisement is sent, and the sender sits at zero credits waiting for a message that was optimised away.

Cycle behaviour. All four subtrahends can move in one cycle. Computing them in one combinational expression is what makes the result self-consistent; computing allocatable incrementally as a register updated by deltas reintroduces every drift bug in this chapter at a new location.

Contract. promised_q is §5's fourth number — the capacity advertised and not yet redeemed by an arrival. A design without it double-counts: it advertises n, the sender consumes n, and before those objects arrive the receiver computes free space that still includes them and advertises them a second time.

Failure. The saturation branch is not decoration. Without it, a transient in which committed_ext exceeds cap_active_q — reachable during §36's capacity reduction, or from an off-by-one in a reservation — produces an unsigned underflow and an advertisement of nearly the full counter range. That is §15's catastrophe in the advertisement path rather than the counter path.

DV. Drive each subtrahend to its maximum independently and together; force committed_ext above cap_active_q and confirm the advertisement is zero rather than enormous; and check the last_advertised_q clear on every epoch advance.

38. Wrong Advertisement — Physical Free Space

// WRONG — free space is not allocatable space.
assign advert_value = cap_active_q - occupancy_q;

Chapter 13.2 §10 established this as a policy error. Here is the arithmetic, and the reason it is worse than it looks.

Worked. Capacity 16. Occupied 8. Reserved for repair 2. Progress reserve 2 (§45). Promised-not-yet-arrived 4.

• Physical free: 16 − 8 = 8
• Actually allocatable: 16 − 8 − 2 − 2 − 4 = 0

The design advertises 8 against an allocatable capacity of zero. The sender admits 8 objects. Four entries do not exist at all, and the two reserves are consumed by traffic they were withheld from.

Four properties.

The over-advertisement is not a small error. It is the sum of every term the expression omitted, and those terms are largest exactly when the receiver is busiest — reservations are held, promises are outstanding, and occupancy is high all at the same time. The error scales with load.

Consuming the progress reserve converts a capacity problem into a deadlock. §46 is that failure in full: the reserve existed to let traffic through that releases other entries, and once it is spent nothing can drain.

The promised omission is the one designers do not see. Reservations are visible in the RTL as a register; the promised quantity is not represented anywhere unless the design chooses to represent it (§5). A reviewer checking that the expression subtracts "everything that is subtracted" will not notice a term that has no register.

And the sender is blameless. It consumed exactly the credit it was granted. Every assertion on the sender's replica passes, because the replica correctly tracks a promise that should never have been made. This is why §39's property belongs at the receiver.

39. SVA — Advertised Never Exceeds Allocatable

// MANDATORY. At the receiver, where the truth lives.
property p_advert_le_allocatable;
  @(posedge clk) disable iff (!rst_n)
    advert_fire |-> (advert_value <= allocatable);
endproperty
a_advert_le_allocatable: assert property (p_advert_le_allocatable);
 
// MANDATORY — the accounting identity itself. Stronger than the bound, and it
// is what catches a reservation that was decremented without being released.
property p_capacity_conserved;
  @(posedge clk) disable iff (!rst_n)
    ((occupancy_q + reserved_q + progress_reserve_q + promised_q + allocatable)
       == cap_active_q);
endproperty
a_capacity_conserved: assert property (p_capacity_conserved);
 
// MANDATORY — occupancy alone never exceeds active capacity. The last line of
// defence, and the one that fires when everything upstream has already failed.
property p_occupancy_bounded;
  @(posedge clk) disable iff (!rst_n)
    (occupancy_q <= cap_active_q);
endproperty
a_occupancy_bounded: assert property (p_occupancy_bounded);
 
// MANDATORY — the progress reserve is never advertised away (Section 45).
property p_progress_reserve_intact;
  @(posedge clk) disable iff (!rst_n)
    (progress_reserve_q >= PROGRESS_MIN) || (fc_state_q != FC_ACTIVE);
endproperty
a_progress_reserve_intact: assert property (p_progress_reserve_intact);

Architecture. A bound, an identity, a floor and a reserve check.

Why the identity is the important one. The bound passes whenever the advertisement is conservative for any reason, including a reason that is itself a bug — a reservation counter that has drifted upward makes every advertisement smaller and every bound property pass, while throughput quietly collapses. The identity fires the moment the five terms stop summing to the capacity, in either direction, which is the only statement that catches both over- and under-advertisement with one property.

Why p_occupancy_bounded is not redundant. It is the property that fires when the far end has already over-sent. It is the receiver's detection of the sender's over-allocation — the last observable before the overflow itself — and it is worth having because it distinguishes "the sender sent too much" from "the advertisement was too large", which the other properties cannot separate.

DV. Drive the receiver to saturation with reservations active; force each term to its extreme; and specifically force a capacity reduction (§36) while occupancy is high, which is the combination that breaks the identity if the quiesce guard is missing.

40. Batching, and Why It Is Not Free

Returning one credit per release is the lowest-latency policy and the highest control-bandwidth one. On a die-to-die link, control bandwidth is a shared, expensive resource — every return competes with real traffic, and the return path may cross a clock boundary, an arbiter, and a serialisation point.

The trade is not symmetric, and that asymmetry is the point of the next three sections. Getting the batching threshold too small costs bandwidth. Getting the flush condition wrong stops the link permanently, with free capacity at the receiver and no correctness failure anywhere in the design.

41. The Pending-Return Accumulator

// ILLUSTRATIVE. Accumulate releases; emit when a flush condition fires; and
// subtract exactly what was emitted, never clear to zero blindly.
logic [CREDIT_W-1:0] pending_return_q;
logic [CREDIT_W-1:0] emit_units;
 
assign emit_units = (pending_return_q > MAX_RETURN_UNITS)
                  ? CREDIT_W'(MAX_RETURN_UNITS)
                  : pending_return_q;
 
always_ff @(posedge clk or negedge rst_n) begin
  if (!rst_n) begin
    pending_return_q <= '0;
  end else if (fc_epoch_advance) begin
    pending_return_q <= '0;                 // Section 31's contract
  end else begin
    unique case ({credit_return_fire, return_emit_fire})
      2'b10  : pending_return_q <= pending_return_q + CREDIT_W'(1);
      2'b01  : pending_return_q <= pending_return_q - emit_units;
      2'b11  : pending_return_q <= pending_return_q - emit_units + CREDIT_W'(1);
      default: pending_return_q <= pending_return_q;
    endcase
  end
end

Architecture. One accumulator, four enumerated arms, and an emit quantity bounded by whatever the control path can carry in one message.

State. Epoch lifetime — cleared by fc_epoch_advance and by nothing else. A reset that clears it outside an epoch advance loses genuine releases; a recovery that fails to clear it reports old-epoch releases into the new epoch (§31).

Cycle behaviour. The 2'b11 arm is the one that matters, and it is the one most often wrong. A release and an emission in the same cycle is normal: the emission takes the value as of this cycle and the new release must survive it. Writing this as two separate if statements loses the release on every such cycle — and those cycles are exactly when the receiver is busy, so the loss rate scales with load and the link drifts short over hours.

Contract. emit_units must be exactly the quantity the emitted message carries. If the message carries fewer than emit_units — because a downstream stage clamps it — the subtraction destroys credits that were never returned, and the link runs permanently short with no assertion anywhere. Tie the subtraction to the accepted emission, not to the requested one.

Failure. §42, which is not about the accumulator at all but about the condition that drains it.

DV. Release and emit in the same cycle repeatedly; emit with pending_return_q above and below MAX_RETURN_UNITS; and check the epoch clear.

42. Wrong Batching — No Partial Flush

This is the chapter's flagship liveness bug. Nothing overflows, nothing corrupts, no counter leaves its range, no assertion in §16, §23, §31 or §39 fires — and the link stops forever with free capacity at both ends.

// WRONG — the ONLY flush condition is the threshold.
assign return_emit_req = (pending_return_q >= CREDIT_W'(BATCH_THRESHOLD));

Worked, with BATCH_THRESHOLD = 8 and a capacity of 16.

The circular wait, stated exactly:

The sender is waiting for credits. The credits are waiting for the threshold. The threshold is waiting for more releases. More releases require more arrivals. More arrivals require credits.

Five properties make this the bug worth building a whole liveness argument for.

Every safety property passes. This is the general lesson 13.3 §19 made at the pipeline level and it is sharper here: safety assertions describe what must not happen, and nothing has happened. The system is in a perfectly legal state, forever.

It requires a specific arrival pattern. The remaining pending count must land strictly below the threshold and no further arrivals must occur. Random traffic almost always supplies another arrival that pushes the count over, so the bug is nearly unreachable in random testing and trivially reachable in production, where a burst followed by a quiet period is the normal shape of real traffic.

The threshold and the depth interact. A threshold at or above the capacity guarantees the deadlock on the first full-drain-minus-one. A threshold well below the capacity makes it rare but not impossible. There is no safe threshold — the fix is not a smaller number, it is an additional condition.

And the diagnostic signature is unmistakable once you know to look: sender credit zero, receiver occupancy well below capacity, pending returns non-zero and unchanging. All three registers stable forever. §63 lists it, and the reason it is worth listing is that it is trivially distinguishable from a genuine full receiver — which is the thing every other zero-credit stall looks like.

43. The Flush Condition

// ILLUSTRATIVE. Three independent reasons to emit. Any one is sufficient, and
// the design needs more than one of them to be live.
logic [TMR_W-1:0] idle_timer_q;
 
always_ff @(posedge clk or negedge rst_n)
  if (!rst_n)                            idle_timer_q <= '0;
  else if (return_emit_fire
           || (pending_return_q == '0))  idle_timer_q <= '0;
  else                                   idle_timer_q <= idle_timer_q + TMR_W'(1);
 
assign return_emit_req =
      (pending_return_q >= CREDIT_W'(BATCH_THRESHOLD))   // bandwidth-efficient
   || ((pending_return_q != '0)
        && (idle_timer_q >= TMR_W'(FLUSH_TIMEOUT)))      // the liveness guarantee
   || ((pending_return_q != '0) && peer_starved);        // the direct signal

Architecture. Three conditions, and the timer is the one that makes the machine live. The threshold is a bandwidth optimisation; the timer is a correctness requirement.

State. A timer, reset on emission and on reaching an empty accumulator.

Cycle behaviour. The timer runs only while returns are pending, so a genuinely idle link does not emit anything and costs nothing.

Contract. FLUSH_TIMEOUT must be shorter than any timeout the peer applies to a stalled transmission, or the peer declares a fault before the flush arrives and the deadlock becomes a recovery loop instead. That is a cross-block parameter relationship, and — following 19.4 §29's treatment of headroom — it belongs in an elaboration check, not in a comment.

On peer_starved. Where the architecture gives the receiver any indication that the peer has exhausted its credits, that signal is the ideal flush trigger: it is immediate and it fires exactly when the flush is needed. Whether such an indication exists is architecture-dependent and is not claimed for UCIe here (§3), which is why the timer must be present regardless. A design that relies on the starvation signal alone has made its liveness dependent on a feature that may not exist.

Failure. A timeout longer than the peer's patience converts a deadlock into a livelock of recoveries — arguably worse, because the link now looks unreliable rather than stuck, and the investigation goes to the PHY.

DV. §44, plus a directed test that produces exactly §42's step 4 and confirms the emission happens on the timer.

44. Liveness SVA — Pending Returns Are Eventually Emitted

// MANDATORY, and the assumptions are the point. Without them this fails on the
// environment rather than on the DUT (Chapter 20.1 Section 28 makes the
// general argument).
//
// ASSUMPTIONS, stated explicitly:
//   A1  the clock continues and reset is not re-asserted
//   A2  the control path eventually accepts an emission
//   A3  the flow-control state is not held in FC_FAULT
assume property (@(posedge clk) s_eventually return_emit_ready);
assume property (@(posedge clk) s_eventually (fc_state_q != FC_FAULT));
 
property p_pending_eventually_emitted;
  @(posedge clk) disable iff (!rst_n)
    (pending_return_q != '0) |-> s_eventually return_emit_fire;
endproperty
a_pending_eventually_emitted: assert property (p_pending_eventually_emitted);
 
// MANDATORY — the bounded form, which is what a simulation can actually check.
// A bound is stronger than eventuality and it names the number that must hold.
property p_pending_emitted_within_bound;
  @(posedge clk) disable iff (!rst_n)
    (pending_return_q != '0)
      |-> ##[1:FLUSH_TIMEOUT+RETURN_PATH_MAX] return_emit_fire;
endproperty
a_pending_emitted_within_bound: assert property (p_pending_emitted_within_bound);
 
// MANDATORY — the deadlock signature itself, as a directly checkable property.
// Free capacity plus zero peer credit plus pending returns is never stable.
property p_no_stranded_capacity;
  @(posedge clk) disable iff (!rst_n)
    ((allocatable != '0) && peer_credit_zero && (pending_return_q != '0))
      |-> ##[1:STRANDED_MAX] return_emit_fire;
endproperty
a_no_stranded_capacity: assert property (p_no_stranded_capacity);

Architecture. An unbounded eventuality for formal, a bounded version for simulation, and a direct statement of §42's signature.

Why the bounded form is the one that finds bugs. s_eventually in simulation only fails at the end of the run, and only if the tool is configured to report unfinished properties. A bounded property fails at a specific cycle with a specific number in the message, and the number tells the engineer whether the timeout parameter or the return path is at fault.

Why the third property exists at all, given the first two. It is written in terms of observable system state rather than internal accumulator state — free capacity, zero peer credit, pending returns — so it holds even if the accumulator is implemented completely differently, and it survives a redesign of the batching logic. It is the property that would have caught §42 in a design where the batching lived somewhere the verification engineer never looked.

On assumption discipline. A2 is an assumption about the environment, not a property of the design, and asserting it as a DUT property would be a category error — Chapter 20.1 §29 develops exactly this boundary. Every liveness claim in this chapter is conditional on A1–A3, and a design review should ask what makes each assumption true in the real system.

DV. Drive §42's exact scenario. Then drive it with the timer disabled and confirm the property fails — a liveness property that has never been observed to fail is a liveness property nobody has tested.

45. The Progress Reserve

Chapter 19.4 §45 introduced reserved entries; this section turns the reserve into a credit rule, which is where it becomes load-bearing.

Some traffic exists to release resources. If that traffic cannot get through because the resources are exhausted, nothing will ever be released.

The canonical shape: completions, responses, acknowledgements and credit returns all free something when they arrive. If bulk requests are allowed to consume every remote entry, the completions that would retire those requests cannot land, the requests stay outstanding, their resources stay held, and the system is deadlocked with every counter in range.

// ILLUSTRATIVE. Per-class credit with a per-class floor. The floor is not a
// separate pool — it is a lower bound on what remains for the classes that
// release resources.
logic [CREDIT_W-1:0] credit_q  [NUM_CLASSES];
logic [CREDIT_W-1:0] reserve_q [NUM_CLASSES];   // floor for this class
 
// A class may consume only down to the reserve of the OTHER classes it can
// starve. For a two-class split this is the readable form:
assign may_consume[CLS_BULK] =
      (credit_q[CLS_BULK] >= consume_units)
   && ((credit_q[CLS_BULK] - consume_units) >= reserve_q[CLS_BULK]);
 
assign may_consume[CLS_CTRL] =
      (credit_q[CLS_CTRL] >= consume_units);     // control is what the reserve protects

Architecture. A floor per class rather than a partition, so the reserve does not permanently strand capacity when the protected class is idle.

State. reserve_q has configuration lifetime and is part of §36's atomic commit — changing a reserve live, while traffic is running, can put credit_q below its own floor, and every subsequent subtraction sees a negative headroom.

Cycle behaviour. Evaluated per admission.

Contract. The reserve must be at least as large as the number of resource-releasing objects that can be simultaneously required. That is a system-level number derived from the maximum outstanding count, not a constant chosen for comfort — 13.3 §17's wait-for graph is how it is derived.

Failure. §46.

DV. Saturate with bulk traffic and confirm that a control object can still be admitted at every point; then set the reserve to zero and confirm the deadlock reproduces, because a reserve that has never been shown to be necessary may be the wrong size.

46. Wrong Sharing — Bulk Consumes Every Entry

// WRONG — one shared pool, no floor. Any class may take the last entry.
assign may_consume[c] = (credit_q_shared >= consume_units);

Worked. 16 remote entries, shared. Bulk requests consume all 16. Each of those requests will be retired by a completion travelling in the opposite direction — but the reverse direction's entries are also exhausted, because completions in that direction are queued behind the same shared pool at the peer.

The wait-for cycle:

Bulk requests hold all 16 entries. They are released when their completions arrive. Completions cannot be admitted because no entries are free. No entries become free until completions arrive.

Four properties.

It is a deadlock, not a stall. No timeout inside the credit machine resolves it; only an external recovery does, and the recovery discards the outstanding work.

It is the same shape as §42 and different in cause. §42 stalls because a message is withheld; this stalls because capacity is withheld. Both present as zero credit with free-looking resources, and the diagnostic that separates them is whether pending returns are non-zero (§63).

It composes with the class-collapse bug of §9. A design with per-class counters but no reserve is exposed to this; a design with a shared counter is exposed to both simultaneously, and the second bug masks the first during debug.

And the direction of the traffic is what makes it invisible in review. The requests and the completions are on opposite paths, often owned by different engineers, and the dependency between them is not visible in either path's RTL. It is visible only in the wait-for graph, which is why 13.3 §16 insists on drawing one.

47. Per-Class Pools, and What Indexes Them

// ILLUSTRATIVE. Per-class state, and the index comes from the EVENT, never
// from a shared "current class" register (13.1 Section 9's failure).
logic [CREDIT_W-1:0] credit_q  [NUM_CLASSES];
logic [CREDIT_W-1:0] pending_q [NUM_CLASSES];
logic [CAP_W-1:0]    cap_q     [NUM_CLASSES];
 
always_ff @(posedge clk or negedge rst_n) begin
  if (!rst_n) begin
    for (int c = 0; c < NUM_CLASSES; c++) credit_q[c] <= '0;
  end else begin
    for (int c = 0; c < NUM_CLASSES; c++) begin
      if (advert_apply && (advert_class == CLS_W'(c))) begin
        credit_q[c] <= CREDIT_W'(advert_value);
      end else begin
        automatic logic signed [CREDIT_W:0] d;
        d = $signed({1'b0, (return_accept && (return_class == CLS_W'(c)))
                            ? return_units : CREDIT_W'(0)})
          - $signed({1'b0, (consume_fire  && (consume_class == CLS_W'(c)))
                            ? consume_units : CREDIT_W'(0)});
        if (d != '0) credit_q[c] <= CREDIT_W'($signed({1'b0, credit_q[c]}) + d);
      end
    end
  end
end

Architecture. The loop makes independence structural — there is no expression in which class c's update can read class e's event. That is not a stylistic preference: a shared "current class" register produces a decrement charged to the wrong class, which keeps the total correct and both individual counts wrong, so a total-based assertion passes while one class is over-committed and another is under-used.

State. NUM_CLASSES counters, accumulators and capacities. NUM_CLASSES is a parameter, not a UCIe-defined count (§3).

Cycle behaviour. Every class can have activity in the same cycle, in any combination of consume and return. With three classes that is 4³ = 64 combinations of the arms, and the interesting ones are where two classes do opposite things simultaneously.

Contract. Each class's counter is a replica of a separate physical structure at the peer (§8). If two classes actually share storage at the receiver, per-class counters over-advertise their sum, which is §9's overflow with more steps.

Failure. Mis-indexing, which §16's per-class bound catches only when it pushes one class out of range — so the conservation property of §53 must also be per class, not aggregate.

DV. Drive all classes simultaneously in every arm combination; then deliberately mis-index one event and confirm the per-class conservation property fires while the aggregate one does not.

48. Credit-Return Arbitration

When the control path carries one credit update per cycle and several domains have pending returns, something must choose. That choice is a liveness mechanism, not a performance tweak.

// ILLUSTRATIVE. Round-robin over domains with pending returns, with the
// rotation advancing on an ACTUAL emission (not on a grant — Section 19).
logic [CLS_W-1:0] rr_ptr_q;
logic [NUM_CLASSES-1:0] ret_req;
 
always_comb
  for (int c = 0; c < NUM_CLASSES; c++)
    ret_req[c] = (pending_q[c] != '0) && flush_cond[c];
 
// Rotate-select: the first requester at or after rr_ptr_q.
always_comb begin
  ret_grant = '0;
  for (int i = 0; i < NUM_CLASSES; i++) begin
    automatic int c = (int'(rr_ptr_q) + i) % NUM_CLASSES;
    if (ret_req[c] && (ret_grant == '0)) ret_grant[c] = 1'b1;
  end
end
 
always_ff @(posedge clk or negedge rst_n)
  if (!rst_n)                  rr_ptr_q <= '0;
  else if (return_emit_fire)   rr_ptr_q <= CLS_W'((int'(emit_class) + 1) % NUM_CLASSES);

Architecture. Rotate-select with the pointer advancing past the class that actually emitted.

State. One pointer, and its update is qualified on return_emit_fire, not on ret_grant. This is §19's rule applied to the arbiter itself: a grant that does not result in an emission must not advance the rotation, or the granted class loses its turn without being served and the "fairness" is fictional.

Cycle behaviour. One emission per cycle; all classes may request every cycle.

Contract. Fairness here is bounded-wait, not equal-share. The guarantee needed is that a class with a pending return waits at most NUM_CLASSES − 1 emissions, which is what §50's property states.

Failure. §49.

DV. All classes requesting continuously; measure the maximum wait per class and compare against the bound.

49. Wrong Arbitration — Strict Priority

// WRONG — a fixed priority encoder over domains.
always_comb begin
  ret_grant = '0;
  for (int c = 0; c < NUM_CLASSES; c++)
    if (ret_req[c] && (ret_grant == '0)) ret_grant[c] = 1'b1;   // class 0 always wins
end

Worked. Class 0 has continuous traffic, so it has continuous pending returns. Class 1's returns are never emitted.

The far end's class-1 credit falls to zero and stays there. Class 1 stalls permanently.

Four properties.

The receiver has free class-1 capacity the whole time. The entries were released; the message saying so was never sent. This is §42's failure with an arbiter in place of a threshold, and it produces the identical diagnostic signature — which is why §63 lists arbitration as one of the causes behind that signature rather than a separate one.

No safety property fires. Class 1's counter sits at zero, a perfectly legal value, forever.

It is invisible under single-class load. Any test that exercises one class at a time passes, and any test with light load on class 0 passes because class 0's requests are intermittent and class 1 gets the gaps. The bug needs sustained class-0 load, which is the production condition and rarely the test condition.

And the same defect appears one level up. 19.2 §15 and 19.3 §41 both address strict priority in the traffic scheduler. Fixing it there and leaving it in the credit-return path recreates the starvation on the control path — where it is much harder to see, because nobody is watching the return arbiter's fairness.

50. SVA — Every Domain's Returns Get Service

// MANDATORY. Bounded wait, per class, under an explicit assumption.
//   ASSUMPTION: the control path eventually accepts an emission.
property p_return_bounded_wait(int c);
  @(posedge clk) disable iff (!rst_n)
    (ret_req[c] && !ret_grant[c])
      |-> ##[1:(NUM_CLASSES-1)*MAX_EMIT_GAP] ret_grant[c];
endproperty
 
// MANDATORY — the rotation advances only on an actual emission.
property p_rr_advances_on_emit_only;
  @(posedge clk) disable iff (!rst_n)
    (rr_ptr_q != $past(rr_ptr_q)) |-> $past(return_emit_fire);
endproperty
a_rr_advances_on_emit_only: assert property (p_rr_advances_on_emit_only);
 
// MANDATORY — no class sits at zero credit while its own returns are pending.
// The system-level statement, independent of how arbitration is implemented.
property p_no_class_starved(int c);
  @(posedge clk) disable iff (!rst_n)
    ((credit_q[c] == '0) && (pending_q[c] != '0))
      |-> ##[1:STARVE_MAX] (credit_q[c] != '0);
endproperty

Architecture. A bounded-wait property, an implementation-discipline property, and a system-level property that does not depend on the arbiter's structure.

Why the third is the durable one. The first two describe this arbiter; the third describes the outcome the arbiter exists to produce. If the arbiter is replaced by a different scheme, the first two must be rewritten and the third does not change — and it is the third that would have caught §49 in a design where the priority encoder was buried in a shared control-path multiplexer that nobody thought of as an arbiter.

DV. Sustained load on the highest-priority class with a starved low-priority class — the exact configuration §49 needs — and confirm the third property fires when the round-robin is replaced by fixed priority.

51. Replay and Credit — the Question This Chapter Does Not Answer

Why this cannot be finessed. Chapter 13.1 §12 established that credits and replay slots are different reservations — a replay entry is local storage retained for retransmission, a credit is a claim on remote storage — and that distinction is solid. What it does not settle is whether the remote claim survives the first attempt. Those are independent facts, and knowing the first does not give you the second.

The observable that decides it, if you have access to a peer. Instrument the receiver: count distinct entry allocations against distinct transport attempts under injected retransmission. If a retried object allocates once, the allocation is retained; if it allocates twice, it is not. That is an empirical answer for one implementation pair, which is useful for bring-up and is not a substitute for reading the specification.

52. Wrong Implementation — Both Directions

// WRONG IF the allocation is retained — a retransmission consumes a new credit.
assign credit_consume_fire = tx_commit_fire;               // no attempt qualification

Worked. One semantic object is retransmitted 5 times before it is acknowledged. Five credits are consumed for one remote entry.

Four credits are destroyed permanently. The link degrades every time reliability is exercised, which is to say every time the link is marginal — so the throughput collapse is correlated with exactly the conditions under which throughput matters most. And the correlation makes it look like a PHY problem, because the retries and the slowdown appear together.

// WRONG IF the allocation is NOT retained — a retransmission consumes nothing.
assign credit_consume_fire = tx_commit_fire && is_first_attempt;

Worked. The same object is retransmitted 5 times and the far end allocates a fresh entry each time. Four entries are consumed with no credit charged. The receiver overflows after enough retransmissions accumulate — the catastrophic direction, and it appears only under error injection or a genuinely marginal link.

Three properties of this pair.

They are not symmetric in severity. The first loses throughput; the second loses data. A design that must guess should guess conservatively — charge the credit — and document the guess loudly, because the conservative choice is recoverable by a specification reading and the aggressive one is recoverable only by silicon.

Neither is detectable by any property in this chapter. Both maintain a self-consistent counter. Only a conservation check against the receiver's actual allocation count (§53's cross-check) distinguishes them — which requires observing the far end, which is why this is a verification-environment problem rather than an assertion problem.

And a mode change can flip the answer. If the link supports both a raw mode with protocol-layer reliability and an Adapter-managed mode, the retained-allocation question may have different answers in the two modes — so requires_new_remote_allocation may need to be a function of the active mode rather than a constant. A design that hardcodes it has hardcoded one mode's answer into both.

53. The Conservation Model

Bounds are not enough, and this is the section that says why. Every silent bug in this chapter — the leak of §18, the duplicate of §24, the straggler of §29, the replay miscount of §52 — produces a counter that stays inside its legal range. What each of them breaks is a relationship, and a relationship must be stated to be checked.

Three equations, at three scopes.

At the sender, per class — the replica identity:

initial_advertised[c]
  +  returns_accepted[c]
  -  new_allocations_consumed[c]
  -  explicit_withdrawals[c]
  ==  credit_q[c]

Every term is counted at an observed event, and credit_q[c] is read from the design. A mismatch means the design applied an update the model did not see, or missed one the model did — and the sign says which.

At the receiver, per class — the capacity identity (§39's p_capacity_conserved):

occupied[c] + reserved[c] + progress_reserve[c] + promised[c] + allocatable[c]
  ==  active_capacity[c]

Across the link — the safety statement, and the only one that catches an over-advertisement:

credit_q[c]                      // what the sender believes it may still use
  +  in_flight[c]                // consumed, not yet arrived
  +  occupied[c]                 // arrived, not yet released
  +  returns_in_flight[c]        // released, return not yet applied
  <=  active_capacity[c]

Read the third one carefully, because its shape is the lesson. It is an inequality, not an equality — and it must be, because the four terms are sampled at different points in a loop with propagation delay. A transient in which the sum is below capacity is normal: it is credit the receiver has released and not yet advertised. A sum above capacity is never legal, and it is exactly the over-allocation this entire chapter exists to prevent.

The four terms live in four places, which is why this cannot be an RTL assertion:

This is a verification-environment property, not a design property. No block can evaluate it, and that is not a limitation to work around — it is the honest statement that flow control is a distributed invariant and can only be checked by something that observes both ends.

54. The Formal Invariant

For formal proof, the conservation equations of §53 are too heavy — they involve monitors and unbounded counts. The formal-friendly restatement replaces counting with a set.

// VERIFICATION ONLY. Not synthesisable, not part of the design.
// One bit per remote entry: has the sender consumed capacity that this entry
// represents and not yet had it returned?
logic [DEPTH-1:0] live_claim;
 
always_ff @(posedge clk or negedge rst_n) begin
  if (!rst_n) begin
    live_claim <= '0;
  end else begin
    if (fc_epoch_advance) live_claim <= '0;                  // agreement voided
    else begin
      if (credit_consume_fire) live_claim[claim_id_alloc] <= 1'b1;
      if (return_accept)       live_claim[claim_id_free]  <= 1'b0;
    end
  end
end
 
// THE INVARIANT. The number of live claims never exceeds the storage that
// backs them. This is the property the whole chapter is trying to preserve.
property p_claims_within_capacity;
  @(posedge clk) disable iff (!rst_n)
    ($countones(live_claim) <= active_capacity);
endproperty
a_claims_within_capacity: assert property (p_claims_within_capacity);
 
// A claim is never set twice without an intervening clear — the duplicate
// consume of Section 20, restated as a set property.
property p_claim_not_double_set(int i);
  @(posedge clk) disable iff (!rst_n)
    (credit_consume_fire && (claim_id_alloc == i)) |-> !live_claim[i];
endproperty
 
// A claim is never cleared twice — the duplicate return of Section 24.
property p_claim_not_double_clear(int i);
  @(posedge clk) disable iff (!rst_n)
    (return_accept && (claim_id_free == i)) |-> live_claim[i];
endproperty

Architecture. A bitmap of live claims, maintained by the verification environment from observed events.

Why a set rather than a counter. A counter can be wrong by a duplicate and stay legal; a bitmap makes a duplicate a set-a-set-bit or clear-a-clear-bit event, which is directly checkable. This is the same argument §26 made about the design's release accounting, applied to verification — and it is the eighth appearance of bitmap, not counter in this curriculum.

The identity assignment. claim_id_alloc and claim_id_free come from the verification environment's own tagging, not from a design signal. Where the return path carries no identity — which is the common case (§27) — the model must assign the freed claim by policy, and the honest policy is oldest-first with an accompanying note that the identity of the freed claim is a model assumption while the count is not. The count is what the invariant checks, so the policy does not weaken it.

What formal proves here that simulation cannot. With a bounded DEPTH and the environment assumptions of §44 written as assume property, p_claims_within_capacity is provable rather than merely untested — which matters because the property's counterexamples are exactly the rare event orderings simulation is worst at reaching.

55. The Credit Scoreboard

PER CLASS c, PER DIRECTION:
 
  physical_capacity[c]      elaboration constant, from the configuration model
  active_capacity[c]        tracked through Section 36's commit events
  epoch[c]                  advanced on OBSERVED resynchronisation completion
 
  advertised[c]             from the observed advertisement, tagged with epoch
  sender_credit[c]          = advertised - consumed + returns_applied
                              -- DERIVED, never read from credit_q
 
  consumed_claims[c]        set of monitor tags whose credit was consumed
  returned_claims[c]        set of tags whose capacity has been returned
  live_claims[c]            = consumed_claims - returned_claims
 
  occupied[c]               from the receive-side monitor, independently
  promised[c]               = live_claims not yet observed arriving
  pending_returns[c]        releases observed, returns not yet observed emitted
 
  stale_returns[c]          returns observed with a non-current epoch
  duplicate_returns[c]      returns for a tag already in returned_claims
 
CHECKS, each naming a distinct failure:
  1  sender_credit[c] == credit_q[c]           -- the replica is right
  2  |live_claims[c]| <= active_capacity[c]    -- Section 54's invariant
  3  advertised[c] <= allocatable[c]           -- Section 39, independently
  4  duplicate_returns[c] == 0                 -- Section 24
  5  stale_returns[c] applied == 0             -- Section 29
  6  every consumed tag eventually returned    -- liveness, under assumptions
  7  pending_returns[c] emitted within bound   -- Section 44
  8  min(sender_credit[c]) over the run        -- a sizing report, not an error

Architecture. One model per class per direction, built entirely from boundary observations — advertisements, transfers, arrivals, releases and return messages — and never from an internal design register except in check 1, where the design's register is the subject of the comparison rather than an input to the model.

Why check 1 and check 2 are both needed. Check 1 catches a design that updates its counter wrongly. Check 2 catches a design whose counter is perfectly consistent with a wrong set of events — §52's replay miscount is exactly that: the counter agrees with the consume events, and the consume events are wrong. Check 1 passes; check 2 fails.

Why check 8 is not an error. A minimum credit that never approached zero means the advertised capacity is larger than the traffic needs, which is not a bug and is evidence for the next sizing review. Printing it is how the depth-versus-throughput argument reaches whoever chose the parameter — the same discipline 19.4 §54 applied to buffer high-water marks.

56. Why a Mirrored Scoreboard Proves Nothing

The single most common way to build a credit scoreboard that catches no credit bugs:

WRONG:
  on credit_consume_fire  ->  model_credit--
  on credit_return_fire   ->  model_credit++
  check: model_credit == credit_q

This checks that the design's counter is consistent with the design's own event signals. It is a check on the adder.

Every bug in this chapter survives it.

The rule that fixes it, and it is one sentence:

The reference model must derive its consume and return events from the contract, not from the design's signals. A consume happens when the environment observes an object crossing the transmit boundary that requires a new remote allocation. A return happens when the environment observes an entry at the receiver becoming reusable. Neither definition mentions a signal inside the design.

Three practical consequences.

The monitors must be at the boundaries, not at the block. A monitor tapping the credit block's own inputs has already inherited the design's interpretation of those events.

The model needs its own identity. The monitor tag of §20 and §54 exists because the model must be able to say "this is the same object" without asking the design.

And where the boundary genuinely cannot be observed — where the far end is a black box — the model degrades to a bound rather than an equality, and that must be stated explicitly rather than papered over by tapping an internal signal. A weaker check that is honest beats a stronger check that is circular. Chapter 20.1 makes this the foundation of the whole verification module.

57. Flagship Trace 1 — Steady State With a Simultaneous Update

Illustrative. Capacity 8, single class, batch threshold 3, flush timeout not reached.

Four things to read.

Cycle 8 is the ordinary simultaneous case — a consume and a release in the same cycle. The credit stays at 4 because the consume takes one and the release does not return one yet; it goes into the accumulator. The counter did not move, and two different things happened. A design with two always_ff blocks would have got this cycle wrong.

Cycle 9 is the batched return — three units at once, so §14's multi-unit arithmetic is exercised. credit_q goes 4 → 7 in one update.

Cycle 12 is the arithmetic that catches designs out: a consume of 1, an arrival, and a release, all in one cycle. Credit 6 → 6 because the consume decrements and nothing returns; occupancy 2 → 3 because one arrived and one released, net +1 with the arrival landing first.

And the sum is conserved throughout. At cycle 12: credit 6 + occupied 3 + pending 1 = 10 against a capacity of 8 — which looks wrong until you subtract the two in-flight objects that have been consumed and not arrived. Conservation closes only when §5's fourth number is included, which is the whole reason it is a number.

58. Flagship Trace 2 — Held valid and the Leak

Illustrative. §18's bug, then the corrected form, on identical stimulus.

One object was transferred. The wrong design charged six credits for it.

Three readings.

The divergence begins at cycle 1 and is never repaired. There is no later event that returns the five lost credits — they describe entries at the far end that are free and will never be used.

The leak rate is the stall length. A 5-cycle stall costs 5 credits; a 50-cycle stall costs 50. On a congested link the counter reaches zero within a few dozen objects, at which point the link stalls completely and looks like a far-end problem.

And the corrected column shows nothing interesting, which is the point. The correct design's counter is flat during the stall because nothing happened — no capacity was committed, so no accounting changed.

59. Flagship Trace 3 — The Straggler After Recovery

Illustrative. §29, with the guard absent and then present. Capacity 16.

Four readings.

Cycle 131 is the entire bug. One cycle, one addition, and the replica is permanently 3 too large.

Cycle 148 is where the two designs visibly diverge in behaviour, 17 cycles after they diverged in state. The correct design stalls; the wrong one keeps going.

Cycle 151 is where the failure is observed — 20 cycles after the cause, and in a completely different block. The receive buffer's overflow assertion fires, the investigation starts at the receive buffer, and the cause is in the sender's credit adder.

And §12's exact-equality property fires at cycle 131, naming the cause at the cycle it happened. That property costs one line and moves the debug from the receive buffer to the credit block, twenty cycles earlier. It is the highest-value single assertion in this chapter.

60. Flagship Trace 4 — The Batching Deadlock

Illustrative. §42, threshold 8, capacity 16, no flush timer.

And with the flush timer of §43, FLUSH_TIMEOUT = 64:

Four readings.

Every register in the deadlocked table is stable and legal. Credit 0 is legal. Occupancy 11 is legal. Pending 5 is legal. The system is in a state no safety property can object to, and it will remain there until something external intervenes.

The receiver has 5 free entries throughout. This is not congestion; it is stranded capacity. The distinction is the whole of §63's diagnostic argument.

The timer's cost is one emission per 64 idle cycles, which is negligible — and it is the entire difference between a link that works and a link that stops.

And the deadlock needs a quiet period to be reachable. Cycle 36 onwards has no new arrivals; any arrival would eventually produce a release and push the count to 8. Random stimulus supplies those arrivals constantly, which is why this bug survives random regression and appears in the field. A directed test that stops the stimulus is the only thing that finds it.

61. Flagship Trace 5 — A Multi-Unit Simultaneous Update

Illustrative. §14's arithmetic, with CREDIT_W = 5 and a capacity of 16.

And the same stimulus through §15's unsigned expression:

Three readings.

Cycle 5 is the divergence, and it is the only one. The unsigned expression is correct on five of six cycles. A test that does not drive a consume larger than the current credit never sees the bug — and a well-behaved design should never issue such a consume, which is precisely why the guard is missing: it protects against a condition the design believes cannot occur.

Cycle 5 in the correct column is a detected fault, not a wrong number. The signed intermediate is −2, the range check fires, the counter holds at 0, and credit_fault is raised. The design stops rather than continuing on a lie.

And cycle 3 shows why the 2'b11 arm of §13 generalises correctly. Consume 2, return 2, delta 0 — no register write at all. The multi-unit form handles the simultaneous case as ordinary arithmetic, with no special arm required, which is one reason to prefer it once either count can exceed one.

62. Instrumentation

// ILLUSTRATIVE. Per credit domain. Free-running counters, read and cleared by
// software; the CLEAR must not touch epoch or credit state (19.6 Section 27).
logic [63:0] zero_credit_cycles_q;    // how long this class had no permission
logic [63:0] return_pending_cycles_q; // how long returns sat unemitted
logic [63:0] consume_count_q;         // total units consumed
logic [63:0] return_count_q;          // total units returned
logic [63:0] stale_return_q;          // rejected by the epoch guard (Section 30)
logic [63:0] duplicate_return_q;      // rejected by the per-entry bit (Section 25)
logic [63:0] credit_fault_q;          // range violations detected (Section 14)
logic [CREDIT_W-1:0] min_credit_q;    // low-water mark, for sizing

Eight counters, and each one answers a question no other counter answers.

zero_credit_cycles_q versus return_pending_cycles_q is the pair that matters most. The first says "we could not send"; the second says "we were holding capacity we had not released". Both non-zero and rising together is §42 or §49; the first alone is a genuinely full receiver. One comparison separates a deadlock from congestion, which is the single most valuable thing this instrumentation does.

stale_return_q and duplicate_return_q count events that are correctly rejected. They are not errors — the guards did their job. But their rate is diagnostic: stale returns during a recovery are expected, and stale returns during steady state mean the epoch is being advanced by something that should not be advancing it (§31's monotonicity property, in counter form). Silently dropping a rejected event throws away the only evidence that the guard is being exercised.

min_credit_q is a sizing report, not an error. A minimum that never fell below half the capacity says the advertisement is larger than the traffic needs.

And the deliberate omission. There is no counter per FSM transition, no counter per advertisement value, no histogram of delta magnitudes. The instrumentation exists to answer the questions in §63 and §66, and a register that answers no question on those lists is area and verification surface with no debug value — 19.6 §42 makes this a rule for reusable IP.

63. Diagnostic Signatures

The four states a struggling credit domain can be in, and the registers that separate them. This table is the fastest path from a symptom to a cause in this chapter.

Read the second column against the third. Occupancy at capacity means the receiver is the bottleneck. Occupancy below capacity with zero credit at the sender means capacity is stranded, and the only question left is whether the return message was never generated (§42) or never scheduled (§49) — which return_pending_cycles_q per class answers immediately, because starvation shows on one class and batching shows on all of them.

The credit-leak signature has a second confirmation worth knowing. Compare consume_count_q against the number of objects the receive-side monitor observed. A ratio above 1.0 is the leak, and the ratio is the average stall length — which points directly at where the qualification is missing.

And the inflation signature is the only one where the sender's own register is out of range. If credit_q exceeds active_capacity at any point, §16 has already fired and the question is only which of §24 or §29 caused it: duplicate_return_q and stale_return_q distinguish them, and if both are zero the guards are missing entirely rather than being exercised.

64. Coverage

// ILLUSTRATIVE. Cover the ARITHMETIC, the EVENTS and the SEQUENCING separately
// — a bin that is never hit is a case that was never designed.
covergroup cg_credit @(posedge clk);
 
  // --- The counter's extremes, which is where the width bugs live ---
  cp_credit_value: coverpoint credit_q {
    bins zero        = {0};
    bins one         = {1};
    bins mid[4]      = {[2:CAP_NOMINAL-1]};
    bins at_capacity = {CAP_NOMINAL};              // Section 11 fails HERE
  }
 
  // --- Simultaneity: the common case at load, and the one designs get wrong ---
  cp_simul: coverpoint {(consume_count != 0), (return_count != 0)} {
    bins idle          = {2'b00};
    bins return_only   = {2'b01};
    bins consume_only  = {2'b10};
    bins both          = {2'b11};                  // Sections 13, 14, 57
  }
 
  // --- Multi-unit magnitudes and the SIGN of the net change ---
  cp_consume_units: coverpoint consume_count { bins n[] = {[0:MAX_UNITS]}; }
  cp_return_units:  coverpoint return_count  { bins n[] = {[0:MAX_UNITS]}; }
  cp_delta_sign: coverpoint delta {
    bins negative = {[-MAX_UNITS:-1]};
    bins zero     = {0};
    bins positive = {[1:MAX_UNITS]};
  }
 
  // --- The state machine and the epoch ---
  cp_fc_state: coverpoint fc_state_q {
    bins reset = {FC_RESET}; bins sync = {FC_SYNC}; bins active = {FC_ACTIVE};
    bins resync = {FC_RESYNC}; bins fault = {FC_FAULT};
  }
  cp_fc_arc: coverpoint fc_state_q {
    bins sync_to_active   = (FC_SYNC   => FC_ACTIVE);
    bins active_to_resync = (FC_ACTIVE => FC_RESYNC);
    bins resync_to_active = (FC_RESYNC => FC_ACTIVE);
    bins active_to_fault  = (FC_ACTIVE => FC_FAULT);
    bins fault_to_resync  = (FC_FAULT  => FC_RESYNC);
  }
  cp_return_epoch: coverpoint return_epoch_matches {
    bins fresh = {1'b1};
    bins stale = {1'b0};                           // Sections 29, 30, 59
  }
 
  // --- Batching, including the case that deadlocks ---
  cp_flush_reason: coverpoint flush_reason {
    bins threshold = {FLUSH_THRESHOLD};
    bins timer     = {FLUSH_TIMER};                // Sections 42, 43, 60
    bins starved   = {FLUSH_STARVED};
  }
  cp_partial_batch: coverpoint pending_return_q iff (return_emit_fire) {
    bins partial = {[1:BATCH_THRESHOLD-1]};        // the flush that prevents Section 42
    bins full    = {[BATCH_THRESHOLD:$]};
  }
 
  // --- Reserves, classes and replay ---
  cp_progress_reserve: coverpoint progress_reserve_engaged { bins yes = {1'b1}; }
  cp_class: coverpoint consume_class { bins c[] = {[0:NUM_CLASSES-1]}; }
  cp_replay_mode: coverpoint requires_new_remote_allocation {
    bins new_alloc  = {1'b1};
    bins retained   = {1'b0};                      // Sections 51, 52
  }
 
  // --- The crosses that matter ---
  x_simul_at_extremes:  cross cp_simul, cp_credit_value;
  x_class_simul:        cross cp_class, cp_simul;
  x_epoch_in_state:     cross cp_return_epoch, cp_fc_state;
  x_replay_and_consume: cross cp_replay_mode, cp_simul;
 
endgroup