Protocol Engines

1 semantic operation        — what the client asked for; the ENGINE owns it
    ↓
N normalised objects        — request metadata, data, completion (§31)
    ↓
N Adapter transport objects — 19.3's subject
    ↓
≥N physical attempts        — retries add attempts, not objects

semantic allocations per operation   == 1        <- Section 19
normalised objects per operation     >= 1        <- Section 31
transport objects per normalised obj == 1
attempts per transport object        >= 1        <- 19.3
semantic completions per operation   == 1        <- Section 35

// ILLUSTRATIVE. NOT a UCIe encoding, and the values carry no normative meaning
// (Section 3). The class exists so that later stages can apply per-protocol
// policy without re-deriving it from the payload.
typedef enum logic [1:0] {
  PROTO_PCIE   = 2'd0,
  PROTO_CXL    = 2'd1,
  PROTO_STREAM = 2'd2
} proto_class_e;

// ILLUSTRATIVE internal object. NOT a UCIe, PCIe or CXL format, and no field
// corresponds to any specified field of any of them (Section 3).
typedef struct packed {
  logic [SEM_ID_W-1:0]  semantic_id;    // the ENGINE's identity for the operation
  logic [GEN_W-1:0]     generation;     // Section 22
  proto_class_e         proto;          // carried, not derived (Section 7)
  logic [TYPE_W-1:0]    type_class;     // the protocol's own operation category
  logic [DEST_W-1:0]    destination;    // captured at acceptance, never recomputed
  logic [LEN_W-1:0]     length;
  logic [PART_W-1:0]    part_idx;       // which part of a multi-object operation
  logic [PART_W-1:0]    part_count;     // Section 31
  logic [CFG_EPOCH_W-1:0] cfg_epoch;    // Section 42
  logic                 has_data;
  logic [META_W-1:0]    metadata;       // protocol-specific, carried OPAQUELY
} protocol_object_t;

// WRONG — two higher-layer operations with different semantics are normalised
// to the same internal type, because they "look the same" at this level.
always_comb
  case (client_op)
    OP_A, OP_B: norm_obj.type_class = TYPE_READ;   // ← A and B are NOT the same
    default:    norm_obj.type_class = TYPE_OTHER;
  endcase

1. A and B both become TYPE_READ.
2. The object crosses. Transport is perfect: clean integrity, no retries.
3. The remote engine reconstructs a TYPE_READ.
4. It cannot tell whether this was an A or a B.
5. -> it applies one protocol's rule to the other's operation.

// MANDATORY. For every accepted client request, the normalised object retains
// every field the far end needs to reconstruct the operation.
//
// tb_required_fields() is TESTBENCH knowledge: it is the reference model's
// statement of what reconstruction needs, derived from the protocol, not from
// the design. Synthesising it would compare the design to itself.
property p_normalisation_lossless(int unsigned rid);
  @(posedge clk) disable iff (!rst_n)
    (norm_fire && (tb_ref_id == rid))
      |-> tb_fields_preserved(rid, norm_obj);
endproperty
a_normalisation_lossless: assert property (p_normalisation_lossless(REF_UT));
 
// The class is carried, not re-derived downstream.
property p_class_stable_through_pipeline;
  @(posedge clk) disable iff (!rst_n)
    obj_live(IDX) |-> $stable(obj_q[IDX].proto);
endproperty
a_class_stable_through_pipeline:
  assert property (p_class_stable_through_pipeline);
 
// The reconstructed operation at the far end equals what was accepted here.
property p_reconstruction_matches(int unsigned rid);
  @(posedge clk) disable iff (!rst_n)
    (remote_reconstruct_fire && (tb_ref_id == rid))
      |-> (remote_op_signature == tb_op_signature(rid));
endproperty
a_reconstruction_matches: assert property (p_reconstruction_matches(REF_UT));

// ILLUSTRATIVE. One queue per protocol class, so a burst in one cannot block
// another's head — 18.2 Section 14's argument, at the protocol boundary.
typedef struct packed {
  logic [SEM_ID_W-1:0]  client_tag;      // the client's own identity
  logic [TYPE_W-1:0]    type_class;
  logic [DEST_W-1:0]    destination;
  logic [LEN_W-1:0]     length;
  logic [META_W-1:0]    metadata;
} ingress_entry_t;
 
// Payload storage — inferred RAM, deliberately NOT reset (19.1 Section 12).
ingress_entry_t   ing_mem [NUM_PROTO][ING_DEPTH];
logic [PTR_W-1:0] ing_wr_q  [NUM_PROTO];
logic [PTR_W-1:0] ing_rd_q  [NUM_PROTO];
logic [OCC_W-1:0] ing_occ_q [NUM_PROTO];
 
