Flow-Control Bugs

Chapters 21.1 and 21.2 got the link operational. This failure class is different in kind: everything works initially, then progress slows or stops — not because a measurement failed, but because the two endpoints have come to disagree about how much room the other has.

1. The One-Sentence Model

A flow-control failure is a disagreement between ownership accounting and physical storage reality. The sender's credit is a replica of a fact that lives at the receiver, and every bug below is that replica diverging from the fact it describes.

Three disagreements, three signatures (§5). And the reason a single counter read never resolves it: the sender's credit reading zero is consistent with a genuinely full receiver, a leak, a stranded return and a downstream blockage — four conditions with four different owners.

2. What This Chapter Owns

19.5 built the credit machine and taught its bugs as design lessons. This chapter diagnoses them from evidence — and the difference is concrete:

19.5 §18 taught that consuming on valid leaks credit. §14 teaches the signature — sender credit trending down while receiver occupancy returns to baseline — and the counter comparison that proves it in one read.

19.5 §42 taught the batching deadlock as a liveness bug. §27 teaches how to recognise it from three stable registers and distinguish it from a genuinely full receiver.

And the chapter's own contribution is the staged counter chain (§11–§12): eight event counters whose consecutive differences localise a lost credit to one of four stages, before any waveform.

3. Sourcing

4. The Four-Way Tuple

Do not start with the sender's credit counter. Read four values together, and the combination localises before any waveform.

Four properties of this table.

Rows 1 to 4 all show sender credit at zero, and they are four different bugs with four different owners. A design exposing only the credit counter cannot distinguish any of them — which is why §41's per-class snapshot exists.

The discriminator between rows 1 and 2 is receiver occupancy. At capacity means the receiver is genuinely the bottleneck; at baseline means capacity was destroyed by the accounting, because the storage is free and the sender believes it is not.

Row 7 is the row that saves the most time and is checked least. Sender credit non-zero and the link still not progressing means flow control is working and the blockage is downstream (§35) — so every credit investigation is wasted.

And row 5's sender credit exceeding capacity is the one condition a local assertion catches (19.5 §16). The other six are all inside legal ranges, which is §25's whole argument.

5. Three Primary Signatures

Every flow-control bug reduces to one of three, and each has a distinctive trend rather than a distinctive value.

Credit leak. Sender credit trends monotonically downward across the run while receiver occupancy returns to baseline between bursts. Eventually the sender reaches zero and never recovers. The rate is proportional to whatever the false event is correlated with — usually congestion (§14).

Credit inflation. Sender credit exceeds legitimate allocatable capacity. The counter may stay inside its declared range for a long time; the receiver eventually overflows, or rejects a transfer the sender believed it was permitted (§19, §24).

Starvation / stranded return. Receiver has free space; returns are pending; sender has zero. Nothing is lost and nothing is inflated — the information that capacity is free never reaches the sender (§26).

And the fourth condition that is not a flow-control bug at all: every accounting identity closes, the receiver is full, and the consumer is not draining (§35). The credit stall is a faithful report of a real shortage whose cause is elsewhere.

6. Ownership Events Across the Link

Three things to read.

Seven arrows are the accounting chain (§11), and each is a counter. A credit that goes missing went missing between two specific adjacent arrows — which is what §12's difference counters localise.

