Completion Credits — The Return Path Has Its Own Budget

FORWARD                                        Requester → Completer
  Requester spends  NPH   advertised by the Completer
  Memory Read Request lands in the Completer's NP receive buffer
 
RETURN                                         Completer → Requester
  Completer spends  CPLH + CPLD   advertised by the REQUESTER
  CplD lands in the Requester's Completion receive buffer

one 256-byte Memory Read Request
   costs 1 NPH going out
 
answered by four 64-byte CplD packets
   costs 4 × (1 CPLH + 4 CPLD)  =  4 CPLH + 16 CPLD coming back

step             1     2     3     4     5     6     7
cpl_valid        1     1     1     1     1     1     0
cpl_kind      CplD  CplD  CplD   Cpl  CplD     -     -
cpl_bytes       64    64    64     0    64     -     -
cplh_cost        1     1     1     1     1     -     -
cpld_cost        4     4     4     0     4     -     -
 
cplh_avail       2     1     0     0     1     1     1
cpld_avail       8     4     0     0     4     0     0
 
eligible         1     1     0     1     1     0     -
send_fire        1     1     0     1     1     0     -
 
cplh_return      0     0     0     0     1     0     0
cpld_return      0     0     0     0     4     0     0

// SYNTHESIZABLE. Derive Completion flow-control cost from normalized
// Completion metadata.
// 1 CPLH per Completion, and n CPLD where n = Roundup(Length / FC unit
// size) with the data unit 4 DW: NORMATIVE (section 1). The descriptor
// shape and the error reports: ILLUSTRATIVE.
package cpl_fc_pkg;
 
  // VERIFIED (section 1): the data credit unit is 4 DW = 16 bytes, the same
  // unit as every other pool in Module 16.
  localparam int FC_DATA_UNIT_BYTES = 16;
 
  // Normalized Completion class, from Chapter 13.1's decode. NOT
  // re-derived from Fmt/Type here.
  typedef enum logic [2:0] {
    CPL_MEM_READ    = 3'd0,  // CplD : 1 CPLH + n CPLD
    CPL_IO_CFG_READ = 3'd1,  // CplD : 1 CPLH + 1 CPLD   (bounded payload)
    CPL_IO_CFG_WRITE= 3'd2,  // Cpl  : 1 CPLH            -- NO data credit
    CPL_ATOMIC      = 3'd3,  // CplD : 1 CPLH + 1 CPLD   (<= 4 aligned DW)
    CPL_NOT_A_CPL   = 3'd4   // not Completion traffic
  } cpl_kind_e;
 
  function automatic bit cpl_has_data(input cpl_kind_e k);
    return (k == CPL_MEM_READ) || (k == CPL_IO_CFG_READ)
        || (k == CPL_ATOMIC);
  endfunction
 
  // CEILING DIVISION, in the only correct form, with the same widening
  // discipline as Chapters 16.2 and 16.3. The addition is performed one bit
  // wider than the input so it cannot wrap before the division shrinks it.
  function automatic logic [11:0]
      cpld_credit_cost(input logic [13:0] payload_bytes);
    logic [14:0] widened;
    widened = {1'b0, payload_bytes} + 15'(FC_DATA_UNIT_BYTES - 1);
    return 12'(widened / 15'(FC_DATA_UNIT_BYTES));
  endfunction
 
endpackage

import cpl_fc_pkg::*;
 
