Adapter Design

ACCEPTED transport object
    →  delivered semantically exactly once at the far end
    OR →  explicitly failed and reported
 
while physical attempts may be:  0, 1, 2, ... N

// ILLUSTRATIVE. NOT a UCIe format, and no field corresponds to any specified
// field (Section 3). Symbolic widths throughout.
typedef struct packed {
  logic [OBJ_ID_W-1:0]     object_id;    // the ADAPTER's identity for this object
  logic [SEM_ID_W-1:0]     sem_id;       // carried opaquely for 19.2's benefit
  logic [GEN_W-1:0]        sem_gen;      // ditto — the Adapter never interprets it
  logic [CLASS_W-1:0]      tclass;       // resource class for admission (Section 34)
  logic [LEN_W-1:0]        length;
  logic [CFG_EPOCH_W-1:0]  cfg_epoch;    // Section 44
  logic                    has_data;
  logic [DATA_W-1:0]       data;
} adapter_object_t;

// ILLUSTRATIVE. Every resource needed to RETAIN the object, secured before the
// object is accepted. Section 10 is the design that accepts first.
assign adapter_accept =
      in_valid
   && staging_space_available                    // somewhere to put it now
   && replay_slot_available                      // somewhere to KEEP it (Section 10)
   && credit_available[in_obj.tclass]            // the far end can take it (19.5)
   && link_accepting                             // the link manager permits it
   && cfg_stable;                                // not mid-commit (Section 44)
 
assign in_ready = adapter_accept;

// WRONG — the object is accepted on staging space alone, and the replay slot
// is sought later, when the object reaches the integrity stage.
assign adapter_accept = in_valid && staging_space_available && link_accepting;
 
// ... several stages later:
always_ff @(posedge clk)
  if (integrity_done && !replay_slot_available)
    stall_or_drop(obj);            // ← neither option is acceptable

// MANDATORY. Every accepted object is held by staging, by replay, or by both.
// tb_object_live() is TESTBENCH knowledge — the design has no signal for it.
property p_object_always_owned(int unsigned rid);
  @(posedge clk) disable iff (!rst_n)
    tb_object_live(rid) |-> (tb_in_staging(rid) || tb_in_replay(rid));
endproperty
a_object_always_owned: assert property (p_object_always_owned(REF_UT));
 
// Acceptance implies a replay slot was reserved.
property p_accept_implies_replay_slot;
  @(posedge clk) disable iff (!rst_n)
    adapter_accept |-> replay_slot_available;
endproperty
a_accept_implies_replay_slot: assert property (p_accept_implies_replay_slot);
 
// An accepted object is never dropped.
property p_no_silent_drop;
  @(posedge clk) disable iff (!rst_n)
    tb_object_accepted(REF_UT) |-> ##[1:$] (tb_object_retired(REF_UT)
                                         || tb_object_failed(REF_UT));
endproperty
a_no_silent_drop: assert property (p_no_silent_drop);
 
// Reservation and acceptance happen together, never one without the other.
property p_reserve_with_accept;
  @(posedge clk) disable iff (!rst_n)
    adapter_accept |=> (staging_alloc_fired && replay_reserved_for(prev_obj_id));
endproperty
a_reserve_with_accept: assert property (p_reserve_with_accept);

// ILLUSTRATIVE. Staging releases only when replay CONFIRMS it holds a durable
// copy. Both own it in between, deliberately (19.1 Section 16).
logic replay_commit;      // the entry is written and its metadata is valid
logic staging_release;
 
assign replay_commit   = replay_alloc_fire && replay_entry_written;
assign staging_release = replay_commit;              // NOT phy_tx_fire
assign staging_pop_fire = staging_release;

// WRONG — one memory, one lifetime, freed when the PHY takes the object.
always_ff @(posedge clk)
  if (phy_tx_fire)
    tx_mem_valid_q[tx_rd_ptr] <= 1'b0;     // ← the ONLY copy, gone at send

1. The object is written into the shared TX memory at admission.
2. The PHY consumes it. The entry is freed.
3. The far end reports an integrity failure — or reports nothing at all,
   and a timeout fires.
4. A retransmission is required.
5. -> there is no copy. The object cannot be retransmitted.
6. The Adapter must fail an object it promised to deliver, for a fault
   that was recoverable.

// ILLUSTRATIVE. ONE next-state owner. Every simultaneous event resolved by an
// explicit arm order — Section 17 is the alternative.
typedef enum logic [2:0] {
  TX_FREE          = 3'd0,
  TX_STAGED        = 3'd1,
  TX_HISTORY_OWNED = 3'd2,
  TX_SENT_WAIT_ACK = 3'd3,
  TX_REPLAY_PENDING= 3'd4,
  TX_RETIRED       = 3'd5,
  TX_FAILED        = 3'd6
} tx_state_e;
 
tx_state_e tx_state_q [MAX_TX_OBJ];
tx_state_e nxt;
 