logic [NUM_PROTO-1:0] ing_request;
always_comb
  for (int p = 0; p < NUM_PROTO; p++)
    ing_request[p] = (ing_occ_q[p] != '0);
 
always_ff @(posedge clk or negedge rst_n)
  if (!rst_n) begin
    for (int p = 0; p < NUM_PROTO; p++) begin
      ing_wr_q[p]  <= '0;
      ing_rd_q[p]  <= '0;
      ing_occ_q[p] <= '0;
    end
  end else begin
    for (int p = 0; p < NUM_PROTO; p++) begin
      if (ing_push_fire[p]) ing_wr_q[p] <= ing_wr_q[p] + 1'b1;
      if (ing_pop_fire[p])  ing_rd_q[p] <= ing_rd_q[p] + 1'b1;
 
      unique case ({ing_push_fire[p], ing_pop_fire[p]})
        2'b10: ing_occ_q[p] <= ing_occ_q[p] + 1'b1;
        2'b01: ing_occ_q[p] <= ing_occ_q[p] - 1'b1;
        default: ;                        // both or neither: hold
      endcase
    end
  end

// WRONG — every protocol pushes into one queue, and classification happens
// after the pop.
assign shared_push = pcie_valid || cxl_valid || stream_valid;

1. A streaming burst of 64 objects fills the shared queue.
2. A latency-sensitive completion from another protocol arrives and queues
   behind all 64.
3. It waits for the entire burst.
4. If that completion is what RELEASES a resource the streaming traffic
   needs, the burst cannot drain either.
5. -> deadlock, on a design where every block is individually correct.

// ILLUSTRATIVE arbiter over per-protocol queues. Rotating fairness plus a
// bounded override for the class that releases resources.
logic [NUM_PROTO-1:0] req, grant;
logic [PR_W-1:0]      last_grant_q;
logic [AGE_W-1:0]     wait_age_q [NUM_PROTO];      // saturating
logic [NUM_PROTO-1:0] is_progress_class;           // static configuration
 
logic [NUM_PROTO-1:0] rotated;
always_comb
  for (int p = 0; p < NUM_PROTO; p++)
    rotated[p] = req[(p + last_grant_q + 1) % NUM_PROTO];
 
logic [NUM_PROTO-1:0] aged_out;
always_comb
  for (int p = 0; p < NUM_PROTO; p++)
    aged_out[p] = req[p] && (wait_age_q[p] >= class_bound(p));
 
always_comb begin
  grant = '0;
  if (!downstream_can_accept)                    grant = '0;
  else if (|(aged_out & is_progress_class))      grant = lowest_set(aged_out & is_progress_class);
  else if (|aged_out)                            grant = lowest_set(aged_out);
  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 p = 0; p < NUM_PROTO; p++) wait_age_q[p] <= '0;
  end else begin
    // THE rule: advance only on an actual transfer.
    if (|grant && xfer_fire)
      last_grant_q <= onehot_to_index(grant);
 
    for (int p = 0; p < NUM_PROTO; p++) begin
      if (req[p] && !(grant[p] && xfer_fire))
        wait_age_q[p] <= (wait_age_q[p] == AGE_MAX) ? AGE_MAX : wait_age_q[p] + 1'b1;
      else if (grant[p] && xfer_fire)
        wait_age_q[p] <= '0;
    end
  end

// MANDATORY. At most one grant, only to a requester, and the pointer moves
// only on a transfer.
property p_one_grant;
  @(posedge clk) disable iff (!rst_n) $onehot0(grant);
endproperty
a_one_grant: assert property (p_one_grant);
 
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);
 
property p_pointer_on_transfer_only;
  @(posedge clk) disable iff (!rst_n)
    $changed(last_grant_q) |-> $past(|grant && xfer_fire);
endproperty
a_pointer_on_transfer_only: assert property (p_pointer_on_transfer_only);
 
