UCIe Buffering

// ILLUSTRATIVE. Production-style: one owner per counter, handshake-qualified
// events, payload RAM not reset, wrap-safe pointers.
module ucie_fifo #(
  parameter int DEPTH = 16,
  parameter int WIDTH = 64
) (
  input  logic             clk,
  input  logic             rst_n,
  input  logic             push,
  input  logic [WIDTH-1:0] wdata,
  output logic             full,
  input  logic             pop,
  output logic [WIDTH-1:0] rdata,
  output logic             empty,
  output logic [$clog2(DEPTH+1)-1:0] occupancy
);
  localparam int PTR_W = $clog2(DEPTH);
  localparam int OCC_W = $clog2(DEPTH+1);       // DEPTH+1 values: 0..DEPTH
 
  // Elaboration checks (Section 14).
  initial begin
    assert (DEPTH >= 2) else $fatal(1, "DEPTH must be at least 2");
    assert (WIDTH >= 1) else $fatal(1, "WIDTH must be positive");
  end
 
  // Payload storage — inferred RAM, deliberately NOT reset.
  logic [WIDTH-1:0] mem [DEPTH];
 
  // Pointers carry an extra MSB so full and empty are distinguishable (Section 11).
  logic [PTR_W:0] wr_ptr_q, rd_ptr_q;
 
  wire [PTR_W-1:0] wr_idx = wr_ptr_q[PTR_W-1:0];
  wire [PTR_W-1:0] rd_idx = rd_ptr_q[PTR_W-1:0];
 
  wire push_fire = push && !full;
  wire pop_fire  = pop  && !empty;
 
  // Occupancy is DERIVED, not maintained — so it cannot drift (Section 8).
  assign occupancy = OCC_W'(wr_ptr_q - rd_ptr_q);
  assign full      = (occupancy == OCC_W'(DEPTH));
  assign empty     = (occupancy == '0);
  assign rdata     = mem[rd_idx];
 
  always_ff @(posedge clk or negedge rst_n)
    if (!rst_n) begin
      wr_ptr_q <= '0;
      rd_ptr_q <= '0;
    end else begin
      if (push_fire) wr_ptr_q <= next_ptr(wr_ptr_q);   // Section 13
      if (pop_fire)  rd_ptr_q <= next_ptr(rd_ptr_q);
    end
 
  always_ff @(posedge clk)
    if (push_fire) mem[wr_idx] <= wdata;
 
endmodule

// If a design does maintain a counter — for instance because occupancy must be
// registered for timing — ONE owner and all four arms, explicitly.
always_ff @(posedge clk or negedge rst_n)
  if (!rst_n) occ_q <= '0;
  else
    unique case ({push_fire, pop_fire})
      2'b10:   occ_q <= occ_q + 1'b1;
      2'b01:   occ_q <= occ_q - 1'b1;
      default: ;                                 // 2'b00 and 2'b11 both hold
    endcase

// WRONG — two independent statements for one register.
always_ff @(posedge clk) begin
  if (push_fire) occ_q <= occ_q + 1'b1;
  if (pop_fire)  occ_q <= occ_q - 1'b1;        // ← the second wins on a tie
end

// MANDATORY. Occupancy matches the pointers — this is what catches Section 9.
property p_occupancy_matches_pointers;
  @(posedge clk) disable iff (!rst_n)
    (occupancy == OCC_W'(wr_ptr_q - rd_ptr_q));
endproperty
a_occupancy_matches_pointers: assert property (p_occupancy_matches_pointers);
 
// Conservation against a testbench count.
property p_conservation;
  @(posedge clk) disable iff (!rst_n)
    (occupancy == (tb_pushes - tb_pops));
endproperty
a_conservation: assert property (p_conservation);
 
property p_no_overflow;
  @(posedge clk) disable iff (!rst_n) (push && full) |-> !push_fire;
endproperty
a_no_overflow: assert property (p_no_overflow);
 
property p_no_underflow;
  @(posedge clk) disable iff (!rst_n) (pop && empty) |-> !pop_fire;
endproperty
a_no_underflow: assert property (p_no_underflow);
 
// The head is stable while it is not taken.
property p_head_stable;
  @(posedge clk) disable iff (!rst_n)
    (!empty && !pop_fire) |=> $stable(rdata);
endproperty
a_head_stable: assert property (p_head_stable);
 
// A simultaneous push and pop leaves occupancy unchanged.
property p_simultaneous_holds;
  @(posedge clk) disable iff (!rst_n)
    (push_fire && pop_fire) |=> (occupancy == $past(occupancy));
endproperty
a_simultaneous_holds: assert property (p_simultaneous_holds);

// WRONG — indices only, and full inferred from equality.
logic [PTR_W-1:0] wr_ptr_q, rd_ptr_q;          // no extra bit
 
assign empty = (wr_ptr_q == rd_ptr_q);
assign full  = (wr_ptr_q + 1'b1 == rd_ptr_q);  // "one slot spare" — but see below

1. It silently reduces usable depth to DEPTH-1, which the sizing arithmetic
   in Sections 21-22 did NOT account for.
2. If DEPTH is not a power of two, `wr_ptr_q + 1` does not wrap at DEPTH —
   it wraps at 2**PTR_W, which is larger. The comparison then never
   matches at the intended point (Section 13).

// WORSE — full and empty conflated.
assign full  = (wr_ptr_q == rd_ptr_q);         // ← also true when EMPTY

// ILLUSTRATIVE. Explicit wrap, so DEPTH need not be a power of two.
function automatic logic [PTR_W:0] next_ptr(input logic [PTR_W:0] p);
  // The MSB is the wrap bit; the low bits are the index.
  if (p[PTR_W-1:0] == PTR_W'(DEPTH-1))
    next_ptr = {~p[PTR_W], PTR_W'(0)};          // wrap index, toggle wrap bit
  else
    next_ptr = {p[PTR_W], p[PTR_W-1:0] + 1'b1};
endfunction

// ILLUSTRATIVE. A bad parameter should fail the build, not produce a silently
// wrong design (18.4's argument, at every buffer).
initial begin
  assert (DEPTH >= 2)
    else $fatal(1, "DEPTH must be at least 2 (a 1-deep queue is a skid — Section 18)");
 
  assert (WIDTH >= 1)
    else $fatal(1, "WIDTH must be positive");
 
  // If THIS instance uses the natural-overflow wrap, say so and enforce it.
  if (USE_POW2_WRAP)
    assert ((DEPTH & (DEPTH-1)) == 0)
      else $fatal(1, "DEPTH must be a power of two for the overflow wrap (Section 13)");
 
  // The watermark must leave room for the in-flight items (Section 29).
  assert (HIGH_WM <= DEPTH - MAX_INFLIGHT_AFTER_STOP)
    else $fatal(1, "HIGH_WM leaves insufficient headroom (Section 29)");
 
  // Hysteresis must actually have a gap (Section 31).
  assert (LOW_WM < HIGH_WM)
    else $fatal(1, "LOW_WM must be below HIGH_WM (Section 32)");
end

// ILLUSTRATIVE. Data and its metadata are ONE entry, written on ONE event.
typedef struct packed {
  logic [OBJ_ID_W-1:0]    object_id;
  logic [CLASS_W-1:0]     tclass;
  logic [LEN_W-1:0]       length;
  logic [CFG_EPOCH_W-1:0] cfg_epoch;
  logic                   last;
  logic [DATA_W-1:0]      data;
} buf_entry_t;
 
buf_entry_t mem [DEPTH];
 
always_ff @(posedge clk)
  if (push_fire) mem[wr_idx] <= push_entry;      // ONE write, ONE pointer

// ILLUSTRATIVE. Two RAMs, ONE pointer, ONE accept event.
logic [DATA_W-1:0] data_mem [DEPTH];
logic [META_W-1:0] meta_mem [DEPTH];
 
always_ff @(posedge clk)
  if (push_fire) begin
    data_mem[wr_idx] <= push_data;               // same index
    meta_mem[wr_idx] <= push_meta;               // same index, same event
  end

// WRONG — two RAMs with two pointers advanced on two conditions.
always_ff @(posedge clk) begin
  if (data_push) begin data_mem[data_wr_q] <= push_data; data_wr_q <= data_wr_q + 1'b1; end
  if (meta_push) begin meta_mem[meta_wr_q] <= push_meta; meta_wr_q <= meta_wr_q + 1'b1; end
end

// MANDATORY. One write event, one index, for both RAMs.
property p_single_accept_event;
  @(posedge clk) disable iff (!rst_n)
    (data_write_en == meta_write_en);
endproperty
a_single_accept_event: assert property (p_single_accept_event);
 
property p_same_write_index;
  @(posedge clk) disable iff (!rst_n)
    data_write_en |-> (data_wr_idx == meta_wr_idx);
endproperty
a_same_write_index: assert property (p_same_write_index);
 
// End-to-end: the metadata popped with an entry is the metadata pushed with it.
property p_entry_association(int unsigned rid);
  @(posedge clk) disable iff (!rst_n)
    (pop_fire && (tb_ref_id == rid))
      |-> (rd_meta == tb_meta_of(rid));
endproperty
a_entry_association: assert property (p_entry_association(REF_UT));

// ILLUSTRATIVE one-entry skid. Its purpose is NOT storage — it is to make
// up_ready independent of dn_ready.
typedef struct packed {
  logic             valid;
  buf_entry_t       entry;
} skid_t;
 
skid_t skid_q;
 
// The whole point: this depends on the skid's own state and nothing downstream.
assign up_ready = !skid_q.valid;
 
assign dn_valid = skid_q.valid || up_valid;
assign dn_entry = skid_q.valid ? skid_q.entry : up_entry;
 
always_ff @(posedge clk or negedge rst_n)
  if (!rst_n) begin
    skid_q.valid <= 1'b0;
  end else begin
    unique case ({skid_q.valid, dn_ready})
      2'b11: skid_q.valid <= 1'b0;                    // held, taken: empties
      2'b10: ;                                        // held, stalled: hold
      2'b00: if (up_valid) begin                      // empty, stalled: CAPTURE
               skid_q.valid <= 1'b1;
               skid_q.entry <= up_entry;
             end
      2'b01: ;                                        // empty, ready: pass through
      default: ;
    endcase
  end

// WRONG — the skid captures only when it is already offering downstream.
always_ff @(posedge clk)
  if (dn_valid && !dn_ready) begin
    skid_q.valid <= 1'b1;
    skid_q.entry <= dn_entry;                 // ← may be the SKID's own entry
  end else if (dn_ready) begin
    skid_q.valid <= 1'b0;
  end

1. The skid is empty. up_ready is high, so upstream sends an item.
2. In the SAME cycle, dn_ready falls.
3. dn_valid is true (from the bypass path) and dn_ready is false, so the
   code captures dn_entry — which IS the upstream item, so this case works.
4. But now consider: the skid is empty, dn_ready is ALREADY low, and
   upstream sends. dn_valid is true via bypass, dn_ready is low, so it
   captures — and then upstream sends AGAIN next cycle because up_ready
   was computed from a stale or wrong condition.
5. -> the second item overwrites the first. An obligation is lost.

// MANDATORY. Nothing accepted upstream is lost — the only detector for Section 19.
property p_skid_conservation;
  @(posedge clk) disable iff (!rst_n)
    (tb_items_in == tb_items_out + (skid_q.valid ? 1 : 0));
endproperty
a_skid_conservation: assert property (p_skid_conservation);
 
// Upstream readiness has no downstream term.
property p_up_ready_independent;
  @(posedge clk) disable iff (!rst_n)
    !skid_q.valid |-> up_ready;
endproperty
a_up_ready_independent: assert property (p_up_ready_independent);
 
// The offered entry is stable while downstream stalls.
property p_dn_stable_under_stall;
  @(posedge clk) disable iff (!rst_n)
    (dn_valid && !dn_ready) |=> (dn_valid && $stable(dn_entry));
endproperty
a_dn_stable_under_stall: assert property (p_dn_stable_under_stall);
 
// The skid never accepts while it already holds an item.
property p_skid_no_overwrite;
  @(posedge clk) disable iff (!rst_n)
    (up_valid && up_ready) |-> !skid_q.valid;
endproperty
a_skid_no_overwrite: assert property (p_skid_no_overwrite);

required_entries  ≈  arrival_rate × blocking_latency  +  headroom
 
     [items/cycle] × [cycles]  =  [items]        <- dimensionally correct

STEP 1 — absorb the stall
  arrival_rate     = 1 item/cycle
  blocking_latency = 12 cycles
  stall_absorption = 1 × 12 = 12 items
 
STEP 2 — headroom for items already in flight when we say stop (§27)
  backpressure_round_trip = 3 cycles
  headroom = 1 item/cycle × 3 cycles = 3 items
 
STEP 3 — total
  DEPTH >= 12 + 3 = 15 items
 
STEP 4 — and the high watermark follows (§29)
  HIGH_WM <= DEPTH - headroom = 15 - 3 = 12

ILLUSTRATIVE, same producer and consumer as Section 22:
 
  DEPTH  4  ->  producer stalls often          ~62% of offered rate
  DEPTH  8  ->  producer stalls occasionally   ~88%
  DEPTH 15  ->  producer never stalls         ~100%
  DEPTH 32  ->  producer never stalls         ~100%    <- no change
  DEPTH 64  ->  producer never stalls         ~100%    <- no change

// WRONG as an architectural response. The downstream is slower than the
// upstream on AVERAGE, and the answer chosen was more storage.
localparam int DEPTH = 4096;      // "that should be enough"

ILLUSTRATIVE:
  sustained arrival rate = 1.0 items/cycle
  sustained service rate = 0.8 items/cycle
  net accumulation       = 0.2 items/cycle
 
  time to fill DEPTH = 4096 / 0.2 = 20,480 cycles
 
  -> the buffer fills, backpressure asserts, and throughput settles at 0.8.
     The 4096 entries bought 20,480 cycles of delay before that happened.

For a bounded queue:      long-term arrival rate  <=  long-term service rate
 
If that is violated:      NO finite buffer bounds the queue.
                          Depth changes WHEN it fills, never WHETHER.

headroom  >=  backpressure_round_trip  ×  maximum_arrival_rate
 
     [cycles] × [items/cycle]  =  [items]

// WRONG — backpressure begins only when there is no room left.
assign upstream_stall = full;

1. Occupancy reaches DEPTH. `full` asserts.
2. The signal takes 3 cycles to reach the producer and stop it (Section 27).
3. During those 3 cycles the producer sends 3 more items.
4. -> three items arrive at a full buffer.

HIGH_WM  <=  DEPTH  -  headroom
         =  DEPTH  -  (backpressure_round_trip × max_arrival_rate)

DEPTH                   = 15 items
backpressure round trip = 3 cycles
max arrival rate        = 1 item/cycle
 
headroom = 3 × 1 = 3 items
HIGH_WM <= 15 - 3 = 12

backpressure round trip = 1 (register) + 1 (wire) + 4 (drain) = 6 cycles
headroom = 6 × 1 = 6 items
HIGH_WM <= 15 - 6 = 9
 
-> the SAME buffer now throttles at 9 instead of 12, purely because the
   producer got deeper. The depth did not change; the usable depth did.

// MANDATORY, with the assumption written down.
//   A1: the producer stops within the stated round trip after the watermark
assume property (@(posedge clk) disable iff (!rst_n)
  high_wm_asserted |-> ##[1:BP_ROUND_TRIP] !producer_offering);
 
property p_never_overflows_after_watermark;
  @(posedge clk) disable iff (!rst_n)
    high_wm_asserted |-> ##[0:BP_ROUND_TRIP] (occupancy <= DEPTH);
endproperty
a_never_overflows_after_watermark:
  assert property (p_never_overflows_after_watermark);
 
// The headroom itself: from the watermark, at most `headroom` more arrive.
property p_headroom_sufficient;
  @(posedge clk) disable iff (!rst_n)
    high_wm_asserted |-> (arrivals_since_watermark <= HEADROOM);
endproperty
a_headroom_sufficient: assert property (p_headroom_sufficient);
 
// And the plain safety property, always.
property p_no_overflow_ever;
  @(posedge clk) disable iff (!rst_n) push_fire |-> !full;
endproperty
a_no_overflow_ever: assert property (p_no_overflow_ever);

// ILLUSTRATIVE. Two thresholds and one state bit — Section 32 is one threshold.
typedef enum logic { WM_ACCEPTING, WM_THROTTLED } wm_state_e;
 
wm_state_e wm_state_q;
 
always_ff @(posedge clk or negedge rst_n)
  if (!rst_n)
    wm_state_q <= WM_ACCEPTING;
  else
    unique case (wm_state_q)
      WM_ACCEPTING: if (occupancy >= HIGH_WM) wm_state_q <= WM_THROTTLED;
      WM_THROTTLED: if (occupancy <= LOW_WM)  wm_state_q <= WM_ACCEPTING;
      default:                                wm_state_q <= WM_ACCEPTING;
    endcase
 
assign upstream_stall = (wm_state_q == WM_THROTTLED);

// WRONG — a single comparison, no memory.
assign upstream_stall = (occupancy >= THRESHOLD);

// MANDATORY. Throttling begins at or before the high watermark.
property p_throttle_at_high_wm;
  @(posedge clk) disable iff (!rst_n)
    (occupancy >= HIGH_WM) |-> upstream_stall;
endproperty
a_throttle_at_high_wm: assert property (p_throttle_at_high_wm);
 
// Release happens only at or below the low watermark.
property p_release_at_low_wm;
  @(posedge clk) disable iff (!rst_n)
    $fell(upstream_stall) |-> ($past(occupancy) <= LOW_WM);
endproperty
a_release_at_low_wm: assert property (p_release_at_low_wm);
 
// Hysteresis: the state does not change twice within a short window.
property p_no_chatter;
  @(posedge clk) disable iff (!rst_n)
    $changed(wm_state_q) |=> $stable(wm_state_q)[*MIN_DWELL];
endproperty
a_no_chatter: assert property (p_no_chatter);
 
// Ordering, checked once at elaboration and again at runtime.
property p_watermark_ordering;
  @(posedge clk) disable iff (!rst_n)
    ((LOW_WM < HIGH_WM) && (HIGH_WM <= DEPTH - HEADROOM));
endproperty
a_watermark_ordering: assert property (p_watermark_ordering);

// ILLUSTRATIVE. Four states per bank, with EXACTLY ONE owner at a time.
typedef enum logic [1:0] {
  BANK_FREE      = 2'd0,   // nobody owns it
  BANK_PRODUCING = 2'd1,   // the producer owns it
  BANK_FULL      = 2'd2,   // filled; ownership is being handed over
  BANK_CONSUMING = 2'd3    // the consumer owns it — DO NOT WRITE
} bank_state_e;
 
bank_state_e bank_state_q [2];
logic        prod_bank_q, cons_bank_q;
 
// The producer may only claim a FREE bank.
assign prod_can_claim = (bank_state_q[prod_bank_q] == BANK_FREE);
// The consumer may only claim a FULL bank.
assign cons_can_claim = (bank_state_q[cons_bank_q] == BANK_FULL);
 
always_ff @(posedge clk or negedge rst_n)
  if (!rst_n) begin
    bank_state_q[0] <= BANK_FREE;
    bank_state_q[1] <= BANK_FREE;
    prod_bank_q     <= 1'b0;
    cons_bank_q     <= 1'b0;
  end else begin
    for (int b = 0; b < 2; b++) begin
      unique case (bank_state_q[b])
        BANK_FREE:      if (prod_claim && (prod_bank_q == b[0]))
                                                  bank_state_q[b] <= BANK_PRODUCING;
        BANK_PRODUCING: if (prod_done  && (prod_bank_q == b[0]))
                                                  bank_state_q[b] <= BANK_FULL;
        BANK_FULL:      if (cons_claim && (cons_bank_q == b[0]))
                                                  bank_state_q[b] <= BANK_CONSUMING;
        // ONLY the consumer releases. Section 36 is the producer releasing.
        BANK_CONSUMING: if (cons_release && (cons_bank_q == b[0]))
                                                  bank_state_q[b] <= BANK_FREE;
        default: ;
      endcase
    end
 
    if (prod_done)    prod_bank_q <= ~prod_bank_q;
    if (cons_release) cons_bank_q <= ~cons_bank_q;
  end

// WRONG — the producer swaps banks when it finishes filling one.
always_ff @(posedge clk)
  if (prod_done) begin
    prod_bank_q <= ~prod_bank_q;              // move to the other bank
    bank_free_q[~prod_bank_q] <= 1'b1;        // ← and declare it free
  end

1. The producer fills bank A and finishes. It swaps to bank B.
2. The consumer is still reading bank B from the previous round.
3. The producer begins writing bank B.
4. -> the consumer's data changes underneath it, mid-block.

// MANDATORY. The producer never writes a bank the consumer owns.
property p_no_write_to_consuming_bank;
  @(posedge clk) disable iff (!rst_n)
    prod_write_fire |-> (bank_state_q[prod_bank_q] == BANK_PRODUCING);
endproperty
a_no_write_to_consuming_bank:
  assert property (p_no_write_to_consuming_bank);
 
// The consumer never reads a bank it does not own.
property p_no_read_unowned_bank;
  @(posedge clk) disable iff (!rst_n)
    cons_read_fire |-> (bank_state_q[cons_bank_q] == BANK_CONSUMING);
endproperty
a_no_read_unowned_bank: assert property (p_no_read_unowned_bank);
 
// A bank becomes FREE only on a consumer release (Section 36).
property p_free_only_on_consumer_release;
  @(posedge clk) disable iff (!rst_n)
    ((bank_state_q[B] == BANK_FREE) && ($past(bank_state_q[B]) == BANK_CONSUMING))
      |-> $past(cons_release && (cons_bank_q == B));
endproperty
a_free_only_on_consumer_release:
  assert property (p_free_only_on_consumer_release);
 
// A bank's contents are stable while the consumer owns it — the EFFECT.
property p_bank_stable_while_consuming;
  @(posedge clk) disable iff (!rst_n)
    (bank_state_q[B] == BANK_CONSUMING) |=> $stable(bank_mem[B]);
endproperty
a_bank_stable_while_consuming:
  assert property (p_bank_stable_while_consuming);

replay_depth  >=  maximum number of objects that can be unresolved at once
 
              =  issue_rate  ×  worst-case resolution latency

ILLUSTRATIVE:
  measured average unresolved objects  = 4
  chosen depth                          = 8      ("2× margin, plenty")
 
  worst-case resolution latency, including one retransmission
    and a degraded link                 = 20 objects' worth
 
  -> the ring fills at 8, admission stops (19.3 §9), and throughput
     collapses to whatever the resolution path can sustain.

reassembly_slots  >=  maximum number of objects that can be simultaneously
                      incomplete at the receiver
 
reassembly_bytes_per_slot  >=  maximum object size

// ILLUSTRATIVE. Slots are RESERVED at the first fragment, not discovered later.
logic [NUM_SLOTS-1:0]  slot_busy_q;
logic [MAX_FRAGS-1:0]  frag_received_q [NUM_SLOTS];
logic [DATA_W-1:0]     reasm_mem       [NUM_SLOTS][MAX_FRAGS];
 
// A first fragment is accepted only if a slot can hold the WHOLE object.
assign first_frag_admit = (slot_busy_q != '1)                       // a slot exists
                       && (frag.frag_count <= MAX_FRAGS);           // it fits

// WRONG — fragments are accepted as they arrive, and space is sought per fragment.
always_ff @(posedge clk)
  if (frag_valid && any_space_available)
    store_fragment(frag);                     // ← no slot reserved for the OBJECT

1. The first fragment of object A is accepted. Space existed.
2. Fragments of objects B, C, D arrive and are accepted. Space still existed.
3. Object A's second fragment arrives. There is now no space.
4. -> the receiver holds a partial object it can never complete, and it is
     occupying a slot that will never be released.

// MANDATORY. Accepting a first fragment implies capacity for the whole object.
property p_first_frag_implies_capacity;
  @(posedge clk) disable iff (!rst_n)
    first_frag_accept |-> ((slot_busy_q != '1) && (frag.frag_count <= MAX_FRAGS));
endproperty
a_first_frag_implies_capacity:
  assert property (p_first_frag_implies_capacity);
 
// A slot holds exactly one object while busy.
property p_slot_single_object;
  @(posedge clk) disable iff (!rst_n)
    slot_busy_q[S] |-> $stable(slot_object_id_q[S]);
endproperty
a_slot_single_object: assert property (p_slot_single_object);
 
// Every accepted partial object eventually completes or is explicitly abandoned.
//   A1: the sender eventually delivers or the link fails explicitly
property p_partial_resolves;
  @(posedge clk) disable iff (!rst_n)
    first_frag_accept |-> ##[1:REASM_BOUND] (object_complete(S) || object_abandoned(S));
endproperty
a_partial_resolves: assert property (p_partial_resolves);
 
// An abandoned slot is released — no permanent leak (Section 41).
property p_abandoned_slot_released;
  @(posedge clk) disable iff (!rst_n)
    object_abandoned(S) |=> !slot_busy_q[S];
endproperty
a_abandoned_slot_released: assert property (p_abandoned_slot_released);

// WRONG — every class allocates from one pool with no reserve.
assign admit = (free_entries != '0);

1. A streaming class fills every entry.
2. A progress-critical completion arrives — one that RELEASES resources.
3. It cannot be admitted.
4. The streaming traffic cannot drain, because draining requires the
   resource that completion would have released.
5. -> deadlock, on a design where every block is individually correct.

// ILLUSTRATIVE. A shared pool with a reserve that bulk traffic cannot touch.
// Generic — no standard is claimed to require it (Section 3).
localparam int PROGRESS_RESERVE = 4;
 
logic [OCC_W-1:0] free_entries;
 
// Bulk may allocate only above the reserve.
assign bulk_admit     = (free_entries > OCC_W'(PROGRESS_RESERVE));
// Progress-critical traffic may use anything that is free.
assign progress_admit = (free_entries != '0);
 
// The reserve is a real parameter — checked at elaboration (Section 14).
initial begin
  assert (PROGRESS_RESERVE > 0)
    else $fatal(1, "reserve of zero is a shared pool — Section 44 is reachable");
  assert (PROGRESS_RESERVE < DEPTH)
    else $fatal(1, "reserve must leave capacity for bulk traffic");
end

// MANDATORY. Bulk traffic never consumes the reserved capacity.
property p_bulk_respects_reserve;
  @(posedge clk) disable iff (!rst_n)
    bulk_push_fire |-> ($past(free_entries) > PROGRESS_RESERVE);
endproperty
a_bulk_respects_reserve: assert property (p_bulk_respects_reserve);
 
// Free entries never fall below the reserve while only bulk is pushing.
property p_reserve_preserved;
  @(posedge clk) disable iff (!rst_n)
    (bulk_push_fire && !progress_push_fire) |=> (free_entries >= PROGRESS_RESERVE);
endproperty
a_reserve_preserved: assert property (p_reserve_preserved);
 
// LIVENESS: progress traffic is admitted within a bound.
//   A1: the consumer eventually drains an entry
//   A2: progress traffic keeps offering until admitted
property p_progress_admitted;
  @(posedge clk) disable iff (!rst_n)
    progress_offering |-> ##[1:PROGRESS_BOUND] progress_push_fire;
endproperty
a_progress_admitted: assert property (p_progress_admitted);

// ILLUSTRATIVE. Standard structure; the point here is what makes it different
// from Section 7's single-clock FIFO. 18.4 Section 18 covers the general case.
logic [PTR_W:0] wr_ptr_bin_q,  wr_ptr_gray_q;    // write domain
logic [PTR_W:0] rd_ptr_bin_q,  rd_ptr_gray_q;    // read domain
logic [PTR_W:0] wr_gray_sync_q [2];              // synchronised INTO read domain
logic [PTR_W:0] rd_gray_sync_q [2];              // synchronised INTO write domain
 
buf_entry_t cdc_mem [DEPTH];                     // NOT reset
 
function automatic logic [PTR_W:0] bin2gray(input logic [PTR_W:0] b);
  return b ^ (b >> 1);
endfunction
 
always_ff @(posedge wr_clk or negedge wr_rst_n)
  if (!wr_rst_n) begin
    wr_ptr_bin_q  <= '0;
    wr_ptr_gray_q <= '0;
  end else if (wr_en && !wr_full) begin
    wr_ptr_bin_q  <= wr_ptr_bin_q + 1'b1;
    wr_ptr_gray_q <= bin2gray(wr_ptr_bin_q + 1'b1);
  end
 
// Full is computed in the WRITE domain, from a STALE read pointer.
assign wr_full = (wr_ptr_gray_q == {~rd_gray_sync_q[1][PTR_W:PTR_W-1],
                                     rd_gray_sync_q[1][PTR_W-2:0]});
// Empty is computed in the READ domain, from a STALE write pointer.
assign rd_empty = (rd_ptr_gray_q == wr_gray_sync_q[1]);

// WRONG — a multi-bit binary pointer crossed through synchronisers.
always_ff @(posedge rd_clk) begin
  wr_ptr_sync_q[0] <= wr_ptr_bin_q;        // ← several bits change at once
  wr_ptr_sync_q[1] <= wr_ptr_sync_q[0];
end

ILLUSTRATIVE: the pointer goes 0111 -> 1000. Four bits change.
 
The destination can sample any combination:
  0111  (old)   ✓ safe
  1000  (new)   ✓ safe
  1111          ✗ a value that was NEVER written
  0000          ✗ likewise
  1011, 0100, ...  ✗ likewise

// WRONG — one signal clears every buffer on the link.
assign flush_all = link_recovery;
 
// ...and every buffer uses it:
always_ff @(posedge clk)
  if (flush_all) begin
    ingress_occ_q  <= '0;
    staging_occ_q  <= '0;
    replay_valid_q <= '0;          // ← the worst one
    output_occ_q   <= '0;
    skid_q.valid   <= 1'b0;
  end

// MANDATORY. The buffers that hold accepted obligations are untouched.
property p_ingress_survives_recovery;
  @(posedge clk) disable iff (!rst_n)
    recovery_entered |=> $stable(ingress_occupancy);
endproperty
a_ingress_survives_recovery: assert property (p_ingress_survives_recovery);
 
property p_staging_survives_recovery;
  @(posedge clk) disable iff (!rst_n)
    recovery_entered |=> $stable(staging_occupancy);
endproperty
a_staging_survives_recovery: assert property (p_staging_survives_recovery);
 
property p_output_survives_recovery;
  @(posedge clk) disable iff (!rst_n)
    recovery_entered |=> $stable(output_occupancy);
endproperty
a_output_survives_recovery: assert property (p_output_survives_recovery);
 
property p_skid_survives_recovery;
  @(posedge clk) disable iff (!rst_n)
    recovery_entered |=> $stable(skid_q.valid);
endproperty
a_skid_survives_recovery: assert property (p_skid_survives_recovery);
 
// And the negative form: no global flush signal reaches these buffers.
property p_no_global_flush;
  @(posedge clk) disable iff (!rst_n)
    recovery_entered |-> !(ingress_flush || staging_flush || output_flush);
endproperty
a_no_global_flush: assert property (p_no_global_flush);

// Diagnostic only, in the POR reset domain (19.1 Section 7).
logic [63:0] occ_sum_q      [NUM_BUFFERS];   // sum of occupancy -> mean
logic [63:0] occ_max_q      [NUM_BUFFERS];   // high-water mark
logic [63:0] full_cycles_q  [NUM_BUFFERS];
logic [63:0] wm_assert_q    [NUM_BUFFERS];   // times the high watermark fired
logic [63:0] wm_dwell_q     [NUM_BUFFERS];   // cycles spent throttled
logic [63:0] overflow_q     [NUM_BUFFERS];   // MUST stay at zero
logic [63:0] reserve_used_q;                 // progress traffic in the reserve
logic [63:0] cdc_full_q     [NUM_CROSSINGS];
logic [63:0] reasm_abandon_q;                // Section 42

// Verification-only. THREE models, because a buffer can be wrong in three
// independent ways: what it holds, what it promised, and what it lost.
class buffer_scoreboard;
 
  // ---- Layer 1: CONTENT model — what SHOULD be in the buffer, in order.
  typedef struct {
    int  ref_id;
    int  meta;                   // the metadata that accompanied it (Section 17)
  } entry_model_t;
  entry_model_t expected [int][$];    // [buffer id] -> queue of entries
 
  // ---- Layer 2: OCCUPANCY model — pushes, pops, and the derived count.
  typedef struct {
    int pushes, pops;
    int design_occupancy;
    int max_observed;
  } occ_model_t;
  occ_model_t occ [int];
 
  // ---- Layer 3: PROMISE model — the admission promises the buffer made.
  typedef struct {
    int  depth, high_wm, low_wm, headroom;
    int  arrivals_since_watermark;
    bit  overflowed;                  // MUST stay false
    bit  reserve_violated;            // Section 46
  } promise_model_t;
  promise_model_t promise [int];
 
  // ---- Catches Sections 9 and 12 — occupancy drift or a bad full/empty.
  function void check_occupancy(int b);
    if (occ[b].design_occupancy != (occ[b].pushes - occ[b].pops))
      $error("BUFFER %0d occupancy %0d != pushes %0d - pops %0d (Sections 9, 12)",
             b, occ[b].design_occupancy, occ[b].pushes, occ[b].pops);
  endfunction
 
  // ---- Catches Sections 16 and 19 — a lost item or a mismatched pair.
  function void check_pop(int b, int got_id, int got_meta);
    entry_model_t e = expected[b].pop_front();
    if (got_id != e.ref_id)
      $error("BUFFER %0d popped id %0d, expected %0d (Section 19 — an item was lost)",
             b, got_id, e.ref_id);
    if (got_meta != e.meta)
      $error("BUFFER %0d popped id %0d with meta %0d, expected %0d (Section 16)",
             b, got_id, got_meta, e.meta);
  endfunction
 
  // ---- Catches Section 28 — the headroom was insufficient.
  function void check_headroom(int b);
    if (promise[b].arrivals_since_watermark > promise[b].headroom)
      $error("BUFFER %0d: %0d arrivals after the watermark, headroom is %0d (Section 28)",
             b, promise[b].arrivals_since_watermark, promise[b].headroom);
  endfunction
 
  // ---- Catches Section 51 — a buffer cleared by a recovery.
  function void check_recovery(int b, int occ_before, int occ_after);
    if ((buffer_policy[b] == POLICY_HOLD) && (occ_after != occ_before))
      $error("BUFFER %0d occupancy changed across a recovery: %0d -> %0d (Section 51)",
             b, occ_before, occ_after);
  endfunction
 
  // ---- Right-sizing evidence, not a failure.
  function void report_sizing(int b);
    if (occ[b].max_observed < (promise[b].depth / 4))
      $display("NOTE: buffer %0d high-water mark %0d of depth %0d — likely oversized",
               b, occ[b].max_observed, promise[b].depth);
  endfunction
 
endclass

covergroup cg_ucie_buffering @(posedge clk);
  option.per_instance = 1;
 
  // --- Occupancy (Sections 7-14).
  cp_occ : coverpoint occupancy {
    bins empty  = {0};
    bins low    = {[1:LOW_WM]};
    bins mid    = {[LOW_WM+1:HIGH_WM-1]};
    bins high   = {[HIGH_WM:DEPTH-1]};
    bins full   = {DEPTH};
  }
  cp_simul_push_pop : coverpoint push_and_pop_same_cycle;      // Section 9
  cp_wrap : coverpoint pointer_wrapped {
    bins none = {0}; bins write = {1}; bins read = {2}; bins both = {3};
  }
  cp_depth_pow2 : coverpoint depth_is_power_of_two;            // Section 13
 
  // --- Metadata alignment (Sections 15-17).
  cp_meta_case : coverpoint metadata_write_case {
    bins together = {0}; bins data_only = {1}; bins meta_only = {2};  // 1,2 = §16
  }
 
  // --- Skid (Sections 18-20).
  cp_skid_case : coverpoint skid_case {
    bins pass_through = {0}; bins captured = {1}; bins held = {2}; bins drained = {3};
  }
  cp_skid_stall_boundary : coverpoint item_offered_as_ready_falls;  // Section 19
 
  // --- Watermarks (Sections 26-33).
  cp_wm_state : coverpoint wm_state_q { bins accepting = {0}; bins throttled = {1}; }
  cp_wm_dwell : coverpoint throttle_dwell {
    bins one_cycle = {1};                    // Section 32's chatter
    bins short = {[2:8]}; bins long = {[9:$]};
  }
  cp_arrivals_after_wm : coverpoint arrivals_since_watermark {
    bins none = {0}; bins some = {[1:HEADROOM-1]};
    bins at_headroom = {HEADROOM};           // Section 28's boundary
    bins over = {[HEADROOM+1:$]};            // MUST stay at zero
  }
 
  // --- Ping-pong (Sections 34-37).
  cp_bank_state : coverpoint bank_state_q_ut { bins each[] = {[0:3]}; }
  cp_pp_cycles : coverpoint completed_pingpong_cycles {
    bins none = {0}; bins one = {1}; bins several = {[2:$]};   // needs 3 blocks
  }
  cp_pp_consumer_slower : coverpoint consumer_slower_than_producer;  // Section 36
 
  // --- Replay and reassembly sizing (Sections 38-42).
  cp_replay_occ : coverpoint replay_occupancy {
    bins empty = {0}; bins mid = {[1:REPLAY_DEPTH-1]}; bins full = {REPLAY_DEPTH};
  }
  cp_replay_full_cause : coverpoint replay_full_cause {
    bins none = {0}; bins throughput = {1}; bins retry = {2}; bins recovery = {3};
  }
  cp_reasm_slots : coverpoint reasm_slots_busy {
    bins none = {0}; bins some = {[1:NUM_SLOTS-1]}; bins all = {NUM_SLOTS};
  }
  cp_first_frag_refused : coverpoint first_fragment_refused;   // Section 41
 
  // --- Partitioning (Sections 43-46).
  cp_reserve : coverpoint free_entries {
    bins above_reserve = {[PROGRESS_RESERVE+1:$]};
    bins at_reserve    = {PROGRESS_RESERVE};      // bulk must be refused here
    bins below_reserve = {[0:PROGRESS_RESERVE-1]};// only progress got in
  }
  cp_reserve_used : coverpoint progress_used_reserve;
 
  // --- CDC (Sections 47-49).
  cp_clock_ratio : coverpoint clock_ratio_class {
    bins same = {0}; bins rd_slower = {1}; bins rd_faster = {2}; bins unrelated = {3};
  }
  cp_cdc_occ : coverpoint cdc_occupancy_class {
    bins empty = {0}; bins mid = {1}; bins full = {2};
  }
 
  // --- Recovery (Sections 50-52).
  cp_recovery : coverpoint recovery_with_buffers {
    bins none = {0};
    bins some_nonempty = {1};
    bins all_nonempty = {2};                 // THE case — Section 58
  }
 
  // --- Crosses that carry the information.
  x_wm_arrivals : cross cp_wm_state, cp_arrivals_after_wm;   // Section 28
  x_pp_speed    : cross cp_bank_state, cp_pp_consumer_slower;// Section 36
  x_clock_cdc   : cross cp_clock_ratio, cp_cdc_occ;          // Section 48
  x_recovery_occ: cross cp_recovery, cp_occ;                 // Section 52
endcovergroup