Credit Issues

Chapter 21.3 found the system signature: a leak, an inflation, a stranding, or a downstream blockage. This chapter answers the next question — which layer boundary did the ownership actually get lost at?

1. The One-Sentence Model

Credit bugs are boundary-accounting bugs. At every layer boundary one side says "I transferred ownership" and the next must say "I accepted ownership." When both sides' local counters are internally consistent and the two layers disagree, the bug lives at that boundary — and no amount of inspecting either layer's internals will find it.

That framing is the whole chapter. 21.3 established that a conservation equation broke; this chapter establishes where, and the answer is always an arrow between two layers rather than a block.

2. What This Chapter Owns

21.3 built a nine-counter chain and five differences. This chapter is what that chain becomes when the counters live in different layers — and four things change:

In-flight terms stop being optional (§10–§11). Within one layer a difference of five is five lost credits; across a boundary with twenty cycles of transport latency it is five messages in flight, and a debugger who does not model the delay reports a leak that does not exist.

Layer-local correctness becomes possible alongside system failure (§17). Both sides' internal equations close; the two layers disagree with each other, and neither team's investigation finds anything.

Event counts and capacity amounts diverge (§31–§34). One event may carry several units. A chain that counts events cannot detect a capacity drift, and one that sums amounts cannot detect a duplicate — both are needed.

And the debug system itself becomes a suspect (§41–§43). A software read of eight live counters is not atomic; the skew manufactures a leak, and §51 is that trace.

3. Sourcing

4. Boundary Accounting

A credit's life is a chain of ownership transfers, and every transfer has two halves.

Four failure modes follow directly, and they are the only four:

Three properties of this table.

The fourth row is the one that defeats a total. It is the only failure where the sum is correct and both domains are wrong — and §15 is the flagship trace.

Rows 1 and 2 are distinguished only by which side leads, which is why the chain must be read in order (§18) rather than as a set of independent comparisons.

And every row is an observation about two counters. A single counter, however carefully instrumented, cannot express any of them — which is why this chapter's instrumentation is nine counters rather than one.

5. The Ledger Chain

The chapter's first centerpiece. Nine arrows, each with a producer event, a consumer event, and a reason the two can legitimately differ at any instant.

Four readings, and the fourth is the diagnostic strategy.

Three arrows have no legitimate transient difference — 2, 5 and 9 — so a nonzero difference there is a bug immediately, with no quiescence requirement and no latency model. 21.3 §12's exact identities, now attributed to specific boundaries.

Arrow 4's difference is the occupancy, which is not a bug at all — it is the buffer doing its job. A reconciliation model that treats it as a mismatch reports a leak equal to the receiver's fill level.

Arrow 6's difference is returns_pending and it is normal during batching. 21.3 §26: stable is the bug, rising and falling is health.

And arrows 3 and 7 are the two with genuine transport latency, which is why §10's in-flight terms exist and §11 is the failure of omitting them.

The ledger is a chain of differences. The same facts also form a single capacity equation, and the two views answer different questions:

ILLUSTRATIVE capacity conservation, per domain, per epoch. This is an
ANALYTICAL model for debugging, NOT a normative UCIe requirement (§3).
 
  advertised_capacity(E)
    ==  free_credit_at_sender          // the sender's usable count
      + capacity_held_by_outstanding   // admitted work not yet released
      + capacity_held_in_local_queues  // staged between layers, pre-transmit
      + returns_legitimately_in_flight // released, return not yet applied
 
  Every term is a PLACE a unit of capacity can be. If the four do not sum to
  the advertisement, a unit is somewhere the model does not know about — and
  the ledger of §5 says WHICH boundary it went missing at.

Three readings, and the third is why both views are kept.

Every term is a location, not a count of events. The ledger counts crossings; this equation asks where the capacity currently is. A unit that satisfies neither view is not merely miscounted — it is unaccounted for.

The third term is the one most often forgotten. Capacity committed to an object sitting in a local staging queue before transmission is neither free nor outstanding at the far end, and a two-term model (free plus outstanding) reports it as leaked for exactly as long as the object is staged.

And the two views fail differently. The ledger detects a flow error — an event that happened once too often or not at all. The capacity equation detects a stock error — a unit that exists nowhere. A design can pass the ledger and fail this, if a unit is double-counted in two places at once, which is §39's split-release for the duration of its one-cycle window.

6. Ownership Handoff, End to End

Three things to read.

The second arrow carries two events on one label — ADAPTER_ACCEPT and CREDIT_CONSUME — because ledger arrow 2 has no legitimate transient difference (§5). Drawing them as one arrow is the contract, and §47 is the trace where they diverge.

The sixth arrow says "reusable", not "read". 19.5 §21: a return is a statement about storage becoming reusable. The read arrow above it is the event a wrong design generates on, and §39 is that split.

And the three muted arrows all follow from one missing event. The return was never generated, so it was never transmitted and never applied — so a debugger reading the sender's credit sees three broken things and there is one cause, at arrow 5.

7. The Boundary Event Vocabulary

// ILLUSTRATIVE, DEBUG-ONLY. Nine boundary events. These are TUTORIAL AND DEBUG
// constructs, not UCIe wire messages (§3) — no protocol carries an event named
// RETURN_GEN, and none of these names appears in any specification.
typedef enum logic [EVENT_W-1:0] {
  EV_SEM_ACCEPT     = 'd0,  // the protocol layer accepted a client operation
  EV_ADAPTER_ACCEPT = 'd1,  // the Adapter accepted the resulting object
  EV_CREDIT_CONSUME = 'd2,  // a credit was charged for it
  EV_REMOTE_ALLOC   = 'd3,  // the far end allocated an entry
  EV_REMOTE_RELEASE = 'd4,  // that entry became REUSABLE (§38)
  EV_RETURN_GEN     = 'd5,  // a return was generated locally at the far end
  EV_RETURN_TX      = 'd6,  // it was transmitted
  EV_RETURN_RX      = 'd7,  // it was received by the sender
  EV_RETURN_APPLY   = 'd8   // it was applied to the credit counter
} boundary_event_e;

Architecture. A closed enumeration so every consumer's case is exhaustive and adding a boundary is a compile-time obligation everywhere (20.4 §7's single-event-type argument).

State. None — it is a tag on an event record (§8).

Event behaviour. Exactly one of these is emitted per boundary crossing per object per domain. EV_ADAPTER_ACCEPT and EV_CREDIT_CONSUME are emitted in the same cycle in a correct design, and their separation is what makes ledger arrow 2 checkable.

Contract. Each event is emitted by the upstream side of its boundary at the instant ownership transfers, observed at the boundary rather than derived from an internal state. 20.4 §9's monitor discipline.

Failure. An enumeration that merges two events — say, one RETURN event covering generation, transmission and application — collapses three ledger arrows into one and makes §49's trace undiagnosable, because a return that was generated and rejected reads identically to one never generated.

Debug/DV. Nine counters, one per event, per domain (§12). The differences between adjacent counters are the diagnosis (§18).

8. The Credit Event Record

// ILLUSTRATIVE, DEBUG-ONLY. One record per boundary crossing. The identity is
// a LOCAL DEBUG TAG, not a protocol field (§3).
typedef struct packed {
  logic [TIME_W-1:0]   timestamp;
  logic [DOMAIN_W-1:0] domain;      // ownership domain — §13
  logic [OBJ_W-1:0]    object_id;   // LOCAL debug identity — §24
  logic [EPOCH_W-1:0]  epoch;       // which agreement — §21
  boundary_event_e     event_kind;
  logic [COUNT_W-1:0]  amount;      // capacity UNITS, which may exceed 1 — §31
  logic [CLASS_W-1:0]  alloc_class; // NEW_ALLOCATION vs RETRANSMISSION — §35
} credit_event_t;

Architecture. Everything needed to reconcile one boundary crossing against its counterpart, in one record, so the two halves can be matched by identity rather than by arrival order.

State. In simulation, a queue per boundary. In silicon, a bounded ring plus the aggregate counters of §12 — because storing every record is not feasible and §26 is the compression discussion.

Event behaviour. Emitted at the boundary crossing. amount is captured from the same source the design charged, so a mismatch between event count and amount sum is detectable (§33).

Contract. object_id must be unique for long enough that a duplicate is distinguishable from a legitimate reuse — 20.4 §21's argument. epoch must be present or §22's cross-recovery comparison is meaningless.

Failure. A record without domain cannot detect §15's cancellation. A record without amount cannot detect a capacity drift where the event counts are correct (§32). A record without alloc_class bakes the retransmission assumption invisibly into the counters (§36).

Debug/DV. The record is what turns a count mismatch into a named object — §25's argument, and it is the difference between "one duplicate exists" and "object 0x1A3 was returned twice."

9. The Boundary Reconciliation Table

The chapter's second centerpiece. Eight comparisons, each with the term that makes it valid.

Four properties.

Rows 2 and 5 are the two that need no latency model and no quiescence. They are checkable at any cycle, in silicon, from two register reads — and between them they cover the false consume and the missing return generation, which are the two most common bugs in the chain.

Row 4 is not a comparison of a credit path at all. Its difference is the receiver's occupancy, and a reconciliation tool that flags it reports a "leak" equal to the fill level — which is §11's failure in its most embarrassing form.

Row 8's reconciliation term is a counter, not a latency. §46's rejection counters: return_rx = return_apply + rejections, and without the rejection counters a correctly-rejected stale return is indistinguishable from a lost one (§44).

And rows 3 and 7 are the two where a debugger must know the latency to interpret a nonzero difference — which is §10.

10. In-Flight Terms

The equation is not upstream == downstream. It is:

ILLUSTRATIVE reconciliation form, per boundary, per domain, per epoch.
 
   upstream_events
     ==  downstream_events
       + events_currently_in_flight
       + events_explicitly_cancelled_or_reconciled
 
  where:
    in_flight            is bounded by the boundary's transport latency
                         times the maximum issue rate
    cancelled/reconciled is architecture-defined — a recovery may explicitly
                         resolve outstanding transfers rather than deliver them

Three consequences.

A nonzero difference is only evidence at quiescence, or when it exceeds the maximum possible in-flight count. With a twenty-cycle return path and at most one return per cycle, a difference of five is unremarkable and a difference of five hundred is not.