// LIVENESS, per class, bounded, with assumptions stated (15.2 §36).
//   A1: the downstream eventually accepts
//   A2: a requesting class keeps requesting until served
assume property (@(posedge clk) disable iff (!rst_n)
  (|grant) |-> ##[1:XFER_BOUND] xfer_fire);
assume property (@(posedge clk) disable iff (!rst_n)
  (req[P] && !xfer_fire) |=> req[P]);
 
property p_class_served_within_its_bound(int p);
  @(posedge clk) disable iff (!rst_n)
    req[p] |-> ##[1:CLASS_BOUND(p)] (grant[p] && xfer_fire);
endproperty
a_pcie_served:   assert property (p_class_served_within_its_bound(PROTO_PCIE));
a_cxl_served:    assert property (p_class_served_within_its_bound(PROTO_CXL));
a_stream_served: assert property (p_class_served_within_its_bound(PROTO_STREAM));

// ILLUSTRATIVE. This is PROTOCOL-ENGINE state. It is NOT replay state — that
// belongs to the Adapter (19.3) and has an entirely different lifetime.
typedef enum logic [2:0] {
  SEM_FREE        = 3'd0,
  SEM_ACCEPTED    = 3'd1,   // the client's request is owned; no object formed yet
  SEM_OBJECTS_OUT = 3'd2,   // one or more normalised objects handed to the Adapter
  SEM_AWAIT_RESP  = 3'd3,
  SEM_PARTIAL     = 3'd4,   // some parts resolved, some pending (Section 32)
  SEM_COMPLETE    = 3'd5,
  SEM_FAILED      = 3'd6
} sem_state_e;
 
typedef struct packed {
  logic                    valid;
  sem_state_e              state;
  proto_class_e            proto;
  logic [SEM_ID_W-1:0]     semantic_id;
  logic [GEN_W-1:0]        generation;
  logic [DEST_W-1:0]       destination;     // captured at acceptance
  logic [CFG_EPOCH_W-1:0]  cfg_epoch;
  logic [MAX_PARTS-1:0]    pending_parts;   // Section 32 — a BITMAP
  logic                    response_expected;
  logic [POLICY_W-1:0]     completion_policy;  // per protocol (Section 35)
} semantic_entry_t;
 
semantic_entry_t sem_q [NUM_SEM_ENTRIES];

// WRONG — the semantic entry is created when the Adapter takes the object.
always_ff @(posedge clk)
  if (adapter_accept_fire) begin
    sem_q[alloc_id].valid <= 1'b1;
    sem_q[alloc_id].state <= SEM_OBJECTS_OUT;
  end

1. The client's request is accepted at cycle 10. client_ready was high.
2. The Adapter is backpressured — no credit, staging full, recovery.
3. It does not accept the object until cycle 210.
4. Between cycles 10 and 210 the operation EXISTS and has NO RECORD.

// ILLUSTRATIVE. Allocate on acceptance; the state machine tracks the rest.
always_ff @(posedge clk)
  if (client_accept_fire) begin
    sem_q[alloc_id].valid       <= 1'b1;
    sem_q[alloc_id].state       <= SEM_ACCEPTED;   // <- exists immediately
    sem_q[alloc_id].generation  <= gen_q[alloc_id];
    sem_q[alloc_id].destination <= client_dest;
    sem_q[alloc_id].cfg_epoch   <= active_cfg_epoch_q;
  end

// MANDATORY. An accepted client request has a semantic entry immediately.
property p_acceptance_implies_entry;
  @(posedge clk) disable iff (!rst_n)
    client_accept_fire |=> (sem_q[$past(alloc_id)].valid
                         && (sem_q[$past(alloc_id)].state != SEM_FREE));
endproperty
a_acceptance_implies_entry: assert property (p_acceptance_implies_entry);
 
// No client request is ever accepted without a free entry to hold it.
property p_no_accept_without_slot;
  @(posedge clk) disable iff (!rst_n)
    client_accept_fire |-> sem_slot_available;
endproperty
a_no_accept_without_slot: assert property (p_no_accept_without_slot);
 
// Exactly one allocation per accepted operation.
property p_one_allocation_per_operation(int unsigned rid);
  @(posedge clk) disable iff (!rst_n)
    (tb_allocations_for(rid) <= 1);
endproperty
a_one_allocation_per_operation:
  assert property (p_one_allocation_per_operation(REF_UT));
 
// The captured destination and epoch never change under a live entry.
property p_capture_immutable;
  @(posedge clk) disable iff (!rst_n)
    sem_q[IDX].valid |-> ($stable(sem_q[IDX].destination)
                       && $stable(sem_q[IDX].cfg_epoch)
                       && $stable(sem_q[IDX].proto));
endproperty
a_capture_immutable: assert property (p_capture_immutable);

// ILLUSTRATIVE. Do NOT index the table by the client's own tag unless that tag
// is provably unique across every client sharing this engine.
logic [NUM_SEM_ENTRIES-1:0] free_q;
 
// Lowest free entry — a priority encoder, not a search.
logic [SEM_ID_W-1:0] alloc_id;
logic                sem_slot_available;
 
always_comb begin
  sem_slot_available = (free_q != '0);
  alloc_id           = lowest_set_index(free_q);
end
 
always_ff @(posedge clk or negedge rst_n)
  if (!rst_n) begin
    free_q <= '1;                                   // all entries free
  end else begin
    unique case ({client_accept_fire, sem_retire_fire})
      2'b10: free_q <= free_q & ~(1 << alloc_id);
      2'b01: free_q <= free_q |  (1 << retire_id);
      2'b11: free_q <= (free_q & ~(1 << alloc_id)) | (1 << retire_id);
      default: ;
    endcase
  end

// WRONG — the entry is freed when the Adapter takes the last object.
always_ff @(posedge clk)
  if (adapter_took_last_object[id])
    free_q <= free_q | (1 << id);          // ← the response has not arrived

// ILLUSTRATIVE. Identity plus generation — 12.2 Section 24's quarantine, at the
// protocol engine.
logic [GEN_W-1:0] gen_q [NUM_SEM_ENTRIES];
 
always_ff @(posedge clk or negedge rst_n)
  if (!rst_n)
    for (int i = 0; i < NUM_SEM_ENTRIES; i++) gen_q[i] <= '0;
  else if (client_accept_fire)
    gen_q[alloc_id] <= gen_q[alloc_id] + 1'b1;

// MANDATORY. No identity is live twice, and the free bitmap is consistent.
property p_id_unique_while_live;
  @(posedge clk) disable iff (!rst_n)
    client_accept_fire |-> !sem_q[alloc_id].valid;
endproperty
a_id_unique_while_live: assert property (p_id_unique_while_live);
 
property p_free_bitmap_consistent;
  @(posedge clk) disable iff (!rst_n)
    (free_q[IDX] == !sem_q[IDX].valid);
endproperty
a_free_bitmap_consistent: assert property (p_free_bitmap_consistent);
 
// A response must name a live entry AND its current generation.
property p_response_matches_generation;
  @(posedge clk) disable iff (!rst_n)
    resp_valid |-> (sem_q[resp_id].valid && (sem_q[resp_id].generation == resp_gen));
endproperty
a_response_matches_generation:
  assert property (p_response_matches_generation);
 
// The identity is not returned to the pool before semantic completion.
property p_free_only_at_completion;
  @(posedge clk) disable iff (!rst_n)
    $rose(free_q[IDX]) |-> $past(sem_retire_fire && (retire_id == IDX));
endproperty
a_free_only_at_completion: assert property (p_free_only_at_completion);

// ILLUSTRATIVE. ONE always_comb, ONE always_ff, and every simultaneous event
// resolved by an explicit arm order.
always_comb begin
  nxt = sem_q[i].state;
  unique case (sem_q[i].state)
    SEM_FREE:        if (client_accept_fire && (alloc_id == i[SEM_ID_W-1:0]))
                                                              nxt = SEM_ACCEPTED;
 
    SEM_ACCEPTED:    if (fault[i])                            nxt = SEM_FAILED;
                     else if (cancel[i])                      nxt = SEM_FAILED;
                     else if (objects_handed[i])              nxt = SEM_OBJECTS_OUT;
 
    SEM_OBJECTS_OUT: if (fault[i])                            nxt = SEM_FAILED;
                     else if (all_objects_away[i])            nxt = SEM_AWAIT_RESP;
 
    SEM_AWAIT_RESP:  if (fault[i])                            nxt = SEM_FAILED;
                     else if (policy_satisfied[i])            nxt = SEM_COMPLETE;
                     else if (part_resolved[i])               nxt = SEM_PARTIAL;
 
    SEM_PARTIAL:     if (fault[i])                            nxt = SEM_FAILED;
                     else if (policy_satisfied[i])            nxt = SEM_COMPLETE;
                     else if (part_resolved[i])               nxt = SEM_AWAIT_RESP;
 
    SEM_COMPLETE:    if (client_ack[i])                       nxt = SEM_FREE;
    SEM_FAILED:      if (client_ack[i])                       nxt = SEM_FREE;
    default:                                                  nxt = SEM_FAILED;
  endcase
end
 
always_ff @(posedge clk or negedge rst_n)
  if (!rst_n) sem_q[i].state <= SEM_FREE;
  else        sem_q[i].state <= nxt;

// WRONG — the acceptance path and the response path each write the state.
// In the front end:
always_ff @(posedge clk)
  if (objects_handed[i]) sem_q[i].state <= SEM_OBJECTS_OUT;
 
// In the response path, a different module:
always_ff @(posedge clk)
  if (part_resolved[i])  sem_q[i].state <= SEM_PARTIAL;

// MANDATORY. Only legal transitions, and the state comes only from the
// next-state function.
property p_legal_transitions;
  @(posedge clk) disable iff (!rst_n)
    $changed(sem_q[IDX].state)
      |-> is_legal_sem_transition($past(sem_q[IDX].state), sem_q[IDX].state);
endproperty
a_legal_transitions: assert property (p_legal_transitions);
 
property p_state_from_next_state_fn;
  @(posedge clk) disable iff (!rst_n)
    $changed(sem_q[IDX].state) |-> (sem_q[IDX].state == $past(nxt_for(IDX)));
endproperty
a_state_from_next_state_fn: assert property (p_state_from_next_state_fn);
 
// An entry is never in a working state with no pending work.
property p_await_implies_pending;
  @(posedge clk) disable iff (!rst_n)
    ((sem_q[IDX].state == SEM_AWAIT_RESP) || (sem_q[IDX].state == SEM_PARTIAL))
      |-> (sem_q[IDX].pending_parts != '0);
endproperty
a_await_implies_pending: assert property (p_await_implies_pending);

// ILLUSTRATIVE. Four fields checked, and arrival order is not one of them.
assign resp_ok =
      sem_q[resp_id].valid
   && (sem_q[resp_id].generation == resp_gen)     // Section 22
   && (sem_q[resp_id].proto      == resp_proto)   // the class must match
   && (sem_q[resp_id].cfg_epoch  == resp_cfg_epoch);

// WRONG — responses are matched to requests by position.
always_ff @(posedge clk)
  if (resp_valid) begin
    complete(pending_fifo[deliver_ptr]);        // ← the oldest request gets it
    deliver_ptr <= deliver_ptr + 1'b1;
  end

// MANDATORY. Identity, generation, class and epoch must all agree.
property p_response_belongs_to_live_entry;
  @(posedge clk) disable iff (!rst_n)
    resp_valid |-> (sem_q[resp_id].valid
                 && (sem_q[resp_id].generation == resp_gen)
                 && (sem_q[resp_id].proto      == resp_proto)
                 && (sem_q[resp_id].cfg_epoch  == resp_cfg_epoch));
endproperty
a_response_belongs_to_live_entry:
  assert property (p_response_belongs_to_live_entry);
 
// A response for a retired entry is reported, never silently dropped.
property p_orphan_response_reported;
  @(posedge clk) disable iff (!rst_n)
    (resp_valid && !sem_q[resp_id].valid) |=> orphan_response_flag;
endproperty
a_orphan_response_reported: assert property (p_orphan_response_reported);
 
// The completion delivered to a client names the operation that client issued.
property p_completion_to_correct_client(int unsigned rid);
  @(posedge clk) disable iff (!rst_n)
    (client_complete_fire && (tb_ref_id == rid))
      |-> (complete_client == tb_issuing_client(rid));
endproperty
a_completion_to_correct_client:
  assert property (p_completion_to_correct_client(REF_UT));

// ILLUSTRATIVE. A BITMAP, for the sixth time in this curriculum. The guard is
// what makes a duplicate part idempotent.
logic [MAX_PARTS-1:0] pending_parts_q [NUM_SEM_ENTRIES];
 
always_ff @(posedge clk)
  if (client_accept_fire)
    pending_parts_q[alloc_id] <= part_mask(client_part_count);
  else if (part_resolve_valid
           && sem_q[part_id].valid
           && (sem_q[part_id].generation == part_gen)
           && pending_parts_q[part_id][part_idx])              // GUARDED
    pending_parts_q[part_id][part_idx] <= 1'b0;
 
assign all_parts_resolved[i] = (pending_parts_q[i] == '0);

// WRONG — a counter cannot distinguish a new part from a repeat.
always_ff @(posedge clk)
  if (client_accept_fire)      parts_left_q[alloc_id] <= client_part_count;
  else if (part_resolve_valid) parts_left_q[part_id]  <= parts_left_q[part_id] - 1'b1;

// MANDATORY. A duplicate part changes nothing.
property p_duplicate_part_idempotent;
  @(posedge clk) disable iff (!rst_n)
    (part_resolve_valid && !pending_parts_q[part_id][part_idx])
      |=> $stable(pending_parts_q[part_id]);
endproperty
a_duplicate_part_idempotent: assert property (p_duplicate_part_idempotent);
 
// A part for a stale generation changes nothing.
property p_stale_generation_part_ignored;
  @(posedge clk) disable iff (!rst_n)
    (part_resolve_valid && (sem_q[part_id].generation != part_gen))
      |=> $stable(pending_parts_q[part_id]);
endproperty
a_stale_generation_part_ignored:
  assert property (p_stale_generation_part_ignored);
 
// Completion requires every declared part.
property p_completion_requires_all_parts;
  @(posedge clk) disable iff (!rst_n)
    sem_retire_fire |-> (pending_parts_q[retire_id] == '0);
endproperty
a_completion_requires_all_parts:
  assert property (p_completion_requires_all_parts);
 
// Only a declared part index can clear a bit.
property p_only_declared_part_clears;
  @(posedge clk) disable iff (!rst_n)
    (part_resolve_valid && (part_idx >= sem_part_count[part_id]))
      |=> $stable(pending_parts_q[part_id]);
endproperty
a_only_declared_part_clears: assert property (p_only_declared_part_clears);

// ILLUSTRATIVE. An abstract policy function. The actual condition for each
// protocol class is THAT PROTOCOL'S to define, and this chapter deliberately
// does not define one (Section 3).
typedef enum logic [POLICY_W-1:0] {
  CPL_ALL_PARTS        = 'd0,   // every declared part resolved
  CPL_ALL_PARTS_AND_ACK= 'd1,   // ...and an explicit acknowledgement
  CPL_POSTED           = 'd2    // no response expected at all
} cpl_policy_e;
 
function automatic logic semantic_done(
  input cpl_policy_e         policy,
  input logic                all_parts,
  input logic                ack_seen,
  input logic                response_expected
);
  unique case (policy)
    CPL_ALL_PARTS:         semantic_done = all_parts;
    CPL_ALL_PARTS_AND_ACK: semantic_done = all_parts && ack_seen;
    CPL_POSTED:            semantic_done = !response_expected;
    default:               semantic_done = 1'b0;      // fail closed
  endcase
endfunction

// WRONG — one rule for every protocol.
assign sem_done[i] = response_received[i];

// ILLUSTRATIVE. Every resource the operation will need, checked BEFORE the
// client's request is accepted (Section 17).
assign client_ready =
      sem_slot_available                    // a semantic entry (Section 20)
   && ingress_space_available[client_proto] // its own class's queue (Section 12)
   && route_valid                           // the destination is known
   && protocol_enabled[client_proto]        // Section 42
   && cfg_stable;                           // not mid-commit

// WRONG — readiness propagates combinationally through the whole pipeline.
assign client_ready  = adapter_ready;
assign adapter_ready = credit_available && !staging_full;
assign staging_full  = (staging_occ == DEPTH) && !ingress_pop;
assign ingress_pop   = ingress_valid && adapter_ready;      // ← back to the start

adapter_ready → staging_full → ingress_pop → adapter_ready

// ILLUSTRATIVE one-entry skid buffer. Breaks the combinational ready path
// without losing the item already offered when readiness falls.
typedef struct packed {
  logic                 valid;
  protocol_object_t     obj;
} skid_t;
 
skid_t skid_q;
 
// Upstream sees a REGISTERED ready: we can take an item whenever the skid is
// empty, regardless of what downstream is doing this cycle.
assign up_ready = !skid_q.valid;
 
// Downstream is offered the skid entry if it holds one, else the bypass path.
assign dn_valid   = skid_q.valid || up_valid;
assign dn_obj     = skid_q.valid ? skid_q.obj : up_obj;
 
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})
      // Holding an item and downstream took it: skid empties.
      2'b11: skid_q.valid <= 1'b0;
      // Holding an item and downstream stalled: hold it, unchanged.
      2'b10: ;
      // Empty and downstream stalled: capture the offered item if there is one.
      2'b00: if (up_valid) begin
               skid_q.valid <= 1'b1;
               skid_q.obj   <= up_obj;
             end
      // Empty and downstream ready: the item passes through; nothing stored.
      2'b01: ;
      default: ;
    endcase
  end

// MANDATORY. Payload stable while the downstream stalls.
property p_skid_payload_stable;
  @(posedge clk) disable iff (!rst_n)
    (dn_valid && !dn_ready) |=> (dn_valid && $stable(dn_obj));
endproperty
a_skid_payload_stable: assert property (p_skid_payload_stable);
 
// Nothing accepted upstream is ever lost — conservation across the skid.
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 does not depend on downstream readiness (Section 38).
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 skid never overflows.
property p_skid_no_overflow;
  @(posedge clk) disable iff (!rst_n)
    (up_valid && up_ready) |-> !skid_q.valid || dn_ready;
endproperty
a_skid_no_overflow: assert property (p_skid_no_overflow);

// ILLUSTRATIVE. Requested-versus-active, for the fifth time in this curriculum
// (14.4 lanes, 17.2 memory map, 17.4 channels, 18.4 topology, and here).
logic [NUM_PROTO-1:0]   requested_enable_q;
logic [NUM_PROTO-1:0]   active_enable_q;
logic [CFG_EPOCH_W-1:0] active_cfg_epoch_q;
 
assign cfg_commit_allowed =
      requested_cfg_validated
   && (live_ops_on_disabled_classes == '0);   // nothing outstanding on a class
                                              // this commit would disable
 
always_ff @(posedge clk or negedge rst_n)
  if (!rst_n) begin
    active_cfg_epoch_q <= '0;
  end else if (cfg_commit_fire) begin
    active_enable_q    <= requested_enable_q;   // atomic
    active_cfg_epoch_q <= active_cfg_epoch_q + 1'b1;
  end
 
assign cfg_stable = !cfg_commit_pending;

// MANDATORY. The active configuration changes only at a guarded commit.
property p_cfg_changes_only_at_commit;
  @(posedge clk) disable iff (!rst_n)
    $changed(active_enable_q) |-> $past(cfg_commit_fire);
endproperty
a_cfg_changes_only_at_commit: assert property (p_cfg_changes_only_at_commit);
 
property p_commit_requires_no_live_ops_on_disabled;
  @(posedge clk) disable iff (!rst_n)
    cfg_commit_fire |-> ($past(live_ops_on_disabled_classes) == '0);
endproperty
a_commit_requires_no_live_ops_on_disabled:
  assert property (p_commit_requires_no_live_ops_on_disabled);
 
// A live operation's captured epoch never changes under it.
property p_entry_epoch_stable;
  @(posedge clk) disable iff (!rst_n)
    sem_q[IDX].valid |-> $stable(sem_q[IDX].cfg_epoch);
endproperty
a_entry_epoch_stable: assert property (p_entry_epoch_stable);

// WRONG — the engine treats a transport event as a reason to forget semantics.
always_ff @(posedge clk)
  if (ucie_recovery_entered)
    for (int i = 0; i < NUM_SEM_ENTRIES; i++) sem_q[i].valid <= 1'b0;

1. Twelve operations are live. The link enters recovery.
2. This code clears all twelve entries and frees all twelve identities.
3. The Adapter, correctly, retains and replays its objects (19.3).
4. The link recovers. Responses arrive for all twelve.
5. Every one of them finds no live entry.
6. -> twelve orphan responses; twelve clients waiting forever.
7. Meanwhile the freed identities have been reallocated to new operations,
   so some of those orphans MATCH a live entry of the wrong generation —
   and only the generation check (Section 22) stops them completing it.

// MANDATORY. The property that makes Section 44 impossible.
property p_sem_table_survives_recovery;
  @(posedge clk) disable iff (!rst_n)
    ucie_recovery_entered |=> ($stable(sem_q[IDX].valid)
                            && $stable(sem_q[IDX].generation)
                            && $stable(sem_q[IDX].destination)
                            && $stable(sem_q[IDX].pending_parts));
endproperty
a_sem_table_survives_recovery:
  assert property (p_sem_table_survives_recovery);
 
// The free bitmap is untouched by a transport event.
property p_free_bitmap_survives_recovery;
  @(posedge clk) disable iff (!rst_n)
    ucie_recovery_entered |=> $stable(free_q);
endproperty
a_free_bitmap_survives_recovery:
  assert property (p_free_bitmap_survives_recovery);
 
// A recovery produces no allocation and no completion.
property p_recovery_produces_no_semantic_event;
  @(posedge clk) disable iff (!rst_n)
    ucie_recovery_entered |=> ($stable(sem_alloc_count) && $stable(sem_retire_count));
endproperty
a_recovery_produces_no_semantic_event:
  assert property (p_recovery_produces_no_semantic_event);
 
// Queued and skid-held work survives too.
property p_queued_work_survives_recovery;
  @(posedge clk) disable iff (!rst_n)
    ucie_recovery_entered |=> ($stable(ing_occ_q[P]) && $stable(skid_q.valid));
endproperty
a_queued_work_survives_recovery:
  assert property (p_queued_work_survives_recovery);

// ILLUSTRATIVE. 14.5's first-fault model at the protocol engine. Write-once,
// and cleared only deliberately.
typedef struct packed {
  logic                    valid;
  logic [ERR_W-1:0]        error_kind;      // Section 46's three kinds
  logic [SEM_ID_W-1:0]     semantic_id;
  logic [GEN_W-1:0]        generation;
  proto_class_e            proto;
  sem_state_e              state_at_error;
  logic [DEST_W-1:0]       destination;
  logic [CFG_EPOCH_W-1:0]  cfg_epoch;
} sem_fault_t;
 
sem_fault_t sem_first_fault_q;
 
always_ff @(posedge clk or negedge por_n)                 // <- POR scope only
  if (!por_n)
    sem_first_fault_q <= '0;
  else if (sem_error_detected && !sem_first_fault_q.valid) // <- FIRST, guarded
    sem_first_fault_q <= capture_sem_context();
  else if (sem_fault_clear)
    sem_first_fault_q <= '0;

// Diagnostic only, in the POR reset domain.
logic [63:0] ops_accepted_q   [NUM_PROTO];
logic [63:0] ops_completed_q  [NUM_PROTO];
logic [63:0] ops_failed_q     [NUM_PROTO];
logic [63:0] sem_full_stall_q;                 // no semantic entry available
logic [63:0] ingress_full_stall_q [NUM_PROTO];
logic [63:0] adapter_stall_q;                  // objects waiting for the Adapter
logic [63:0] orphan_resp_q;                    // Section 30
logic [63:0] stale_gen_resp_q;                 // Section 22
logic [63:0] duplicate_part_q;                 // Section 32
logic [63:0] class_wait_max_q  [NUM_PROTO];    // worst arbiter wait

// Verification-only. THREE models. Adapter and replay state belong to 19.3's
// scoreboard and are deliberately NOT modelled here.
class protocol_engine_scoreboard;
 
  // ---- Layer 1: SEMANTIC model — what the client asked for.
  typedef struct {
    int  semantic_id, generation;
    int  proto;
    int  destination;
    int  cfg_epoch;
    int  state;
    int  allocations;          // MUST be 1
    int  completions;          // MUST be <= 1
    int  completion_policy;
    bit  retired;
    bit  crossed_recovery;
  } sem_model_t;
  sem_model_t sem [int];       // keyed by {semantic_id, generation}
 
  // ---- Layer 2: OBJECTISATION model — what the operation SHOULD become.
  typedef struct {
    int        expected_parts;
    bit [63:0] parts_emitted;   // bitmap: which parts were handed over
    bit [63:0] parts_resolved;  // bitmap: which parts came back
    bit [63:0] required_fields; // Section 11 — what reconstruction needs
  } objectise_model_t;
  objectise_model_t obj [int];
 
  // ---- Layer 3: RESPONSE model — where each response should have gone.
  typedef struct {
    int  claimed_id, claimed_gen, claimed_proto;
    int  matched_key;            // what the design matched it to
    int  expected_key;           // what the model says it belongs to
  } resp_model_t;
  resp_model_t resp [int];
 
  // ---- Catches Section 10 — a distinction lost in normalisation.
  function void check_lossless(int key, bit [63:0] emitted_fields);
    if ((emitted_fields & obj[key].required_fields) != obj[key].required_fields)
      $error("NORMALISATION LOSSY key %0d: required %0h, emitted %0h (Section 10)",
             key, obj[key].required_fields, emitted_fields);
  endfunction
 
  // ---- Catches Sections 21 and 29 — a response bound to the wrong operation.
  function void check_response_binding(int r);
    if (resp[r].matched_key != resp[r].expected_key)
      $error("RESPONSE MISBOUND: matched key %0d, belongs to %0d (Sections 21, 29)",
             resp[r].matched_key, resp[r].expected_key);
  endfunction
 
  // ---- Catches Section 33 — retired with a part outstanding.
  function void check_parts(int key);
    if (sem[key].retired && (obj[key].parts_resolved != obj[key].parts_emitted))
      $error("RETIRED WITH PARTS OUTSTANDING key %0d: emitted %0h resolved %0h",
             key, obj[key].parts_emitted, obj[key].parts_resolved);
  endfunction
 
  // ---- Catches Sections 18 and 44 — allocation timing and survival.
  function void check_lifetime(int key);
    if (sem[key].allocations != 1)
      $error("OPERATION %0d allocated %0d times (must be 1)", key, sem[key].allocations);
    if (sem[key].crossed_recovery && sem[key].retired && (sem[key].completions == 0))
      $error("OPERATION %0d lost across a recovery (Section 44)", key);
  endfunction
 
endclass

covergroup cg_protocol_engine @(posedge clk);
  option.per_instance = 1;
 
  // --- Protocol mix (Sections 12-15).
  cp_proto : coverpoint accepted_proto { bins each[] = {[0:NUM_PROTO-1]}; }
  cp_simultaneous : coverpoint num_protos_requesting {
    bins one = {1}; bins two = {2}; bins all = {[3:$]};    // Section 13
  }
  cp_class_wait : coverpoint class_wait_ut {
    bins none = {0}; bins some = {[1:CLASS_BOUND_UT-1]}; bins at_bound = {CLASS_BOUND_UT};
  }
  cp_ingress_occ : coverpoint ing_occ_q_ut {
    bins empty = {0}; bins mid = {[1:ING_DEPTH-1]}; bins full = {ING_DEPTH};
  }
 
  // --- Semantic lifetime (Sections 16-23).
  cp_sem_state : coverpoint sem_state_q_ut { bins each[] = {[0:6]}; }
  cp_sem_occ : coverpoint sem_occupancy {
    bins empty = {0}; bins mid = {[1:NUM_SEM_ENTRIES-1]}; bins full = {NUM_SEM_ENTRIES};
  }
  cp_alloc_retire_simul : coverpoint alloc_and_retire_same_cycle;
  cp_id_wrap : coverpoint generation_wrapped;
  cp_event_in_stall_window : coverpoint semantic_event_while_adapter_stalled;  // Section 18
 
  // --- Responses (Sections 28-30).
  cp_resp_order : coverpoint response_reorder_distance {
    bins in_order = {0}; bins near = {[1:3]}; bins far = {[4:$]};   // Section 29
  }
  cp_resp_outcome : coverpoint response_outcome {
    bins matched = {0};
    bins orphan  = {1};
    bins stale_gen = {2};
    bins wrong_class = {3};
    bins wrong_epoch = {4};                 // all four rejection reasons
  }
 
  // --- Multi-part (Sections 31-34).
  cp_parts : coverpoint part_count {
    bins one = {1}; bins few = {[2:3]}; bins many = {[4:$]};
  }
  cp_part_event : coverpoint part_event {
    bins normal = {0}; bins duplicate = {1}; bins missing = {2}; bins stale_gen = {3};
  }
 
  // --- Completion policy (Sections 35-36).
  cp_policy : coverpoint active_policy {
    bins all_parts = {0}; bins all_parts_and_ack = {1}; bins posted = {2};
  }
  cp_policy_mix : coverpoint distinct_policies_active {
    bins one = {1}; bins several = {[2:$]};   // Section 36 needs >1
  }
 
  // --- Backpressure and configuration (Sections 37-42).
  cp_ready_refusal : coverpoint client_ready_false_reason {
    bins sem_full = {0}; bins ingress_full = {1}; bins route = {2};
    bins disabled = {3}; bins cfg_commit = {4};   // each term alone
  }
  cp_skid : coverpoint skid_case {
    bins pass_through = {0}; bins captured = {1}; bins held = {2}; bins drained = {3};
  }
  cp_cfg_context : coverpoint cfg_commit_context {
    bins idle = {0}; bins blocked_by_live_ops = {1}; bins forced = {2};
  }
 
  // --- Recovery (Sections 43-45).
  cp_recovery : coverpoint recovery_context {
    bins none = {0};
    bins table_nonempty = {1};
    bins parts_outstanding = {2};
    bins queues_nonempty = {3};
    bins all = {4};                          // THE case — Section 53
  }
 
  // --- Crosses that carry the information.
  x_simul_wait   : cross cp_simultaneous, cp_class_wait;     // Section 13
  x_parts_event  : cross cp_parts, cp_part_event;            // Section 33
  x_policy_mix   : cross cp_policy, cp_policy_mix;           // Section 36
  x_recovery_sem : cross cp_recovery, cp_sem_occ;            // Section 53
endcovergroup