Accelerator Fabrics

Chapter 18.1 treated one accelerator chiplet at a time and assumed the fabric between them worked. This chapter removes that assumption.

1. The One-Sentence Model

An accelerator fabric is a distributed resource-allocation machine. It allocates paths, queue slots, credits, output bandwidth, ordering domains and completion state — and packets are only the visible result. Every failure in this chapter is an allocation that was made, released, or refused at the wrong moment.

2. What This Chapter Owns

What is new here, and none of it exists in Module 13:

Module 13 taught flow control and arbitration on one link. This chapter has many sources, many destinations and a switching structure between them, and almost every failure below requires that: head-of-line blocking across independent outputs (§14), a route recomputed mid-packet (§10), a credit returned to the wrong resource (§24), a multicast retired on the first acceptance (§28), a wait-for cycle spanning four resources (§36), and one link's recovery pausing the package (§47).

Deadlock is the chapter's centre of gravity. §36 builds a concrete four-node cycle in which every local assertion passes, §37 gives the analysis method, and §38–§39 give the structural fix. Safety verification has nothing to say about any of it.

And multicast is treated as a first-class resource problem (§26–§29), because collective traffic is what accelerator systems actually generate and because a scalar cannot track it.

3. Sourcing

4. The Fabric

Four allocation decisions are visible in that picture — a route, a queue slot, a grant, and a credit — and §36's deadlock is a cycle among them plus the return path. Every structure that appears is a resource somebody can be waiting for.

5. Topologies, and What Each Costs

Two consequences, and no claim that UCIe mandates any of them (§3).