So the in-flight bound must be known, and it is derived from the boundary's latency and rate — not measured, and not guessed. A boundary whose in-flight bound is undocumented has a reconciliation that cannot be interpreted.

And the third term is why §22's cross-recovery comparison needs care. A recovery may explicitly reconcile outstanding transfers; those are neither delivered nor lost, and an equation without the term reports them as lost forever.

The in-flight term can be measured rather than bounded, and where it can, the reconciliation becomes exact under load:

// ILLUSTRATIVE. The in-flight count at one boundary, maintained as a DERIVED
// difference rather than an independent counter — so it cannot drift from the
// two counters it reconciles (21.3 §11's derived-occupancy argument).
//
// This is the term that turns an inequality into an EQUALITY under load.
logic [31:0] inflight_tx_rx_q   [NUM_DOMAINS];   // returns sent, not yet received
logic [31:0] inflight_max_q     [NUM_DOMAINS];   // high-water — §10's bound, MEASURED
 
always_ff @(posedge clk or negedge por_n) begin
  for (int d = 0; d < NUM_DOMAINS; d++) begin
    if (!por_n) begin
      inflight_tx_rx_q[d] <= '0;
      inflight_max_q[d]   <= '0;
    end else begin
      // +1 on transmit, -1 on receive. Both may fire in the same cycle, so the
      // update is a single signed expression, never two sequential statements
      // (19.5 §14).
      inflight_tx_rx_q[d] <= inflight_tx_rx_q[d]
                           + 32'(ret_tx_fire[d]) - 32'(ret_rx_fire[d]);
      // High-water is the EMPIRICAL bound. A measured maximum well below the
      // architectural bound means the bound is loose; ABOVE it is a finding.
      if ((inflight_tx_rx_q[d] > inflight_max_q[d]) && (inflight_max_q[d] != '1))
        inflight_max_q[d] <= inflight_tx_rx_q[d];
    end
  end
end
 
// With the measured term, arrow 7 becomes EXACT at every cycle (§9 row 7).
a_arrow7_exact_with_inflight: assert property (
  @(posedge clk) disable iff (!por_n)
    (cnt_return_tx_q[0] == cnt_return_rx_q[0] + 64'(inflight_tx_rx_q[0]))
);
 
// And the in-flight count can never exceed the architectural bound.
a_inflight_bounded: assert property (
  @(posedge clk) disable iff (!por_n)
    (inflight_tx_rx_q[0] <= 32'(MAX_RET_IN_FLIGHT))
);

Architecture. A per-boundary in-flight count, maintained as a running difference, which converts a bounded comparison into an exact one under load.

State. One counter and one high-water register per domain per instrumented boundary.

Event behaviour. Incremented on the upstream event, decremented on the downstream one, in a single signed expression so a same-cycle transmit-and-receive nets to zero rather than being lost by two sequential assignments (19.5 §14).

Contract. The counter must be derived from the same two events the ledger counts, not from an independent observation of the transport — otherwise it is a third opinion that can disagree with both, and a disagreement between three counters is harder to read than between two.

Failure. An in-flight counter maintained by two if branches loses a same-cycle pair, so it drifts downward and a_arrow7_exact_with_inflight fires on correct hardware — which gets the assertion deleted rather than the counter fixed.

Debug/DV. Two payoffs. Arrow 7 becomes checkable without quiescence, which matters most in silicon where quiescence is expensive to arrange. And inflight_max is the measured bound, so §16's MAX_RET_IN_FLIGHT can be reviewed against reality rather than trusted — a measured maximum that exceeds the architectural bound is a finding in its own right, and one that no conservation check would surface.

11. Wrong Model — Comparing Cumulative Counters Directly

WRONG reconciliation, at a live moment:
 
  return_gen  = 100
  return_apply = 95
 
  CONCLUSION DRAWN: "5 returns lost."

What was actually happening. The return path has twenty cycles of transport latency and the design is issuing returns steadily. Five returns are in flight.

Four properties.

The difference is exactly the pipeline occupancy and it is constant under steady load. A debugger who samples again a microsecond later sees 5 again and concludes the leak is stable — which is the reading a genuine leak would also produce.

The discriminating observation is to stop the traffic. At quiescence, in-flight goes to zero and the difference should too. A difference that persists at quiescence is a real loss; one that vanishes was latency.

Or, without stopping traffic: compare the difference against the bound. Five, against a bound of twenty, is inside the envelope. Five hundred is not, and needs no quiescence to interpret.

And the same mistake at row 4 of §9 is worse, because occupancy can be large and steady: a receiver holding 12 of 16 entries produces a permanent difference of 12 that looks exactly like a twelve-credit leak.

12. Stage Counters

// ILLUSTRATIVE. Nine counters, per domain. Wide enough not to wrap in a soak
// (21.3 §46), and the ONLY aggregate state a silicon implementation needs (§55).
logic [63:0] cnt_sem_accept_q     [NUM_DOMAINS];
logic [63:0] cnt_adapter_accept_q [NUM_DOMAINS];
logic [63:0] cnt_consume_q        [NUM_DOMAINS];
logic [63:0] cnt_remote_alloc_q   [NUM_DOMAINS];
logic [63:0] cnt_remote_release_q [NUM_DOMAINS];
logic [63:0] cnt_return_gen_q     [NUM_DOMAINS];
logic [63:0] cnt_return_tx_q      [NUM_DOMAINS];
logic [63:0] cnt_return_rx_q      [NUM_DOMAINS];
logic [63:0] cnt_return_apply_q   [NUM_DOMAINS];
 
// And the AMOUNT sums alongside, because events and units are different
// quantities (§31).
logic [63:0] amt_consume_q        [NUM_DOMAINS];
logic [63:0] amt_return_apply_q   [NUM_DOMAINS];
 
always_ff @(posedge clk or negedge por_n) begin
  if (!por_n) begin
    for (int d = 0; d < NUM_DOMAINS; d++) begin
      cnt_sem_accept_q[d] <= '0;  cnt_adapter_accept_q[d] <= '0;
      cnt_consume_q[d]    <= '0;  cnt_remote_alloc_q[d]   <= '0;
      cnt_remote_release_q[d] <= '0; cnt_return_gen_q[d]  <= '0;
      cnt_return_tx_q[d]  <= '0;  cnt_return_rx_q[d]      <= '0;
      cnt_return_apply_q[d] <= '0;
      amt_consume_q[d]    <= '0;  amt_return_apply_q[d]   <= '0;
    end
  end else if (evt_valid) begin
    // ONE increment per observed boundary event, indexed by the EVENT's domain
    // — never by a shared "current domain" register (19.5 §47).
    unique case (evt.event_kind)
      EV_SEM_ACCEPT:     cnt_sem_accept_q[evt.domain]     <= cnt_sem_accept_q[evt.domain] + 64'd1;
      EV_ADAPTER_ACCEPT: cnt_adapter_accept_q[evt.domain] <= cnt_adapter_accept_q[evt.domain] + 64'd1;
      EV_CREDIT_CONSUME: begin
        cnt_consume_q[evt.domain] <= cnt_consume_q[evt.domain] + 64'd1;
        amt_consume_q[evt.domain] <= amt_consume_q[evt.domain] + 64'(evt.amount);
      end
      EV_REMOTE_ALLOC:   cnt_remote_alloc_q[evt.domain]   <= cnt_remote_alloc_q[evt.domain] + 64'd1;
      EV_REMOTE_RELEASE: cnt_remote_release_q[evt.domain] <= cnt_remote_release_q[evt.domain] + 64'd1;
      EV_RETURN_GEN:     cnt_return_gen_q[evt.domain]     <= cnt_return_gen_q[evt.domain] + 64'd1;
      EV_RETURN_TX:      cnt_return_tx_q[evt.domain]      <= cnt_return_tx_q[evt.domain] + 64'd1;
      EV_RETURN_RX:      cnt_return_rx_q[evt.domain]      <= cnt_return_rx_q[evt.domain] + 64'd1;
      EV_RETURN_APPLY:   begin
        cnt_return_apply_q[evt.domain] <= cnt_return_apply_q[evt.domain] + 64'd1;
        amt_return_apply_q[evt.domain] <= amt_return_apply_q[evt.domain] + 64'(evt.amount);
      end
      default: ;
    endcase
  end
end

Architecture. Nine event counters and two amount sums, per domain. They are the entire aggregate state the chain needs, and they are what transfers to silicon (§55).

State. 9 × NUM_DOMAINS 64-bit event counters plus amount sums. Wide rather than saturating, because differences must remain meaningful — 21.3 §46's policy table.

Event behaviour. One increment per observed boundary event. The domain index comes from the event, never from a shared register — 19.5 §47's failure produces a count charged to the wrong domain, which keeps the total right and both domains wrong, and is §15 arriving from the instrumentation rather than the design.

Contract. Every event must be observed at its boundary. A counter fed from a design-internal signal inherits that signal's definition — 21.3 §10's shadow failure, and it makes the whole chain agree with the bug.

Failure. A shared "current domain" register mis-indexes; a saturating counter makes late differences meaningless; and a counter that wraps in a soak reports a perfect balance (§34).

Debug/DV. These nine numbers, read in order, produce §18's first-divergence answer — with no waveform and no simulation.

13. Per-Domain Indexing

Every counter, every comparison, every assertion must be per ownership domain.

The test is physical, not logical. Two flows share a domain if and only if they draw from one physical pool of entries at the receiver (19.5 §8). If they draw from different structures, one counter cannot describe both.

And the reason this chapter restates it — 21.3 §39 already made the argument — is that a layered chain multiplies the exposure. Nine boundaries times N domains, and a design that is per-domain at some boundaries and total at others has a chain that cannot be reconciled at all, because the totals cannot be decomposed back into domains.

14. Wrong — One Chain for All Domains

// WRONG — nine counters, no domain index.
logic [63:0] cnt_consume_q, cnt_return_apply_q;   // totals only

Three consequences beyond 21.3 §39's cancellation.

The chain becomes non-decomposable. Even if a mismatch is detected, it cannot be attributed to a domain — so the investigation has no starting point, and every domain's logic is a candidate.

Misattribution becomes invisible. §4's fourth row: an event charged to the wrong domain is a real bug in the design, and a total-only chain cannot see it at all because the total is unaffected.

And the per-boundary structure is wasted. Nine boundaries localise a bug to an arrow; without domains, the answer is "arrow 5, in one of eight domains" — which is a small fraction of the localisation the chain was built to provide.

15. Flagship — Cross-Domain Cancellation

The failure that makes every total useless, worked in full.

Five properties.

The total is exactly right and both domains are exactly wrong. Not approximately — exactly, because a misattribution moves a count from one domain to another and the sum is conserved by construction.

The two failures have opposite symptoms. Domain A stalls; domain B overflows. A team investigating the stall and a team investigating the overflow are chasing one bug from two directions, and neither will find it in a total.

Cancellation becomes more likely over a long run, not less. 21.3 §39: magnitudes converge, so the longer the soak, the more perfectly the total closes.

The root cause is usually a single mis-indexing, not two independent bugs — a shared domain register (§12), a domain field taken from the wrong pipeline stage, or a return applied to the domain that happened to be current rather than the one the return named.

And the discriminating observation is one read per domain. The moment the counters are per domain, this failure is trivial; the moment they are not, it is undetectable.

16. SVA — Conservation Per Domain

// MANDATORY. Per domain, and the two exact identities need no in-flight term
// (§9's rows 2 and 5) so they are checkable at every cycle.
generate
  for (genvar d = 0; d < NUM_DOMAINS; d++) begin : g_conserve
 
    // Ledger arrow 2 — no legitimate transient difference.
    a_accept_equals_consume: assert property (
      @(posedge clk) disable iff (!por_n)
        (cnt_adapter_accept_q[d] == cnt_consume_q[d])
    );
 
    // Ledger arrow 5 — release and generation are the SAME event (§38).
    a_release_equals_return_gen: assert property (
      @(posedge clk) disable iff (!por_n)
        (cnt_remote_release_q[d] == cnt_return_gen_q[d])
    );
 
    // Arrow 8 — reconciled by the explicit rejection counters (§46).
    a_rx_equals_apply_plus_rejects: assert property (
      @(posedge clk) disable iff (!por_n)
        (cnt_return_rx_q[d] == cnt_return_apply_q[d] + cnt_reject_total_q[d])
    );
 
    // The LATENCY-BEARING arrows need a bounded form, not an equality.
    a_consume_alloc_bounded: assert property (
      @(posedge clk) disable iff (!por_n)
        ((cnt_consume_q[d] - cnt_remote_alloc_q[d]) <= 64'(MAX_OBJ_IN_FLIGHT))
    );
    a_tx_rx_bounded: assert property (
      @(posedge clk) disable iff (!por_n)
        ((cnt_return_tx_q[d] - cnt_return_rx_q[d]) <= 64'(MAX_RET_IN_FLIGHT))
    );
 
  end
endgenerate

Architecture. Three exact identities and two bounded ones, per domain. The split follows §9's table exactly — the arrows with no legitimate transient get equalities, the transport arrows get bounds.

State. None beyond the counters.

Event behaviour. Evaluated every cycle. The exact identities can fail at the cycle the bug happens, which is the whole point of separating them from the bounded ones.

Contract. MAX_OBJ_IN_FLIGHT and MAX_RET_IN_FLIGHT must be derived from the boundary's latency and rate (§10), not chosen. An undocumented bound cannot be reviewed and will be raised the first time it fires.

Failure. Asserting equality on a latency-bearing arrow fires constantly on correct hardware and gets deleted, taking the bounded check with it — 20.2 §16's pattern. Asserting only a total is satisfied by §15's cancellation.

Debug/DV. The two exact identities are also readable registers in silicon (§55), which is why they are the highest-value rows in the whole chain.

Four more properties, each tied to a specific failure above rather than restating an assignment:

// (1) NEVER CONSUME WITHOUT CAPACITY. English: a credit may only be charged
// when a unit is available AFTER accounting for anything returned in the same
// cycle. Architectural. Fires on the over-allocation that §50's misattribution
// eventually produces. NEXT-STATE form, because a same-cycle return may
// legitimately cover the consume (19.5 §14) — the cause-form written against
// the REGISTERED value fires on correct hardware and gets deleted.
logic signed [CRD_W:0] credit_next [NUM_DOMAINS];
generate
  for (genvar d = 0; d < NUM_DOMAINS; d++) begin : g_cap
    assign credit_next[d] = $signed({1'b0, credit_q[d]})
                          + $signed({1'b0, ret_amount[d]})
                          - $signed({1'b0, con_amount[d]});
 
    a_never_consume_without_capacity: assert property (
      @(posedge clk) disable iff (!por_n) (credit_next[d] >= 0)
    );
 
    // (2) RETURN ONLY FOR A PREVIOUSLY CONSUMED CREDIT. English: cumulative
    // units restored can never exceed cumulative units charged. Fires in
    // PHASE 2 of §25's double-return trace — thousands of cycles before the
    // receiver overflows. This is the highest-value property in the chapter.
    a_no_return_without_consume: assert property (
      @(posedge clk) disable iff (!por_n)
        (amt_return_apply_q[d] <= amt_consume_q[d])
    );
 
    // (3) DIAGNOSTIC COUNTERS NEVER WRAP SILENTLY. English: a 64-bit total
    // must not roll over, because §34's wrapped soak reports a false balance.
    // Checked as "never decreases" — a wrap is the only way a monotonic
    // counter goes backwards, and this catches it at the cycle it happens.
    a_counters_monotonic: assert property (
      @(posedge clk) disable iff (!por_n)
        (cnt_consume_q[d] >= $past(cnt_consume_q[d])) &&
        (amt_consume_q[d] >= $past(amt_consume_q[d]))
    );
 
    // (4) RECOVERY CANNOT SILENTLY CREATE OR DESTROY OWNERSHIP. English: at an
    // epoch boundary, what was outstanding must be either carried or explicitly
    // reconciled (§23) — never simply forgotten. Fires on §22's asymmetric
    // reset, at the re-advertisement.
    a_epoch_close_accounts: assert property (
      @(posedge clk) disable iff (!por_n)
        epoch_close_fire[d] |-> (outstanding_at_close[d] == reconciled_count[d])
    );
  end
endgenerate

Architecture. Four invariants: a capacity floor, a restoration ceiling, counter integrity, and an epoch-boundary accounting rule.

State. Only the counters already present, plus the combinational next-state credit.

Event behaviour and sampled timing. All four sample in the preponed region, so they see the registered values from the previous cycle. Property (1) deliberately evaluates credit_next, a combinational expression of this cycle's events — which is the whole point, because a consume and a return landing together must be evaluated as one update rather than two. Property (3) uses $past, which is undefined in the first cycle after reset — disable iff (!por_n) covers it, and without that guard it fires spuriously at time zero.

Contract. Property (1)'s arithmetic must match the design's documented same-cycle semantics. If the architecture does not permit a same-cycle return to cover a consume, the next-state form is too permissive and the registered form is correct — and choosing between them to stop an assertion firing is 21.6 §9's error. Property (4) requires the design to count what it reconciled, which many do not (§23).

Failure. Property (2) omitted is the expensive one: §25's inflation then goes undetected through its entire profitable phase, and is discovered as receiver corruption four boundaries away. Property (3) omitted means §34's soak silently reports success.

Debug/DV. These are illustrative architectural properties, not UCIe requirements (§3). Property (2) is the one to build first — it is two registers, needs no latency model, and fires at the first excess return.

17. Layer-Local Correctness With System Failure

The situation this chapter exists for, and it is worth stating as its own section because it defeats both teams independently.

Four properties.

Every layer-local check passes, so a receiver-side investigation finds nothing and a sender-side investigation finds nothing.

Both implementations may be entirely correct. The messages were generated correctly, transmitted correctly, and everything that arrived was applied correctly — the transport lost them.

The bug is invisible to anybody who does not compare across the boundary, and that comparison requires counters on both sides expressed in the same units and the same domains — which is a system-level instrumentation decision, not a block-level one.

And this is why §18's algorithm reads the chain in order rather than checking each layer. A per-layer check set, however thorough, has a hole exactly at each boundary between layers.

18. The First-Divergence Algorithm

Read the nine counters in order. The first adjacent pair whose reconciled difference exceeds its bound names the boundary.

ILLUSTRATIVE reading, one domain, at quiescence.
 
  cnt_sem_accept       1000
  cnt_adapter_accept   1000     d1 = 0     OK
  cnt_consume          1000     d2 = 0     OK   <- arrow 2 exact
  cnt_remote_alloc     1000     d3 = 0     OK   (quiescent: in-flight = 0)
  cnt_remote_release    850     d4 = 150   OK   <- THIS IS OCCUPANCY (§9 row 4)
  cnt_return_gen        850     d5 = 0     OK   <- arrow 5 exact
  cnt_return_tx         850     d6 = 0     OK   (quiescent: pending = 0)
  cnt_return_rx         842     d7 = 8     ***  <- FIRST DIVERGENCE
  cnt_return_apply      842     d8 = 0     OK
 
  FIRST DIVERGENCE: arrow 7, return_tx -> return_rx, 8 messages.
  At quiescence, in-flight is zero, so 8 returns were LOST IN TRANSPORT.
  INVESTIGATE: the return message path, its clock-domain crossing, any filter.
  DO NOT INVESTIGATE: the sender's credit decrement RTL, the consume
  qualification, the return generator — all four have closed above.

Four properties, and the fourth is the practical payoff.

d4 = 150 is not a divergence. It is the receiver's occupancy at the moment of the read — and a tool that flags it reports a 150-credit leak that does not exist (§11).

Reading in order matters. A later mismatch is frequently a consequence of an earlier one; the first one is the cause, and checking the arrows independently loses that ordering.

Quiescence removes the in-flight terms, which is why it is worth the effort to reach it. Without quiescence the same reading requires the bounds of §10 and produces a weaker conclusion.

And the "do not investigate" list is half the value. Four subsystems eliminated by four closed comparisons — and each of those is a plausible hypothesis that would otherwise cost a day.

19. Automating the Comparison

// ILLUSTRATIVE, VERIFICATION-ONLY. Returns the earliest boundary whose
// reconciled equation fails, or BND_NONE. Independent of the DUT (20.4 §17).
typedef enum {
  BND_NONE, BND_SEM_ADAPTER, BND_ADAPTER_CONSUME, BND_CONSUME_ALLOC,
  BND_ALLOC_RELEASE, BND_RELEASE_GEN, BND_GEN_TX, BND_TX_RX, BND_RX_APPLY
} boundary_e;
 
function automatic boundary_e first_mismatch(fc_snapshot_t s, bit quiescent);
  // Arrow 1 — bounded by objects queued between layers.
  if ((s.sem_accept - s.adapter_accept) > s.max_interlayer_queue)
    return BND_SEM_ADAPTER;
  // Arrow 2 — EXACT, always.
  if (s.adapter_accept != s.consume)          return BND_ADAPTER_CONSUME;
  // Arrow 3 — bounded by objects in flight.
  if ((s.consume - s.remote_alloc) > (quiescent ? 0 : s.max_obj_in_flight))
    return BND_CONSUME_ALLOC;
  // Arrow 4 — the difference IS occupancy; only an IMPOSSIBLE value is a bug.
  if ((s.remote_alloc - s.remote_release) > s.active_capacity)
    return BND_ALLOC_RELEASE;
  // Arrow 5 — EXACT, always.
  if (s.remote_release != s.return_gen)       return BND_RELEASE_GEN;
  // Arrow 6 — bounded by pending returns.
  if ((s.return_gen - s.return_tx) > (quiescent ? 0 : s.max_pending_returns))
    return BND_GEN_TX;
  // Arrow 7 — bounded by messages in flight.
  if ((s.return_tx - s.return_rx) > (quiescent ? 0 : s.max_ret_in_flight))
    return BND_TX_RX;
  // Arrow 8 — reconciled by the explicit rejection counters (§46).
  if (s.return_rx != (s.return_apply + s.reject_total))
    return BND_RX_APPLY;
  return BND_NONE;
endfunction

Architecture. One pass over the snapshot, in ledger order, returning the earliest failing boundary.

State. None — a pure function of a snapshot, so it can be run offline on a captured register dump.

Event behaviour. Called on a snapshot (§20), not per cycle.

Contract. The snapshot must be atomic (§41), or the function reads counters from different instants and reports a boundary that is an artefact of the skew — which is §51's trace.

Failure. Two specific ones. Checking arrow 4 as an equality reports a leak equal to the occupancy. Omitting the quiescent distinction makes every latency-bearing arrow fire under load, so the function is disabled and the exact arrows go with it.

Debug/DV. It is deliberately independent of the design — 20.4 §17's rule — so it can be run against a silicon register dump, a simulation snapshot, or a scoreboard's own model, and disagreement between those three is itself a finding.

20. The Debug Snapshot

// ILLUSTRATIVE. One snapshot, per domain, captured atomically (§42).
typedef struct packed {
  logic [DOMAIN_W-1:0] domain;
  logic [EPOCH_W-1:0]  epoch;
  // the nine stage counters
  logic [63:0] sem_accept, adapter_accept, consume, remote_alloc;
  logic [63:0] remote_release, return_gen, return_tx, return_rx, return_apply;
  // reconciliation terms
  logic [31:0] max_interlayer_queue, max_obj_in_flight;
  logic [31:0] max_pending_returns,  max_ret_in_flight;
  logic [31:0] active_capacity, reject_total;
  // amounts (§33)
  logic [63:0] amt_consume, amt_return_apply;
  // context
  logic [31:0] occupancy_now, credit_now, oldest_boundary_age;
  logic [OBJ_W-1:0] first_dup_object;      // §27
} fc_snapshot_t;

Architecture. Everything §19's function needs, plus the context that interprets its answer.

State. One frozen copy per domain, written by a trigger (§42).

Event behaviour. Captured on a trigger, not continuously. Four triggers are worth wiring: sender credit reaching zero unexpectedly (21.3 §42), credit exceeding active capacity, an exact-identity assertion diverging (§16), and a boundary age crossing its threshold (§29).

Contract. All fields must describe the same instant (§41). A snapshot assembled by successive software reads is not a snapshot.

Failure. A torn snapshot produces a first-divergence answer that is an artefact — §51.

Debug/DV. The snapshot is the artefact that travels: it can be dumped from silicon, replayed offline through §19's function, and compared against a simulation snapshot of the same scenario.

21. Epoch Partitioning

Counters are only comparable within an agreement.

ILLUSTRATIVE. The equation, per epoch, with the baseline term explicit.
 
  Within epoch E:
     sender_credit(E)  ==  advertised(E)
                         + returns_applied_in_E
                         -  consumes_in_E
 
  Across E -> E+1 the equation RESTARTS. advertised(E+1) is a NEW baseline,
  and E's consumes and returns are NOT terms of E+1's equation.
 
  So a lifetime total spanning several epochs reconciles only if the
  per-epoch baselines and any explicit reconciliation terms are included.

Two consequences.

Counters must either be snapshotted at each epoch boundary or be free-running with a per-epoch snapshot recorded. 21.3 §41: the second is preferable because it preserves history, which 14.2 §14's capture-before-retrain rule requires.

And a mismatch that appears only across a boundary is frequently not a bug at all — it is the missing baseline term, which is §22.

22. Wrong Comparison Across a Recovery

WRONG reading, lifetime totals across two epochs:
 
  Epoch 4:  consumes 1000,  returns applied 995
  Recovery: sender re-baselined to active capacity
  Epoch 5:  consumes  400,  returns applied 400
 
  LIFETIME: consumes 1400, returns applied 1395
  CONCLUSION DRAWN: "5 credits permanently leaked."

What may actually have happened. Those five obligations were explicitly reconciled during the recovery — the agreement was voided, the outstanding transfers resolved by the resynchronisation, and the new epoch started from a fresh advertisement. Nothing was lost.

Four properties.

The lifetime difference is expected whenever an epoch boundary explicitly reconciles outstanding transfers, so the reading is not merely uncertain — it is predicted by a correct design.

The discriminating observation is the per-epoch equation. Epoch 4 in isolation: 1000 consumed, 995 returned, 5 outstanding at the boundary — which the recovery then reconciled. Epoch 5 in isolation: 400 and 400, closed.

A design without a reconciliation term cannot express this, and the honest response is to record how many transfers the recovery resolved — which is a counter, and it belongs in §20's snapshot.

And the mirror error is real too: if the recovery did not reconcile them and they genuinely leaked, the per-epoch equation shows epoch 4 with 5 outstanding at its close and epoch 5 starting short — a different reading, from the same discipline.

The worst case is when only one side re-baselines.

Five readings, and the first is what makes this class so dangerous.

Both sides are internally consistent. The local credit block's arithmetic is correct against its own epoch-5 baseline; the remote buffer's occupancy is correct against its own state. §17's layer-local correctness, produced by a reset scope rather than by a logic bug.

The sender will over-issue by exactly the retained count — 17 — and the receiver will overflow only under enough load to consume the phantom capacity, which may be far from the reset.

The epoch mismatch is the direct evidence and it costs one comparison. Local epoch 5 against remote epoch 4 is an impossible pairing; 19.5 §31's monotonicity property is about one side's epoch advancing, and this needs the cross-side check — which is a different property and is frequently absent.

The second-order evidence is in the rejection counters (§46): with the epochs mismatched, returns generated under epoch 4 arrive at a sender expecting epoch 5 and are rejected as REJ_STALE_EPOCH — a burst of stale rejections immediately after a recovery, which §49 warns can be legitimate stragglers. The discriminator is whether they stop. Stragglers drain in a round trip; an epoch mismatch produces them forever.

And the structural fix is a reset-scope question, not a credit question (19.6 §27): the agreement is bilateral, so anything that voids it must void it on both sides or not at all — and the check that proves it is a cross-side epoch comparison at every re-advertisement.

23. Epoch-Tagged Reconciliation

// ILLUSTRATIVE. Per-epoch statistics, so §22's two readings are distinguishable.
typedef struct packed {
  logic [EPOCH_W-1:0] epoch;
  logic [63:0]        consume;
  logic [63:0]        returned;
  logic [63:0]        reconciled;    // explicitly resolved at the boundary
  logic [63:0]        outstanding_at_close;
  logic [31:0]        advertised_at_open;
} fc_epoch_stats_t;
 
fc_epoch_stats_t epoch_hist [EPOCH_HIST_DEPTH][NUM_DOMAINS];

Architecture. A bounded history of per-epoch statistics, so a lifetime question decomposes into per-epoch questions.

State. A small ring — epochs are counted in tens over a run, not thousands, so the depth is modest.

Event behaviour. A row is closed at an epoch boundary and a new one opened, with advertised_at_open captured from the new advertisement (19.5 §12's exactness).

Contract. reconciled must be counted by whatever performs the reconciliation. A design that reconciles implicitly — by simply re-baselining and forgetting — cannot fill this field, and that is itself a finding: it means the design cannot distinguish a reconciled obligation from a lost one either.

Failure. Without reconciled, §22's two readings are indistinguishable and every recovery looks like a small leak.

Debug/DV. Reading the ring backwards answers "which epoch did the shortfall appear in?" — and a shortfall that appears in one epoch is a different investigation from one that accumulates a little in every epoch.

24. Duplicate Detection Needs Identity

Counters detect a count mismatch. Identity proves which object.

// ILLUSTRATIVE, VERIFICATION-SIDE. An associative set keyed by the tuple that
// makes an event unique. A count cannot answer "which object?" (§25).
typedef struct {
  int unsigned domain;
  int unsigned epoch;
  int unsigned object_id;
  int unsigned event_kind;
} evt_key_t;
 
int unsigned seen_count [evt_key_t];    // how many times this exact event occurred
 
function automatic void observe(credit_event_t e);
  evt_key_t k = '{ domain: e.domain, epoch: e.epoch,
                   object_id: e.object_id, event_kind: e.event_kind };
  if (seen_count.exists(k)) begin
    seen_count[k]++;
    report_error(ERR_DUPLICATE_BOUNDARY_EVENT, e.object_id,
                 $sformatf("%s seen %0d times for object 0x%0h, domain %0d, epoch %0d",
                           e.event_kind.name(), seen_count[k], e.object_id,
                           e.domain, e.epoch));
  end else begin
    seen_count[k] = 1;
  end
endfunction

Architecture. A set keyed by domain, epoch, object and event kind — the four fields that together make a boundary event unique.

State. One entry per distinct event, retired when the object retires (or the epoch closes).

Event behaviour. Every observed boundary event is offered. A second occurrence of the same key is a duplicate, reported at the cycle it happens.

Contract. object_id must be a local debug tag unique for long enough, not a protocol identity that is legitimately reused (20.4 §21). Keying on a reused identity produces false duplicates on every legitimate reuse.

Failure. Without the epoch in the key, an object identity reused in a new epoch collides with the old one. Without the event kind, a legitimate RETURN_TX after a RETURN_GEN for the same object reads as a duplicate.

Debug/DV. This is the mechanism that turns "d3 is −14" into "object 0x1A3 generated two returns in domain 0, epoch 7, at cycles 8,412 and 8,419" — which is a fix rather than a search.

25. Wrong — the Scalar Diagnosis

Counters say:   return_gen  = release + 1
 
CONCLUSION:     "one duplicate return exists"
CANNOT SAY:     which object, which cycle, which path generated it

Three properties.

The count is correct and unactionable. One duplicate among a thousand releases; the search space is a thousand objects.

The mechanism is unknown. 21.3 §18 lists five ways duplicates arise — a level sampled twice, a pulse crossing a domain, a retransmitted message, a pop-plus-flush, two structures sharing an index. Each leaves a different fingerprint in the identity record and none in the count.

And the fix cannot be verified. After a change, the count returns to zero — which is also what a change that merely made the duplicate rarer produces. With identity, the specific object and path are known and the fix is checkable.

Worked in full, because the double return is the failure that improves the numbers before it destroys the link.

Five readings.

Phase 3 is the best throughput the link ever achieves, and it is the sickest the link has ever been. The sender believes it has more capacity than exists, so it stops throttling — and a performance regression run in phase 3 records an improvement.

The symptom appears at the receiver, thousands of cycles after the cause at the sender's applier. 21.3 §8's inflation signature: the overflow is the consequence, and the investigation that starts there is four boundaries away from the bug.

The discriminating observation is available in phase 2, long before any corruption: return_apply > return_gen is arithmetically impossible — more returns applied than were ever generated. No latency term can make it legitimate, in either direction.

And that is checkable at every cycle from two registers, which is why §16's arrow-8 identity matters more than its position in the chain suggests: it is the one instrument that fires in phase 2 rather than phase 4.

The mechanisms are 21.3 §18's five, and identity distinguishes them: a duplicate carrying the same object_id is a message counted twice; a duplicate carrying the next object_id is a generator firing on a level rather than an edge.

26. Identity in Silicon

Storing every object's history is not feasible. Four compressions, with honest limitations.

Three notes.

The first row is the one to build. 14.5 §8's sticky-first argument: the first duplicate is the informative one, and later ones are frequently consequences of the same mechanism.

The XOR signature is genuinely useful and must be described honestly. At quiescence, XOR of every allocated ID against every released ID should be zero; a nonzero residue proves an imbalance and names nothing. And two independent errors can XOR to zero — so a zero residue is weaker evidence than it looks, and this must be stated wherever the signature is reported.

And a bounded ring plus a wrapped flag (21.1 §12) is the right shape for the recent-history case — with the flag, because a wrapped ring whose earliest record is not the first event reads as a complete history that starts mysteriously late.

27. First-Duplicate Capture

// ILLUSTRATIVE. Sticky-first, per domain. One register set, and it converts
// §25's unactionable count into a named object.
logic                  dup_valid_q      [NUM_DOMAINS];
logic [OBJ_W-1:0]      dup_object_q     [NUM_DOMAINS];
logic [EPOCH_W-1:0]    dup_epoch_q      [NUM_DOMAINS];
logic [EVENT_W-1:0]    dup_event_kind_q [NUM_DOMAINS];
logic [TIME_W-1:0]     dup_time_q       [NUM_DOMAINS];
logic [15:0]           dup_count_q      [NUM_DOMAINS];   // how many since
 
always_ff @(posedge clk or negedge por_n) begin
  for (int d = 0; d < NUM_DOMAINS; d++) begin
    if (!por_n) begin
      dup_valid_q[d] <= 1'b0;
      dup_count_q[d] <= '0;
    end else if (diag_clear_fire) begin
      dup_valid_q[d] <= 1'b0;
      dup_count_q[d] <= '0;
    end else if (dup_detected && (dup_domain == DOMAIN_W'(d))) begin
      if (!dup_valid_q[d]) begin            // STICKY FIRST (14.5 §8)
        dup_valid_q[d]      <= 1'b1;
        dup_object_q[d]     <= dup_object;
        dup_epoch_q[d]      <= dup_epoch;
        dup_event_kind_q[d] <= dup_kind;
        dup_time_q[d]       <= time_q;
      end
      if (dup_count_q[d] != '1) dup_count_q[d] <= dup_count_q[d] + 16'd1;
    end
  end
end

Architecture. Sticky-first identity plus a running count, per domain. The pair distinguishes one duplicate from a systematic one.

State. Six small registers per domain.

Event behaviour. Captured once; the count keeps rising, which is deliberate — one duplicate is a glitch, a thousand is a structural defect, and the count distinguishes them.

Contract. Cleared only by an explicit diagnostic clear (14.5 §25) — never by a recovery, or the first duplicate before a recovery is lost.

Failure. Last-wins capture reports whichever duplicate happened most recently, which after a cascade is a consequence (14.5 §9).

Debug/DV. dup_count = 1 with a named object is a specific event to reproduce; dup_count = 4,000 with the same event kind is a mechanism, and the event kind names which ledger arrow (§7).

28. Missing Events Cannot Be Captured Directly

A duplicate is an event and can be detected. A missing event is an absence — and absences are detected by ageing.

An object that crossed boundary N and has not crossed boundary N+1 within the boundary's bound has a missing event.

That is the only way to find it, and it requires per-object outstanding state at each boundary, or — the practical compression — the age of the oldest object waiting at each boundary (§29).

29. Boundary Age

// ILLUSTRATIVE. The age of the OLDEST object waiting at each boundary, per
// domain. Different ages identify different blocked boundaries.
logic [AGE_W-1:0] age_consume_to_alloc_q  [NUM_DOMAINS];
logic [AGE_W-1:0] age_release_to_gen_q    [NUM_DOMAINS];
logic [AGE_W-1:0] age_gen_to_tx_q         [NUM_DOMAINS];
logic [AGE_W-1:0] age_tx_to_rx_q          [NUM_DOMAINS];
 
// One boundary shown; the others follow the same shape.
always_ff @(posedge clk or negedge por_n) begin
  for (int d = 0; d < NUM_DOMAINS; d++) begin
    if (!por_n)                                   age_gen_to_tx_q[d] <= '0;
    // Reset ONLY when the queue at this boundary drains to empty — not on any
    // service, which is 21.3 §30's failure.
    else if (pending_gen_to_tx_q[d] == '0)        age_gen_to_tx_q[d] <= '0;
    else if (age_gen_to_tx_q[d] != '1)            age_gen_to_tx_q[d] <= age_gen_to_tx_q[d] + AGE_W'(1);
    // else: SATURATE (21.1 §21)
  end
end

Architecture. One saturating age per boundary per domain. Four boundaries have a meaningful queue and therefore a meaningful age.

State. 4 × NUM_DOMAINS age counters.

Event behaviour. Reset on the boundary's queue reaching empty; incrementing otherwise; saturating rather than wrapping.

Contract. "Empty", not "serviced". 21.3 §30: a boundary serviced continuously but never drained has a genuinely old oldest item, and resetting on service hides it — more effectively the busier the boundary is.

Failure. A wrapping age reports a fresh boundary during an ancient stall (21.1 §21), and then nothing fires. A service-reset age hides starvation entirely.

Debug/DV. The saturated age names the boundary, and it is the only instrument that finds a missing event (§28). A saturated age_release_to_gen says releases are happening and generations are not — which is arrow 5, before any counter difference has grown large enough to notice.

30. The Oldest-Obligation Tracker

// ILLUSTRATIVE, VERIFICATION-SIDE. Which object is the oldest at each boundary
// — the identity behind §29's age. Simulation can afford this; silicon uses
// the age alone (§26).
typedef struct {
  int unsigned object_id;
  int unsigned domain;
  int unsigned epoch;
  longint      entered_cycle;
} pending_obj_t;
 
pending_obj_t pending_at[boundary_e][int unsigned];   // per boundary, keyed by object
 
function automatic void on_boundary_event(credit_event_t e);
  boundary_e produced = boundary_of_producer(e.event_kind);
  boundary_e consumed = boundary_of_consumer(e.event_kind);
  if (produced != BND_NONE)
    pending_at[produced][e.object_id] = '{ e.object_id, e.domain, e.epoch, $time };
  if (consumed != BND_NONE)
    if (pending_at[consumed].exists(e.object_id))
      pending_at[consumed].delete(e.object_id);
    else
      report_error(ERR_CONSUMER_WITHOUT_PRODUCER, e.object_id,
                   "boundary event with no matching upstream event");
endfunction

Architecture. Per-boundary sets of objects that have crossed the producer side and not the consumer side. The set's oldest member is what §29's age measures.

State. One associative array per boundary; its size is bounded by the design's outstanding capacity, and a set larger than that is itself a finding (20.4 §36's live-set-explosion check).

Event behaviour. Insert on the producer event, delete on the consumer event.

Contract. Every consumer event must find a matching producer entry. The else branch is not defensive padding — a consumer event with no producer is §4's "invented transfer", detected directly rather than inferred from a count.

Failure. Silently ignoring an unmatched consumer event (20.4 §41's silent-drop failure) loses the invented-transfer detection entirely.

Debug/DV. The oldest entry at the first-divergent boundary is the object to trace, and its entered_cycle is where to start looking.

31. Events Are Not Amounts

One boundary event may carry several capacity units, and the two quantities detect different bugs.

Both are needed, and the reason is a worked case:

Case A. One object consumes 4 units. One return applies 4 units. Events: 1 and 1. Amounts: 4 and 4. Both close.

Case B. One object consumes 4 units. One return applies 1 unit. Events: 1 and 1 — closes. Amounts: 4 and 1 — broken. The event chain sees nothing.

Case C. One object consumes 4 units. Two returns apply 2 units each. Events: 1 and 2 — broken. Amounts: 4 and 4 — closes. The amount chain sees nothing.

So the two chains are complementary and neither subsumes the other.

32. Wrong — One Event Means One Credit

// WRONG — the chain counts events and reports them as credits.
assign credits_outstanding = cnt_consume_q - cnt_return_apply_q;   // EVENTS

Worked, with multi-unit objects. Ten objects consumed, each 4 units: 40 units of capacity are committed. The chain reports 10.

Three properties.

The number is off by the average object size, which varies with traffic — so the error is not a constant offset and cannot be calibrated away.

It reports a healthy link as leaking, or a leaking link as healthy, depending on which side of the chain the multi-unit events are on. Case B of §31 is invisible; a duplicate carrying one unit looks like four units lost.

And the fix is to carry amount in the event record (§8) and maintain both sums (§12) — which is two extra counters per domain and removes an entire class of misreading.

33. Amount Conservation

// MANDATORY where amounts can exceed one. The amount identity, per domain,
// alongside the event identity — both are needed (§31).
generate
  for (genvar d = 0; d < NUM_DOMAINS; d++) begin : g_amt
    // Units consumed and units restored must balance, reconciled by the same
    // in-flight and rejection terms as the event chain.
    a_amount_conserved: assert property (
      @(posedge clk) disable iff (!por_n)
        (amt_consume_q[d] - amt_return_apply_q[d]) <= 64'(active_capacity_q[d])
    );
    // And the sender's credit is a UNIT quantity, so it reconciles against
    // amounts, never against event counts (§32).
    a_credit_matches_amounts: assert property (
      @(posedge clk) disable iff (!por_n)
        (credit_q[d] == (advertised_q[d] + amt_return_apply_q[d] - amt_consume_q[d]))
    );
  end
endgenerate

Architecture. Two properties per domain: a bound on committed units, and the credit identity expressed in units.

State. The two amount sums of §12.

Event behaviour. Evaluated every cycle; a_credit_matches_amounts is the identity that ties the whole chain to the register the sender actually uses.

Contract. advertised_q is epoch-scoped (§21), so this identity restarts at each epoch boundary — and asserting it across a boundary without the baseline is §22's error.

Failure. Expressing the credit identity in event counts is §32. Omitting the amount chain entirely makes §31's Case B undetectable.

Debug/DV. When the event chain closes and the amount chain does not, the bug is in the quantity carried by some event — a truncated amount field, a wrong unit conversion, a partial return — which is a much narrower search than "somewhere in the credit path".

34. Wrong Amount Width

// WRONG — a 32-bit amount sum in a design that runs for hours.
logic [31:0] amt_consume_q, amt_return_apply_q;

Worked. At a few units per object and a high rate, a 32-bit sum wraps in a long soak. Both sums wrap at roughly the same time.

The difference returns to a small value. The chain reports a perfect balance.

Three properties.

It destroys the evidence for the exact bug the soak was run to find — 21.3 §45's slow leak, which needs hours to accumulate and a chain that survives them.

Both sums wrapping at similar times is what makes it insidious. If only one wrapped, the difference would be enormous and obviously wrong; wrapping together restores a plausible small difference.

And the policy is 21.3 §46's: event and amount totals are 64-bit and wide, ages saturate, and differences are computed signed. A 64-bit unit sum does not wrap in any realistic run.

35. Replay Classification — the Danger Zone

36. Wrong Classification

Worked. The design classifies every transmission as ALLOC_NEW, including retransmissions. The debug chain records ALLOC_NEW too, because it takes the classification from the design.

Every check passes. The design may still be wrong — if the architecture retains the allocation, four credits leak per five-attempt object.

Three properties.

This is 21.3 §10's shadow failure at the classification level. The instrumentation inherited the design's interpretation of what kind of event this is, so it cannot disagree about it.

The independent classification comes from the object lifecycle, not from the design's flag. 20.4 §18's transport model records attempt_cycles per object — so attempt 2 of object X is a retransmission by observation, regardless of what the design labelled it.

And the discriminating counter is cnt_attempt_retransmit, derived from the model's attempt count rather than from the design's class field. Comparing it against cnt_consume_retransmit exposes a misclassification that the design and a naive chain agree about.

37. The Release Boundary

Ledger arrow 5 is exact (§9) only if both sides mean the same thing by "release". They frequently do not.

And the failure is not that one is wrong — it is that different consumers of the release event use different ones (§39).

38. One Semantic Definition

Define the storage-reusable event once. Every consumer — the occupancy decrement, the free-list update, the credit return generation — derives from it, or is explicitly reconciled against it.

// ILLUSTRATIVE. One event, three consumers, no independent derivations.
assign entry_reusable_fire = entry_pop_fire && read_complete[pop_idx];
 
// All three derive from the SAME expression.
assign occupancy_dec      = entry_reusable_fire;
assign freelist_release   = entry_reusable_fire;
assign return_gen_fire    = entry_reusable_fire && !entry_returned_q[pop_idx];

Architecture. One expression, three consumers, so the three cannot disagree.

State. The per-entry entry_returned_q guard (19.5 §25) — the only additional state, and it is what makes the return-once property checkable.

Event behaviour. One cycle, three effects. return_gen_fire carries the extra guard because a duplicated release must not duplicate the return (21.3 §19).

Contract. "Reusable" must mean the same thing to the allocator as to these three. If allocation can hand out an entry a downstream stage is still reading, the release was right and the allocator is the bug — and the two are easy to get out of step when a pipeline stage is added later (19.5 §21).

Failure. §39.

Debug/DV. The single expression makes the three counters structurally equal. Three independent derivations make them three separate opportunities to diverge, and a chain that finds occupancy_dec != return_gen has found a definition mismatch rather than a lost message.

39. Wrong — the Split Release

// WRONG — three derivations, three definitions.
assign occupancy_dec    = entry_pop_fire;                        // at pop
assign freelist_release = entry_pop_fire_d1;                     // one cycle later
assign return_gen_fire  = entry_pop_fire;                        // at pop

Worked, over two cycles.

For one cycle, the far end has been told an entry is available while the free-list still owns it.

Five properties.

Under light load nothing happens. The advertised credit takes a round trip to be used, and by then the free-list has caught up. The bug is invisible.

Under heavy load with a short round trip, the replacement object arrives while the free-list still owns the entry — and depending on the allocator, it is dropped, blocked, or written over an entry the design believes is allocated.

It is a one-cycle window, so it is intermittent and load-correlated — the hardest class to reproduce.

The chain sees occupancy_dec == return_gen — both fire at pop, so arrow 5 closes. The mismatch is between those two and the free-list, which is why the free-list release must be a fourth counter if this failure class is in scope.

And the correct fix is §38's single expression, not a delay adjustment: equalising the pipeline works until somebody changes it, while one shared expression makes the divergence unrepresentable.

40. SVA — a Return Implies Reusable Storage

// MANDATORY. ILLUSTRATIVE ARCHITECTURAL CONTRACT (§3).
property p_return_implies_reusable;
  @(posedge clk) disable iff (!por_n)
    return_gen_fire |-> (entry_reusable_fire && !entry_valid_q[pop_idx]);
endproperty
a_return_implies_reusable: assert property (p_return_implies_reusable);
 
// MANDATORY. The three derivations agree — this is §39's direct check.
property p_release_derivations_agree;
  @(posedge clk) disable iff (!por_n)
    (occupancy_dec == freelist_release) && (occupancy_dec == entry_reusable_fire);
endproperty
a_release_derivations_agree: assert property (p_release_derivations_agree);
 
// MANDATORY. The EFFECT form — an entry whose credit was returned is not read
// again before reallocation. Written against a DIFFERENT observable than the
// return condition, so a shared misconception cannot satisfy it (19.5 §23).
property p_no_read_after_return(int idx);
  @(posedge clk) disable iff (!por_n)
    (return_gen_fire && (pop_idx == idx))
      |=> !(entry_read_fire && (read_idx == idx))
          until (entry_alloc_fire && (alloc_idx == idx));
endproperty

Architecture. A cause check, a derivation-agreement check, and an effect check.

State. None beyond the design's own.

Event behaviour. All three evaluated per cycle.

Contract. The second property is the one specific to this chapter: it asserts that the three consumers of the release event agree, which is §38's whole design turned into a property.

Failure. With only the first property, a design where all three derivations are wrong in the same way passes — because the cause check is written against the same signal the designer used. The third property is written against a different observable and cannot be satisfied that way (20.3 §27).

Debug/DV. p_release_derivations_agree fires at the cycle of §39's split — one cycle, deterministic, before any load-dependent corruption.

41. Snapshot Atomicity

Reading eight 64-bit counters via software is not a snapshot. The counters keep moving between reads.

Worked. Software reads consume at t, then return_apply at t + 200 cycles. In those 200 cycles, 30 more consumes and 30 more returns occurred.

The reported difference is skewed by whatever happened in the gap — and the skew is systematic, because the reads happen in a fixed order.

Three properties.

The skew has a sign. Reading upstream counters before downstream ones inflates every difference by the traffic in the gap, so every boundary looks like it is leaking.

It scales with load and with read latency, so a busy link and a slow debug interface produce a large fictitious leak — exactly when the engineer is most inclined to believe it.

And it is indistinguishable from a real leak in a single sample. The discriminating observation is to read the same counters again in the reverse order: a real leak is unchanged, a skew artefact changes sign.

42. The Snapshot Register Bank

// ILLUSTRATIVE. A trigger copies every live counter into a frozen bank in one
// cycle, so software reads a consistent instant (§41).
fc_snapshot_t snap_q [NUM_DOMAINS];
logic         snap_valid_q;
logic [15:0]  snap_seq_q;          // increments per capture — §43's guard
 
always_ff @(posedge clk or negedge por_n) begin
  if (!por_n) begin
    snap_valid_q <= 1'b0;
    snap_seq_q   <= '0;
  end else if (snap_trigger) begin        // §20's four triggers
    for (int d = 0; d < NUM_DOMAINS; d++) begin
      snap_q[d].domain          <= DOMAIN_W'(d);
      snap_q[d].epoch           <= credit_epoch_q[d];
      snap_q[d].sem_accept      <= cnt_sem_accept_q[d];
      snap_q[d].adapter_accept  <= cnt_adapter_accept_q[d];
      snap_q[d].consume         <= cnt_consume_q[d];
      snap_q[d].remote_alloc    <= cnt_remote_alloc_q[d];
      snap_q[d].remote_release  <= cnt_remote_release_q[d];
      snap_q[d].return_gen      <= cnt_return_gen_q[d];
      snap_q[d].return_tx       <= cnt_return_tx_q[d];
      snap_q[d].return_rx       <= cnt_return_rx_q[d];
      snap_q[d].return_apply    <= cnt_return_apply_q[d];
      snap_q[d].reject_total    <= cnt_reject_total_q[d];
      snap_q[d].amt_consume     <= amt_consume_q[d];
      snap_q[d].amt_return_apply<= amt_return_apply_q[d];
      snap_q[d].occupancy_now   <= occupancy_q[d];
      snap_q[d].credit_now      <= credit_q[d];
      snap_q[d].first_dup_object<= dup_object_q[d];
    end
    snap_valid_q <= 1'b1;
    snap_seq_q   <= snap_seq_q + 16'd1;
  end
end

Architecture. A frozen parallel copy, written in one cycle by a trigger.

State. One fc_snapshot_t per domain plus a validity bit and a sequence number.

Event behaviour. One capture per trigger. Every field is written in the same cycle, which is the entire point.

Contract. Software must read snap_seq before and after reading the bank, and discard the read if it changed — which is why the sequence number is not optional (§43). And the trigger must not re-fire during a read, or the bank changes underneath it.

Failure. Without the bank, §41's skew. Without the sequence number, a bank re-captured mid-read produces a torn snapshot that looks atomic — the same failure one layer up.

Debug/DV. The bank is what makes §19's function trustworthy: a first-divergence answer computed from a torn snapshot is an artefact (§51).

43. Wrong — Sequential Live Reads

WRONG software debug procedure:
 
  read cnt_consume        -> 10,000
  ... 200 cycles of bus latency ...
  read cnt_remote_alloc   ->  9,970
  ... 200 cycles ...
  read cnt_remote_release ->  9,100
  ... 200 cycles ...
  read cnt_return_apply   ->  9,050
 
  CONCLUSION: "30 objects lost in transport, and 50 returns lost."

What actually happened. The link was running at roughly one object per seven cycles. In each 200-cycle gap, about 30 events occurred at every stage. Both "losses" are the read gap.

Four properties.

Every difference is inflated by the same mechanism, so the pattern looks like a systematic multi-boundary leak — which is a plausible and alarming reading.

The magnitudes are proportional to the read latency, so a slower debug interface produces a bigger apparent leak. A team that switches to a faster interface sees the "leak" shrink and concludes their fix worked.

The discriminating observations are two, and both are cheap: read in reverse order (a real leak is unchanged; the artefact changes sign), or read at quiescence (no traffic, no skew).

And the structural fix is §42's bank — one trigger, one cycle, one consistent instant, plus the sequence number so a re-capture during the read is detected rather than silently absorbed.

44. Transport Drop Versus Stale Rejection

Arrows 7 and 8 both produce a downstream shortfall and they are completely different bugs.

Three properties.

Row 3 is not a bug — the guard did its job (19.5 §30). But it raises a second question: why were they stale?

Without rejection counters, rows 2 and 3 are indistinguishable, and the natural reading is "lost" — so a correctly working epoch guard is reported as a transport defect.

And rows 1 and 2 need different teams. One is the link's return path; the other is the credit block's acceptance logic.

45. The Rejection Taxonomy

// ILLUSTRATIVE. GENERIC engineering categories — these are NOT UCIe-defined
// codes (§3). Each reason implies a different next question.
typedef enum logic [RSN_W-1:0] {
  REJ_NONE          = 'd0,
  REJ_STALE_EPOCH   = 'd1,  // belongs to a dead agreement (19.5 §30)
  REJ_DUPLICATE     = 'd2,  // this unit was already returned
  REJ_INVALID_DOMAIN= 'd3,  // names a domain that does not exist here
  REJ_UNEXPECTED_ST = 'd4,  // arrived while not in an accepting state
  REJ_MALFORMED     = 'd5   // failed a structural check
} reject_reason_e;

Five reasons, five different next questions.

And REJ_INVALID_DOMAIN is the row worth noticing. It catches §15's cancellation at the boundary rather than by comparing per-domain totals — because a return naming a domain that does not exist here is a misattribution proved at the moment it arrives.

46. Rejection Counters

// ILLUSTRATIVE. Per reason, per domain. These reconcile arrow 8 (§9 row 8).
logic [63:0] cnt_reject_q [NUM_DOMAINS][NUM_REJECT_REASONS];
logic [63:0] cnt_reject_total_q [NUM_DOMAINS];
 
always_ff @(posedge clk or negedge por_n) begin
  for (int d = 0; d < NUM_DOMAINS; d++) begin
    if (!por_n) begin
      cnt_reject_total_q[d] <= '0;
      for (int r = 0; r < NUM_REJECT_REASONS; r++) cnt_reject_q[d][r] <= '0;
    end else if (return_reject_fire && (reject_domain == DOMAIN_W'(d))) begin
      cnt_reject_q[d][reject_reason] <= cnt_reject_q[d][reject_reason] + 64'd1;
      cnt_reject_total_q[d]          <= cnt_reject_total_q[d] + 64'd1;
    end
  end
end

Architecture. One counter per reason per domain, plus a total that reconciles arrow 8.

State. NUM_REASONS × NUM_DOMAINS counters. Modest, and it converts an ambiguous gap into a named cause.

Event behaviour. Incremented at the rejection, which is the same cycle the return would otherwise have been applied.

Contract. cnt_reject_total must be exactly the sum of the per-reason counters, and arrow 8's identity is return_rx == return_apply + reject_total (§16). A rejection that is not counted breaks that identity and reads as a loss.

Failure. Silently dropping a rejected return — the most common omission — makes §44's rows 2 and 3 indistinguishable, so a working guard is reported as a transport defect.

Debug/DV. The distribution is the diagnosis: all REJ_STALE_EPOCH immediately after a recovery is expected; the same count during steady operation means the epoch is advancing when nothing should advance it (19.5 §31's monotonicity property, in counter form).

47. Trace 1 — False Consume, Localised to Arrow 2

Illustrative. 21.3 §14's leak, now attributed to a boundary.

Five readings.

d2 is negative, and arrow 2 is exact (§9), so this is a bug with no interpretation required — no quiescence needed, no latency model, no in-flight term.

Every other arrow closes, which eliminates the transport, the receiver, the return generator, the return path and the applier — five subsystems, from one reading.

remote_alloc matching adapter_accept rather than consume is the confirming detail: the far end allocated 5,000 entries, so 240 consumes correspond to no allocation anywhere.

The ratio consume / adapter_accept is 1.048, which is not a stable integer — so this is 21.3 §17's load-varying signature: a consume firing on a stalled cycle, not a structural double-charge.

And the fix and its check are both known: qualify the consume on a completed handshake (19.5 §17), and a_accept_equals_consume (§16) prevents recurrence at the cycle of the cause.

48. Trace 2 — Release With No Return Generated

Illustrative. Arrow 5, which is also exact.

Four readings.

Arrow 5 is exact, so 19 releases produced no return — no latency term, no ambiguity.

The receiver is fully drained (d4 = 0), which rules out the entry still being held: the storage genuinely became reusable and the return was not generated.

age_release_to_gen saturating is the independent confirmation (§29), and it would have fired long before the difference grew to 19 — which is why the ages are worth building alongside the counters.

And §38 is the likely mechanism: three derivations of "release", with the return generator using a different one — or the per-entry entry_returned_q guard clearing at the wrong time, so a legitimate release found the guard already set.

49. Trace 3 — Generated, Transmitted, Stale-Rejected

Illustrative. Arrow 8, and the finding is not a loss.

Five readings, and the first inverts the usual conclusion.

No credits were lost. The identity closes once rejections are included — so arrow 8 is not broken at all, and a chain without rejection counters would have reported 60 lost returns.

The real question is why 60 were stale. 19.5 §30's guard rejected them correctly; the finding is about epoch lifetime, not about credits.

The discriminating detail is when they occurred. Sixty stale rejections immediately after a recovery are stragglers — expected. Sixty spread through steady operation mean the epoch is advancing when nothing should advance it, which points at a reset scope touching the epoch register (19.6 §27).

And the credits those 60 returns represented are genuinely gone from this epoch — correctly, because they belonged to an agreement that no longer exists. They were re-established by the new advertisement, which is why the sender is not short.

The lesson is that a closed identity with a nonzero rejection count is a different investigation — one about epochs and recovery, in a different chapter's territory (14.2) — and misreading it as a leak sends the work to the wrong place entirely.

50. Trace 4 — Per-Class Cancellation

Illustrative. §15, as a counter reading.

Five readings.

The total closes exactly at every arrow, including arrow 8. A total-only chain reports a perfectly healthy credit system.

Per domain, arrow 8 breaks in both directions — A is short, B is long. One mechanism, two symptoms.

REJ_INVALID_DOMAIN is zero, which is itself informative: the returns were not rejected as belonging to the wrong domain — they were applied to the wrong domain. The applier's domain index was wrong, not its validity check.

Domain A will stall and domain B will overflow, and the two will be reported as separate bugs by separate people.

And the root cause is a single mis-indexing, most likely the applier taking the domain from a shared register rather than from the return message (19.5 §47) — which is one line, found only because the counters were per domain.

51. Trace 5 — the Torn Snapshot

Illustrative. §41's artefact, and the trace that teaches the debug system can be wrong.

Reading A — sequential live reads, upstream first:

Conclusion drawn: 60 lost in transport, 60 returns lost.

Reading B — the same counters, read in reverse order:

Reading C — from the frozen snapshot bank (§42):

Every arrow closes. There is no leak.

Four readings.

Reading A is the one that gets reported, because it is the natural order and it produces an alarming, plausible number.

Reading B is the two-minute experiment that falsifies it. 21.1 §51's question 40 — what observation would prove this hypothesis wrong? — and here the answer is simply to read in the other order.

Reading C's 840 is the occupancy, not a loss (§9 row 4) — which a chain that checks arrow 4 as an equality would also have flagged.

And the durable lesson is that the debug apparatus is part of the system under investigation. A torn snapshot, a wrapped counter (§34), a shadow sharing the design's signal (21.3 §10), and an age that resets on service (21.3 §30) are all instruments that lie — and every conclusion drawn from an instrument is downstream of that instrument's correctness.

52. Using the Scoreboard to Localise

20.4 owns the independent model. This chapter uses where the model and the design first disagree as the boundary answer.

Two notes.

Do not rebuild the scoreboard here. 20.4 §17's independence rule and §18's transport model already exist; this chapter adds the reading — that a divergence at a known boundary is a localisation, not merely a failure.

And the scoreboard's advantage over the counters is identity. The counters say arrow 5 is short by 19; the scoreboard says which 19 objects, which is §24's point arriving from the verification side.

The mechanism is a cross-layer correlator — one object's full journey assembled from events observed at six different places:

// ILLUSTRATIVE, VERIFICATION-ONLY. One row per object, filled in by monitors at
// six different boundaries. The row is COMPLETE when every stage has a
// timestamp; an INCOMPLETE row at retirement names the boundary that failed.
typedef struct {
  int unsigned  object_id;
  int unsigned  domain;
  int unsigned  epoch;
  int unsigned  amount;
  alloc_class_e alloc_class;
  // one timestamp per ledger arrow; -1 means "never observed"
  longint       t [boundary_event_e];
} object_journey_t;
 
object_journey_t journey [int unsigned];      // keyed by local debug object id
 
// Each monitor calls this from ITS OWN layer. The monitors do not share state
// and do not talk to each other — the correlator is the only join (20.4 §17).
function automatic void record(int unsigned obj, boundary_event_e ev, longint now);
  if (!journey.exists(obj)) begin
    // The FIRST event for an object must be SEM_ACCEPT. Anything else means an
    // event was missed upstream, or an object appeared from nowhere (§4 row 2).
    if (ev != EV_SEM_ACCEPT)
      report_error(ERR_JOURNEY_STARTS_MIDSTREAM, obj, ev.name());
    journey[obj] = '{ object_id: obj, domain: 0, epoch: 0, amount: 0,
                      alloc_class: ALLOC_NEW, t: '{default: -1} };
  end
  if (journey[obj].t[ev] != -1)
    report_error(ERR_DUPLICATE_STAGE, obj,
                 $sformatf("%s recorded twice: %0d then %0d",
                           ev.name(), journey[obj].t[ev], now));
  journey[obj].t[ev] = now;
endfunction
 
// At retirement, the FIRST stage with no timestamp names the boundary.
function automatic boundary_event_e first_missing_stage(int unsigned obj);
  object_journey_t j = journey[obj];
  for (boundary_event_e e = EV_SEM_ACCEPT; e <= EV_RETURN_APPLY; e = e.next())
    if (j.t[e] == -1) return e;
  return EV_RETURN_APPLY;              // complete
endfunction

Architecture. One row per object, written by six independent monitors, joined only by the object identity. The row is the ledger, per object rather than per counter.

State. One row per live object; retired on completion or on epoch close, and a set that grows without bound is 20.4 §36's live-set-explosion finding.

Event behaviour. Each monitor records its own boundary's timestamp. No monitor reads another's state, which is what keeps the six observations independent.

Contract. The first event for an object must be SEM_ACCEPT. A journey that starts midstream means either a monitor missed an event or an object materialised inside the stack — and the two are distinguished by which stage is missing, not by the count.

Failure. Correlating on a reused identity merges two objects' journeys into one row, producing a spurious duplicate-stage error on every reuse (20.4 §21). Correlating on the design's own tag rather than a monitor-assigned one inherits any tagging bug.

Debug/DV. Three answers the counters cannot give. Which objects failed (§25's gap). The per-boundary latency distribution, because each row carries six timestamps — so a boundary that is slow rather than broken is visible. And first_missing_stage per object, which is §18's algorithm applied to a single object rather than to aggregates: when nineteen objects all report the same first missing stage, that is the boundary, proved nineteen times over.

53. Representative Properties

20.3 owns assertion methodology. This chapter's contribution is a small, boundary-indexed set — one or two properties per ledger arrow, rather than a general catalogue.

The three exact equalities are the highest-value rows — arrows 2, 5 and 8 — because they need no latency model, fire at the cycle of the cause, and are readable as registers in silicon (§55).

54. Was the Boundary Case Exercised?

20.5 owns the coverage model. The question this chapter adds is narrower: was the boundary condition in the failing trace ever deliberately produced?

And the reading is 20.5 §11's: an uncovered boundary condition means the chain's behaviour there is unknown, not that it works. A conservation identity that has never seen a simultaneous consume-and-return has not been tested against the case most likely to break it.

55. What Silicon Actually Needs

The chain is large in simulation and must be small in silicon. The compact set, in priority order:

Three notes.

Rank 2 is not optional and is frequently omitted. Ranks 1, 3 and 4 are all read by software, and without the frozen bank every one of them is subject to §43's skew — so the most expensive instrumentation in the list is worthless without the cheapest.

Not on the list: per-object history. The event ring and the associative sets of §24 and §30 are simulation instruments; silicon gets the aggregate counters plus rank 6's single named object.

And the whole set is passive. Nothing here changes a design decision, gates a transfer, or is in a timing path — 14.5 §5's rule, and it is what makes the instrumentation safe to leave enabled.

56. Debug Checklist

Thirty-six questions, in the order they should be asked.

Scope the reading first (1–7).

1. Which ownership domain? Are the counters per domain at every boundary, or totals somewhere?
2. Which epoch? Does the reading span an epoch boundary (§21)?
3. Is the snapshot atomic, or assembled from sequential live reads (§41)?
4. Did the sequence number change during the read (§42)?
5. Is the link quiescent, or must in-flight terms be applied (§10)?
6. Did any diagnostic counter wrap (§34)?
7. Are these event counts or capacity units (§31)?

Walk the ledger in order (8–19). 8. sem_accept versus adapter_accept — is the difference within the inter-layer queue? 9. adapter_accept versus consume — exact; is it zero? (§47) 10. Did a consume occur without an adapter acceptance, or the reverse? 11. consume versus remote_alloc — within the in-flight bound? 12. Did remote allocation occur for every consumed object? 13. remote_alloc versus remote_release — is this the occupancy, or an impossible value? (§9 row 4) 14. Did physical occupancy change, or only a counter? 15. Was storage actually reusable at release, or only logically freed (§37)? 16. remote_release versus return_gen — exact; is it zero? (§48) 17. return_gen versus return_tx — is the difference the pending count, and is it moving (§9 row 6)? 18. return_tx versus return_rx — within the in-flight bound (§44)? 19. return_rx versus return_apply — does it equal the rejection total? (§46)

Interpret a rejection (20–24). 20. Were any returns rejected, and how many? 21. Why — stale epoch, duplicate, invalid domain, unexpected state, malformed (§45)? 22. If stale: when — after a recovery, or during steady operation (§49)? 23. If invalid domain: is this §50's misattribution caught at the boundary? 24. Does the arrow-8 identity close once rejections are included?

Amounts and classification (25–29). 25. Do the amount sums close where the event counts do (§31)? 26. Can an event carry more than one unit, and does the chain record it (§8)? 27. Is the sender's credit reconciled against amounts, not event counts (§33)? 28. How is a retransmission classified, and is the classification independent of the design's own flag (§36)? 29. Is cnt_consume_retransmit / cnt_attempt_retransmit 0, 1, or something inconsistent (§35)?

Identity and ageing (30–33). 30. Which object first duplicated (§27), and how many since? 31. Which obligation is oldest, and at which boundary (§30)? 32. Which boundary age is saturated (§29)? 33. Does the age reset on empty or on service (§29)?

Interrogate the instrumentation (34–36). 34. Is any counter reading a design-internal signal rather than the boundary event (21.3 §10)? 35. Does reading in the reverse order change the sign of the differences (§43)? 36. Can a directed fault reproduce the named boundary mismatch — and does the assertion of §53 fire on it?

57. Common Misconceptions

"If total credits balance, accounting is correct." §15 and §50: a misattribution conserves the total exactly and breaks both domains.

"Each layer can be debugged independently." §17: every layer-local check can pass while the boundary between two of them loses messages.

"Cumulative counters should always be equal." §10: three arrows are exact and five have legitimate transient differences, one of which is the receiver's occupancy.

"One credit event always means one unit." §32: with multi-unit objects the event chain is off by the average object size, which varies with traffic.

"Recovery does not affect counter interpretation." §22: a lifetime total across an epoch boundary needs the baseline and reconciliation terms, or every recovery reads as a small leak.

"If a return was received, it must be applied." §44: it may have been correctly rejected — and without rejection counters that is indistinguishable from a loss.

"Rejected credit returns are lost returns." §49: the identity closes once rejections are counted. The finding is about epoch lifetime, not credits.

"A duplicate count tells you which object duplicated." §25: it tells you one exists among a thousand. Identity tells you which.

"Live counter reads form an atomic snapshot." §43: they are skewed by the read latency, systematically, in one direction.

"The sender's credit register is the best place to start." §18: it is the last arrow. Start at the first one that diverges, which is usually five arrows upstream.

"A replay is obviously a new allocation." §35: whether a retransmission consumes new capacity is a specification question, and assuming it fails in one of two opposite directions.

"Occupancy decrement means storage is reusable." §39: three derivations of "release" can disagree by a cycle, and one cycle is enough to overwrite an entry under load.

"A shadow counter driven by the design's consume signal is independent." §36 and 21.3 §10: it inherits the design's definition, including the bug.

"One global counter is enough for all classes." §14: it cannot be decomposed, so even a detected mismatch has no starting point.

"The latest mismatch is the root cause." §18: read in order — a later mismatch is usually a consequence of an earlier one.

58. Understanding Check

59. Summary

The ledger, and where each arrow's bug lives.

Six things that carry beyond UCIe.

A layer boundary is where a system bug hides, because both sides can be internally correct (§17) — and no per-layer verification plan, however complete, covers the arrows between the layers.

Latency makes a naive comparison wrong, and the same naive comparison at the buffer boundary reports the fill level as a leak (§11).

Totals cancel, exactly and increasingly with runtime, so every counter is per domain or the chain has a blind spot by construction (§15).

Events and amounts are different quantities and detect different bugs, neither subsuming the other (§31).

A missing event is found by ageing, never by capture (§28) — which is why the four boundary ages are worth their small cost.

And the debug apparatus is itself under test. A torn snapshot manufactures a leak (§51), a wrapped counter erases one (§34), and a shadow sharing the design's signal agrees with the bug (§36). Every conclusion is downstream of an instrument, and the instrument gets checked first.