always_comb begin
  nxt = tx_state_q[i];
  unique case (tx_state_q[i])
    TX_FREE:           if (admit_fire[i])                     nxt = TX_STAGED;
 
    TX_STAGED:         if (fatal[i])                          nxt = TX_FAILED;
                       else if (history_commit[i])            nxt = TX_HISTORY_OWNED;
 
    TX_HISTORY_OWNED:  if (fatal[i])                          nxt = TX_FAILED;
                       else if (attempt_launch[i])            nxt = TX_SENT_WAIT_ACK;
 
    // Priority here is the section's point: fatal, then retry, then resolve.
    TX_SENT_WAIT_ACK:  if (fatal[i])                          nxt = TX_FAILED;
                       else if (retry_indication[i])          nxt = TX_REPLAY_PENDING;
                       else if (resolved[i])                  nxt = TX_RETIRED;
 
    TX_REPLAY_PENDING: if (fatal[i])                          nxt = TX_FAILED;
                       else if (attempts_q[i] >= ATTEMPT_BUDGET)
                                                              nxt = TX_FAILED;
                       else if (attempt_launch[i])            nxt = TX_SENT_WAIT_ACK;
 
    TX_RETIRED:        if (slot_reclaim[i])                   nxt = TX_FREE;
    TX_FAILED:         if (slot_reclaim[i])                   nxt = TX_FREE;
    default:                                                  nxt = TX_FAILED;
  endcase
end
 
always_ff @(posedge clk or negedge rst_n)
  if (!rst_n) tx_state_q[i] <= TX_FREE;
  else        tx_state_q[i] <= nxt;

// WRONG — the acknowledgement path and the retry path each write the state.
// In the ack handler:
always_ff @(posedge clk) if (resolved[i])          tx_state_q[i] <= TX_RETIRED;
// In the retry handler, a different module:
always_ff @(posedge clk) if (retry_indication[i])  tx_state_q[i] <= TX_REPLAY_PENDING;

// MANDATORY. Only legal transitions, and the state comes from one function.
property p_legal_tx_transitions;
  @(posedge clk) disable iff (!rst_n)
    $changed(tx_state_q[IDX])
      |-> is_legal_tx_transition($past(tx_state_q[IDX]), tx_state_q[IDX]);
endproperty
a_legal_tx_transitions: assert property (p_legal_tx_transitions);
 
property p_tx_state_single_source;
  @(posedge clk) disable iff (!rst_n)
    $changed(tx_state_q[IDX]) |-> (tx_state_q[IDX] == $past(nxt_for(IDX)));
endproperty
a_tx_state_single_source: assert property (p_tx_state_single_source);
 
// A retry indication and a resolution together must NOT retire (Section 16).
property p_retry_beats_resolve;
  @(posedge clk) disable iff (!rst_n)
    ((tx_state_q[IDX] == TX_SENT_WAIT_ACK) && retry_indication[IDX] && resolved[IDX])
      |=> (tx_state_q[IDX] == TX_REPLAY_PENDING);
endproperty
a_retry_beats_resolve: assert property (p_retry_beats_resolve);
 
// An object in a working state always has a history entry.
property p_working_implies_history;
  @(posedge clk) disable iff (!rst_n)
    ((tx_state_q[IDX] == TX_SENT_WAIT_ACK) || (tx_state_q[IDX] == TX_REPLAY_PENDING))
      |-> replay_entry_valid_for(IDX);
endproperty
a_working_implies_history: assert property (p_working_implies_history);

// ILLUSTRATIVE. NOT a UCIe sequence format, and no width is claimed (Section 3).
typedef struct packed {
  logic                    valid;
  logic [OBJ_ID_W-1:0]     object_id;
  logic [SEQ_W-1:0]        seq;          // reliability identity (Section 8)
  logic [LEN_W-1:0]        length;
  logic [CFG_EPOCH_W-1:0]  cfg_epoch;    // Section 44
  logic [ATTEMPT_W-1:0]    attempts;     // evidence, and the budget (Section 16)
  logic [DATA_W-1:0]       data;         // the retained copy
} replay_entry_t;
 
// Payload storage — inferred RAM, deliberately NOT reset (19.1 Section 12).
replay_entry_t replay_mem [REPLAY_DEPTH];

// ILLUSTRATIVE circular replay buffer with three pointers. Wrap-safe compares
// via an extra bit — Section 23 is the version that uses equality alone.
localparam int PTR_W = $clog2(REPLAY_DEPTH);
 
logic [PTR_W:0] alloc_ptr_q;    // next entry to allocate      (extra MSB = wrap)
logic [PTR_W:0] send_ptr_q;     // next entry to transmit
logic [PTR_W:0] retire_ptr_q;   // oldest unresolved entry
 
// Index into the RAM with the low bits; compare with all bits.
wire [PTR_W-1:0] alloc_idx  = alloc_ptr_q[PTR_W-1:0];
wire [PTR_W-1:0] send_idx   = send_ptr_q[PTR_W-1:0];
wire [PTR_W-1:0] retire_idx = retire_ptr_q[PTR_W-1:0];
 