module completion_credit_cost #(
  parameter int LEN_W  = 14,       // payload bytes; 14 bits covers 4096
  parameter int COST_W = 12
) (
  input  cpl_kind_e           cpl_kind,
  input  logic [LEN_W-1:0]    payload_bytes,
 
  output logic                needs_cplh,
  output logic [COST_W-1:0]   cplh_cost,
  output logic                needs_cpld,
  output logic [COST_W-1:0]   cpld_cost,
  output logic                cost_valid,
  output logic                cost_error
);
 
  wire is_cpl   = (cpl_kind != CPL_NOT_A_CPL);
  wire has_data = cpl_has_data(cpl_kind);
 
  // THE HEADER COST IS A CONSTANT -- one per Completion, whatever the
  // header size (Chapter 16.1 section 5). Every Completion pays it,
  // including a Cpl that carries nothing.
  assign needs_cplh = is_cpl;
  assign cplh_cost  = is_cpl ? COST_W'(1) : '0;
 
  // KEYED TO THE COMPLETION FORM, NOT TO THE LENGTH FIELD (section 5).
  // A Cpl has no payload and must be charged NO data credit; deriving this
  // from `payload_bytes != 0` would work by accident and break the moment
  // a malformed descriptor arrived with a stale length.
  assign needs_cpld = has_data;
 
  always_comb begin
    cpld_cost = '0;
    if (has_data) begin
      unique case (cpl_kind)
        // Scales with the data actually returned.
        CPL_MEM_READ : cpld_cost = COST_W'(cpld_credit_cost(14'(payload_bytes)));
        // Bounded by the source: an AtomicOp Completion returns at most
        // four aligned DW, and an I/O or Configuration Read Completion at
        // most one -- both inside a single 16-byte credit.
        CPL_IO_CFG_READ, CPL_ATOMIC : cpld_cost = COST_W'(1);
        default : cpld_cost = '0;
      endcase
    end
  end
 
  // A CplD claiming zero payload, or a Cpl claiming payload, is a
  // descriptor fault. Reported, and cost_valid withheld, rather than
  // silently costed as zero.
  wire zero_len_cpld = has_data && (cpl_kind == CPL_MEM_READ)
                                && (payload_bytes == '0);
  wire len_on_a_cpl  = !has_data && is_cpl && (payload_bytes != '0);
 
  assign cost_error = !is_cpl || zero_len_cpld || len_on_a_cpl;
  assign cost_valid = is_cpl && !zero_len_cpld && !len_on_a_cpl;
 
endmodule

import cpl_fc_pkg::*;
 
// SYNTHESIZABLE. Gate a Completion on every resource it needs.
// The CPLH/CPLD costs are NORMATIVE (section 1), and the atomic
// multi-pool rule is stated by a vendor source (section 1: "A transaction
// cannot be transmitted unless there is at least 1 header credit and
// enough data credits for the packet payload"). The composition and the
// per-pool reason flags are ILLUSTRATIVE.
module completion_eligibility #(
  parameter int CRED_W = 12,
  parameter int COST_W = 12,
  parameter int LEN_W  = 14
) (
  input  logic clk,
  input  logic rst_n,
 
  // ---- Head of the Completion transmit queue ----------------------------
  input  logic                cpl_valid,
  input  cpl_kind_e           cpl_kind,
  input  logic [LEN_W-1:0]    payload_bytes,
 
  // ---- Other launch resources (Chapter 16.1 section 10) -----------------
  input  logic                replay_space,
  input  logic                tx_path_ready,
 
  // ---- Credit plumbing for the COMPLETION pools -------------------------
  // Advertised by the REQUESTER, spent by this Completer (section 2).
  input  logic                init_valid,
  input  logic [CRED_W-1:0]   init_cplh_capacity,
  input  logic                init_cplh_infinite,   // Endpoint: TRUE (s7)
  input  logic [CRED_W-1:0]   init_cpld_capacity,
  input  logic                init_cpld_infinite,
  input  logic                cplh_return_valid,
  input  logic [CRED_W-1:0]   cplh_return_count,
  input  logic                cpld_return_valid,
  input  logic [CRED_W-1:0]   cpld_return_count,
 
  // ---- Outputs ------------------------------------------------------------
  output logic                cpl_ready,
  output logic                send_fire,
  output logic [CRED_W-1:0]   cplh_available,
  output logic [CRED_W-1:0]   cpld_available,
  output logic                blocked_on_cplh,
  output logic                blocked_on_cpld,
  output logic                blocked_on_replay,
  output logic                blocked_on_path,
  output logic                cpl_error
);
 
  logic needs_cplh, needs_cpld, cost_valid, cost_err, credit_eligible, pair_err;
  logic [COST_W-1:0] cplh_cost, cpld_cost;
 
  completion_credit_cost #(.LEN_W(LEN_W), .COST_W(COST_W)) u_cost (
    .cpl_kind, .payload_bytes,
    .needs_cplh, .cplh_cost, .needs_cpld, .cpld_cost,
    .cost_valid, .cost_error(cost_err)
  );
 
  // ATOMIC ACROSS THE COMPLETION POOLS (Chapter 16.1 section 9). A Cpl
  // engages only the header pool: it must be neither charged to nor
  // blocked by CPLD (section 5).
  credit_pair_gate #(.CRED_W(CRED_W), .COST_W(COST_W)) u_pair (
    .clk, .rst_n,
    .pkt_valid(cpl_valid && cost_valid),
    .needs_header(needs_cplh), .header_cost(cplh_cost),
    .needs_data(needs_cpld),   .data_cost(cpld_cost),
    .send_fire,
    .hdr_return_valid(cplh_return_valid), .hdr_return_count(cplh_return_count),
    .dat_return_valid(cpld_return_valid), .dat_return_count(cpld_return_count),
    .init_valid,
    .init_hdr_capacity(init_cplh_capacity),
    .init_hdr_infinite(init_cplh_infinite),
    .init_dat_capacity(init_cpld_capacity),
    .init_dat_infinite(init_cpld_infinite),
    .eligible(credit_eligible),
    .hdr_available(cplh_available), .dat_available(cpld_available),
    .pool_error(pair_err)
  );
 
  // A descriptor whose cost could not be computed NEVER launches. Sending a
  // Completion with an unknown cost is how a pool goes wrong silently.
  wire all_ready = cost_valid && credit_eligible && replay_space && tx_path_ready;
 
  assign cpl_ready = all_ready;
  assign send_fire = cpl_valid && all_ready;
 
  assign blocked_on_cplh   = cpl_valid && needs_cplh
                                       && (cplh_available < CRED_W'(cplh_cost));
  assign blocked_on_cpld   = cpl_valid && needs_cpld
                                       && (cpld_available < CRED_W'(cpld_cost));
  assign blocked_on_replay = cpl_valid && !replay_space;
  assign blocked_on_path   = cpl_valid && !tx_path_ready;
  assign cpl_error         = cost_err | pair_err;
 
endmodule

import cpl_fc_pkg::*;
 
// SYNTHESIZABLE. A small Completion transmit queue whose head is gated on
// Completion credit.
// The decoupling of "Completion produced" from "Completion transmitted" is
// ILLUSTRATIVE ARCHITECTURE; the credit gating it feeds is normative
// (section 1). DEPTH is a teaching choice, not a protocol requirement.
module completion_tx_queue #(
  parameter int DEPTH  = 4,
  parameter int LEN_W  = 14,
  // Opaque context carried with the descriptor -- Tag, Requester ID and
  // whatever else Chapter 12.3 needs. NOT interpreted here.
  parameter int CTX_W  = 32,
  // GUARDED INDEX WIDTH. $clog2(1) is zero, and a zero-width pointer
  // cannot index anything (Chapter 15.2's parameter corner).
  parameter int PTR_W  = (DEPTH <= 1) ? 1 : $clog2(DEPTH)
) (
  input  logic clk,
  input  logic rst_n,
 
  // ---- From the target / completion builder (Chapter 12.3) --------------
  input  logic                enq_valid,
  output logic                enq_ready,
  input  cpl_kind_e           enq_kind,
  input  logic [LEN_W-1:0]    enq_bytes,
  input  logic [CTX_W-1:0]    enq_ctx,
 
  // ---- Head, to the credit gate ------------------------------------------
  output logic                head_valid,
  input  logic                head_ready,          // = send_fire (section 10)
  output cpl_kind_e           head_kind,
  output logic [LEN_W-1:0]    head_bytes,
  output logic [CTX_W-1:0]    head_ctx,
 
  output logic [PTR_W:0]      occupancy,           // one bit wider than PTR_W
  output logic                queue_full
);
 
  generate
    if (DEPTH < 1) $error("DEPTH must be at least 1");
    if ((DEPTH > 1) && ((1 << PTR_W) < DEPTH))
      $error("PTR_W too narrow to index DEPTH");
  endgenerate
 
  cpl_kind_e        kind_q  [DEPTH];
  logic [LEN_W-1:0] bytes_q [DEPTH];
  logic [CTX_W-1:0] ctx_q   [DEPTH];
 
  logic [PTR_W-1:0] rd_q, wr_q;
  // OCCUPANCY IS A COUNTER, ONE BIT WIDER THAN THE POINTERS. Full and empty
  // are never inferred from pointer equality (Chapter 14.4 section 10).
  logic [PTR_W:0]   cnt_q;
 
  assign occupancy  = cnt_q;
  assign queue_full = (cnt_q == (PTR_W+1)'(DEPTH));
  assign enq_ready  = !queue_full;
 
  assign head_valid = (cnt_q != '0);
  assign head_kind  = kind_q[rd_q];
  assign head_bytes = bytes_q[rd_q];
  assign head_ctx   = ctx_q[rd_q];
 
  wire push = enq_valid  && enq_ready;
  wire pop  = head_valid && head_ready;
 
  // EXPLICIT WRAP at DEPTH-1. Never rely on a pointer wrapping naturally --
  // it only does at a power-of-two DEPTH, and DEPTH is a free parameter.
  function automatic logic [PTR_W-1:0] next_idx(input logic [PTR_W-1:0] i);
    return (i == PTR_W'(DEPTH-1)) ? '0 : (i + PTR_W'(1));
  endfunction
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      rd_q <= '0; wr_q <= '0; cnt_q <= '0;
    end else begin
      if (push) begin
        kind_q[wr_q]  <= enq_kind;
        bytes_q[wr_q] <= enq_bytes;
        ctx_q[wr_q]   <= enq_ctx;
        wr_q          <= next_idx(wr_q);
      end
      if (pop) rd_q <= next_idx(rd_q);
 
      // Push and pop in the same cycle leave occupancy unchanged. Written
      // as one expression so the two cannot disagree.
      unique case ({push, pop})
        2'b10   : cnt_q <= cnt_q + (PTR_W+1)'(1);
        2'b01   : cnt_q <= cnt_q - (PTR_W+1)'(1);
        default : ;
      endcase
    end
  end
 
endmodule

// VERIFICATION-ONLY. Independent reference for Completion credit cost,
// written from section 1's Table 5 rather than from section 9's structure.
typedef struct { int cplh; int cpld; } cpl_cost_t;
 
function automatic cpl_cost_t ref_cpl_cost(string kind, int payload_bytes);
  cpl_cost_t c;
  c.cplh = 1;                                   // every Completion, always
  case (kind)
    // Scales with the returned payload. COUNTED, not divided -- a rounding
    // bug cannot be present in both this and section 9.
    "MEM_READ_CPL" : begin
      c.cpld = 0;
      while (payload_bytes > 0) begin
        c.cpld = c.cpld + 1;
        payload_bytes = payload_bytes - 16;     // 4 DW, verified
      end
    end
    "IO_CFG_READ_CPL" : c.cpld = 1;             // bounded payload
    "ATOMIC_CPL"      : c.cpld = 1;             // <= 4 aligned DW
    "IO_CFG_WRITE_CPL": c.cpld = 0;             // Cpl -- NO data credit
    default           : begin c.cplh = 0; c.cpld = 0; end
  endcase
  return c;
endfunction
 
// Independent Completion-pool model. Driven from OBSERVED sends and
// OBSERVED updates -- never from the DUT's available counters.
class cpl_pool_model;
  int cplh, cpld;
  bit cplh_infinite, cpld_infinite;
  function void on_send(cpl_cost_t c);
    if (!cplh_infinite) cplh -= c.cplh;
    if (!cpld_infinite) cpld -= c.cpld;
  endfunction
  function void on_return(int h, int d);
    if (!cplh_infinite) cplh += h;
    if (!cpld_infinite) cpld += d;
  endfunction
  // An infinite pool is never decremented and never blocks (section 7).
  function bit eligible(cpl_cost_t c);
    return (cplh_infinite || cplh >= c.cplh)
        && (cpld_infinite || cpld >= c.cpld);
  endfunction
endclass

// SVA over completion_credit_cost, completion_eligibility and
// completion_tx_queue. These assert the VERIFIED Completion costs and the
// local issue contract. Nothing here asserts credit-return timing (an
// environment property -- Chapter 16.1 section 15), Completion Status
// (13.2), split boundaries (13.3), spend policy (16.5), or the update
// protocol (16.6).
 
// ---- ENVIRONMENT ------------------------------------------------------
// A1: cpl_kind is Chapter 13.1's normalized class, not re-decoded here.
assume property (@(posedge clk) disable iff (!rst_n)
  cpl_valid |-> (cpl_kind != CPL_NOT_A_CPL));
// A2: the descriptor is stable while offered and not taken.
assume property (@(posedge clk) disable iff (!rst_n)
  (cpl_valid && !cpl_ready) |=> ($stable(cpl_kind) && $stable(payload_bytes)));
 
// ---- COST -------------------------------------------------------------
 
// P1: EVERY Completion costs exactly one header credit -- including a Cpl.
property p_cplh_is_one;
  @(posedge clk) disable iff (!rst_n)
  needs_cplh |-> (cplh_cost == COST_W'(1));
endproperty
a_cplh_one : assert property (p_cplh_is_one);
 
// P2: A Cpl CONSUMES NO DATA CREDIT. The chapter's sharpest cost property,
// and the one whose violation surfaces as a read-bandwidth collapse.
property p_cpl_costs_no_cpld;
  @(posedge clk) disable iff (!rst_n)
  (cpl_kind == CPL_IO_CFG_WRITE) |-> (!needs_cpld && (cpld_cost == '0));
endproperty
a_cpl_no_cpld : assert property (p_cpl_costs_no_cpld);
 
// P3: and it is never CHARGED one either -- asserted at the pool, not just
// at the cost, because a design could compute zero and decrement anyway.
property p_cpl_send_leaves_cpld;
  @(posedge clk) disable iff (!rst_n)
  (send_fire && (cpl_kind == CPL_IO_CFG_WRITE)) |=> $stable(cpld_available);
endproperty
a_cpl_pool : assert property (p_cpl_send_leaves_cpld);
 
// P4: the Memory Read Completion data cost matches an INDEPENDENT model
// (section 12's counting loop, not section 9's division).
property p_cpld_matches_reference;
  @(posedge clk) disable iff (!rst_n)
  (cpl_kind == CPL_MEM_READ)
    |-> (cpld_cost == COST_W'(ref_cpl_cost("MEM_READ_CPL",
                                           int'(payload_bytes)).cpld));
endproperty
a_cpld_ref : assert property (p_cpld_matches_reference);
 
// P4b: CEILING, NOT FLOOR -- stated directly so a failure names itself.
property p_cpld_is_ceiling;
  @(posedge clk) disable iff (!rst_n)
  ((cpl_kind == CPL_MEM_READ) && (payload_bytes != '0))
    |-> ((COST_W'(cpld_cost) * 16 >= payload_bytes)
      && ((COST_W'(cpld_cost) - 1) * 16 < payload_bytes));
endproperty
a_ceiling : assert property (p_cpld_is_ceiling);
 
// P5: the bounded-payload Completions cost exactly one CPLD -- never n.
property p_bounded_cpl_one_cpld;
  @(posedge clk) disable iff (!rst_n)
  (cpl_kind inside {CPL_IO_CFG_READ, CPL_ATOMIC})
    |-> (needs_cpld && (cpld_cost == COST_W'(1)));
endproperty
a_bounded : assert property (p_bounded_cpl_one_cpld);
 
// P6: a descriptor whose cost could not be computed NEVER launches.
property p_no_send_without_cost;
  @(posedge clk) disable iff (!rst_n)
  send_fire |-> cost_valid;
endproperty
a_cost_gate : assert property (p_no_send_without_cost);
 
// ---- ISSUE ------------------------------------------------------------
 
// P7: no Completion issues without sufficient CPLH.
property p_no_issue_without_cplh;
  @(posedge clk) disable iff (!rst_n)
  (send_fire && needs_cplh) |-> (cplh_available >= CRED_W'(cplh_cost));
endproperty
a_cplh_gate : assert property (p_no_issue_without_cplh);
 
// P8: no CplD issues without sufficient CPLD.
property p_no_issue_without_cpld;
  @(posedge clk) disable iff (!rst_n)
  (send_fire && needs_cpld) |-> (cpld_available >= CRED_W'(cpld_cost));
endproperty
a_cpld_gate : assert property (p_no_issue_without_cpld);
 
// P9: ATOMICITY. A failed CPLD eligibility consumes NO CPLH.
property p_failed_cpld_leaves_cplh;
  @(posedge clk) disable iff (!rst_n)
  (cpl_valid && needs_cpld && (cpld_available < CRED_W'(cpld_cost)))
    |=> $stable(cplh_available);
endproperty
a_atomic : assert property (p_failed_cpld_leaves_cplh);
 
// P10: and the mirror.
property p_failed_cplh_leaves_cpld;
  @(posedge clk) disable iff (!rst_n)
  (cpl_valid && needs_cplh && (cplh_available < CRED_W'(cplh_cost)))
    |=> $stable(cpld_available);
endproperty
a_atomic_mirror : assert property (p_failed_cplh_leaves_cpld);
 
// P11: a credit-starved Completion is STABLE -- descriptor unchanged.
property p_starved_stable;
  @(posedge clk) disable iff (!rst_n)
  (cpl_valid && !cpl_ready)
    |=> (cpl_valid && $stable(cpl_kind) && $stable(payload_bytes));
endproperty
a_stable : assert property (p_starved_stable);
 
// P12: SPLIT COMPLETIONS PAY INDEPENDENTLY. Each packet of a split costs
// its own CPLH -- the second must not reuse the first's accounting.
// (g_cplh_spent and g_cpl_sent are testbench ghost counters.)
property p_split_pays_per_packet;
  @(posedge clk) disable iff (!rst_n)
  send_fire |=> (g_cplh_spent == $past(g_cplh_spent) + 1);
endproperty
a_split : assert property (p_split_pays_per_packet);
 
// P13: AN INFINITE POOL NEVER BLOCKS AND NEVER MOVES (section 7). On an
// Endpoint path this is the whole behaviour, and a design storing the
// zero advertisement as capacity fails here immediately.
property p_infinite_never_blocks;
  @(posedge clk) disable iff (!rst_n)
  (init_cplh_infinite && cpl_valid) |-> !blocked_on_cplh;
endproperty
a_infinite : assert property (p_infinite_never_blocks);
 
// ---- CROSS-CLASS NON-INTERFERENCE -------------------------------------
 
// P14: THE DIRECTIONAL PROPERTY. A Completion NEVER consumes NP credit --
// the NPH that carried the Request out is a different pool on a different
// direction (section 2).
property p_completion_spends_no_np;
  @(posedge clk) disable iff (!rst_n)
  send_fire |=> ($stable(dut_np_engine.nph_available)
              && $stable(dut_np_engine.npd_available));
endproperty
a_not_np : assert property (p_completion_spends_no_np);
 
// P15: nor Posted credit.
property p_completion_spends_no_posted;
  @(posedge clk) disable iff (!rst_n)
  send_fire |=> ($stable(dut_posted_engine.ph_available)
              && $stable(dut_posted_engine.pd_available));
endproperty
a_not_posted : assert property (p_completion_spends_no_posted);
 
// P16: and the reverse -- consuming NPH for a Request does not reduce the
// Completion pools. Credits are not transferred through a transaction.
property p_np_send_leaves_completion_pools;
  @(posedge clk) disable iff (!rst_n)
  (dut_np_engine.launch && !send_fire)
    |=> ($stable(cplh_available) && $stable(cpld_available));
endproperty
a_no_transfer : assert property (p_np_send_leaves_completion_pools);
 
// P17: a full replay buffer blocks the launch and touches no credit.
property p_replay_is_not_credit;
  @(posedge clk) disable iff (!rst_n)
  !replay_space |=> ($stable(cplh_available) && $stable(cpld_available));
endproperty
a_not_replay : assert property (p_replay_is_not_credit);
 
// ---- QUEUE ------------------------------------------------------------
 
// P18: the queue entry is freed only on an actual send.
property p_pop_only_on_send;
  @(posedge clk) disable iff (!rst_n)
  (head_valid && !head_ready) |=> ($stable(occupancy) || push);
endproperty
a_pop : assert property (p_pop_only_on_send);
 
// P19: occupancy is bounded and never underflows.
property p_occupancy_sane;
  @(posedge clk) disable iff (!rst_n)
  (occupancy <= (PTR_W+1)'(DEPTH)) && !(pop && (occupancy == '0));
endproperty
a_occ : assert property (p_occupancy_sane);