The release arrow is dashed and marked "entry reusable" deliberately. 19.5 §21: a return is a statement about storage becoming reusable, not about data movement — and the read arrow above it is the event a wrong design returns on (§22's mirror case).

And the three muted arrows are the three signatures (§5), drawn at the points where each occurs: the leak at the sender, the stranding at the return path, the inflation at the acceptance.

7. Waveform — the Credit Leak

Four readings, and the third is the diagnosis.

sender_credit reaching zero is the symptom the report arrives with, and it carries no information about why.

consume_wrong firing five times is the mechanism, and it is visible only because the waveform plots the consume event separately from valid. A design that does not expose the consume event cannot show this.

rx_occupancy reading 1 while credit fell by 5 is the contradiction — and it is the observation that could not occur in a correct implementation (21.1 §1). Four credits describe storage that is free.

And the leak rate is the stall length. A five-cycle stall costs five credits; a fifty-cycle stall costs fifty — so the leak is fastest under congestion, which is exactly when flow control matters, and invisible when the link is idle.

8. The Conservation Snapshot

// ILLUSTRATIVE debug record, per credit domain. One read, so the fields cannot
// disagree about which cycle they describe (21.1 §11's torn-snapshot argument).
typedef struct packed {
  logic [CREDIT_W-1:0] sender_credit;     // the replica
  logic [OCC_W-1:0]    rx_occupied;       // the fact it describes
  logic [OCC_W-1:0]    rx_capacity;       // ACTIVE capacity (19.5 §36)
  logic [OCC_W-1:0]    rx_reserved;       // safety + progress reserve
  logic [RET_W-1:0]    returns_pending;   // released, not yet advertised
  logic [CREDIT_W-1:0] in_flight;         // consumed, not yet arrived (19.5 §5)
  logic [EPOCH_W-1:0]  credit_epoch;
  logic [CLS_W-1:0]    domain;
} fc_snapshot_t;

Four fields carry the diagnostic weight, and one of them has no register anywhere unless the design chooses to build it.

rx_occupied against rx_capacity is §4's row-1-versus-row-2 discriminator, and it is the single most valuable comparison in the chapter.

returns_pending separates §4's rows 3 and 4 — stranded versus lost, which are different subsystems.

in_flight is 19.5 §5's fourth quantity: consumed and not yet arrived. No single register holds it in a correct design — it is an implication of two counters on two dies — so the debug snapshot must derive and expose it, or the conservation equation cannot close (§11).

And credit_epoch is what makes a cross-recovery comparison meaningful (§44). Comparing counters across an epoch boundary without an initialisation term is comparing two different agreements.

9. Shadow Accounting

A shadow counter recomputes the credit independently and compares. Its entire value rests on the word independently.

// ILLUSTRATIVE. The shadow's expected credit, derived from RAW SEMANTIC EVENTS
// rather than from the design's own consume/return signals (§10).
logic [CREDIT_W:0] shadow_credit;
 
// The three raw events, counted at the BOUNDARY:
//   tx_accept      — a completed handshake at the transmit boundary
//   new_alloc_req  — that object requires a NEW remote allocation
//   return_accept  — a return message accepted from the peer
assign shadow_credit = $signed({1'b0, initial_advertised})
                     + $signed({1'b0, returns_accepted_cnt})
                     - $signed({1'b0, new_allocations_cnt});
 
assign shadow_mismatch = (shadow_credit != $signed({1'b0, sender_credit_q}));

And the harder, better form for silicon: record the events, recompute offline.

// ILLUSTRATIVE. Rather than a hardware shadow that can inherit the bug, expose
// the RAW EVENT COUNTS and let software or DV recompute the identity (§11).
logic [63:0] cnt_tx_accept_q;        // handshake completions at the boundary
logic [63:0] cnt_new_alloc_q;        // requiring a new remote allocation
logic [63:0] cnt_consume_q;          // the DESIGN's consume events
logic [63:0] cnt_return_accept_q;    // returns accepted

Three notes.

cnt_tx_accept and cnt_consume are separate counters deliberately. In a correct design they are equal — and their difference is §14's leak, measured directly rather than inferred from a credit trend.

The offline form is stronger because software can recompute the identity any way it likes, including ways the hardware designer did not anticipate. A hardware shadow computes one expression, chosen by the same person who wrote the design.

And cnt_new_alloc versus cnt_consume is the retransmission question (19.5 §51's open normative point, restated below in §23). The counters record the fact; they do not assert the rule.

10. Wrong Instrumentation — the Shadow That Shares the Signal

// WRONG — the shadow decrements on the DESIGN's consume signal.
always_ff @(posedge clk)
  if (credit_consume) shadow_credit_q <= shadow_credit_q - 1'b1;
  else if (credit_return) shadow_credit_q <= shadow_credit_q + 1'b1;

Worked, against §7's leak. The design consumes on valid, five times for one transfer. The shadow consumes on the same signal, five times.

The engineer reads "shadow matches" and concludes the accounting is correct.

Four properties.

This is 20.4 §16's mirroring failure in hardware. The shadow agrees with the design about when a credit is consumed, which is precisely the thing that is wrong — so it can only detect an adder bug, not an event bug.

Every bug in this chapter survives it. §14's false consume, §19's duplicate return, §22's lost return, §24's straggler — all are event-definition bugs, and the shadow shares the definition.

Its silence is worse than no shadow. A design with no shadow prompts an investigation; a design whose shadow agrees is reported as having verified accounting.

And the fix is the same as it is in verification: derive from the contract. A consume happens when an object crosses the transmit boundary requiring a new remote allocation — which is a handshake completion and an allocation flag, neither of which is the design's credit_consume wire.

11. The Event-Counter Chain

Eight counters along the ownership chain of §6. Their consecutive differences localise a lost or invented credit to one stage.

And the identities that should hold, with the in-flight terms stated explicitly:

ILLUSTRATIVE identities for one domain, one epoch. Terms in [brackets] are
in-flight quantities that make the equation an INEQUALITY at any instant and
an EQUALITY only when the link is quiescent.
 
  I1   consume        == new_alloc                      (exactly, every cycle)
  I2   rx_arrival     == new_alloc     - [in flight]
  I3   rx_alloc       == rx_arrival    - [being decoded]
  I4   rx_release     <= rx_alloc                       (occupancy = difference)
  I5   ret_generated  == rx_release                     (exactly — §19)
  I6   ret_transmitted<= ret_generated  - [pending]     (§26)
  I7   ret_accepted   <= ret_transmitted - [in flight]  (§22)
  I8   sender_credit  == initial + ret_accepted - consume

Two properties.

I1 and I5 are exact equalities and everything else is an inequality. That is the point: the two exact identities are the two places a bug can be proved from counters alone, with no timing knowledge and no quiescence requirement.

And I8 is the identity a shadow checks (§9). It closes only if every stage above it closed — so a mismatch at I8 says something is wrong and the staged differences say where.

12. Difference Counters — the First Nonzero Stage

The chapter's centerpiece diagnostic. Compute four differences; the first nonzero one names the stage.

// ILLUSTRATIVE debug derivations. Each difference is ZERO in a correct design
// at quiescence, and the FIRST nonzero one localises the bug.
assign d1_consume_vs_alloc  = cnt_consume_q        - cnt_new_alloc_q;
assign d2_arrival_vs_alloc  = cnt_new_alloc_q      - cnt_rx_arrival_q;
assign d3_release_vs_gen    = cnt_rx_release_q     - cnt_ret_generated_q;
assign d4_gen_vs_transmit   = cnt_ret_generated_q  - cnt_ret_transmitted_q;
assign d5_transmit_vs_accept= cnt_ret_transmitted_q- cnt_ret_accepted_q;

Four properties of this table, and it is why the chain is worth nine counters.

Two rows can be read without waiting for quiescence: d1 and d3. They correspond to the exact identities I1 and I5 (§11), so a nonzero value is a bug immediately — no in-flight term to subtract, no need to stop traffic.

d3 negative proves a duplicate return locally, at the receiver, before the sender's credit inflates and long before an overflow. 19.5 §24's duplicate return normally waits for the receiver to be genuinely full — hours later — and this counter catches it on the first duplicate.

d4 positive and stable is the stranding signature. Positive and rising is batching in progress, which is normal; positive and stable while the sender is at zero is §27's deadlock.

And d5 cannot distinguish lost from rejected. A return dropped in transport and one rejected by the epoch guard both leave d5 positive — which is why §23's stale counter exists as a separate register.

13. The Diagnostic Table

Observation to area, in one place. This is the table to read before opening a waveform.

Two notes.

Row 2 and row 3 are the "normal" rows, and including them is deliberate. A diagnostic table without non-bug rows sends investigations after correct behaviour — and "returns are pending" is correct behaviour in any batched design.

And row 9 is the one that a total-only design cannot reach at all (§42). Per-class conservation is not a refinement of total conservation; it is a different check, and the total can close while every class is broken.

14. False Consume

The most common flow-control bug, and 19.5 §18 taught the RTL. Here is the diagnosis.

The signature, in three registers:

And the confirming ratio: cnt_consume / cnt_tx_accept. In a correct design it is at most 1; the excess is the average stall length — which points directly at where the qualification is missing.

Four properties that make it hard to catch without the counters.

The direction is survivable, so it lives. The link becomes slow, then stops. No corruption, no overflow — so a team under pressure raises the initial credit value, throughput returns, and the leak continues at the same rate with a longer time-to-symptom.

The rate scales with congestion. Invisible when idle, fastest when the link is loaded. A directed test at low utilisation will not find it.

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

And the far end looks perfectly healthy, because it is — its occupancy drains, its buffers empty, every check it runs passes. The asymmetry is the finding.

15. The Consume Event, Correctly

// ILLUSTRATIVE. Two terms, both necessary. 19.5 §17's rule, with the debug
// counters alongside so the design's own event can be compared to the contract.
assign tx_accept_fire = tx_valid && tx_ready;                  // a real transfer
 
assign credit_consume_fire = tx_accept_fire
                          && requires_new_remote_allocation;   // §23's question
 
// DEBUG: count both, separately, so d1 (§12) is computable.
always_ff @(posedge clk or negedge por_n) begin
  if (!por_n) begin
    cnt_tx_accept_q <= '0; cnt_new_alloc_q <= '0; cnt_consume_q <= '0;
  end else begin
    if (tx_accept_fire)        cnt_tx_accept_q <= cnt_tx_accept_q + 64'd1;
    if (tx_accept_fire && requires_new_remote_allocation)
                               cnt_new_alloc_q <= cnt_new_alloc_q + 64'd1;
    if (credit_consume_fire)   cnt_consume_q   <= cnt_consume_q   + 64'd1;
  end
end

Three notes.

cnt_consume and cnt_new_alloc are counted from different expressions deliberately, even though a correct design makes them equal. That redundancy is the entire diagnostic — a shared expression would make d1 structurally zero and the check vacuous, which is §10's failure in counter form.

tx_accept_fire is a conjunction, not a level. 19.5 §18 and §7's waveform.

And requires_new_remote_allocation is where §23's normative question lives. The counters record what the design did; they do not assert what it should have done, because that rule is not established here.

16. SVA — the Consume Event

// MANDATORY. A consume coincides with an actual commit requiring a new
// allocation — never a bare valid, never a grant (19.5 §20).
property p_consume_on_commit_only;
  @(posedge clk) disable iff (!por_n)
    credit_consume_fire |-> (tx_accept_fire && requires_new_remote_allocation);
endproperty
a_consume_on_commit_only: assert property (p_consume_on_commit_only);
 
// MANDATORY. The named form of §7's failure — it fires with a message that
// says what happened rather than what the qualification should have been.
property p_no_consume_while_stalled;
  @(posedge clk) disable iff (!por_n)
    (tx_valid && !tx_ready) |-> (consume_units == '0);
endproperty
a_no_consume_while_stalled: assert property (p_no_consume_while_stalled);
 
// MANDATORY. The COUNTER identity, asserted continuously — this is d1 == 0
// and it is exact (§11's I1), so it needs no quiescence assumption.
property p_consume_matches_allocation;
  @(posedge clk) disable iff (!por_n)
    (cnt_consume_q == cnt_new_alloc_q);
endproperty
a_consume_matches_allocation: assert property (p_consume_matches_allocation);

Why the third property is the one that matters in a debug context. The first two catch the bug at the cycle it happens in a simulation where they are bound. The third is an identity over counters — so it is equally checkable in silicon by reading two registers, and it is the bridge between the SVA world and the lab (§54).

17. Double Consume

Two pipeline stages each generating an allocation pulse for one object.

// WRONG — stage A and stage B both pulse for the same object.
assign consume_a = stage_a_fire && stage_a_new_alloc;
assign consume_b = stage_b_fire && stage_b_new_alloc;
assign credit_consume_fire = consume_a || consume_b;   // BOTH fire per object

The signature is identical to §14's — d1 > 0 — and the ratio distinguishes them:

That ratio is the whole diagnosis. A stable integer ratio means a structural duplication; a load-varying ratio means an event-qualification bug. Two different fixes, distinguished by one division.

And the fix requires object identity, not just a better qualification:

// ILLUSTRATIVE. A local debug tag per accepted object, so a duplicate
// allocation for the SAME object is detectable. Not a protocol field (§3).
logic [DTAG_W-1:0]       dbg_tag_q;
logic [MAX_OUTSTANDING-1:0] dbg_charged_q;    // has this object been charged?
 
always_ff @(posedge clk or negedge por_n) begin
  if (!por_n) begin
    dbg_tag_q <= '0; dbg_charged_q <= '0;
  end else begin
    if (tx_accept_fire) dbg_tag_q <= dbg_tag_q + DTAG_W'(1);
    if (credit_consume_fire) begin
      if (dbg_charged_q[consume_tag])
        dbg_double_charge_q <= dbg_double_charge_q + 1'b1;   // the finding
      dbg_charged_q[consume_tag] <= 1'b1;
    end
    if (obj_retired) dbg_charged_q[retire_tag] <= 1'b0;
  end
end

A bitmap, not a counter — 19.5 §26's argument. A count cannot answer "have I already charged this object?", and that is the question a double consume requires.

18. Duplicate Return

The dangerous direction: capacity is manufactured. 19.5 §24 taught the design side; the diagnosis is much easier than the design suggests.

Five ways duplicates arise, and none is exotic:

And the reason it is normally caught late. Each duplicate inflates the sender's replica by one; the counter stays comfortably inside its declared range, because the sender is also spending. The overflow happens the first time the receiver is genuinely full — which may be hours or days after the duplicates accumulated.

19. The Counter Signature That Catches It Immediately

d3 = rx_release − ret_generated negative proves a local return-generation bug, at the receiver, on the first duplicate.

Three properties of that statement.

It is local. Both counters are at the receiver, so no cross-die comparison, no timing assumption, no quiescence requirement. I5 is an exact identity (§11).

It fires on the first duplicate, not on the eventual overflow. The difference is hours.

And it names the stage precisely. A negative d3 is generation; a duplicate at the sender — from a retransmitted message — leaves d3 at zero and shows in d5 instead. Two mechanisms, two counters, and the design that exposes only the sender's credit sees neither.

// MANDATORY. The identity, asserted. This is the cheapest assertion in the
// chapter relative to what it prevents.
property p_returns_match_releases;
  @(posedge clk) disable iff (!por_n)
    (cnt_ret_generated_q == cnt_rx_release_q);
endproperty
a_returns_match_releases: assert property (p_returns_match_releases);
 
// MANDATORY. Per entry, one return: the guard 19.5 §25 designs, asserted.
property p_return_once_per_entry(int idx);
  @(posedge clk) disable iff (!por_n)
    (ret_gen_fire && (ret_idx == idx)) |-> !entry_returned_q[idx];
endproperty

20. Return Lost in Transport

d3 == 0 and d5 > 0 at quiescence. Releases and generation agree; returns were sent and not accepted.

Three sub-hypotheses, and one register separates them:

And the mirror case, which is a different bug entirely: d3 > 0 at quiescence — releases with no return generated. That is the generator failing to fire, and it produces exactly the same sender-side symptom as a lost return with a completely different owner. The two are indistinguishable from the sender and trivially distinguishable from the receiver's counters.

21. The Early Return — the Mirror of a Lost One

19.5 §22's use-after-free across a die boundary, seen from the counters.

A design that returns when the read begins rather than when the entry is released has d3 and d5 both at zero — every count agrees. The identity closes.

And the failure is data corruption, not a stall: the sender is granted the entry while a downstream stage is still reading the previous occupant.

Two consequences for diagnosis.

No accounting evidence exists. The counters are consistent because the design is consistently early. This is the one flow-control bug the counter chain cannot see, and it is worth stating plainly.

So it needs a different check: the effect form. 19.5 §23's property — an entry whose credit was returned is not read again before reallocation — written against a different observable than the return condition itself:

// MANDATORY. The EFFECT check, because the cause check can be written against
// the same wrong signal the designer used (19.5 §23, 20.3 §27).
property p_no_read_after_return(int idx);
  @(posedge clk) disable iff (!por_n)
    (ret_gen_fire && (ret_idx == idx))
      |=> !(entry_read_fire && (read_idx == idx))
          until (entry_alloc_fire && (alloc_idx == idx));
endproperty

22. Stale-Epoch Returns

Separately from that question, a stale return — one belonging to a dead agreement — must be rejected and counted.

// ILLUSTRATIVE. 19.5 §30's guard, with the counter that makes it diagnostic.
assign return_accept = return_valid && (return_epoch == credit_epoch_q)
                                   && (fc_state == FC_ACTIVE);
assign return_stale  = return_valid && (return_epoch != credit_epoch_q);
 
always_ff @(posedge clk or negedge por_n)
  if (!por_n)                                        cnt_stale_return_q <= '0;
  else if (return_stale && (cnt_stale_return_q != '1))
                                                     cnt_stale_return_q <= cnt_stale_return_q + 1'b1;

And the reading that matters is when the stale returns occurred:

23. Recovery-Induced Inflation

19.5 §29's flagship, as a diagnosis.

Three notes.

Row 3 is the decisive one. A recovery with stragglers in flight and a zero stale count means nothing was rejected, so either no straggler arrived — checkable against d5 — or the guard does not exist.

Row 5 is the case people miss. An epoch that does not advance makes every stale return epoch-current, so the guard passes them all and looks like it is working (19.5 §31's atomicity property is what catches it).

And the mirror direction is silent. If the re-baseline happens after the straggler rather than before, the straggler is overwritten and the link runs permanently short — with no assertion, no bound exceeded, and only reduced throughput as evidence. 19.5 §29's last note; its only diagnostic is the conservation identity I8.

24. Why the Bound Assertion Is Necessary and Insufficient

// NECESSARY. Catches gross inflation and the unsigned wrap of 19.5 §15.
property p_credit_within_capacity;
  @(posedge clk) disable iff (!por_n)
    (sender_credit_q <= active_capacity_q);
endproperty
a_credit_within_capacity: assert property (p_credit_within_capacity);

Five bugs in this chapter that pass it forever:

Two consequences.

The bound catches a consequence, and the identities catch a cause. 19.5 §53's argument: every silent credit bug keeps the counter inside its legal range, and what each breaks is a relationship.

And where the bound does fire, it fires late. §23's straggler exceeds capacity at the moment of absorption — so the bound and the exactness property fire at the same cycle, and only the exactness property says why (19.5 §12).

25. Stranded Returns

Receiver has free space. Returns are pending. Sender has zero. Nothing is lost or inflated.

Five causes, and each is a different owner:

Two notes.

Row 3 is separated from rows 4 and 5 by per-class counters (§41). A total-only design sees "returns pending" and cannot tell whether one class is starved or the whole path is stopped — which is §42.

And row 5 is the one that reads as a hardware fault. A recovery gate never released leaves the return path structurally disabled; the returns are generated, queued, and never eligible — and fc_state is the register that says so.

26. The Batch-Threshold Deadlock

19.5 §42's flagship liveness bug, as a diagnosis. Three registers, all stable, forever.

The circular wait, stated from the evidence:

The sender waits for credit. The credit waits for the batch threshold. The threshold waits for more releases. More releases require more arrivals. More arrivals require credit.

Four properties that make it distinctive.

All three registers are stable, and that is the signature. Not falling, not rising — stable indefinitely. Every other failure in this chapter has a trend; this one has none.

Every safety property passes. Credit 0 is legal, occupancy 11 is legal, pending 5 is legal. The system is in a perfectly legal state forever (13.3 §19's argument).

Five free entries at the receiver throughout. This is stranded capacity, not congestion — and the distinction is §4's row 1 versus row 3.

And it needs a quiet period to be reached. A burst followed by silence; random traffic almost always supplies another arrival that pushes the count over the threshold, so the bug survives random regression and appears in the field (20.5 §54).

27. The Diagnostic Invariant

If returns_pending > 0 and the sender has been starved for longer than any legitimate flush interval, a return service must have occurred. It did not. That is the bug.

// ILLUSTRATIVE. The invariant as a checkable condition, with the age that makes
// it decidable. This is 19.5 §44's third property in debug form.
assign stranded_condition = (returns_pending_q != '0)
                         && (sender_credit_observed == '0)
                         && (rx_occupancy_q < active_capacity_q);
 
logic [AGE_W-1:0] stranded_age_q;
 
always_ff @(posedge clk or negedge por_n) begin
  if (!por_n)                          stranded_age_q <= '0;
  else if (!stranded_condition)        stranded_age_q <= '0;
  else if (stranded_age_q != '1)       stranded_age_q <= stranded_age_q + AGE_W'(1);
  // saturates — 21.1 §21's argument
end
 
assign stranded_detected = (stranded_age_q >= AGE_W'(STRANDED_BOUND));

Three notes.

The condition is a conjunction of three observations, which is what makes it specific. Pending returns alone is normal; pending returns with a starved sender and a non-full receiver is not.

The age saturates (21.1 §21) — because a wrapping age reports a fresh stranding during an ancient one, and then nothing fires.

And STRANDED_BOUND must exceed any legitimate flush interval, which is derived from the flush timer plus the return-path latency (19.5 §43). A bound below that fires on normal batching.

28. Return-Arbitration Starvation

19.5 §49's strict-priority failure, and it produces §26's signature for one class only.

Two notes.

Per-class evidence is mandatory here and a total cannot substitute. Total pending returns is non-zero — which is also true during normal batching — and only the per-class split shows that one class is never serviced (§41).

And service_count per class is the decisive register. A class with pending returns and a service count that has not moved was never granted, which is arbitration rather than batching. A class whose service count is moving while pending stays high is a rate problem — service is happening and not keeping up, which is a different fix.

29. Pending-Age, Per Class

// ILLUSTRATIVE. The age of the OLDEST unsent return per class — not the age of
// the pending count, which is §31's bug.
logic [AGE_W-1:0] oldest_pending_age_q [NUM_CLASSES];
logic [CNT_W-1:0] service_count_q      [NUM_CLASSES];
 
always_ff @(posedge clk or negedge por_n) begin
  if (!por_n) begin
    for (int c = 0; c < NUM_CLASSES; c++) begin
      oldest_pending_age_q[c] <= '0;
      service_count_q[c]      <= '0;
    end
  end else begin
    for (int c = 0; c < NUM_CLASSES; c++) begin
      // Reset ONLY when the queue actually drains to empty, or when the
      // OLDEST item is serviced — not on any change to the count (§31).
      if (returns_pending_q[c] == '0)      oldest_pending_age_q[c] <= '0;
      else if (oldest_pending_age_q[c] != '1)
                                           oldest_pending_age_q[c] <= oldest_pending_age_q[c] + AGE_W'(1);
      if (ret_service_fire[c])             service_count_q[c] <= service_count_q[c] + CNT_W'(1);
    end
  end
end

Two properties.

Reset on empty, not on service. A class serviced continuously but never drained — because new returns arrive as fast as old ones are sent — has a genuinely old oldest item, and resetting on service would hide that.

And saturating, per 21.1 §21. A wrapped age is worse than no age.

30. Wrong Age Counter — Reset on Any Change

// WRONG — the age resets whenever the pending count changes.
always_ff @(posedge clk)
  if (returns_pending_q != $past(returns_pending_q)) pending_age_q <= '0;
  else                                              pending_age_q <= pending_age_q + 1'b1;

Worked. Class 1 is starved by strict priority. New releases keep arriving, so returns_pending climbs: 1, 2, 3, 4, 5 …

Every increment resets the age. The age never exceeds the inter-arrival gap.

Three properties.

Starvation is hidden forever, and it is hidden more effectively the busier the class is — which is exactly backwards.

The register reads plausibly. A small age looks like a healthy, actively serviced class. It is the same contradiction shape as 21.1 §21's wrapping timer: a diagnostic reporting freshness during an ancient stall.

And the fix is to age the oldest item, not the count (§29). A count is a quantity; a starvation question is about a duration, and only the oldest item's age answers it.

31. Liveness, With Assumptions

// MANDATORY, with the assumptions named (20.3 §42). Unconstrained liveness
// here fails on the environment, gets called noisy, and gets deleted.
//
//   A1  the clock runs; the hard reset is not re-asserted
//   A2  the return control path eventually accepts an emission
//   A3  the flow-control state is not held in a fault state
//   A4  the consumer eventually drains the receive buffer
assume property (@(posedge clk) s_eventually ret_service_ready);
assume property (@(posedge clk) s_eventually (fc_state != FC_FAULT));
 
// The BOUNDED form, which is what simulation can check and what silicon can
// approximate with §27's age counter.
property p_pending_serviced_within_bound(int unsigned c);
  @(posedge clk) disable iff (!por_n)
    (returns_pending_q[c] != '0)
      |-> ##[1:FLUSH_TIMEOUT + RETURN_PATH_MAX] ret_service_fire[c];
endproperty
 
// The SYSTEM-LEVEL form, independent of how batching or arbitration is built —
// the property that survives a redesign (19.5 §44).
property p_no_stranded_capacity;
  @(posedge clk) disable iff (!por_n)
    stranded_condition |-> ##[1:STRANDED_MAX] ret_service_fire[stranded_class];
endproperty
a_no_stranded_capacity: assert property (p_no_stranded_capacity);

Why the third property is the durable one. The first two describe this batching and this arbiter; the third describes the outcome they exist to produce — free capacity is never permanently unreachable — and it holds regardless of the mechanism. It is the property that would catch §26 in a design whose batching lives somewhere nobody looked.

32. Genuine Receiver-Full

Sender credit 0. RX occupancy at active capacity. Pending returns 0. Every identity closes.

This may be entirely correct. Flow control is doing its job: the receiver is full and the sender is correctly refused.

So the question changes, and it is no longer a flow-control question:

Why is the consumer not draining?

And row 3 is the row that must be considered before any code is changed. A producer faster than a consumer, with a buffer sized for a burst rather than a rate mismatch, produces exactly this and is a sizing decision rather than a defect (13.5).

33. Downstream Blockage

All identities close. Sender credit non-zero or zero. No progress. Flow control is reporting a real shortage, and the cause is elsewhere.

The critical instruction:

Do not inspect every full queue. Find the first queue that stopped draining, and work from there.

Because backpressure propagates upstream (13.3 §10), so every queue between the blockage and the sender is full as a consequence. Inspecting the sender's queue finds a full queue and no cause.

34. The Occupancy Waterfall

The table that localises a downstream blockage in one read per queue.

Illustrative. Four queues in series, a consumer behind Q3, and the timestamps at which each became full.

Four readings, and the ordering is the entire diagnosis.

Q3 filled first, at cycle 1,200. The blockage is behind Q3 — the consumer, or whatever the consumer waits on. Everything upstream is a consequence.

The sender reaching zero at cycle 1,460 is 260 cycles after the cause. A debugger starting at the sender's credit counter is four queues and 260 cycles downstream of the finding.

Every identity closes throughout. No leak, no inflation, no stranding — so the entire counter chain of §11 reads clean, which is itself the discriminating observation (§13's row 8).

And the fill order is what carries the information, not the fill state. At cycle 1,460 all four queues are full and the order is unrecoverable — which is why the waterfall needs per-queue first-full timestamps, not just occupancy:

// ILLUSTRATIVE. A first-full timestamp per queue makes the waterfall
// reconstructible from a single snapshot taken long after the event.
logic [TIME_W-1:0] first_full_time_q [NUM_QUEUES];
logic              first_full_valid_q [NUM_QUEUES];
 
always_ff @(posedge clk or negedge por_n)
  for (int q = 0; q < NUM_QUEUES; q++)
    if (!por_n) first_full_valid_q[q] <= 1'b0;
    else if (queue_full[q] && !first_full_valid_q[q]) begin
      first_full_valid_q[q] <= 1'b1;
      first_full_time_q[q]  <= now_q;          // sticky-first (14.5 §8)
    end

The queue with the earliest timestamp is nearest the cause. One read, and it survives the whole system filling up afterwards.

35. Deadlock, Starvation and Congestion

Four conditions, routinely conflated, with four different responses.

Three properties.

Row 4 is the discriminator that matters most. Only a credit leak breaks the identities — the other three are all accounting-correct. So a clean counter chain eliminates the leak class outright, which is a large elimination for one read.

Rows 3 and 5 separate starvation from deadlock. In starvation other flows progress; in deadlock nothing in the cycle does. And starvation always has free capacity somewhere, which deadlock need not.

And congestion resolving on its own is what makes it identifiable by waiting. A stall that clears is congestion; one that does not is one of the other three — and that is the cheapest experiment available.

36. The Wait-For Graph

For a suspected deadlock, the graph is the diagnosis and it is built from ownership, not from occupancy.

ILLUSTRATIVE wait-for graph. Nodes are flows or resources; an edge means
"waits for". A CYCLE is a deadlock; no cycle means starvation or congestion.
 
   [bulk request flow]  --waits for-->  [remote bulk credit]
   [remote bulk credit] --waits for-->  [bulk entry released]
   [bulk entry released]--waits for-->  [completion delivered]
   [completion delivered]--waits for--> [remote completion credit]
   [remote completion credit]--waits for-->[completion entry free]
   [completion entry free]--waits for-->[bulk entry released]   <-- CYCLE
 
  READING: bulk traffic has consumed the entries that completions need in
  order to land, and the completions are what would release the bulk entries.
  This is 19.5 §46's progress-reserve failure, and the fix is a reserve —
  not more credit, which makes it worse.

Two notes.

The cycle is not visible in occupancy. Every queue is full and every counter is legal; the cycle exists in the dependency structure, which is why 13.3 §16 insists on drawing one.

And the fix direction is counter-intuitive. More credit lets bulk traffic consume the remaining entries faster, making the deadlock arrive sooner. 19.5 §45's progress reserve is the fix, and §37 is the evidence that a reserve was violated.

37. Progress-Reserve Violation

19.5 §45's reserve, and the evidence that it was consumed.

// ILLUSTRATIVE. The one condition that proves a reserve violation, counted.
assign reserve_violated = bulk_accept_fire
                       && ((free_entries_q - 1) < progress_reserve_q);
 
always_ff @(posedge clk or negedge por_n)
  if (!por_n)                     cnt_reserve_violation_q <= '0;
  else if (reserve_violated && (cnt_reserve_violation_q != '1))
                                  cnt_reserve_violation_q <= cnt_reserve_violation_q + 1'b1;

And the five registers that together prove or disprove it:

Two notes.

cnt_reserve_violation non-zero is a proof, not a hint. One condition, one counter, and it fires at the cycle a bulk object was admitted into the reserve — long before the deadlock it causes.

And a reserve violation is the cause of §36's cycle. The graph shows the deadlock; this counter shows the admission that created it, which is the actionable finding.

38. Per-Class Counters

Everything in this chapter must be per credit domain, and §42 is what a total costs.

And the reading rule: compare across classes, not against a threshold. One class with a saturated oldest_pending_age and a static service_count while others are healthy is starvation, proved by the comparison — no absolute bound required.

39. Wrong Instrumentation — Totals Only

// WRONG — one counter per event type, summed across all classes.
logic [63:0] total_consume_q, total_return_q;

Worked, and this is the chapter's most instructive instrumentation failure.

Class A leaks 100 credits over a run. Class B receives 100 duplicate returns.

The total conservation identity closes exactly. Two serious bugs cancel.

Four properties.

The cancellation is arithmetic, not coincidental. Any leak in one domain and any inflation in another of the same magnitude cancel in a sum — and over a long run, magnitudes converge, so cancellation becomes more likely rather than less.

Both classes are broken and neither is visible. Class A stalls; class B eventually overflows. The total says the accounting is perfect.

A total-only design therefore cannot check conservation at all, in the sense that matters. Conservation must close at the ownership domain granularity — because a credit is a claim on a specific pool, and summing claims across pools discards the identity of what was claimed.

And this is 19.5 §9's global-pool argument in instrumentation form. A scalar counter for several physical structures is wrong for the same reason a scalar credit counter is: it counts the wrong thing.

40. Cross-Domain Cancellation, Stated as a Rule

Never allow a sum over classes to be the conservation check. The identity must close per domain, and a total that closes tells you nothing about any domain.

Two corollaries.

A design exposing only totals has no conservation check, however many counters it has. Nine total counters cancel just as readily as two.

And the per-class requirement extends to the snapshot (§8). A snapshot without a domain field cannot be attributed, so a sequence of snapshots taken during a stall may describe different classes and appear inconsistent.

41. The Credit-Domain Epoch

Comparisons are valid only within an epoch (19.5 §28).

ILLUSTRATIVE. The identity across a recovery, with the initialisation term
made explicit. Comparing counters across an epoch boundary WITHOUT this term
is comparing two different agreements.
 
  Within epoch E:
    sender_credit  ==  advertised(E)
                     + returns_accepted_in_E
                     -  consumes_in_E
 
  Across a boundary E -> E+1:
    the equation RESTARTS. advertised(E+1) is the new initialisation term,
    and returns/consumes from E are NOT terms of E+1's equation.
 
  So the debug counters must either:
    (a) be snapshotted and cleared at each epoch boundary, OR
    (b) be free-running with a per-epoch snapshot recorded, so software can
        difference them  -- (b) is preferable: it preserves history (14.2 §14)

Two notes.

Option (b) is preferable and it is the one that preserves evidence. Clearing counters at an epoch boundary loses everything before the recovery — which is 14.2 §14's capture-before-retrain rule. A free-running counter plus a snapshot at each boundary gives both the per-epoch difference and the history.

And a mismatch that appears only across a boundary is not a bug. It is the missing initialisation term. A debug procedure that differences counters across a recovery and reports a discrepancy has found its own arithmetic error — which is worth knowing before it is reported as a design defect.

42. The Zero-Credit Snapshot

The highest-value single piece of flow-control instrumentation: capture the whole tuple at the moment credit reaches zero.

// ILLUSTRATIVE. Sticky-first snapshot on the nonzero -> zero transition, per
// class. This is what turns "the link stalled" into a localisation.
fc_snapshot_t zero_snap_q [NUM_CLASSES];
logic         zero_snap_valid_q [NUM_CLASSES];
 
always_ff @(posedge clk or negedge por_n) begin
  for (int c = 0; c < NUM_CLASSES; c++) begin
    if (!por_n)                       zero_snap_valid_q[c] <= 1'b0;
    else if (diag_clear_fire)         zero_snap_valid_q[c] <= 1'b0;
    else if ((credit_q[c] == '0) && ($past(credit_q[c]) != '0)
             && !zero_snap_valid_q[c]) begin
      zero_snap_valid_q[c]     <= 1'b1;
      zero_snap_q[c].sender_credit   <= '0;
      zero_snap_q[c].rx_occupied     <= rx_occupancy_observed[c];
      zero_snap_q[c].rx_capacity     <= active_capacity_q[c];
      zero_snap_q[c].rx_reserved     <= reserve_q[c];
      zero_snap_q[c].returns_pending <= returns_pending_q[c];
      zero_snap_q[c].in_flight       <= in_flight_derived[c];
      zero_snap_q[c].credit_epoch    <= credit_epoch_q[c];
      zero_snap_q[c].domain          <= CLS_W'(c);
    end
  end
end

Three properties.

It resolves §4's table at the moment of the transition, not later. By the time software reads a live snapshot, the receiver may have drained and row 1 has become row 2 — so the live tuple can misattribute a genuine full condition as a leak.

It is sticky-first and cleared only by a diagnostic clear (14.5 §25) — so a link that reaches zero credit a thousand times preserves the first occasion, which is the informative one.

And it is per class, because the tuple is only meaningful within a domain (§40).

43. Zero Credit Is Not Always an Error

A design that reports zero credit as a fault will report it constantly, and the report will be ignored.

The snapshot is what makes this distinguishable (§42), and the consequence for reporting is specific:

Zero credit is a condition, not an error. Report the stranded and leaked combinations as errors, and the others as performance counters.

A design that raises an interrupt on zero credit trains software to mask it — 14.5 §28's storm-suppression argument — and then the genuinely diagnostic combinations are masked with it.

44. First Divergence Versus Final Stall

The timeline that justifies the whole counter chain.

Three readings.

The report arrives at cycle 10,100 and the cause is at cycle 100 — ten thousand cycles and one subsystem apart.

d1 becomes nonzero at cycle 100. An identity assertion (§16) fails there; a counter read at any point after it shows a nonzero d1 — so the evidence is available at the cause, in silicon, without a waveform.

And debugging from cycle 10,100 is nearly impossible. The stall is a stable state with no recent activity; the interesting event is ten thousand cycles in the past and the trace buffer has long since wrapped. The counters are what survive.

45. The Long-Run Soak

A leak of one credit per million transfers passes every directed test and stops the link after a day.

Three requirements to catch it.

Conservation counters that do not wrap (§46). A 64-bit counter is adequate; a 16-bit one wraps and the difference becomes meaningless.

A long run. Directed tests are too short by construction. The identity must be checked over hours of traffic, which means it must be a register rather than an assertion in a short simulation.

And coverage of the simultaneous cases (20.5 §21): a leak that requires a simultaneous consume and return, or a stall of a particular length, needs the coverage bin to have been hit — otherwise the soak ran without exercising the condition.

46. Wraparound in the Diagnostic Itself

If a diagnostic counter wraps, the evidence is destroyed and the difference becomes noise.

Two notes.

Differences must be computed signed. cnt_ret_generated − cnt_rx_release is negative for a duplicate return (§19); an unsigned subtraction wraps to an enormous positive number and the sign — which is the diagnosis — is lost.

And the last row matters. A functional credit counter's width is set by the architecture (19.5 §10); widening it as a debug measure changes behaviour. Debug counters are separate registers.

47. Unsigned Arithmetic Hiding a Negative Credit

19.5 §15's catastrophic direction, as a diagnosis.

The signature is distinctive: sender credit jumps from a small value to a very large one in one cycle, with no advertisement event.

Two notes.

This is the one flow-control bug the bound assertion catches at the cycle of the cause rather than at a consequence — because the wrapped value is grossly out of range.

And the diagnostic that catches it before the wrap is the pre-truncation range check (19.5 §16): the signed intermediate is negative, and a debug counter of credit_fault events records it even if the design's response is to hold rather than to wrap.

48. Fault Injection for Flow Control

Inject at contract boundaries (20.2 §43), and six injections cover this chapter.

Two notes.

The first injection is a stimulus change, not a fault at all — and it is the one most likely to be absent from a regression, because it reduces throughput. A test suite optimised for bandwidth never holds ready low for long.

And rows 3 and 4 are the two nobody builds. 19.5 §24's duplicate and 18.4 §20's lost return both live there, and both produce a link that slowly stops with every safety property passing.

49. Why Forcing the Credit Register Is Poor Reproduction

// WRONG — force the credit counter to reproduce a "low credit" scenario.
initial begin
  wait (link_operational);
  force dut.credit_q[0] = 5'd1;
  #100ns;
  release dut.credit_q[0];
end

Four properties.

It creates a state with no causal path. The counter reads 1 and no sequence of consumes and returns produced it — so the reference models disagree with the design for a reason that is the testbench's fault (20.6 §22).

It tests the downstream behaviour, not the bug. "What happens when credit is low" is a different question from "why did credit become low" — and the second is the one being investigated.

The models produce a cascade of false failures, because the forced value generated no observable event and their conservation identities now break.

And the corner is reachable legitimately. Low credit is produced by issuing objects while withholding releases — a burst plus a stalled consumer, which is two primitives any environment already has. The force was a shortcut around a scenario the plan needed anyway.

50. Scoreboard Correlation at the First Divergence

20.4's resource model, used at the moment d1 or d3 becomes nonzero.

ILLUSTRATIVE report at first divergence. Small, specific, and it names the
stage and the object rather than dumping a log.
 
  FIRST DIVERGENCE: d1 (consume - new_alloc) became 1
    cycle              2,814
    domain / class     0
    credit_epoch       7
    expected_credit    (model)   12
    observed_credit    (design)  11
    cnt_tx_accept                  418
    cnt_new_alloc                  418
    cnt_consume                    419      <-- the extra one
    last tx_accept object tag       0x1A3
    tx_valid / tx_ready at 2,814   1 / 0    <-- NO TRANSFER
  READING: a consume fired on a stalled cycle. §14.

Two notes.

The last two lines are the diagnosis and they are two bits. valid high with ready low at the divergence cycle proves the consume was not a transfer — and that is the observation that could not occur in a correct implementation.

And the report is short deliberately. 20.4 §38's argument: a first-divergence report that names the stage, the cycle and the contradicting signals beats a log of ten thousand credit events.

51. Hardware Versus Simulation Observability

Two consequences.

The counter chain is the design decision that makes silicon flow-control debug possible. Nine wide counters plus a snapshot plus a few ages — and without them, a credit stall in silicon has essentially no evidence, because the interesting event is thousands of cycles in the past.

And the one row that does not transfer is the last. valid/ready at the divergence cycle is what §50's report turns on; in silicon it requires a small trace ring triggered by the identity becoming nonzero — which is a cheap and very high-value trigger, because it captures the cause rather than the symptom.

52. Flagship Trace 1 — False Consume

Illustrative. §7's waveform as a twenty-cycle table with the counters.

Five readings.

d1 becomes 1 at cycle 100 — the cause. Ten thousand cycles before the stall, and a counter read at any later point still shows it.

Five consumes for one transfer. cnt_consume rose by 5 while cnt_tx_accept rose by 1.

RX occupancy reaches 4 at cycle 112 and returns to 3 at cycle 130 — one object arrived and drained. Four credits describe storage that is free, which is §7's contradiction.

The credit's net movement is −4 over the sequence, and it never recovers, because the return only restores the one credit that corresponded to a real object.

And d1 rising monotonically is the trend that distinguishes this from §17. A false consume on valid gives a load-varying excess; a double consume gives exactly 2× and a linear d1 (§17's ratio).

53. Flagship Trace 2 — Lost Return

Illustrative. Counters at quiescence, which is when the inequalities become equalities.

Four readings.

d5 = 12 with a zero stale count is the finding, and it takes one read of two registers.

Every earlier difference is zero, which eliminates the consume event, the transport of objects, the receiver's allocation and release, the return generator and the return transmitter — six stages, eliminated.

The sender's credit being short by exactly 12 confirms the arithmetic and rules out a second, independent bug.

And the investigation is now the return transport path: a dropped message, a clock-domain crossing losing a pulse (19.1 §40), or a receive-side filter. Three candidates, one subsystem.

54. Flagship Trace 3 — Duplicate Return

Illustrative. The signature that fires early.

Four readings.

d3 negative is the proof, and it is local to the receiver. No cross-die comparison. It was already −1 after the very first duplicate, long before the credit exceeded capacity.

The bound assertion fired later — at the cycle the inflated credit crossed the capacity, which may be thousands of cycles after the first duplicate. §24's argument: the bound catches a consequence.

A zero stale count eliminates §23's recovery straggler, so this is a local generation bug rather than an epoch failure.

And the fix is 19.5 §25's per-entry return bit, verified by the per-entry assertion of §19 — which converts the duplicate from an inflation into a no-op.

55. Flagship Trace 4 — the Batching Deadlock

Illustrative. Threshold 8, capacity 16, no flush timer.

And with a flush timer of 64:

Four readings.

Every register is stable and legal, forever. §26's signature. No trend, no assertion, no error.

Five free entries at the receiver throughout — stranded, not congested.

d4 = 5 stable is the discriminator against normal batching, where d4 rises and falls.

And §27's stranded_age saturating is what makes it reportable. Without it the link is simply stopped; with it, a diagnostic says free capacity has been unreachable for longer than any legitimate flush interval.

56. Flagship Trace 5 — Downstream Congestion Misdiagnosed

Illustrative. The trace that looks like a credit bug and is not.

Four readings.

Every accounting identity closes. §35's row 4: only a leak breaks them, so the leak class is eliminated in one read of five differences.

The receiver is genuinely full and the pending count is zero, which is §4's row 1 — normal backpressure faithfully reported.

The first-full timestamps order the queues, and Q3 filled first at cycle 1,200 (§34). The blockage is behind Q3.

And the correct action is to investigate the consumer's downstream, not the credit machine. A team that spent a week on flow control here would find nothing wrong, because nothing in flow control is wrong — which is the most common wasted investigation in this chapter and the reason §4's row 7 and §13's row 8 exist.

57. The Assertion Inventory

Three observations.

Rows 3, 7 and 18 are identities over counters, and they are the rows that transfer to silicon. Everything else needs a simulator; these three are two register reads and a comparison — which is why the counter chain is the chapter's central design recommendation.

Rows 6 and 15 are effect forms. 20.3 §27: written against a different observable than the mechanism, so a shared designer-and-verifier misconception cannot satisfy them.

And row 18 must be per class. A total conservation assertion is satisfied by §39's cancellation — so the assertion inherits the instrumentation's flaw.

The six rows unique to this chapter, written out — the rest are 19.5's and 20.3's:

// ROW 4. No object is charged twice. A BITMAP, not a counter, because a count
// cannot answer "have I already charged this object?" (19.5 §26, §17 above).
property p_no_double_charge;
  @(posedge clk) disable iff (!por_n)
    credit_consume_fire |-> !dbg_charged_q[consume_tag];
endproperty
a_no_double_charge: assert property (p_no_double_charge);
 
// ROW 15. The SYSTEM-LEVEL stranded-capacity property — written against
// observable system state rather than against the batching mechanism, so it
// survives a redesign of the batching or the arbiter (19.5 §44).
property p_no_stranded_capacity_bounded;
  @(posedge clk) disable iff (!por_n)
    stranded_condition |-> ##[1:STRANDED_MAX] ret_service_fire[stranded_class];
endproperty
a_no_stranded_capacity_bounded: assert property (p_no_stranded_capacity_bounded);
 
// ROW 16. The progress reserve is never consumed by bulk traffic. One
// condition, and it fires at the admission that creates §36's deadlock cycle
// rather than at the deadlock itself.
property p_reserve_not_consumed_by_bulk;
  @(posedge clk) disable iff (!por_n)
    bulk_accept_fire |-> ((free_entries_q - 1) >= progress_reserve_q);
endproperty
a_reserve_not_consumed_by_bulk: assert property (p_reserve_not_consumed_by_bulk);
 
// ROW 18. Per-class conservation. Note the generate loop: one instance per
// class, because a summed version is satisfied by §39's cancellation.
generate
  for (genvar c = 0; c < NUM_CLASSES; c++) begin : g_conserve
    a_class_conservation: assert property (
      @(posedge clk) disable iff (!por_n)
        (chk_advertised[c] - chk_consumed[c] + chk_returned[c]) == credit_q[c]
    );
    // And the two exact identities, per class (§16, §19) — these are the
    // rows that also exist as readable registers in silicon (§51).
    a_class_consume_matches_alloc: assert property (
      @(posedge clk) disable iff (!por_n)
        (cnt_consume_q[c] == cnt_new_alloc_q[c])
    );
    a_class_returns_match_releases: assert property (
      @(posedge clk) disable iff (!por_n)
        (cnt_ret_generated_q[c] == cnt_rx_release_q[c])
    );
  end
endgenerate
 
// AND THE INSTRUMENTATION-INTEGRITY PROPERTIES. A diagnostic that can lie must
// be checked, because every conclusion drawn from it is downstream of its
// correctness (20.4 §42, 21.1 §43).
property p_diag_counters_monotonic;
  @(posedge clk) disable iff (!por_n)
    (cnt_consume_q >= $past(cnt_consume_q))
 && (cnt_ret_generated_q >= $past(cnt_ret_generated_q));
endproperty
a_diag_counters_monotonic: assert property (p_diag_counters_monotonic);
 
property p_stranded_age_saturates;
  @(posedge clk) disable iff (!por_n)
    (stranded_age_q == '1) |=> ((stranded_age_q == '1) || !stranded_condition);
endproperty
a_stranded_age_saturates: assert property (p_stranded_age_saturates);

Three notes on which of these matter most in a debug context.

The two exact per-class identities are the only rows that transfer to silicon (§51). They are register comparisons, so the same check that fails in simulation at the cause cycle is readable in a lab from two register reads — which is the whole reason the counter chain is a design recommendation rather than a verification one.

The reserve property fires at the admission, not at the deadlock. 19.5 §46's cycle takes many cycles to close after the reserve is breached; this property fires on the breach, which is thousands of cycles earlier and names the admission that caused it.

And the last two assert the instrumentation. A diagnostic counter that decreases, or a stranded age that wraps, makes every conclusion drawn from it void — and 21.1 §21's wrapping-age trap is exactly that failure destroying its own evidence.

58. Coverage

// ILLUSTRATIVE. The bins without which this chapter's failures are unverified.
covergroup cg_flow_control;
  // The stall that produces §14 — and a regression optimised for bandwidth
  // never generates it.
  cp_stall_length: coverpoint stall_cycles_before_accept {
    bins none = {0}; bins short = {[1:3]};
    bins long = {[4:63]}; bins very_long = {[64:$]};
  }
  // Simultaneity — should be among the MOST hit (19.5 §13).
  cp_consume_return: coverpoint {consume_fire, return_fire} {
    bins idle = {2'b00}; bins consume_only = {2'b10};
    bins return_only = {2'b01}; bins both = {2'b11};
  }
  // Credit boundaries (20.5 §22).
  cp_credit: coverpoint credit_bucket {
    bins zero = {CB_ZERO}; bins one = {CB_ONE};
    bins mid = {CB_MID};   bins at_cap = {CB_AT_CAPACITY};
  }
  // The four-way tuple states — §4's rows, as bins.
  cp_tuple_state: coverpoint fc_tuple_class {
    bins genuine_full   = {TS_FULL};
    bins leak_shape     = {TS_LEAK};        // credit 0, occupancy baseline
    bins stranded_shape = {TS_STRANDED};    // §26 — the critical bin
    bins inflated       = {TS_INFLATED};
    bins downstream     = {TS_DOWNSTREAM};  // §56 — the not-a-bug shape
  }
  // Batching — the partial flush is §26's precondition.
  cp_flush_cause: coverpoint flush_cause {
    bins threshold = {FC_THRESHOLD}; bins timer = {FC_TIMER};
    bins starved = {FC_STARVED};
  }
  cp_partial_batch: coverpoint pending_at_flush {
    bins partial = {[1:BATCH_THRESHOLD-1]};   // §26 — MUST be non-empty
    bins full    = {[BATCH_THRESHOLD:$]};
  }
  // Epoch and recovery.
  cp_stale_return: coverpoint stale_seen { bins yes = {1}; bins no = {0}; }
  cp_recovery_with_credit: coverpoint credit_at_recovery {
    bins zero = {0}; bins partial = {[1:$]};   // returns in flight
  }
  // Per class — §39's cancellation is unverified without this.
  cp_class: coverpoint credit_class { bins c[] = {[0:NUM_CLASSES-1]}; }
  cp_reserve: coverpoint reserve_engaged { bins yes = {1}; }
 
  // Crosses, each with a named bug (20.5 §31).
  x_stall_x_consume:   cross cp_stall_length, cp_consume_return;   // §14
  x_zero_x_occupancy:  cross cp_credit, cp_rx_occupancy_bucket;    // §4 rows 1/2
  x_class_x_starve:    cross cp_class, cp_tuple_state;             // §28
endgroup

Four bins that must be non-empty or this chapter's failures are unverified.

cp_stall_length.long — §14 needs a sustained stall, and a bandwidth-optimised regression never produces one.

cp_partial_batch.partial — §26's deadlock precondition. If it is empty the flush timer has never fired.

cp_tuple_state.stranded_shape — the tuple combination that is the bug, distinct from the four that are not.

And cp_consume_return.both should be among the most-hit bins (19.5 §13). If it is rare, the stimulus is not loading the link and every simultaneity bug is unverified.

59. Debug Taxonomy

Seven symptoms, each with the fastest resolving read.

Link stops after minutes or hours. Read the five differences (§12). A nonzero d1 is a leak; the first nonzero one names the stage.

Link stops and every difference is zero. Not flow control. Read the four-way tuple (§4) — full receiver with zero pending is §56's downstream blockage, and the first-full timestamps order the queues.

Sender credit exceeds capacity. Inflation. Read d3 and the stale count — negative d3 is a local duplicate; a non-zero stale count with an unchanged epoch is §23's row 5.

Receiver has free space and the sender is at zero. Stranded. Read d4 and the per-class oldest-pending age — stable d4 across all classes is batching; one class only is arbitration.

One class works and another does not. Read per-class conservation (§40). A total that closes proves nothing (§39).

Credit jumps from small to huge in one cycle. §47's unsigned wrap. Check for an advertisement in that cycle — its absence confirms it.

And it worked before the recovery and not after. §23. Read the epoch, the stale count and the exactness of the re-baseline — an unchanged epoch means the guard cannot work at all.

60. Debug Checklist

Traffic stalls on an operational link. In order:

1. Is the receiver actually full, or below capacity (§4)?
2. What is returns_pending — zero, rising, or stable (§4)?
3. Which of §4's seven rows does the tuple match?
4. Is d1 = consume − new_alloc zero (§12)?
5. If not, is the ratio consume / tx_accept a stable integer or load-varying (§17)?
6. Is d3 = rx_release − ret_generated zero (§19)?
7. If negative, how many duplicates, and is the stale count zero (§54)?
8. Is d4 zero, rising, or stable (§26)?
9. Is d5 zero at quiescence (§20)?
10. If d5 is positive, is the stale count zero — lost or rejected (§20)?
11. Are all five differences per class, or only totals (§39)?
12. Does conservation close per class (§40)?
13. What is the credit epoch, and did it change across the last recovery (§41)?
14. Are counters being differenced across an epoch boundary (§41)?
15. Is there a zero-credit snapshot, and what does it say (§42)?
16. Was the snapshot taken at the transition, or read live (§42)?
17. Does the credit exceed active capacity at any point (§24)?
18. Did credit ever jump upward with no advertisement (§47)?
19. Is the per-class oldest-pending age saturated for any class (§29)?
20. Is the age counter reset on service or on empty (§30)?
21. Has service_count moved for the starved class (§28)?
22. Is cnt_reserve_violation non-zero (§37)?
23. Is progress_occupancy zero while bulk is at capacity (§37)?
24. Which queue has the earliest first-full timestamp (§34)?
25. Is the consumer stalled, and on what (§32)?
26. Does the stall clear on its own — congestion versus the other three (§35)?
27. Do other flows progress — starvation versus deadlock (§35)?
28. Is there a cycle in the wait-for graph (§36)?
29. Does the shadow counter share the design's consume signal (§10)?
30. Are any diagnostic counters wrapping (§46)?
31. Are the differences computed signed (§46)?
32. Did DV ever hold ready low for a long stall (§58)?
33. Is cp_partial_batch.partial non-empty (§58)?
34. What observation would prove the current hypothesis wrong?

61. Common Misconceptions

"Sender credit is zero, so we have a credit bug." Four of §4's rows show zero credit and only two are credit bugs. The discriminator is receiver occupancy, and one of the four is not a flow-control problem at all.

"The shadow counter agrees, so the accounting is correct." If the shadow is fed by the design's own consume signal it agrees about when a credit is consumed — which is the thing that is wrong (§10), and every bug in this chapter survives it.

"The credit counter never exceeded capacity, so there is no accounting bug." Five bugs keep the counter inside its range forever (§24). Bounds catch consequences; identities catch causes.

"Total conservation closes, so the accounting is fine." A leak in one class and an inflation in another cancel exactly, and over a long run cancellation becomes more likely (§39). Conservation must close per domain.

"A duplicate return only wastes a little bandwidth." It manufactures capacity, stays inside every legal bound, and overflows the receiver the first time it is genuinely full — possibly days later (§18).

"Pending returns means something is wrong." It is normal in any batched design. Pending returns stable while the sender is starved and the receiver is not full is the bug (§26).

"Returns are pending, so raise the batch threshold." That makes the deadlock more likely. There is no safe threshold; the fix is a flush condition (§26, 19.5 §43).

"The age counter shows the class is being serviced." If it resets on any change to the pending count, a busy starved class shows a small age forever (§30) — and the busier it is, the better hidden.

"More credit will fix the stall." Against a leak it postpones the symptom; against a progress-reserve deadlock it makes it arrive sooner (§36).

"All the queues are full, so start at the sender." Backpressure propagates upstream, so every intermediate queue is full as a consequence. The queue that filled first is nearest the cause (§34).

"Force the credit register to reproduce it." That creates a state with no causal path, breaks every model's identity, and tests the downstream behaviour rather than the bug (§49).

"The link stalled at cycle ten thousand, so look at cycle ten thousand." The cause was at cycle 100 and d1 has been nonzero since (§44). The counters are what survive; the trace buffer wrapped long ago.

"Zero credit should raise an interrupt." Then it raises constantly, software masks it, and the genuinely diagnostic combinations are masked with it (§43).

62. Understanding Check

63. Summary and What Comes Next

A flow-control failure is a disagreement between ownership accounting and physical storage. The sender's credit is a replica; every bug is that replica diverging from the fact it describes.

Read the four-way tuple, not the credit counter. Four conditions produce zero credit, they have four different owners, and one of them is not a flow-control problem at all.

Nine event counters, five differences, and the first nonzero one names the stage. Two of the identities are exact at every cycle, so they are readable in silicon without stopping traffic — and one of them catches a duplicate return on the first occurrence rather than hours later at an overflow.

A shadow fed by the design's own consume signal agrees with the bug. Derive from the contract, or better, expose raw events and recompute offline.

Conservation must close per domain. A leak in one class and an inflation in another cancel exactly in a total, and cancellation becomes more likely over a long run.

Age the oldest pending item, not the count. An age that resets on any change hides starvation more effectively the busier the starved class is.

Order the queues by when they filled, not by whether they are full. Backpressure propagates upstream, so every intermediate queue is full as a consequence, and only a sticky first-full timestamp survives the system filling up.

And bounds catch consequences while identities catch causes. Five bugs here keep the credit counter inside its legal range forever, and the one condition a bound does catch, it catches thousands of cycles after the event.

Three failure families are now debuggable from evidence: a link that never comes up, a link that trains forever without converging, and a link that works and then stops because the accounting drifted. The remaining families in this module narrow further — per-layer credit accounting, throughput that falls short of its budget without any correctness failure, protocol violations read from a trace, and the lab, where every diagnostic in these three chapters exists only if somebody built the register for it.

• 21.4 — Credit Issues (planned) — per-layer credit-accounting bugs.

Browse the full path on the UCIe tutorials index.