The topology decides where the min cut is (15.4's argument). A tree's shared upper levels are a cut that no amount of leaf bandwidth widens, which is why an all-to-one collective (§30) collapses a tree far worse than a crossbar.

And every topology except a crossbar can route the same packet more than one way, which makes routing a decision with a lifetime (§9) rather than a lookup.

6. Three Objects, Again

The hierarchy this curriculum has used since 16.3 §5, specialised to a fabric:

1 semantic fabric packet     — one logical transfer, owned by the source
    ↓
1 route decision             — made once, at acceptance, and never remade (§10)
    ↓
N flits or fragments         — how the packet is carried internally (§50)
    ↓
≥N transport attempts        — one or more per fragment, if the path retries

semantic packets per transfer     == 1
route decisions per packet        == 1        <- Section 9's failure
fragments per packet              >= 1
attempts per fragment             >= 1
SEMANTIC DELIVERIES per packet    <= 1        <- Section 45

A count at one level says nothing about another, and §58's four scoreboard models exist because of that sentence.

7. The Fabric Packet

// ILLUSTRATIVE fabric metadata. NOT a UCIe format and NOT a claim about any
// fabric's encoding (Section 3).
typedef struct packed {
  logic [SRC_W-1:0]     src;
  logic [DST_W-1:0]     dst;           // for multicast, an index into a dest set
  logic [VC_W-1:0]      vc;            // dependency class (§38)
  logic [CLASS_W-1:0]   traffic_class; // bulk / control / completion (§32)
  logic [TXN_W-1:0]     txn_id;        // the SOURCE's identity
  logic [ORDER_W-1:0]   order_domain;  // what must stay ordered with what (§40)
  logic                 multicast;
  logic [FRAG_W-1:0]    frag_idx;      // §50
  logic [FRAG_W-1:0]    frag_count;
} fabric_meta_t;

Architecture. Nine fields, and each answers a question some stage of the fabric must ask. vc and order_domain are the two most often omitted, and each has a section: without the first there is no way to separate dependency classes (§38); without the second the fabric must either order everything or order nothing (§40).

State. One register per pipeline stage, packed with the payload (§42).

Cycle behaviour. Formed at acceptance and held stable while offered (§44). Nothing downstream recomputes any field.

Contract. Routing reads dst; arbitration reads traffic_class; credits read vc; reassembly reads txn_id and the fragment fields. Five consumers, one object — which is exactly why it must travel as one object (§43).

Failure. Omitting txn_id and relying on arrival order to reassemble (§51). Or making order_domain implicit — "same source, same destination" — which is a rule the fabric then cannot be told to change.

DV. Assert stability under stall (§44); assert every field a stage uses was carried rather than derived.

8. Routing Is Configuration With a Lifetime

// ILLUSTRATIVE. A route table, and the requested/active discipline this
// curriculum has applied to lanes, memory maps and channel masks.
logic [PORT_W-1:0] active_route_q    [NUM_DESTS];
logic [PORT_W-1:0] requested_route_q [NUM_DESTS];
logic [EPOCH_W-1:0] route_epoch_q;
 
assign route_commit_allowed =
      requested_route_validated          // every entry names a usable port
   && (packets_in_flight_on_changed_routes == '0);   // §11's guard
 
always_ff @(posedge clk or negedge rst_n)
  if (!rst_n) begin
    route_epoch_q <= '0;
  end else if (route_commit_fire) begin
    active_route_q <= requested_route_q;    // atomic, whole table
    route_epoch_q  <= route_epoch_q + 1'b1;
  end

Architecture. A destination-indexed output-port table, with the same requested-versus-active split used for lane repair (14.4), memory maps (17.2 §12) and channel masks (17.4 §37). This is the fourth appearance of the pattern, which is a measure of how general it is.

State. Two tables plus an epoch counter.

Cycle behaviour. The whole table transfers in one cycle. Not entry by entry — a partial commit is a window in which two destinations disagree about the same port, and a packet accepted during it is routed inconsistently.

Contract. Every packet in flight relies on its route being stable for its whole life. That is not a property of this table; it is a property of the capture in §10.

Failure. §9.

DV. Assert the active table changes only at a commit; assert the epoch advances with it (§11).

9. Wrong RTL — the Route Table Updated Under Live Packets

// WRONG — the output port is looked up per flit, from the live table.
always_comb
  flit_out_port = active_route_q[flit.dst];    // ← recomputed for EVERY flit

If the table changes between the head and the tail of a packet, the packet splits.

Four properties, and this is a catastrophic failure rather than merely a wrong one.

Two partial packets now exist. Port 2 holds a head with no tail; port 5 holds a body and tail with no head. Neither is a valid packet and neither can ever complete.

And in a wormhole-style fabric the resources leak. The head allocated an output reservation on port 2 that only its tail can release — and the tail went to port 5. The reservation is held forever, so port 2 is permanently unusable by anyone (§18's contract, violated by absence).

The receiving side sees a malformed transfer at best. If it reassembles by position rather than identity, it may splice the head of one packet onto the tail of another (§51) — and produce a well-formed packet that is entirely wrong.

The failure requires a reconfiguration during traffic, which is rare and inevitable: link repair, degradation, load rebalancing and topology reconfiguration all cause it. A design tested with a static routing table will never see it.

10. Capture the Route, Do Not Recompute It

// ILLUSTRATIVE. The route is a DECISION made once at packet acceptance and
// carried, alongside the epoch that produced it.
typedef struct packed {
  logic                 valid;
  logic [TXN_W-1:0]     txn_id;
  logic [PORT_W-1:0]    out_port;      // captured at acceptance
  logic [EPOCH_W-1:0]   route_epoch;   // and the configuration that chose it
  logic [VC_W-1:0]      vc;
  logic [FRAG_W-1:0]    frags_sent;
} fabric_txn_t;
 
fabric_txn_t txn_q [MAX_INFLIGHT];
 
// Every flit of the packet uses the captured decision.
assign flit_out_port = txn_q[flit.txn_id].out_port;

Architecture. The route stored with the transaction rather than derived per flit. One lookup per packet instead of one per flit — cheaper as well as correct, which is unusual and worth noticing.

State. MAX_INFLIGHT entries. route_epoch is what makes a late arrival attributable to a configuration (§11).

Cycle behaviour. Written once at acceptance; read by every flit. frags_sent advances only on a flit that actually transferred — 13.4 §18's rule.

Contract. The output reservation, the credit accounting and the reassembly all assume every flit of a packet takes one port. Two independent defences again: the commit guard prevents the reconfiguration, and the capture survives it happening anyway.

Failure. §9. Also capturing out_port and not route_epoch, which leaves a returning completion unable to prove which configuration routed it.

DV. §11's properties.

11. SVA — a Packet's Route Is Stable For Its Lifetime

// MANDATORY. The property that makes Section 9 impossible.
property p_route_stable_during_packet;
  @(posedge clk) disable iff (!rst_n)
    txn_q[IDX].valid |-> ($stable(txn_q[IDX].out_port)
                       && $stable(txn_q[IDX].route_epoch)
                       && $stable(txn_q[IDX].vc));
endproperty
a_route_stable_during_packet: assert property (p_route_stable_during_packet);
 
// The active table changes only at a guarded commit.
property p_route_table_commit_only;
  @(posedge clk) disable iff (!rst_n)
    !route_commit_fire |=> $stable(active_route_q);
endproperty
a_route_table_commit_only: assert property (p_route_table_commit_only);
 
// A commit requires no packets in flight on any changed route.
property p_commit_requires_quiesce;
  @(posedge clk) disable iff (!rst_n)
    route_commit_fire |-> (packets_in_flight_on_changed_routes == '0);
endproperty
a_commit_requires_quiesce: assert property (p_commit_requires_quiesce);
 
// Every flit of a packet leaves by the captured port.
property p_all_flits_one_port;
  @(posedge clk) disable iff (!rst_n)
    flit_fire |-> (flit_out_port == txn_q[flit_txn].out_port);
endproperty
a_all_flits_one_port: assert property (p_all_flits_one_port);

Architecture. Four properties: the capture is immutable, the table is committed, the commit is guarded, and every flit obeys the capture.

Why the fourth exists given the first. The first proves the record is stable; the fourth proves the datapath actually reads it — a design can capture the route correctly and still have a downstream stage that looks up the live table, which is §9 with the record present and unused.

DV. The third needs a commit attempted with packets in flight (§59's cp_route_commit), which must be constructed.

12. Input Buffering — Three Structures

Two consequences.

VOQs and VCs solve different problems and a design usually needs both. VOQs remove head-of-line blocking; VCs break dependency cycles (§38). A fabric with VOQs and one VC still deadlocks in §36; a fabric with VCs and one shared queue per input still blocks in §13.

And the storage cost is the reason designs try to avoid them. A hybrid — a shared pool with per-output reservations — is the usual compromise, and it must guarantee a non-zero reservation for every output or it degenerates to §13 under load.

13. Head-of-Line Blocking, Worked

Input 1's shared queue, oldest first:
 
  [ P0 -> output 0 ]   output 0 is BLOCKED (no credit)
  [ P1 -> output 1 ]   output 1 is FREE
  [ P2 -> output 3 ]   output 3 is FREE
  [ P3 -> output 1 ]   output 1 is FREE
 
  A FIFO reads only the head. P0 cannot go. P1, P2, P3 do not move.
  -> input 1 delivers ZERO packets while three of its four could have gone.

Illustrative throughput impact. With uniformly random destinations across N outputs and one blocked output, the probability the head targets the blocked one is 1/N; but once blocked, the whole queue stalls for the duration. The classic result is that a single-FIFO input-queued switch saturates well below full load even with perfect arbitration.

Three readings.

The blocking is caused by an unrelated output. P1's destination is free. The only reason P1 waits is that P0 is in front of it, which is an ordering the fabric imposed and the traffic never required.

And it compounds with §32. If P0 is a bulk packet and P1 is a completion, the fabric has now delayed a progress-critical message behind a bulk one for reasons that have nothing to do with priority.

The fix is structural, not a policy. No arbitration policy helps, because the queue offers only its head. VOQs make every packet at an input independently eligible (§14).

14. Virtual Output Queues

// ILLUSTRATIVE VOQ structure. Storage is per input PER OUTPUT — the reason
// VOQs are expensive and the reason they work.
typedef struct packed {
  logic [TXN_W-1:0]  txn_id;
  logic [VC_W-1:0]   vc;
  logic [CLASS_W-1:0] traffic_class;
  logic [DATA_W-1:0] data;
  logic              last;
} voq_entry_t;
 
// Payload storage — inferred RAM, deliberately NOT reset (17.4 §14).
voq_entry_t voq_mem [NUM_INPUTS][NUM_OUTPUTS][VOQ_DEPTH];
 
// Control state — small, and reset.
logic [PTR_W-1:0] voq_wr_q  [NUM_INPUTS][NUM_OUTPUTS];
logic [PTR_W-1:0] voq_rd_q  [NUM_INPUTS][NUM_OUTPUTS];
logic [OCC_W-1:0] voq_occ_q [NUM_INPUTS][NUM_OUTPUTS];
 
// Every input's request vector is now per output — this is the whole point.
logic [NUM_OUTPUTS-1:0] input_request [NUM_INPUTS];
always_comb
  for (int i = 0; i < NUM_INPUTS; i++)
    for (int o = 0; o < NUM_OUTPUTS; o++)
      input_request[i][o] = (voq_occ_q[i][o] != '0);

Architecture. One queue per input-output pair, so an input requests every output it has work for, simultaneously. The arbiter can then match a free output to any input that wants it, which is impossible when an input offers only one head.

State. NUM_INPUTS × NUM_OUTPUTS × VOQ_DEPTH payload entries — the cost, and it grows as the product. Control state is three small registers per pair.

Cycle behaviour. Push on acceptance into the queue for the captured output (§10); pop on a grant that fired. The payload RAM is not reset — occupancy starts at zero and gates every pop, so contents are unobservable before they are written (17.4 §14's argument, and a reset loop here would be enormous).

Contract. The arbiter reads input_request; admission reads voq_occ_q[i][o] for the packet's own output, never an aggregate (17.4 §17's bug in a new place).

Failure. Sizing VOQ_DEPTH uniformly under skewed traffic, which wastes storage on cold pairs and backs up hot ones. A shared pool with per-pair reservations is the alternative and must reserve a non-zero minimum per pair.

DV. Cover every input-output pair as occupied; cover one pair full with others empty; assert admission uses the selected pair.

15. Occupancy Accounting

// ILLUSTRATIVE. One owner per counter; simultaneous push and pop explicit.
always_ff @(posedge clk or negedge rst_n)
  if (!rst_n) begin
    for (int i = 0; i < NUM_INPUTS; i++)
      for (int o = 0; o < NUM_OUTPUTS; o++) voq_occ_q[i][o] <= '0;
  end else begin
    for (int i = 0; i < NUM_INPUTS; i++)
      for (int o = 0; o < NUM_OUTPUTS; o++)
        unique case ({push_fire[i][o], pop_fire[i][o]})
          2'b10: voq_occ_q[i][o] <= voq_occ_q[i][o] + 1'b1;
          2'b01: voq_occ_q[i][o] <= voq_occ_q[i][o] - 1'b1;
          default: ;                       // 2'b00 and 2'b11 hold
        endcase
  end

Architecture. NUM_INPUTS × NUM_OUTPUTS counters, each with one owner and all four combinations enumerated.

Cycle behaviour. Both fires are handshake-qualified — a grant the output did not accept is not a pop. Crediting an unaccepted grant is the most-repeated counter bug in this curriculum.

Contract. Admission and arbitration both read these. An overcount refuses a pair with room; an undercount admits into a full one and overwrites a live packet.

Failure. Two independent if statements, whose drift is slow, monotonic, and eventually either blocks a pair permanently or corrupts it.

DV. Bounds, and the simultaneous push-pop property per pair.

16. What an Arbiter Must Guarantee

Three separate properties, and they are frequently conflated.

Fairness and liveness are different claims. A rotating arbiter is fair and can still fail liveness if the pointer advances on a grant that never transferred (§18) — the input is "fairly" skipped every time.

17. A Rotating Arbiter

// ILLUSTRATIVE per-output arbiter. Rotating priority, one grant, and the
// pointer advances ONLY on an actual transfer.
logic [NUM_INPUTS-1:0] req;              // input_request[*][this_output]
logic [NUM_INPUTS-1:0] grant;
logic [IN_W-1:0]       last_grant_q;
logic [AGE_W-1:0]      wait_age_q [NUM_INPUTS];   // saturating, per input
 
// Rotate the request vector so the search starts just after the last winner.
logic [NUM_INPUTS-1:0] rotated;
always_comb
  for (int i = 0; i < NUM_INPUTS; i++)
    rotated[i] = req[(i + last_grant_q + 1) % NUM_INPUTS];
 
logic [NUM_INPUTS-1:0] aged_out;
always_comb
  for (int i = 0; i < NUM_INPUTS; i++)
    aged_out[i] = req[i] && (wait_age_q[i] >= FAIRNESS_BOUND);
 
always_comb begin
  grant = '0;
  if (!out_credit_available)          grant = '0;              // no credit, no grant
  else if (|aged_out)                 grant = lowest_set(aged_out);   // bounded override
  else if (|rotated)                  grant = unrotate(lowest_set(rotated), last_grant_q);
end
 
always_ff @(posedge clk or negedge rst_n)
  if (!rst_n) begin
    last_grant_q <= '0;
    for (int i = 0; i < NUM_INPUTS; i++) wait_age_q[i] <= '0;
  end else begin
    // THE rule: advance only when the grant actually transferred.
    if (|grant && xfer_fire)
      last_grant_q <= onehot_to_index(grant);
 
    for (int i = 0; i < NUM_INPUTS; i++) begin
      if (req[i] && !(grant[i] && xfer_fire))
        wait_age_q[i] <= (wait_age_q[i] == AGE_MAX) ? AGE_MAX : wait_age_q[i] + 1'b1;
      else if (grant[i] && xfer_fire)
        wait_age_q[i] <= '0;
    end
  end

Architecture. Rotating priority for fairness plus a bounded age override for liveness — two mechanisms, because §16 established they are two properties. The credit check gates the grant entirely, so the arbiter never grants an output that cannot accept.

State. One pointer and NUM_INPUTS saturating ages per output. Saturating, because a wrapping age reports a fresh requester at the moment it has waited longest (13.4 §13).

Cycle behaviour. grant is combinational. Both the pointer advance and the age reset are qualified by xfer_fire.

Contract. The VOQs rely on eventual service; the sources rely on a bound. Neither is visible at this block's interface, which is why §20 asserts both.

Failure. §18. Also omitting the credit gate and relying on the downstream to refuse — which produces grants that never transfer, and then §18's bug becomes reachable even with correct pointer logic.

DV. Saturate every input and measure the worst inter-grant gap per input against FAIRNESS_BOUND.

18. Wrong RTL — Rotate on Request Rather Than on Transfer

// WRONG — the pointer advances whenever a grant is asserted, transferred or not.
always_ff @(posedge clk)
  if (|grant)
    last_grant_q <= onehot_to_index(grant);      // ← not qualified by xfer_fire

Illustrative, four inputs, with input 2 targeting a blocked output.

Input 2 is granted repeatedly, transfers nothing, and loses its priority each time.

Four properties.

It looks perfectly fair. Every input is granted in rotation, and a grant-count histogram is uniform. The unfairness is invisible in the metric people check.

Input 2 makes no progress and its age counter climbs, which is what the override in §17 exists to catch — but if the design also omitted the override, input 2 starves indefinitely while the arbiter reports perfect rotation.

And the grants are wasted output cycles. Every cycle spent granting a blocked input is a cycle another input could have used. Throughput falls as well as fairness, so the bug costs twice.

The rule generalises: this is the fifth appearance in this curriculum of advance state only on an actual transfer (13.4 §18, 17.3 §17, 17.4 §15, 18.1 §8). It recurs because the grant signal is local and the transfer signal requires the downstream's cooperation.

19. SVA — Arbiter Safety

// MANDATORY. At most one grant per output per cycle.
property p_one_grant_per_output;
  @(posedge clk) disable iff (!rst_n)
    $onehot0(grant);
endproperty
a_one_grant_per_output: assert property (p_one_grant_per_output);
 
// A grant goes only to a requester.
property p_grant_implies_request;
  @(posedge clk) disable iff (!rst_n)
    (grant != '0) |-> ((grant & req) == grant);
endproperty
a_grant_implies_request: assert property (p_grant_implies_request);
 
// A grant implies a credit was available for that output and VC.
property p_grant_implies_credit;
  @(posedge clk) disable iff (!rst_n)
    (grant != '0) |-> (credit_q[this_output][grant_vc] != '0);
endproperty
a_grant_implies_credit: assert property (p_grant_implies_credit);
 
// The rotation pointer advances only on an actual transfer (Section 18).
property p_pointer_advances_on_transfer_only;
  @(posedge clk) disable iff (!rst_n)
    $changed(last_grant_q) |-> $past(|grant && xfer_fire);
endproperty
a_pointer_advances_on_transfer_only:
  assert property (p_pointer_advances_on_transfer_only);

Architecture. Four safety properties. The fourth is the one that catches §18, and it is a single $changed implication.

Why $onehot0 and not $onehot. No grant is a legal outcome — no requests, or no credit. Asserting $onehot fails on every idle cycle.

DV. All four always-on and cheap. The third needs an attempted grant with zero credit, which requires driving the output to credit exhaustion (§59).

20. SVA — Bounded Fairness and Liveness

// LIVENESS, bounded, with assumptions stated (15.2 §36).
//
//   A1: the downstream eventually accepts, when the output is up
//   A2: credits are eventually returned for outstanding grants (§24)
//   A3: an input keeps requesting until granted
//   A4: port recovery terminates (14.2 §30)
assume property (@(posedge clk) disable iff (!rst_n)
  (|grant && (port_state_q[this_output] == PORT_UP))
    |-> ##[1:XFER_ACCEPT_BOUND] xfer_fire);
assume property (@(posedge clk) disable iff (!rst_n)
  (req[IN_UT] && !xfer_fire) |=> req[IN_UT]);
 
property p_input_served_within_bound;
  @(posedge clk) disable iff (!rst_n)
    (req[IN_UT] && (port_state_q[this_output] == PORT_UP))
      |-> ##[1:FAIRNESS_BOUND] (grant[IN_UT] && xfer_fire);
endproperty
a_input_served_within_bound: assert property (p_input_served_within_bound);
 
// Progress-critical traffic has a TIGHTER bound (§34).
property p_progress_class_served;
  @(posedge clk) disable iff (!rst_n)
    (req_progress_class && (port_state_q[this_output] == PORT_UP))
      |-> ##[1:PROGRESS_BOUND] (grant_progress && xfer_fire);
endproperty
a_progress_class_served: assert property (p_progress_class_served);

Architecture. Two liveness bounds with four explicit assumptions.

Why A2 is not optional. Without an assumption that credits return, every liveness property in this chapter is vacuously unprovable — an output with no credits never grants, forever, and the proof correctly fails. A2 makes the credit machinery's obligation explicit, and §24 is where it is verified rather than assumed.

Why the two bounds differ. PROGRESS_BOUND must be small and is guaranteed by reservation (§33); FAIRNESS_BOUND is larger and comes from rotation. One property with one bound cannot tell you which guarantee broke.

DV. Prove both. Then remove the progress reservation and confirm the second fails — verifying the reservation is load-bearing.

21. Credits Belong to a Resource

A credit is permission to occupy one slot in one specific downstream structure. It is not "capacity in the fabric", and the moment a design treats it as a scalar pool, it has lost the ability to say what is full.

Merging any two of those breaks the property the separation existed to provide. Merging VCs in particular re-creates the dependency cycle VCs were introduced to break (§38), which is why §22 indexes by both.

22. Credit State

// ILLUSTRATIVE. Credits indexed by BOTH output and VC — Section 23 is what
// happens when the indices are confused.
logic [CREDIT_W-1:0] credit_q [NUM_OUTPUTS][NUM_VCS];
 
always_ff @(posedge clk or negedge rst_n)
  if (!rst_n) begin
    for (int o = 0; o < NUM_OUTPUTS; o++)
      for (int v = 0; v < NUM_VCS; v++) credit_q[o][v] <= CREDIT_INIT[CREDIT_W-1:0];
  end else begin
    for (int o = 0; o < NUM_OUTPUTS; o++)
      for (int v = 0; v < NUM_VCS; v++) begin
        // Consume on a transfer TO this (output, VC); return on a release FROM it.
        unique case ({xfer_fire && (xfer_out == o) && (xfer_vc == v),
                      credit_return_fire && (ret_out == o) && (ret_vc == v)})
          2'b10: credit_q[o][v] <= credit_q[o][v] - 1'b1;
          2'b01: credit_q[o][v] <= credit_q[o][v] + 1'b1;
          default: ;                       // hold on none and on both
        endcase
      end
  end

Architecture. A two-dimensional array, consumed and returned by the same pair of indices. The default arm holding on the simultaneous case is what makes a consume-and-return in one cycle net to zero, which is correct and which two independent statements get wrong.

State. NUM_OUTPUTS × NUM_VCS counters, each wide enough for the advertised depth. CREDIT_INIT must equal the downstream queue's actual depth — advertising more overflows it, advertising fewer wastes it, and neither is detected by anything except §24.

Cycle behaviour. Consumed on a transfer, not a grant. Returned when the downstream releases the slot, which is a message from the far side and can be delayed arbitrarily.

Contract. The arbiter refuses to grant without a credit (§17, §19). The whole flow-control guarantee rests on the counter being exactly right, which is why §24 checks conservation rather than just bounds.

Failure. §23.

DV. §24.

23. Wrong RTL — a Credit Returned to the Wrong Resource

// WRONG — the credit is consumed from the DESTINATION's pool and returned to
// the SOURCE's index. The indices are both in scope and both plausible.
always_ff @(posedge clk) begin
  if (xfer_fire)           credit_q[xfer_out][xfer_vc] <= credit_q[xfer_out][xfer_vc] - 1'b1;
  if (credit_return_fire)  credit_q[ret_src][ret_vc]   <= credit_q[ret_src][ret_vc] + 1'b1;
  //                                  ^^^^^^^ source index, not output index
end

One resource leaks and another inflates, one credit at a time.

Four properties, and this is an excellent bug.

Nothing fails immediately. With light traffic the initial credits are never exhausted, so the design works perfectly until sustained traffic drains output 3's pool.

Then output 3 stops forever. Its credit count is zero and nothing will ever return one to it. The symptom is a permanently dead output on a fabric that reports no errors, appearing after a long run.

And the other index is over-credited, so at some point the fabric transfers into a full downstream queue and overflows it — a second, unrelated-looking failure from the same line.

Bounds checks do not catch it. credit_q[1][v] growing past CREDIT_INIT is the only bound violated, and only if the assertion checks the upper bound as well as the lower — which is exactly why §24 asserts both and then adds conservation.

24. Credit Conservation

// MANDATORY. Bounds on BOTH sides — Section 23 violates only the upper one.
property p_credit_bounded(int o, int v);
  @(posedge clk) disable iff (!rst_n)
    (credit_q[o][v] <= CREDIT_INIT);
endproperty
a_credit_bounded: assert property (p_credit_bounded(OUT_UT, VC_UT));
 
// Conservation: advertised = available + consumed-and-not-yet-returned.
// The second term is TESTBENCH knowledge — it counts what is downstream.
property p_credit_conserved(int o, int v);
  @(posedge clk) disable iff (!rst_n)
    (credit_q[o][v] + tb_outstanding_at_downstream(o, v) == CREDIT_INIT);
endproperty
a_credit_conserved: assert property (p_credit_conserved(OUT_UT, VC_UT));
 
// A transfer consumes from the resource it targeted.
property p_credit_consumed_from_target;
  @(posedge clk) disable iff (!rst_n)
    xfer_fire |=> (credit_q[$past(xfer_out)][$past(xfer_vc)]
                   == $past(credit_q[$past(xfer_out)][$past(xfer_vc)]) - 1
                   || $past(credit_return_fire && (ret_out == xfer_out) && (ret_vc == xfer_vc)));
endproperty
a_credit_consumed_from_target:
  assert property (p_credit_consumed_from_target);
 
// No transfer without a credit.
property p_no_transfer_without_credit;
  @(posedge clk) disable iff (!rst_n)
    xfer_fire |-> ($past(credit_q[xfer_out][xfer_vc]) != '0);
endproperty
a_no_transfer_without_credit: assert property (p_no_transfer_without_credit);

Architecture. Four properties: two-sided bounds, conservation, correct-index consumption, and the flow-control guarantee.

Why conservation is the valuable one. Bounds catch §23 only after enough drift to breach CREDIT_INIT, which can take a very long run. Conservation fires on the first mis-indexed return, because the sum stops matching immediately.

Why the outstanding term must be testbench knowledge. The design cannot know how many slots are occupied downstream — that is exactly the information credits exist to approximate. A model that counts it directly is the reference the design is being checked against.

DV. All four always-on, per output and VC. Run long enough to drain a pool, because §23's symptom is a slow leak.

25. Multicast Is Not N Unicasts

Accelerator systems generate genuine one-to-many traffic: command fan-out, parameter distribution, synchronisation.

Two consequences.

Replication position is a bandwidth-against-buffering trade. Replicating at the source costs N × source bandwidth; replicating at the switch costs switch buffering; replicating at destination groups is in between. No position is universally right, and the choice determines where the congestion appears.

And the retirement condition is what makes multicast a resource problem. One destination stalling holds state for all of them — which is §27's bug when handled wrongly and §33's starvation risk when handled correctly.

26. The Multicast Pending Bitmap

// ILLUSTRATIVE. A BITMAP, not a counter — the same argument as 18.1 §35 and
// 16.2 §21, for the third time in this curriculum.
typedef struct packed {
  logic                    valid;
  logic [TXN_W-1:0]        txn_id;
  logic [NUM_DESTS-1:0]    pending_dest;    // who has NOT accepted
  logic [NUM_DESTS-1:0]    dest_set;        // who was addressed
  logic [EPOCH_W-1:0]      route_epoch;
} mcast_txn_t;
 
mcast_txn_t mcast_q [MAX_MCAST];
 
always_ff @(posedge clk)
  if (mcast_alloc_fire) begin
    mcast_q[alloc_idx].valid        <= 1'b1;
    mcast_q[alloc_idx].pending_dest <= alloc_dest_set;
    mcast_q[alloc_idx].dest_set     <= alloc_dest_set;
  end else if (dest_accept_fire
               && mcast_q[acc_idx].valid
               && mcast_q[acc_idx].pending_dest[acc_dest]) begin   // GUARDED
    mcast_q[acc_idx].pending_dest[acc_dest] <= 1'b0;
  end
 
assign mcast_complete = mcast_q[idx].valid && (mcast_q[idx].pending_dest == '0);

Architecture. One bit per destination, cleared by that destination's acceptance. The guard — pending_dest[acc_dest] in the condition — makes a duplicate acceptance idempotent, which matters because a transport retry can deliver the same acceptance twice.

State. MAX_MCAST entries of NUM_DESTS bits. Both pending_dest and dest_set are kept: the first is progress, the second is the original membership, needed for diagnostics and for any retry of the remaining destinations.

Cycle behaviour. Set as a whole at allocation; cleared one bit at a time. Retirement requires pending_dest == '0', which is §28.

Contract. The source's transaction entry is held until every destination has accepted. A destination that never accepts holds the entry indefinitely — which is correct behaviour and which makes multicast entries a starvation-sensitive resource (§33).

Failure. §27. Also using a counter, which lets a duplicated acceptance retire the transaction with a destination still unserved — the same failure as 18.1 §35's barrier and 16.2 §21's response counter.

DV. §28's properties; cover a duplicate acceptance and a partial fan-out.

27. Wrong Multicast — Retire on the First Acceptance

// WRONG — the source entry is freed as soon as any destination accepts.
always_ff @(posedge clk)
  if (dest_accept_fire)
    mcast_q[acc_idx].valid <= 1'b0;        // ← one acceptance, all done?

Illustrative: a command multicast to A, B and C, where A accepts first.

Four properties.

Nothing reports an error. A got its command and acknowledged it. The source's transaction completed successfully by its own accounting.

And the symptom appears somewhere entirely different. B and C never received a command they are waiting for, so a later barrier hangs (18.1 §33) or a phase produces partial results. The cause is a fabric retirement condition; the symptom is a compute-level hang.

It is worse when the command has side effects. If the multicast configured something, the package is now in a mixed configuration — A configured, B and C not — which is a class of failure that can persist across many subsequent operations.

And a counter-based version fails the same way for a different reason (§26): a duplicate acceptance from A drives a count of three down by one too many, and the transaction retires with C still unserved.

28. SVA — Multicast Retires Only When All Destinations Are Served

// MANDATORY. Retirement requires an empty pending set.
property p_mcast_retire_requires_empty;
  @(posedge clk) disable iff (!rst_n)
    mcast_retire_fire |-> (mcast_q[retire_idx].pending_dest == '0);
endproperty
a_mcast_retire_requires_empty:
  assert property (p_mcast_retire_requires_empty);
 
// A duplicate acceptance changes nothing (Section 26's guard).
property p_duplicate_accept_idempotent;
  @(posedge clk) disable iff (!rst_n)
    (dest_accept_fire && !mcast_q[acc_idx].pending_dest[acc_dest])
      |=> $stable(mcast_q[acc_idx].pending_dest);
endproperty
a_duplicate_accept_idempotent:
  assert property (p_duplicate_accept_idempotent);
 
// Only an addressed destination can clear a bit.
property p_only_addressed_dest_clears;
  @(posedge clk) disable iff (!rst_n)
    (dest_accept_fire && !mcast_q[acc_idx].dest_set[acc_dest])
      |=> $stable(mcast_q[acc_idx].pending_dest);
endproperty
a_only_addressed_dest_clears:
  assert property (p_only_addressed_dest_clears);
 
// Every addressed destination eventually accepts, under assumptions (§20's A1-A4).
property p_all_dests_eventually_served;
  @(posedge clk) disable iff (!rst_n)
    mcast_alloc_fire |-> ##[1:MCAST_BOUND] mcast_complete_for(alloc_idx);
endproperty
a_all_dests_eventually_served:
  assert property (p_all_dests_eventually_served);

Architecture. Four properties: the retirement condition, idempotence, membership, and bounded completion.

Why the third is not paranoia. With several multicasts in flight, an acceptance carries an index and a destination. A mis-indexed acceptance clears a bit in the wrong transaction, retiring it early — §27's failure through a different door, and only a membership check catches it.

DV. The second needs a duplicated acceptance; the fourth needs a destination that stalls and then resumes. Both must be injected (§59).

29. Collective Traffic Creates Hotspots by Design

Accelerator workloads generate structured patterns, not random ones.

Illustrative, all-to-one with 8 sources. Each source offers X bytes/s to one destination:

offered to that destination = 8X
that output's capacity      = X            (illustratively, one link's worth)
oversubscription            = 8×
 
sustained throughput  = X   (the output's capacity)
per-source share      = X/8
queueing              = builds until backpressure reaches all 8 sources
other 7 outputs       = IDLE

Three readings.

The fabric's aggregate capacity is irrelevant to this pattern. Seven outputs are idle and cannot help. This is 15.4's min-cut with a cut of one link.

And backpressure propagates to all eight sources, so a reduction slows every participant — which then delays the barrier that follows it (18.1 §37).

All-to-all is the opposite stress: every output loaded at once, so the bisection rather than any single output is the constraint. A topology tuned for one pattern is frequently poor at the other, and both occur in the same workload.

30. Why Uniform Random Traffic Is Not a Verification Plan

A fabric that passes uniform random traffic has been shown to work in the case it was least likely to fail. Every failure in this chapter needs contention, structure, or both — and a performance verification plan built on random traffic will report healthy numbers for a fabric that collapses on its actual workload.

31. Traffic Classes

The last two classes release resources; the first consumes them. 11.3 §28's principle, at a fabric: a message that frees a resource must never queue behind one that acquires resources.

No claim is made that UCIe defines these classes (§3). The classification is the design's, and what matters is that one exists and that the releasing classes are protected.

32. Wrong Priority — Bulk Data First

// WRONG at system scope. Completion and synchronisation traffic can be starved.
assign grant = bulk_req ? lowest_set(bulk_req) : lowest_set(other_req);

1. A large transfer saturates output 3.
2. Completions returning through output 3 are never granted.
3. Sources waiting on those completions cannot retire their transactions.
4. Their transaction entries, VOQ slots and credits stay allocated.
5. New bulk traffic from those sources cannot be admitted — no entries free.
6. The bulk transfer itself eventually needs a completion held at step 2.
7. -> deadlock, on a fabric with enormous unused aggregate bandwidth.

Four properties.

Every participant is correct and no safety assertion fires. Nothing is corrupted, duplicated or misrouted. The fabric is simply stopped, and safety verification has nothing to say about it.

The metric picture is actively misleading. Output 3 shows high utilisation; the other outputs show low. A capacity-planning conclusion drawn from that is "we need more bandwidth on output 3", which is wrong — the fabric has plenty and is spending it on the wrong class.

It is delayed and load-dependent. At moderate load, completions get through in the gaps. The failure appears at saturation, which is the operating point a performance campaign creates.

And unlike 13.4 §16's single-link version, this one does not self-resolve. There, a full buffer eventually throttled admission and let the starved class through. Here the starved class is what would free the buffers, so the pressure never releases.

33. Progress Reservation

// ILLUSTRATIVE. A reserved credit pool and a bounded arbitration override for
// classes that RELEASE resources. Generic — no standard is claimed to require it.
logic [CREDIT_W-1:0] bulk_credit_q     [NUM_OUTPUTS];
logic [CREDIT_W-1:0] progress_credit_q [NUM_OUTPUTS];   // reserved, non-zero
 
logic [AGE_W-1:0]    progress_age_q    [NUM_OUTPUTS];   // saturating
 
// Bulk may use only the bulk pool; progress traffic may use EITHER.
assign bulk_may_send     = (bulk_credit_q[o] != '0);
assign progress_may_send = (progress_credit_q[o] != '0) || (bulk_credit_q[o] != '0);
 
// A bounded override: progress wins once it has waited too long.
assign progress_override = (progress_age_q[o] >= PROGRESS_BOUND);

Architecture. Two mechanisms. The split pool guarantees capacity that bulk can never consume; the override guarantees service even if the reserved pool is momentarily empty. Either alone leaves a hole.

State. Two credit counters and one saturating age per output. The reservation need not be large — it needs to be non-zero and guaranteed, because what must be broken is a dependency cycle, and a cycle is broken by any guaranteed service.

Cycle behaviour. Progress traffic may borrow from the bulk pool when available, so the reservation costs nothing when bulk is idle. The asymmetry is deliberate: bulk may never borrow from the progress pool.

Contract. §20's PROGRESS_BOUND property depends on this. Set progress_credit_q initialisation to zero and that property becomes unprovable — which is the DV check that the reservation is real.

Failure. Reserving so much that bulk throughput collapses — the over-correction, and it is a performance failure rather than a deadlock, which is the better direction to err in and still worth measuring (§55).

DV. Saturate with bulk, trickle completions, confirm progress_age_q never reaches AGE_MAX. Then zero the reservation and confirm the deadlock in §36 becomes reachable.

34. SVA — Progress Traffic Is Served

// MANDATORY. The reserved pool is never consumed by bulk.
property p_bulk_never_uses_progress_pool;
  @(posedge clk) disable iff (!rst_n)
    (xfer_fire && (xfer_class == CLASS_BULK))
      |=> $stable(progress_credit_q[$past(xfer_out)]);
endproperty
a_bulk_never_uses_progress_pool:
  assert property (p_bulk_never_uses_progress_pool);
 
// The reservation is non-zero — a configuration check, not a runtime one.
initial begin
  assert (PROGRESS_CREDIT_INIT > 0)
    else $fatal(1, "progress reservation is zero — Section 32 is reachable");
end
 
// Progress traffic is served within its bound (§20's assumptions apply).
property p_progress_served;
  @(posedge clk) disable iff (!rst_n)
    (progress_req[OUT_UT] && (port_state_q[OUT_UT] == PORT_UP))
      |-> ##[1:PROGRESS_BOUND] (progress_grant[OUT_UT] && xfer_fire);
endproperty
a_progress_served: assert property (p_progress_served);

Architecture. A runtime property, a configuration assertion, and the liveness bound.

Why the elaboration check earns its place. PROGRESS_CREDIT_INIT = 0 is a parameterisation that silently removes the guarantee while leaving every line of code that implements it. Catching it at build time costs nothing and is the difference between a design that has the protection and one that only appears to.

DV. All three. The third is the property that proves §32 cannot occur, and it should be run at saturation.

35. The Wait-For Graph — a Concrete Cycle

A deadlock that needs no unfairness, no bug in any block, and no protocol violation.

Setup: input A holds a packet for output X.
       Output X's downstream queue is full — no credits.
       The credit return for X comes from agent B.
       B's return message must go out through output Y.
       Output Y's queue is full of requests waiting on completions from A.
 
WAIT-FOR GRAPH:
 
   A's input buffer  --waits for-->  output X credit
   output X credit   --waits for-->  B's credit return
   B's credit return --waits for-->  output Y slot
   output Y slot     --waits for-->  A's completion
   A's completion    --waits for-->  A's input buffer   (A cannot proceed)
 
   -> a cycle of length 5.

Four properties, and this is the chapter's centre.

Every local assertion passes. Each arbiter grants at most one requester, only to requesters, only with credit. Each credit counter is bounded and conserved. Each queue respects its depth. Not one property in §19, §24 or §28 is violated, because none of them is about a cycle.

Nothing is corrupted and nothing progresses. This is a pure liveness failure. A verification plan consisting of safety properties will pass a deadlocked fabric.

The cycle spans four resource classes — input buffers, credits, output slots and completions. No single block can see it, which is why the analysis must be structural (§36).

And it appears only at saturation. At moderate load some resource always has slack and the cycle never closes. It is a full-load phenomenon, discovered late.

36. Channel Dependency Analysis

The method, stated generally.

1. Enumerate the RESOURCE CLASSES a packet can hold or wait for:
     input buffers, per-VC output buffers, credits, output reservations,
     completion-tracking entries, reassembly slots.
 
2. Draw an edge R1 -> R2 whenever holding R1 can require waiting for R2.
 
3. If the graph has a CYCLE, deadlock is reachable under some traffic.
 
4. Break every cycle by either:
     (a) an ordering on resource acquisition that no packet may violate, or
     (b) a class of resource that is RESERVED for the traffic that releases
         others — an escape path that cannot itself be blocked.

Two consequences for verification.

The graph is a design artefact, not a simulation result. It is built by reading the architecture, and it finds cycles that no test reaches. That is its value: §35's cycle needs a specific saturation pattern to manifest and is visible in the graph immediately.

And every claimed cycle-breaking mechanism becomes a property to assert. If VCs break a cycle, the property is that the two classes never share a buffer (§39). If a reservation breaks it, the property is §34.

37. Virtual Channels Separate Dependency Classes

Virtual channels are not a performance feature that happens to help with deadlock. Their primary architectural purpose is to give dependent traffic classes independent buffering, so that one class blocking cannot block the other.

The rule that follows: classes with a dependency between them must not share a buffer or a credit pool. A response is generated because a request arrived, so responses depend on requests — and if requests also depend on responses (because responses free the entries requests need), the two together form a cycle unless they are separated.

38. Wrong Design — Requests and Responses on One VC

// WRONG — one buffer and one credit pool for both directions of the dependency.
assign vc_sel = 1'b0;                       // everything on VC 0

1. Under saturation, output X's VC 0 queue fills with REQUESTS.
2. RESPONSES to earlier requests also need VC 0 on output X. No room.
3. The requesters waiting on those responses cannot retire their entries.
4. They therefore cannot accept the responses even if delivered, and
   they continue holding the buffers the new requests would need.
5. -> the request queue stays full, the responses stay blocked, and the
     dependency is circular.

Three properties.

It is 16.3 §26's cross-link deadlock at fabric scope, and it recurs because a single VC is simpler, cheaper, and works perfectly below saturation.

Adding buffer depth does not fix it, it only delays it. The cycle is structural: a deeper queue takes longer to fill and deadlocks the same way. This is the clearest demonstration that deadlock is not a capacity problem.

And the fix is small. Two VCs with separate credit pools, requests on one and responses on the other, and the graph becomes acyclic. The cost is one extra credit counter per output and a VC field in the metadata (§7).

39. Ordering Domains

Global ordering is safe and ruinous. No ordering is fast and wrong. The answer is an explicit domain.

// ILLUSTRATIVE. Packets in the same order domain must not be reordered relative
// to each other; packets in different domains may be reordered freely.
logic [ORDER_W-1:0] order_domain;      // carried in the metadata (§7)
 
// Illustrative per-domain in-order tracking at the destination.
logic [SEQ_W-1:0] expected_seq_q [NUM_DOMAINS];

The domain is where the design records what actually depends on what (16.3 §17's principle). Making it explicit is what allows the fabric to reorder the large majority of traffic that has no dependency at all.

40. Wrong Architecture — One Globally Ordered Queue

// WRONG for performance — a single ordered queue guarantees correctness by
// serialising everything, including traffic that has no relationship at all.
assign can_send = (txn_id == global_next_expected_q);

Illustrative. Eight accelerators sending to eight different destinations, all independent.

Three readings.

It is not a bug and it is not acceptable. Every result is correct. The fabric delivers an eighth of what it was built for, and no assertion fires.

It is the most tempting wrong answer under schedule pressure, because it makes an entire class of ordering questions go away at a stroke.

And it usually appears as a "temporary" simplification. The performance cost is discovered at integration, by which point the ordering domains were never designed and the information about what actually depends on what has been lost.

41. Metadata Must Travel With Its Payload

// ILLUSTRATIVE. Metadata and payload as ONE packed object through every stage.
typedef struct packed {
  fabric_meta_t meta;
  logic [DATA_W-1:0] data;
  logic              last;
} fabric_flit_t;
 
fabric_flit_t stage_q [PIPE_DEPTH];
 
always_ff @(posedge clk)
  if (stage_advance)
    for (int s = PIPE_DEPTH-1; s > 0; s--)
      stage_q[s] <= stage_q[s-1];

Architecture. One packed object shifted as a unit. There is no way to advance the route without advancing the payload, because they are the same register.

State. PIPE_DEPTH copies — more area than a narrow tag beside a wide bus, and that cost buys a structural guarantee.

Cycle behaviour. All fields advance on one enable. No field has its own valid, enable or bypass.

Contract. Every stage associates a payload with a destination, a VC and a class. If that association can be wrong, every downstream decision is made about the wrong thing — and the payload will be perfectly intact.

Failure. §42.

DV. §43, plus an end-to-end check that the metadata recovered at the destination equals what was assigned at acceptance.

42. Wrong RTL — Route Metadata One Stage Shorter

// WRONG — the metadata path is one stage shorter than the payload path.
always_ff @(posedge clk) begin
  meta_q1 <= meta_in;    meta_q2 <= meta_q1;                      // 2 stages
  data_q1 <= data_in;    data_q2 <= data_q1;   data_q3 <= data_q2; // 3 stages
end
assign out_meta = meta_q2;      // ← off by one, forever
assign out_data = data_q3;

Every flit after the first carries the previous flit's destination.

Four properties, and it is catastrophic rather than merely wrong.

The payload is perfect. Every bit crossed correctly, CRC clean, no retries. It is being delivered to the wrong place.

And it is not a malformed packet. The receiving output gets a well-formed flit with a valid VC and class. Nothing rejects it, so it is processed as legitimate traffic belonging to a different transaction.

Packets also split, because a multi-flit packet's flits now target different outputs — which produces §9's partial-packet resource leak as a secondary effect.

It is systematic and one-off, which makes it nearly impossible to spot in a waveform — each individual cycle looks entirely reasonable — and trivial to find once suspected.

43. SVA — Payload and Metadata Stable Under Stall

// MANDATORY. An offered flit does not change while it is waiting.
property p_flit_stable_under_stall;
  @(posedge clk) disable iff (!rst_n)
    (out_valid && !out_ready) |=> (out_valid && $stable({out_meta, out_data}));
endproperty
a_flit_stable_under_stall: assert property (p_flit_stable_under_stall);
 
// Metadata and payload advance together.
property p_meta_payload_move_together;
  @(posedge clk) disable iff (!rst_n)
    $changed(out_data) |-> $changed(out_meta) || meta_legitimately_repeats;
endproperty
 
// The destination recovered at the output equals the one assigned at acceptance.
// tb_dst_of() is TESTBENCH knowledge (Section 41).
property p_destination_survives_the_fabric(int unsigned rid);
  @(posedge clk) disable iff (!rst_n)
    (out_valid && (tb_ref_id == rid)) |-> (out_meta.dst == tb_dst_of(rid));
endproperty
a_destination_survives_the_fabric:
  assert property (p_destination_survives_the_fabric(REF_UT));

Architecture. Stability, joint movement, and the end-to-end destination check.

Why the third must use a testbench reference. The wire carries a destination field. The knowledge that "this payload was addressed to X at acceptance" belongs to whatever generated the traffic — synthesising it into the design would build a second copy of the routing logic, with the same bug.

DV. §42's off-by-one is caught by the third property on the second flit of any stream — so it needs at least two back-to-back flits with different destinations, which is a trivial test that a single-packet smoke test does not contain.

44. The UCIe Boundary — Attempts Are Not Semantic Objects

A fabric packet leaving the package crosses UCIe and becomes a transport object (16.4 §8's hierarchy).

A UCIe retry must not: allocate another fabric transaction, consume another multicast destination (§26), advance a reassembly bitmap (§51), consume another credit (§22), or change any ordering state (§39).

The construction is the same as everywhere in this curriculum: the fabric acts on semantic delivery, never on physical arrival (16.3 §11). And the mode caveat applies — in Raw Mode there is no Adapter history to lean on (16.4 §6), so the fabric must supply the equivalent.

45. SVA — Transport Retries Are Semantically Invisible

// MANDATORY. A duplicate transport attempt allocates nothing and consumes nothing.
property p_retry_allocates_no_transaction;
  @(posedge clk) disable iff (!rst_n)
    (transport_arrived && duplicate_attempt) |=> $stable(txn_alloc_count);
endproperty
a_retry_allocates_no_transaction:
  assert property (p_retry_allocates_no_transaction);
 
property p_retry_consumes_no_credit;
  @(posedge clk) disable iff (!rst_n)
    (transport_arrived && duplicate_attempt)
      |=> $stable(credit_q[OUT_UT][VC_UT]);
endproperty
a_retry_consumes_no_credit: assert property (p_retry_consumes_no_credit);
 
property p_retry_changes_no_multicast_state;
  @(posedge clk) disable iff (!rst_n)
    (transport_arrived && duplicate_attempt)
      |=> $stable(mcast_q[IDX].pending_dest);
endproperty
a_retry_changes_no_multicast_state:
  assert property (p_retry_changes_no_multicast_state);

Architecture. Three properties covering the three resources a duplicate could wrongly consume.

Why credits deserve their own property. A duplicate consuming a credit leaks that credit permanently — the downstream slot it represents was never actually occupied a second time, so nothing will return it. §23's leak, arriving through the retry path instead.

DV. All three need a retry while fabric transactions are live, which is §59's cp_retry_during_traffic and never occurs spontaneously.

46. Recovery on One Output

One output's UCIe link enters recovery (14.2). Every other output is unaffected by anything except a design that couples them.

A per-output failure must have a per-output blast radius. §47 is the design that makes it global.

47. Wrong Design — a Global Fabric Pause

// WRONG — any output in recovery stops the whole fabric.
assign fabric_accept = ready_terms && !(|port_recovering);

Illustrative, 8 outputs, each recovering an illustrative 1% of the time independently:

P(all 8 available) = 0.99^8 ≈ 0.923
fraction of time this design accepts NOTHING ≈ 7.7%
fraction lost with per-output handling        ≈ 1% (only that output's traffic)

And it worsens with scale: at 16 outputs, 0.99^16 ≈ 0.851 — nearly 15% lost, to avoid 1% of unavailability.

Three properties.

It is functionally correct. No packet is sent to a recovering output; nothing is corrupted; every transfer completes eventually. A functional regression passes.

The failure scales in the wrong direction with the parameter meant to deliver the bandwidth — the same shape as 17.4 §29's global maintenance stall, and it is worth recognising as a recurring architectural anti-pattern: a local unavailability given a global scope.

And the diagnostic signature is misleading. Utilisation is low across all outputs simultaneously, which reads as a source-side shortage. Only a per-output recovery counter correlated against fabric accept-stall cycles reveals it (§55).

48. Per-Output Health

// ILLUSTRATIVE per-output state. Four states because four responses differ.
typedef enum logic [1:0] {
  PORT_UP         = 2'd0,
  PORT_RECOVERING = 2'd1,   // temporarily unusable — HOLD, do not fail
  PORT_DEGRADED   = 2'd2,   // usable, lower capacity — Section 53
  PORT_DOWN       = 2'd3    // unusable — explicit policy required
} port_state_e;
 
port_state_e port_state_q [NUM_OUTPUTS];

Architecture. Four states because four distinct responses are required. DEGRADED is a serving state — the output works, more slowly — and a design that lacks it must classify a degraded link as either fully healthy (and over-schedule it) or down (and lose it entirely).

Contract. The arbiter, the load balancer, the failure policy and the liveness assumptions in §20 all read this. Four consumers, four states.

Failure. Collapsing to one bit, which forces a single behaviour for recovery and permanent loss — either hanging on a dead port or failing traffic during a routine retrain.

DV. Cover all four; confirm queued packets survive RECOVERING and are explicitly failed on DOWN.

49. Rerouting Constraints

If alternate paths exist, rerouting is possible — and it is constrained.

A packet that has begun transmission must not be rerouted mid-flight — that is §9's split packet arrived at deliberately. Rerouting applies to packets not yet started, and a design that cannot tell the difference must not reroute at all.

50. Multi-Link Striping and Fragments

A large transfer may be striped across several links for bandwidth.

// ILLUSTRATIVE fragment descriptor. NOT a UCIe striping rule (Section 3).
typedef struct packed {
  logic [TXN_W-1:0]  txn_id;
  logic [FRAG_W-1:0] frag_idx;
  logic [FRAG_W-1:0] frag_count;
  logic [DATA_W-1:0] data;
} fabric_frag_t;

Architecture. Identity, position and extent per fragment. All three are required: identity to associate, position to reassemble, extent to know when it is complete.

Contract. Fragments of one transaction take different links with independent latency, congestion and retry behaviour, so they arrive out of order and possibly interleaved with other transactions' fragments. Order carries no information; identity and index do.

Failure. §51.

DV. Cover fragments arriving in order, reversed, and interleaved with another transaction.

51. Wrong Striping — Reassembly Without Fragment Identity

// WRONG — fragments are reassembled in arrival order into a per-link buffer,
// then concatenated.
always_ff @(posedge clk)
  if (frag_valid)
    reasm_buf[reasm_ptr] <= frag_data;   // ← position, not frag_idx

Fragments arriving out of order are reassembled in the wrong order.

Four properties.

Every fragment's CRC passes. Each crossed its link perfectly and contains exactly the bytes it was sent with. The payload is scrambled at the block level, not corrupted at the bit level — which no transport check can see.

And a duplicate fragment satisfies a missing one. A counter-based "have I received four fragments?" check is satisfied by F0, F1, F1, F2 — so a lost fragment is reported as a complete transaction with duplicated content.

The result may be plausible. For structured data, a block-swapped payload can pass a coarse sanity check and fail only in the final answer — which is attributed to the computation rather than the fabric.

The fix is a bitmap, not a counter (§52) — the fourth appearance of that argument in this curriculum (16.2 §21, 18.1 §35, §26, and here).

52. Reassembly Bitmap

// ILLUSTRATIVE. Position-indexed storage and a received BITMAP.
logic [MAX_FRAGS-1:0] received_q [MAX_INFLIGHT];
logic [DATA_W-1:0]    reasm_mem  [MAX_INFLIGHT][MAX_FRAGS];
 
always_ff @(posedge clk)
  if (frag_valid && txn_q[frag.txn_id].valid) begin
    // Indexed by frag_idx — NOT by arrival order.
    reasm_mem[frag.txn_id][frag.frag_idx] <= frag.data;
    // GUARDED set: a duplicate finds the bit already set and changes nothing.
    if (!received_q[frag.txn_id][frag.frag_idx])
      received_q[frag.txn_id][frag.frag_idx] <= 1'b1;
  end
 
assign reasm_complete =
    (received_q[idx] & ((1 << txn_q[idx].frag_count) - 1))
    == ((1 << txn_q[idx].frag_count) - 1);

Architecture. Storage indexed by fragment index and a bitmap of what has arrived. A duplicate writes the same data to the same slot and sets an already-set bit — idempotent by construction.

State. MAX_INFLIGHT × MAX_FRAGS bits plus the payload storage. The payload is not reset, for the same reason as §14: the bitmap gates every read and starts at zero.

Cycle behaviour. Set on arrival, checked for completeness against frag_count. A fragment for a dead transaction is ignored entirely, which is the same stale-arrival discipline as everywhere else.

Contract. Nothing downstream may consume the payload until reasm_complete. A design that begins consuming early reads slots that have not arrived.

Failure. §51's counter. Also masking against a fixed width rather than the transaction's own frag_count, which reports incomplete transactions as complete when a transfer uses fewer than the maximum fragments.

DV. §53's property; cover reversed arrival, a duplicate, and a missing fragment.

53. SVA — Reassembly and Load Balancing

// MANDATORY. Completion requires the full bitmap for THIS transaction's count.
property p_reassembly_requires_full_bitmap;
  @(posedge clk) disable iff (!rst_n)
    reasm_deliver_fire |-> ((received_q[idx] & frag_mask(txn_q[idx].frag_count))
                            == frag_mask(txn_q[idx].frag_count));
endproperty
a_reassembly_requires_full_bitmap:
  assert property (p_reassembly_requires_full_bitmap);
 
// A duplicate fragment changes nothing.
property p_duplicate_fragment_idempotent;
  @(posedge clk) disable iff (!rst_n)
    (frag_valid && received_q[frag.txn_id][frag.frag_idx])
      |=> $stable(received_q[frag.txn_id]);
endproperty
a_duplicate_fragment_idempotent:
  assert property (p_duplicate_fragment_idempotent);
 
// A fragment for a retired transaction is ignored.
property p_stale_fragment_ignored;
  @(posedge clk) disable iff (!rst_n)
    (frag_valid && !txn_q[frag.txn_id].valid) |=> $stable(received_q);
endproperty
a_stale_fragment_ignored: assert property (p_stale_fragment_ignored);

Architecture. Three properties: completeness against the transaction's own count, idempotence, and stale rejection.

Why the first masks by frag_count. A transaction using three of a possible eight fragments must complete at three. Masking against MAX_FRAGS would leave it permanently incomplete, and masking against nothing would let it complete at one.

DV. All three; the second and third must be injected.

54. Load Balancing Needs More Than One Signal

Where alternate paths exist, the choice must use several signals.

// ILLUSTRATIVE. A composite score, not a single signal.
always_comb
  for (int p = 0; p < NUM_PATHS; p++)
    path_score[p] = (port_state_q[p] == PORT_UP)      ? (credit_q[p] + recent_xfer_q[p])
                  : (port_state_q[p] == PORT_DEGRADED) ? ((credit_q[p] + recent_xfer_q[p]) >> 1)
                  : '0;                                 // RECOVERING or DOWN: unusable

And the ordering constraint overrides the score entirely: packets in the same order domain must take the same path (§39, §49), or the balancer has reordered traffic the design promised not to reorder. A balancer that ignores order domains is fast and wrong.

55. Performance Instrumentation

// Diagnostic only. Per input, per output, per VC — three keys, three questions.
logic [63:0] accepted_bytes_q  [NUM_INPUTS];
logic [63:0] delivered_bytes_q [NUM_OUTPUTS];
logic [63:0] arb_stall_q       [NUM_OUTPUTS];   // requested, not granted
logic [63:0] credit_stall_q    [NUM_OUTPUTS][NUM_VCS];  // granted-eligible, no credit
logic [63:0] recovery_stall_q  [NUM_OUTPUTS];   // port not UP
logic [63:0] progress_stall_q  [NUM_OUTPUTS];   // progress class waiting  <- §32
logic [63:0] hol_stall_q       [NUM_INPUTS];    // head blocked, others eligible <- §13
logic [63:0] mcast_pending_q   [NUM_DESTS];     // cycles a dest held a multicast
logic [63:0] fabric_accept_stall_q;             // ingress refused  <- §47

Two properties.

Every counter's incrementing event is defined, and delivered_bytes_q increments on an actual transfer, never a grant (15.3 §14) — a counter incremented on grant reports bandwidth §18's design never delivered.

And progress_stall_q is the highest-value counter here. A rising value is the precursor to §32's deadlock, visible long before the system stops.

56. One Primary Stall Cause Per Cycle

// ILLUSTRATIVE. 15.5 §10's causal-priority classifier, per output.
typedef enum logic [3:0] {
  FAB_TRANSFER   = 4'd0,
  FAB_NO_REQUEST = 4'd1,   // nothing wanted this output   <- must be early
  FAB_PORT_DOWN  = 4'd2,
  FAB_RECOVERING = 4'd3,
  FAB_ROUTE_QUIESCE = 4'd4, // deliberate hold for a commit (§8)
  FAB_NO_CREDIT  = 4'd5,
  FAB_ARB_LOST   = 4'd6,   // requested, another input won — ordinary contention
  FAB_MCAST_WAIT = 4'd7,   // held for an unserved destination (§26)
  FAB_REASM_FULL = 4'd8,
  FAB_UNATTRIB   = 4'd9    // must stay at zero
} fab_reason_e;
 
fab_reason_e reason_d;
 
always_comb begin
  unique case (1'b1)
    xfer_fire                       : reason_d = FAB_TRANSFER;
    (req == '0)                     : reason_d = FAB_NO_REQUEST;
    (port_state_q[o] == PORT_DOWN)  : reason_d = FAB_PORT_DOWN;
    (port_state_q[o] == PORT_RECOVERING) : reason_d = FAB_RECOVERING;
    route_quiesce_active            : reason_d = FAB_ROUTE_QUIESCE;
    (credit_q[o][req_vc] == '0)     : reason_d = FAB_NO_CREDIT;
    mcast_waiting_dest              : reason_d = FAB_MCAST_WAIT;
    !reasm_space                    : reason_d = FAB_REASM_FULL;
    (grant == '0)                   : reason_d = FAB_ARB_LOST;
    default                         : reason_d = FAB_UNATTRIB;
  endcase
end

Architecture. Ten mutually exclusive reasons in causal priority, one counter each, summing to elapsed cycles.

FAB_NO_REQUEST is second so idle cycles never inflate a resource bin — the most common way a classifier lies (17.2 §32).

And FAB_UNATTRIB must stay at zero. A non-zero value means a stall cause exists that the design does not model. That is the most valuable bin in the list, because it is the one that tells you the instrument itself is incomplete.

Failure. Independent counters per condition, which double-count and produce percentages exceeding 100%.

57. Scaling and Oversubscription

aggregate_fabric_throughput <= min(
    total source demand,
    total input capacity,
    switch / bisection capacity,        // Section 5's topology decides this
    total output and UCIe capacity,
    destination service capacity,
    return and completion capacity      // Section 32 — frequently forgotten
)

Oversubscription, defined:

oversubscription = sum(input peak demand) / shared fabric capacity

Worked, illustratively. Eight inputs each capable of X, through a shared structure of capacity 4X:

oversubscription = 8X / 4X = 2×

Two readings.

Oversubscription is a legitimate design choice, not a defect. If the eight inputs do not peak simultaneously, a 2× oversubscribed fabric is correctly sized and half the silicon of a non-blocking one. The question is whether the workload peaks together — and §29 says collective phases do exactly that.

And the last term is the one omitted. Return and completion capacity is sized after everything else, if at all. §32 is what happens when it is undersized, and it converts a capacity shortfall into a deadlock rather than a slowdown.

58. The Fabric Scoreboard

// Verification-only. FOUR models — routing, resources, packets, and progress.
class fabric_scoreboard;
 
  // ---- Layer 1: ROUTING model — predicted independently, per epoch.
  typedef struct { int out_port; int epoch; } route_model_t;
  route_model_t routes [int][int];      // [epoch][dst] — every epoch retained
 
  // ---- Layer 2: RESOURCE model.
  typedef struct {
    int credits_available;
    int credits_outstanding;    // consumed and not yet returned
    int occupancy;
  } resource_model_t;
  resource_model_t res [int][int];      // [output][vc]
 
  // ---- Layer 3: PACKET model.
  typedef struct {
    int  src, dst, vc, traffic_class, order_domain;
    int  captured_port;
    int  predicted_port;        // from Layer 1, at the ACCEPT epoch
    bit [63:0] dest_pending;    // multicast (§26)
    bit [63:0] frags_received;  // reassembly (§52)
    int  frag_count;
    int  semantic_deliveries;   // MUST be <= 1 (§45)
    bit  retired;
  } packet_model_t;
  packet_model_t pkts [int];            // keyed by txn_id
 
  // ---- Layer 4: PROGRESS model — the only one that can see a deadlock.
  typedef struct {
    int  age;                   // cycles since this packet became eligible
    int  blocked_on;            // which resource class
    int  blocked_by_txn;        // which transaction holds it
  } progress_model_t;
  progress_model_t prog [int];
 
  // ---- Catches Section 9 and Section 42.
  function void check_route(int id);
    if (pkts[id].captured_port != pkts[id].predicted_port)
      $error("MISROUTED txn %0d dst %0d: took port %0d, epoch-%0d model says %0d",
             id, pkts[id].dst, pkts[id].captured_port,
             routes[pkts[id].vc][pkts[id].dst].epoch, pkts[id].predicted_port);
  endfunction
 
  // ---- Catches Section 23 — the leak, before it drains a pool.
  function void check_credit_conservation(int o, int v);
    if (res[o][v].credits_available + res[o][v].credits_outstanding != CREDIT_INIT)
      $error("CREDIT NOT CONSERVED out %0d vc %0d: %0d + %0d != %0d",
             o, v, res[o][v].credits_available, res[o][v].credits_outstanding, CREDIT_INIT);
  endfunction
 
  // ---- Catches Section 27.
  function void check_mcast_retire(int id);
    if (pkts[id].retired && (pkts[id].dest_pending != '0))
      $error("MULTICAST %0d retired with pending destinations %0h", id, pkts[id].dest_pending);
  endfunction
 
  // ---- Catches Section 51.
  function void check_reassembly(int id);
    bit [63:0] full = (64'd1 << pkts[id].frag_count) - 1;
    if (pkts[id].retired && ((pkts[id].frags_received & full) != full))
      $error("REASSEMBLY INCOMPLETE txn %0d: have %0h need %0h",
             id, pkts[id].frags_received, full);
  endfunction
 
  // ---- Catches Sections 32, 35, 38 — the only layer that can.
  function void check_progress();
    foreach (prog[id])
      if (prog[id].age > DEADLOCK_THRESHOLD)
        $error("NO PROGRESS txn %0d for %0d cycles, blocked on class %0d held by txn %0d",
               id, prog[id].age, prog[id].blocked_on, prog[id].blocked_by_txn);
  endfunction
 
endclass

Architecture. Four models keyed by epoch-and-destination, by output-and-VC, by transaction, and by progress.

Layer 4 exists because layers 1 to 3 cannot see a deadlock. §35's cycle violates no safety property — every route is right, every credit is conserved, every packet is well-formed, and nothing moves. A progress model that ages every eligible packet and records what it is blocked on is the only detector, and the blocked_by_txn field is what turns "it hung" into a wait-for chain you can read.

Layer 1 retains every routing epoch, for the same reason 17.2 §35 retains map epochs: a packet accepted under one configuration must be checked against that one.

And Layer 2's credits_outstanding is counted by the model, not read from the design — because that is precisely the quantity §23's bug corrupts.

59. Coverage

covergroup cg_fabric @(posedge clk);
  option.per_instance = 1;
 
  // --- Traffic patterns (Sections 29, 30).
  cp_pattern : coverpoint traffic_pattern_class {
    bins uniform_random = {0};
    bins all_to_one     = {1};       // Section 29
    bins one_to_all     = {2};
    bins all_to_all     = {3};
    bins neighbour      = {4};
  }
  cp_input_output : cross_coverage_input_output;   // every src->dst pair
  cp_load : coverpoint offered_load_class {
    bins light = {0}; bins moderate = {1}; bins saturated = {2};  // deadlock needs this
  }
 
  // --- Input structure (Sections 13, 14).
  cp_hol : coverpoint head_blocked_others_eligible;
  cp_voq_occ : coverpoint voq_occ_ut {
    bins empty = {0}; bins mid = {[1:VOQ_DEPTH-1]}; bins full = {VOQ_DEPTH};
  }
  cp_one_pair_full : coverpoint one_voq_pair_full_others_empty;
 
  // --- Arbitration (Sections 17-20).
  cp_simultaneous_req : coverpoint num_inputs_requesting_one_output {
    bins one = {1}; bins some = {[2:NUM_INPUTS-1]}; bins all = {NUM_INPUTS};
  }
  cp_rr_wrap : coverpoint rotation_pointer_wrapped;
  cp_age_override : coverpoint fairness_override_fired;
  cp_grant_no_xfer : coverpoint grant_asserted_without_transfer;   // Section 18
 
  // --- Credits (Sections 21-24).
  cp_credit : coverpoint credit_q_ut {
    bins zero = {0}; bins low = {[1:2]}; bins full = {CREDIT_INIT};
  }
  cp_credit_simul : coverpoint consume_and_return_same_cycle;
 
  // --- Multicast (Sections 25-28).
  cp_mcast_fanout : coverpoint mcast_dest_count {
    bins two = {2}; bins some = {[3:NUM_DESTS-1]}; bins all = {NUM_DESTS};
  }
  cp_mcast_partial : coverpoint mcast_one_dest_stalled;             // Section 27
  cp_mcast_dup : coverpoint duplicate_dest_acceptance;
 
  // --- Classes and deadlock (Sections 31-38).
  cp_class : coverpoint traffic_class_ut { bins each[] = {[0:3]}; }
  cp_progress_wait : coverpoint progress_age_q_ut {
    bins none = {0}; bins some = {[1:PROGRESS_BOUND-1]}; bins at_bound = {PROGRESS_BOUND};
  }
  cp_deadlock_injected : coverpoint deadlock_scenario_injected;      // Section 35
  cp_vc_usage : coverpoint vcs_in_use {
    bins one = {1};                  // request/response SHARING — Section 38
    bins separated = {[2:$]};
  }
 
  // --- Ordering (Sections 39, 40).
  cp_order_domains : coverpoint distinct_order_domains_active {
    bins one = {1}; bins several = {[2:$]};
  }
  cp_reorder_across_domains : coverpoint packets_reordered_across_domains;
 
  // --- Configuration and health (Sections 8, 46-48).
  cp_route_commit : coverpoint route_commit_context {
    bins idle = {0}; bins blocked_by_inflight = {1}; bins forced_with_inflight = {2};
  }
  cp_port_state : coverpoint port_state_q_ut { bins each[] = {[0:3]}; }
  cp_ports_recovering : coverpoint num_ports_recovering {
    bins none = {0}; bins one = {1}; bins several = {[2:$]};        // Section 47
  }
 
  // --- Striping (Sections 50-53).
  cp_frag_count : coverpoint frag_count_ut { bins one = {1}; bins few = {[2:3]}; bins many = {[4:$]}; }
  cp_frag_order : coverpoint fragment_arrival_order {
    bins in_order = {0}; bins reversed = {1}; bins interleaved = {2}; bins duplicate = {3};
  }
 
  // --- Attribution (Section 56).
  cp_reason : coverpoint reason_d { bins each[] = {[0:9]}; }
 
  // --- Crosses that carry the information.
  x_pattern_load   : cross cp_pattern, cp_load;              // Section 30
  x_vc_load        : cross cp_vc_usage, cp_load;             // Section 38
  x_mcast_stall    : cross cp_mcast_fanout, cp_mcast_partial;
  x_recovery_scope : cross cp_ports_recovering, cp_reason;   // Section 47
  x_class_progress : cross cp_class, cp_progress_wait;       // Section 32
endcovergroup