// Occupancy is a subtraction on the wide pointers — never an equality test.
wire [PTR_W:0] outstanding = alloc_ptr_q - retire_ptr_q;
wire           replay_full  = (outstanding == REPLAY_DEPTH[PTR_W:0]);
wire           replay_empty = (outstanding == '0);
wire           replay_slot_available = !replay_full;

// WRONG — allocation is gated on a check that does not account for wrap.
wire replay_full_wrong = (alloc_ptr_q[PTR_W-1:0] == retire_ptr_q[PTR_W-1:0]);
assign replay_slot_available = !replay_full_wrong;    // ← also true when EMPTY

1. The ring is full: REPLAY_DEPTH unresolved entries.
2. alloc_idx == retire_idx, so replay_full_wrong is TRUE... but the design
   may be using the opposite polarity, or checking only in one direction.
3. Allocation proceeds and overwrites the OLDEST UNRESOLVED entry.
4. That entry's object may still need retransmission.
5. A retry is later requested for it.
6. -> the ring returns the NEW object's data under the OLD sequence identity.

retire_ptr  <=  send_ptr  <=  alloc_ptr                (in wrap-extended order)
 
alloc_ptr - retire_ptr  <=  REPLAY_DEPTH               <- Section 21
send_ptr  - retire_ptr  <=  alloc_ptr - retire_ptr     <- cannot send unallocated

// MANDATORY. Occupancy never exceeds the depth (Section 21).
property p_replay_never_overfull;
  @(posedge clk) disable iff (!rst_n)
    ((alloc_ptr_q - retire_ptr_q) <= REPLAY_DEPTH);
endproperty
a_replay_never_overfull: assert property (p_replay_never_overfull);
 
// Allocation requires a free slot.
property p_alloc_requires_slot;
  @(posedge clk) disable iff (!rst_n)
    replay_alloc_fire |-> !replay_full;
endproperty
a_alloc_requires_slot: assert property (p_alloc_requires_slot);
 
// A live entry is never overwritten.
property p_no_overwrite_live_entry;
  @(posedge clk) disable iff (!rst_n)
    replay_alloc_fire |-> !replay_mem[alloc_idx].valid;
endproperty
a_no_overwrite_live_entry: assert property (p_no_overwrite_live_entry);
 
// Pointer ordering holds (Section 22).
property p_pointer_ordering;
  @(posedge clk) disable iff (!rst_n)
    (((send_ptr_q - retire_ptr_q) <= (alloc_ptr_q - retire_ptr_q))
     && ((alloc_ptr_q - retire_ptr_q) <= REPLAY_DEPTH));
endproperty
a_pointer_ordering: assert property (p_pointer_ordering);
 
// The retained copy is stable while the entry is valid (Section 19).
property p_replay_data_stable;
  @(posedge clk) disable iff (!rst_n)
    replay_mem[IDX].valid |-> $stable(replay_mem[IDX].data);
endproperty
a_replay_data_stable: assert property (p_replay_data_stable);

// ILLUSTRATIVE. At high load these coincide constantly. Pointers are
// independent, so each advances on its own event; occupancy is DERIVED and
// therefore never drifts.
always_ff @(posedge clk or negedge rst_n)
  if (!rst_n) begin
    alloc_ptr_q  <= '0;
    send_ptr_q   <= '0;
    retire_ptr_q <= '0;
  end else begin
    if (replay_alloc_fire)  alloc_ptr_q  <= alloc_ptr_q  + 1'b1;
    if (attempt_launch_any) send_ptr_q   <= send_ptr_q   + 1'b1;
    if (replay_retire_fire) retire_ptr_q <= retire_ptr_q + 1'b1;
  end

// ILLUSTRATIVE integrity pipeline. The function is abstract on purpose.
logic [CRC_W-1:0] crc_partial_q;
logic             crc_active_q;
 
always_ff @(posedge clk or negedge rst_n)
  if (!rst_n) begin
    crc_partial_q <= CRC_INIT;
    crc_active_q  <= 1'b0;
  end else if (crc_start) begin
    crc_partial_q <= crc_next(CRC_INIT, chunk_in);      // abstract (Section 25)
    crc_active_q  <= 1'b1;
  end else if (crc_feed && crc_active_q) begin
    crc_partial_q <= crc_next(crc_partial_q, chunk_in);
  end else if (crc_final && crc_active_q) begin
    crc_active_q  <= 1'b0;
  end
 
assign crc_result = crc_finalise(crc_partial_q);

// ILLUSTRATIVE. Everything the result covers travels as ONE object, so a stall
// cannot advance one part without the other.
typedef struct packed {
  logic [META_W-1:0] meta;      // whatever the architecture requires covered
  logic [DATA_W-1:0] data;
  logic              last;
  logic              valid;
} crc_input_t;
 
crc_input_t crc_in_q;

// WRONG — metadata is taken from a live signal while the data path stalls.
assign crc_input = {live_meta, staged_data};       // ← two different lifetimes

1. The CRC is computed over {meta = A, data = D}.
2. The data path stalls; the object waits.
3. live_meta changes to B — a new configuration, a new class, a re-derived field.
4. The object is finally transmitted as {meta = B, data = D}.
5. The far end recomputes over {B, D} and gets a different result.
6. -> integrity FAILS on data that is completely correct.

// MANDATORY. The covered bundle does not change while the object waits.
property p_crc_input_stable_under_stall;
  @(posedge clk) disable iff (!rst_n)
    (crc_in_q.valid && !crc_consume) |=> $stable(crc_in_q);
endproperty
a_crc_input_stable_under_stall:
  assert property (p_crc_input_stable_under_stall);
 
// The result accompanies the object it was computed over.
property p_crc_accompanies_its_object(int unsigned rid);
  @(posedge clk) disable iff (!rst_n)
    (phy_tx_fire && (tb_ref_id == rid))
      |-> (tx_crc == tb_expected_crc(rid));
endproperty
a_crc_accompanies_its_object:
  assert property (p_crc_accompanies_its_object(REF_UT));
 
// The accumulator is bounded to exactly one object.
property p_crc_active_one_object;
  @(posedge clk) disable iff (!rst_n)
    crc_start |-> !crc_active_q;
endproperty
a_crc_active_one_object: assert property (p_crc_active_one_object);
 
// The result's valid is aligned with the object's (Section 29).
property p_crc_valid_aligned;
  @(posedge clk) disable iff (!rst_n)
    tx_obj_valid |-> tx_crc_valid;
endproperty
a_crc_valid_aligned: assert property (p_crc_valid_aligned);

// WRONG — the result path is one stage longer than the object path.
always_ff @(posedge clk) begin
  obj_q1 <= obj_in;   obj_q2 <= obj_q1;                       // 2 stages
  crc_q1 <= crc_in;   crc_q2 <= crc_q1;   crc_q3 <= crc_q2;   // 3 stages
end
assign tx_obj = obj_q2;
assign tx_crc = crc_q3;          // ← object N is sent with the result for N-1

// ILLUSTRATIVE. Five terms, evaluated COMBINATIONALLY into the delivery.
// Section 31 is the version that delivers first.
assign rx_semantic_deliver =
      rx_object_complete       // every part of the object arrived (Section 39)
   && rx_integrity_ok          // it passed (Section 25)
   && !rx_duplicate            // the window says it is new (Section 32)
   && rx_in_window             // and it is within the acceptable range
   && rx_downstream_space;     // the protocol engine can take it

// WRONG — the object is delivered as it is reconstructed, and checked after.
always_ff @(posedge clk)
  if (rx_object_complete) begin
    deliver_to_protocol(rx_obj);        // ← delivered
    start_integrity_check(rx_obj);      // ← checked
    update_duplicate_window(rx_obj);    // ← and novelty decided
  end

// ILLUSTRATIVE receive window. A BITMAP over a bounded sequence range, not a
// single last-sequence register — Section 33 is that version.
logic [WINDOW-1:0] received_q;        // one bit per sequence position
logic [SEQ_W:0]    window_base_q;     // wrap-extended, like the ring (Section 20)
 
wire [SEQ_W:0] offset = rx_seq - window_base_q;
wire           in_window = (offset < WINDOW[SEQ_W:0]);
wire           is_duplicate = in_window && received_q[offset[$clog2(WINDOW)-1:0]];
 
always_ff @(posedge clk or negedge rst_n)
  if (!rst_n) begin
    received_q     <= '0;
    window_base_q  <= '0;
  end else begin
    // Record, guarded so a duplicate changes nothing.
    if (rx_accept_fire && in_window && !is_duplicate)
      received_q[offset[$clog2(WINDOW)-1:0]] <= 1'b1;
 
    // Slide the base past a contiguous run of received positions.
    if (received_q[0]) begin
      received_q    <= {1'b0, received_q[WINDOW-1:1]};
      window_base_q <= window_base_q + 1'b1;
    end
  end

// WRONG — only the most recent accepted sequence is remembered.
always_ff @(posedge clk)
  if (rx_accept_fire) last_seq_q <= rx_seq;
 
assign is_duplicate = (rx_seq == last_seq_q);       // ← only ONE back

// MANDATORY. The property the entire receive architecture exists for.
int unsigned tb_deliveries [int];      // reference object id -> semantic deliveries
 
always @(posedge clk) if (rx_semantic_deliver)
  tb_deliveries[tb_ref_id_of(rx_obj)]++;
 
property p_delivery_at_most_once(int unsigned rid);
  @(posedge clk) disable iff (!rst_n)
    (tb_deliveries[rid] <= 1);
endproperty
a_delivery_at_most_once: assert property (p_delivery_at_most_once(REF_UT));
 
// A duplicate delivers nothing.
property p_duplicate_delivers_nothing;
  @(posedge clk) disable iff (!rst_n)
    (rx_object_complete && rx_duplicate) |-> !rx_semantic_deliver;
endproperty
a_duplicate_delivers_nothing: assert property (p_duplicate_delivers_nothing);
 
// A duplicate is still acknowledged (14.3 Section 22).
property p_duplicate_still_acknowledged;
  @(posedge clk) disable iff (!rst_n)
    (rx_object_complete && rx_duplicate) |-> ##[1:ACK_BOUND] rx_ack_sent;
endproperty
a_duplicate_still_acknowledged:
  assert property (p_duplicate_still_acknowledged);
 
// A failed integrity check delivers nothing.
property p_corrupt_delivers_nothing;
  @(posedge clk) disable iff (!rst_n)
    (rx_object_complete && !rx_integrity_ok) |-> !rx_semantic_deliver;
endproperty
a_corrupt_delivers_nothing: assert property (p_corrupt_delivers_nothing);
 
// The window record is idempotent.
property p_window_record_idempotent;
  @(posedge clk) disable iff (!rst_n)
    (rx_accept_fire && is_duplicate) |=> $stable(received_q);
endproperty
a_window_record_idempotent: assert property (p_window_record_idempotent);

// ILLUSTRATIVE. Position-indexed storage, and a BITMAP of what has arrived.
logic [MAX_FRAGS-1:0] frag_received_q [MAX_RX_INFLIGHT];
logic [DATA_W-1:0]    reasm_mem       [MAX_RX_INFLIGHT][MAX_FRAGS];
 
always_ff @(posedge clk)
  if (frag_valid && rx_obj_q[frag.obj_slot].valid) begin
    reasm_mem[frag.obj_slot][frag.frag_idx] <= frag.data;   // by INDEX
    if (!frag_received_q[frag.obj_slot][frag.frag_idx])     // GUARDED
      frag_received_q[frag.obj_slot][frag.frag_idx] <= 1'b1;
  end
 
assign rx_object_complete[s] =
    (frag_received_q[s] & frag_mask(rx_obj_q[s].frag_count))
    == frag_mask(rx_obj_q[s].frag_count);

// WRONG — a count of received fragments.
always_ff @(posedge clk)
  if (frag_valid) frag_count_q[slot] <= frag_count_q[slot] + 1'b1;
 
assign rx_object_complete[slot] = (frag_count_q[slot] == expected_frags[slot]);

// MANDATORY. Completion requires the full unique set for THIS object.
property p_reassembly_complete_unique;
  @(posedge clk) disable iff (!rst_n)
    rx_deliver_fire |-> ((frag_received_q[dslot] & frag_mask(rx_obj_q[dslot].frag_count))
                         == frag_mask(rx_obj_q[dslot].frag_count));
endproperty
a_reassembly_complete_unique:
  assert property (p_reassembly_complete_unique);
 
property p_duplicate_fragment_idempotent;
  @(posedge clk) disable iff (!rst_n)
    (frag_valid && frag_received_q[frag.obj_slot][frag.frag_idx])
      |=> $stable(frag_received_q[frag.obj_slot]);
endproperty
a_duplicate_fragment_idempotent:
  assert property (p_duplicate_fragment_idempotent);
 
property p_stale_fragment_ignored;
  @(posedge clk) disable iff (!rst_n)
    (frag_valid && !rx_obj_q[frag.obj_slot].valid) |=> $stable(frag_received_q);
endproperty
a_stale_fragment_ignored: assert property (p_stale_fragment_ignored);

// ILLUSTRATIVE. Per class, because the classes have independent downstream
// resources. The arithmetic and the return path are 19.5's.
logic [CREDIT_W-1:0] credit_q [NUM_CLASSES];
assign credit_available[c] = (credit_q[c] != '0);

// WRONG — one counter for every class.
logic [CREDIT_W-1:0] credit_q;
assign credit_available = (credit_q != '0);

// ILLUSTRATIVE. Three contenders with a bounded policy — Sections 41 and 42
// are the two strict-priority designs.
logic new_pending, replay_pending, mgmt_pending;
logic [AGE_W-1:0] replay_age_q;      // saturating
logic [AGE_W-1:0] new_age_q;         // saturating
logic [BUD_W-1:0] replay_budget_q;   // consecutive replays before yielding
 
wire replay_starved = (replay_age_q >= REPLAY_BOUND);
wire new_starved    = (new_age_q    >= NEW_BOUND);
wire replay_capped  = (replay_budget_q == '0);
 
always_comb begin
  tx_select = SEL_NONE;
  if (mgmt_pending)                                    tx_select = SEL_MGMT;
  else if (replay_pending && replay_starved)           tx_select = SEL_REPLAY;
  else if (new_pending && new_starved)                 tx_select = SEL_NEW;
  else if (replay_pending && !replay_capped)           tx_select = SEL_REPLAY;
  else if (new_pending)                                tx_select = SEL_NEW;
  else if (replay_pending)                             tx_select = SEL_REPLAY;
end

// WRONG — a pending replay waits behind every new object, forever.
assign tx_select = new_pending ? SEL_NEW : SEL_REPLAY;

1. Under sustained load new_pending is permanently true.
2. A pending replay is never scheduled.
3. Its ring entry is never resolved, so retire_ptr never advances.
4. The ring fills.
5. Admission stops (Section 9), so new_pending eventually falls.
6. -> the replay finally goes — but only after the entire ring has filled,
     and only after admission has stalled completely.

// WRONG — new traffic waits behind every pending replay, forever.
assign tx_select = replay_pending ? SEL_REPLAY : SEL_NEW;

1. A marginal link causes a steady retry rate.
2. Every replay that fails becomes another pending replay.
3. replay_pending is permanently true.
4. New traffic is never scheduled.
5. -> the link is fully utilised and delivers nothing new, indefinitely.

// LIVENESS, bounded, both directions, with assumptions stated (15.2 §36).
//
//   A1: the PHY eventually accepts a selected object
//   A2: a pending class stays pending until served
//   A3: recovery terminates (14.2 §30)
assume property (@(posedge clk) disable iff (!rst_n)
  ((tx_select != SEL_NONE) && !recovery_active) |-> ##[1:PHY_BOUND] phy_tx_fire);
assume property (@(posedge clk) disable iff (!rst_n)
  (replay_pending && !phy_tx_fire) |=> replay_pending);
 
property p_replay_eventually_scheduled;
  @(posedge clk) disable iff (!rst_n)
    replay_pending |-> ##[1:REPLAY_BOUND] ((tx_select == SEL_REPLAY) && phy_tx_fire);
endproperty
a_replay_eventually_scheduled:
  assert property (p_replay_eventually_scheduled);
 
property p_new_eventually_scheduled;
  @(posedge clk) disable iff (!rst_n)
    new_pending |-> ##[1:NEW_BOUND] ((tx_select == SEL_NEW) && phy_tx_fire);
endproperty
a_new_eventually_scheduled: assert property (p_new_eventually_scheduled);
 
// The replay budget is real — not a parameter set to infinity.
initial begin
  assert (REPLAY_BUDGET > 0 && REPLAY_BUDGET < 32'hFFFF_FFFF)
    else $fatal(1, "replay budget must be finite and non-zero (Section 42)");
end

// WRONG — the replay entry is freed when the PHY takes the object.
always_ff @(posedge clk)
  if (phy_tx_fire) begin
    replay_mem[send_idx].valid <= 1'b0;
    retire_ptr_q <= retire_ptr_q + 1'b1;      // ← retirement, at the send
  end

// MANDATORY. An entry retires only on resolution.
property p_retire_requires_resolution;
  @(posedge clk) disable iff (!rst_n)
    replay_retire_fire |-> resolved_for(retire_idx);
endproperty
a_retire_requires_resolution: assert property (p_retire_requires_resolution);
 
// The entry is not freed at the send.
property p_not_freed_on_send;
  @(posedge clk) disable iff (!rst_n)
    (phy_tx_fire && !resolved_for(send_idx)) |=> $stable(retire_ptr_q);
endproperty
a_not_freed_on_send: assert property (p_not_freed_on_send);
 
// Retirement is in order — the oldest unresolved entry retires first.
property p_retire_in_order;
  @(posedge clk) disable iff (!rst_n)
    replay_retire_fire |-> (retire_idx == retire_ptr_q[PTR_W-1:0]);
endproperty
a_retire_in_order: assert property (p_retire_in_order);
 
// An object is never retired while a retransmission is pending for it.
property p_no_retire_with_replay_pending;
  @(posedge clk) disable iff (!rst_n)
    replay_retire_fire |-> (tx_state_q[retire_obj] != TX_REPLAY_PENDING);
endproperty
a_no_retire_with_replay_pending:
  assert property (p_no_retire_with_replay_pending);

// ILLUSTRATIVE. Requested-versus-active, and the commit guard that a
// retransmission makes necessary.
link_cfg_t              requested_cfg_q, active_cfg_q;
logic [CFG_EPOCH_W-1:0] active_cfg_epoch_q;
 
assign cfg_commit_allowed =
      cfg_validated
   && (staging_occupancy == '0)
   && (replay_outstanding == '0);     // ← the term a block-level design omits
 
always_ff @(posedge clk or negedge rst_n)
  if (!rst_n)
    active_cfg_epoch_q <= '0;
  else if (cfg_commit_fire) begin
    active_cfg_q       <= requested_cfg_q;
    active_cfg_epoch_q <= active_cfg_epoch_q + 1'b1;
  end

// MANDATORY. The active configuration changes only at a guarded commit.
property p_cfg_only_at_commit;
  @(posedge clk) disable iff (!rst_n)
    $changed(active_cfg_q) |-> $past(cfg_commit_fire);
endproperty
a_cfg_only_at_commit: assert property (p_cfg_only_at_commit);
 
property p_commit_requires_drain_and_empty_ring;
  @(posedge clk) disable iff (!rst_n)
    cfg_commit_fire |-> (($past(staging_occupancy) == '0)
                      && ($past(replay_outstanding) == '0));
endproperty
a_commit_requires_drain_and_empty_ring:
  assert property (p_commit_requires_drain_and_empty_ring);
 
// A live object's captured epoch never changes under it.
property p_object_epoch_stable;
  @(posedge clk) disable iff (!rst_n)
    replay_mem[IDX].valid |-> $stable(replay_mem[IDX].cfg_epoch);
endproperty
a_object_epoch_stable: assert property (p_object_epoch_stable);
 
// A retransmission uses the object's captured epoch, not the live one.
property p_retransmit_uses_captured_epoch;
  @(posedge clk) disable iff (!rst_n)
    (phy_tx_fire && is_retransmit) |-> (tx_cfg_epoch == replay_mem[send_idx].cfg_epoch);
endproperty
a_retransmit_uses_captured_epoch:
  assert property (p_retransmit_uses_captured_epoch);

// WRONG — a recovery is treated as a reason to start clean.
always_ff @(posedge clk)
  if (recovery_entered) begin
    for (int i = 0; i < REPLAY_DEPTH; i++) replay_mem[i].valid <= 1'b0;
    alloc_ptr_q  <= '0;
    send_ptr_q   <= '0;
    retire_ptr_q <= '0;
    received_q   <= '0;                       // the duplicate window too
  end

// MANDATORY. Obligations, identities and evidence survive a recovery.
property p_replay_survives_recovery;
  @(posedge clk) disable iff (!rst_n)
    recovery_entered |=> ($stable(replay_mem[IDX].valid)
                       && $stable(replay_mem[IDX].object_id)
                       && $stable(replay_mem[IDX].cfg_epoch)
                       && $stable(replay_mem[IDX].attempts));
endproperty
a_replay_survives_recovery: assert property (p_replay_survives_recovery);
 
// The duplicate window is not cleared (Section 50).
property p_window_survives_recovery;
  @(posedge clk) disable iff (!rst_n)
    recovery_entered |=> $stable(received_q);
endproperty
a_window_survives_recovery: assert property (p_window_survives_recovery);
 
// A recovery produces neither an acceptance nor a retirement.
property p_recovery_no_transport_event;
  @(posedge clk) disable iff (!rst_n)
    recovery_entered |=> ($stable(accept_count) && $stable(retire_count));
endproperty
a_recovery_no_transport_event:
  assert property (p_recovery_no_transport_event);
 
// No new admission while the link manager forbids it.
property p_no_admission_during_recovery;
  @(posedge clk) disable iff (!rst_n)
    recovery_active |-> !adapter_accept;
endproperty
a_no_admission_during_recovery:
  assert property (p_no_admission_during_recovery);
 
// The first fault survives (19.1 Section 35).
property p_first_fault_survives;
  @(posedge clk) disable iff (!rst_n)
    recovery_entered |=> $stable(first_fault_q);
endproperty
a_first_fault_survives: assert property (p_first_fault_survives);

// Diagnostic only, in the POR reset domain (19.1 Section 7).
logic [63:0] integrity_fail_q;
logic [63:0] retry_count_q;
logic [63:0] replay_attempts_q;
logic [63:0] duplicate_suppressed_q;      // Section 32 — the guard working
logic [63:0] out_of_window_q;             // Section 32 — stale or corrupt
logic [63:0] recovery_cycles_q;
logic [63:0] replay_full_stall_q;         // Section 9's second term biting
logic [63:0] staging_full_stall_q;
logic [63:0] incomplete_object_q;         // Section 35 — abandoned reassembly

// ILLUSTRATIVE. 15.5 Section 10's causal-priority classifier, at admission.
typedef enum logic [3:0] {
  ADP_ACCEPT     = 4'd0,
  ADP_NO_INPUT   = 4'd1,   // nothing offered           <- must be early
  ADP_RECOVERY   = 4'd2,
  ADP_CFG_COMMIT = 4'd3,   // a deliberate quiesce
  ADP_LINK_DOWN  = 4'd4,
  ADP_STAGING_FULL = 4'd5,
  ADP_REPLAY_FULL  = 4'd6, // Section 9's second term
  ADP_NO_CREDIT    = 4'd7,
  ADP_PHY_STALL    = 4'd8,
  ADP_UNATTRIB     = 4'd9  // must stay at zero
} adp_stall_e;
 
adp_stall_e adp_reason_d;
 
always_comb begin
  unique case (1'b1)
    adapter_accept              : adp_reason_d = ADP_ACCEPT;
    !in_valid                   : adp_reason_d = ADP_NO_INPUT;
    recovery_active             : adp_reason_d = ADP_RECOVERY;
    !cfg_stable                 : adp_reason_d = ADP_CFG_COMMIT;
    !link_accepting             : adp_reason_d = ADP_LINK_DOWN;
    !staging_space_available    : adp_reason_d = ADP_STAGING_FULL;
    !replay_slot_available      : adp_reason_d = ADP_REPLAY_FULL;
    !credit_available[in_class] : adp_reason_d = ADP_NO_CREDIT;
    !phy_tx_ready               : adp_reason_d = ADP_PHY_STALL;
    default                     : adp_reason_d = ADP_UNATTRIB;
  endcase
end

// Verification-only. FOUR models. 19.2's semantic model stays separate.
class adapter_scoreboard;
 
  // ---- Layer 1: OBJECT model — accepted, state, epoch, retired.
  typedef struct {
    bit  accepted;
    int  state;
    int  cfg_epoch;
    bit  in_staging, in_replay;      // TWO fields — Section 11's window
    bit  retired, failed;
    bit  crossed_recovery;
  } object_model_t;
  object_model_t objs [int];
 
  // ---- Layer 2: REPLAY / HISTORY model — attempts and resolution.
  typedef struct {
    int  seq;
    int  attempts;                   // >= 1 once sent
    bit  resolved;
    bit  overwritten;                // Section 21 — must never be set
  } history_model_t;
  history_model_t hist [int];
 
  // ---- Layer 3: RX-DELIVERY model — integrity, novelty, delivery count.
  typedef struct {
    bit  integrity_ok;
    bit  was_duplicate;
    bit  in_window;
    int  semantic_deliveries;        // MUST be <= 1
    bit [63:0] frags_received;
    int  frag_count;
  } rx_model_t;
  rx_model_t rx [int];
 
  // ---- Layer 4: RESOURCE model — occupancies and credits by class.
  typedef struct {
    int staging_occ, replay_occ;
    int credits_available, credits_outstanding;
  } resource_model_t;
  resource_model_t res [int];
 
  // ---- Catches Sections 10 and 14 — an object owned by nothing.
  function void check_ownership(int id);
    if (objs[id].accepted && !objs[id].retired && !objs[id].failed
        && !objs[id].in_staging && !objs[id].in_replay)
      $error("OBJECT %0d owned by NOTHING (Sections 10, 14)", id);
  endfunction
 
  // ---- Catches Section 21 — the overwrite, before it corrupts a retry.
  function void check_no_overwrite(int id);
    if (hist[id].overwritten)
      $error("HISTORY %0d overwritten while unresolved (Section 21)", id);
  endfunction
 
  // ---- Catches Sections 31, 33, 36 — delivery more than once.
  function void check_delivery(int id);
    if (rx[id].semantic_deliveries > 1)
      $error("OBJECT %0d delivered %0d times (must be <= 1)", id, rx[id].semantic_deliveries);
    if ((rx[id].semantic_deliveries > 0) && !rx[id].integrity_ok)
      $error("OBJECT %0d delivered with failed integrity (Section 31)", id);
    if ((rx[id].semantic_deliveries > 0)
        && ((rx[id].frags_received & frag_mask(rx[id].frag_count))
            != frag_mask(rx[id].frag_count)))
      $error("OBJECT %0d delivered incomplete (Section 36)", id);
  endfunction
 
  // ---- Catches Section 45 — retired before resolution.
  function void check_retirement(int id);
    if (objs[id].retired && !hist[id].resolved)
      $error("OBJECT %0d retired without resolution (Section 45)", id);
  endfunction
 
  // ---- Catches Section 50.
  function void check_recovery(int id);
    if (objs[id].crossed_recovery && !objs[id].retired && !objs[id].failed
        && !objs[id].in_replay)
      $error("OBJECT %0d lost its history across a recovery (Section 50)", id);
  endfunction
 
endclass

covergroup cg_adapter @(posedge clk);
  option.per_instance = 1;
 
  // --- Admission (Sections 9-11).
  cp_admit_refusal : coverpoint admit_refusal_reason {
    bins staging = {0}; bins replay = {1}; bins credit = {2};
    bins link = {3}; bins cfg = {4};                    // each term alone
  }
  cp_staging_occ : coverpoint staging_occupancy {
    bins empty = {0}; bins mid = {[1:STAGING_DEPTH-1]}; bins full = {STAGING_DEPTH};
  }
  cp_replay_occ : coverpoint replay_outstanding {
    bins empty = {0}; bins mid = {[1:REPLAY_DEPTH-1]}; bins full = {REPLAY_DEPTH};
  }
  cp_dual_window : coverpoint dual_ownership_window_active;   // Section 13
  cp_error_in_window : coverpoint error_during_ownership_handoff;
 
  // --- TX state (Sections 15-18).
  cp_tx_state : coverpoint tx_state_q_ut { bins each[] = {[0:6]}; }
  cp_simul_retry_resolve : coverpoint retry_and_resolve_same_cycle;  // Section 16
  cp_attempts : coverpoint attempts_q_ut {
    bins one = {1}; bins few = {[2:3]}; bins budget = {ATTEMPT_BUDGET};
  }
 
  // --- Ring (Sections 20-24).
  cp_ring_wrap : coverpoint ring_pointer_wrapped {
    bins none = {0}; bins alloc = {1}; bins send = {2}; bins retire = {3};
  }
  cp_simul_alloc_retire : coverpoint alloc_and_retire_same_cycle;
  cp_ring_full_sustained : coverpoint ring_full_for_n_cycles {
    bins none = {0}; bins brief = {[1:16]}; bins sustained = {[17:$]};  // Section 21
  }
 
  // --- Integrity (Sections 25-29).
  cp_crc_outcome : coverpoint integrity_outcome {
    bins pass = {0}; bins fail = {1};
  }
  cp_stall_during_crc : coverpoint stall_between_crc_and_send;   // Section 27
  cp_back_to_back : coverpoint consecutive_objects_differing;    // Section 29
 
  // --- Receive (Sections 30-37).
  cp_rx_outcome : coverpoint rx_object_outcome {
    bins delivered = {0}; bins corrupt = {1}; bins duplicate = {2};
    bins out_of_window = {3}; bins no_space = {4};      // all five gate terms
  }
  cp_dup_position : coverpoint duplicate_window_position {
    bins at_base = {0}; bins middle = {1}; bins far_edge = {2};   // Section 33
  }
  cp_frag_event : coverpoint fragment_event {
    bins in_order = {0}; bins reordered = {1}; bins duplicate = {2}; bins missing = {3};
  }
 
  // --- Scheduler (Sections 40-43).
  cp_sched_select : coverpoint tx_select_ut {
    bins none = {0}; bins new_traffic = {1}; bins replay = {2}; bins mgmt = {3};
  }
  cp_replay_budget : coverpoint replay_budget_q_ut {
    bins full = {REPLAY_BUDGET}; bins some = {[1:REPLAY_BUDGET-1]}; bins spent = {0};
  }
  cp_starvation : coverpoint starvation_override_fired {
    bins none = {0}; bins replay_override = {1}; bins new_override = {2};
  }
 
  // --- Configuration and recovery (Sections 47-51).
  cp_cfg_context : coverpoint cfg_commit_context {
    bins idle = {0}; bins blocked_by_staging = {1};
    bins blocked_by_replay = {2}; bins forced = {3};
  }
  cp_recovery_context : coverpoint recovery_with_state {
    bins none = {0};
    bins ring_nonempty = {1};
    bins window_populated = {2};
    bins reassembly_partial = {3};
    bins all = {4};                                    // THE case — Section 56
  }
 
  // --- Attribution (Section 52).
  cp_stall_reason : coverpoint adp_reason_d { bins each[] = {[0:9]}; }
 
  // --- Crosses that carry the information.
  x_ring_retry     : cross cp_ring_full_sustained, cp_attempts;     // Section 21
  x_dup_position   : cross cp_dup_position, cp_rx_outcome;          // Section 33
  x_recovery_ring  : cross cp_recovery_context, cp_replay_occ;      // Section 56
  x_sched_budget   : cross cp_sched_select, cp_replay_budget;       // Section 42
endcovergroup