Non-Posted Credits — Free Tags Are Not Permission

NP Request arrives
  → occupies the receiver's NP receive buffer      ← NPH accounts for THIS
  → moves into internal servicing machinery        ← implementation-defined
  → receive buffer is free
  → credit can be returned
  → ... later ... the Completion is produced       ← CPLH/CPLD, other direction

step             1     2     3     4     5     6     7     8
read_valid       1     1     1     1     1     1     0     0
 
ctx_free         4     3     2     1     1     1     1     2
nph_available    3     2     1     0     0     1     1     1
 
eligible         1     1     1     0     0     1     -     -
launch           1     1     1     0     0     1     -     -
 
nph_return       0     0     0     0     1     0     0     0
cpl_arrives      0     0     0     0     0     0     0     1

// SYNTHESIZABLE. Derive Non-Posted flow-control cost from a normalized
// packet descriptor.
// The per-class costs are NORMATIVE (section 1). The descriptor shape and
// the error report are ILLUSTRATIVE.
package np_fc_pkg;
 
  // VERIFIED (section 1), identical to the Posted data unit.
  localparam int FC_DATA_UNIT_BYTES = 16;
 
  typedef enum logic [2:0] {
    NP_MEM_READ    = 3'd0,   // 1 NPH            -- NO data credit
    NP_IO_READ     = 3'd1,   // 1 NPH
    NP_CFG_READ    = 3'd2,   // 1 NPH
    NP_IO_WRITE    = 3'd3,   // 1 NPH + 1 NPD    -- at most one aligned DW
    NP_CFG_WRITE   = 3'd4,   // 1 NPH + 1 NPD
    NP_ATOMIC      = 3'd5,   // 1 NPH + n NPD
    NP_NOT_NP      = 3'd6    // Posted -- Chapter 16.2
  } np_kind_e;
 
  // Only AtomicOp needs this. Same ceiling form and same widening
  // discipline as Chapter 16.2 section 6.
  function automatic logic [11:0]
      npd_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 np_fc_pkg::*;
 
module np_credit_cost #(
  parameter int LEN_W  = 14,
  parameter int COST_W = 12
) (
  input  np_kind_e            pkt_kind,
  // Meaningful ONLY for the payload-carrying kinds. For a read this field
  // describes how much data is REQUESTED, and charging NPD for it would
  // charge the request for the Completion's payload -- on the wrong pool,
  // in the wrong direction (section 3).
  input  logic [LEN_W-1:0]    payload_bytes,
 
  output logic                uses_nph,
  output logic [COST_W-1:0]   nph_cost,
  output logic                uses_npd,
  output logic [COST_W-1:0]   npd_cost,
 
  output logic                cost_error
);
 
  wire is_np = (pkt_kind != NP_NOT_NP);
 
  // A CONSTANT, exactly as in Chapter 16.2: every NP request costs one
  // header credit, whatever its header size (Chapter 16.1 section 5).
  assign uses_nph = is_np;
  assign nph_cost = is_np ? COST_W'(1) : '0;
 
  // NOT A MIRROR OF THE POSTED DERIVER (section 3). A lookup, because the
  // protocol is lopsided here and the code should say so.
  always_comb begin
    uses_npd = 1'b0;
    npd_cost = '0;
    unique case (pkt_kind)
      NP_MEM_READ, NP_IO_READ, NP_CFG_READ : begin
        // NO DATA CREDIT. The request carries nothing.
        uses_npd = 1'b0;
        npd_cost = '0;
      end
      NP_IO_WRITE, NP_CFG_WRITE : begin
        // Exactly one, always. The source states the data written is never
        // more than one aligned DW, so no division is possible or needed.
        uses_npd = 1'b1;
        npd_cost = COST_W'(1);
      end
      NP_ATOMIC : begin
        uses_npd = (payload_bytes != '0);
        npd_cost = (payload_bytes != '0)
                     ? COST_W'(npd_credit_cost(14'(payload_bytes))) : '0;
      end
      default : ;                       // NP_NOT_NP: nothing, reported below
    endcase
  end
 
  // A Posted kind reaching this deriver, or a read claiming a payload it
  // cannot carry. Reported rather than silently costed.
  assign cost_error = (!is_np)
                   || ((pkt_kind inside {NP_MEM_READ, NP_IO_READ, NP_CFG_READ})
                       && (payload_bytes != '0) && uses_npd);
 
endmodule

import np_fc_pkg::*;
 
// SYNTHESIZABLE. Multi-resource admission for a Non-Posted Request.
// The NPH/NPD costs are NORMATIVE (section 1). That a read ALSO needs a
// requester context, replay-buffer space and a transmit opportunity comes
// from Chapters 12.1, 14.4 and 16.1 -- this module composes them and owns
// none of them.
// The single-cycle commit model is ILLUSTRATIVE (section 8's callout).
module np_read_admission #(
  parameter int CRED_W = 12,
  parameter int COST_W = 12,
  parameter int LEN_W  = 14
) (
  input  logic clk,
  input  logic rst_n,
 
  // ---- Local read request ------------------------------------------------
  input  logic                local_read_valid,
  output logic                local_read_ready,
  input  np_kind_e            pkt_kind,
  input  logic [LEN_W-1:0]    payload_bytes,
 
  // ---- The four resources, each owned elsewhere -------------------------
  // Chapter 12.1: a free requester context / Tag. NOT allocated here.
  input  logic                ctx_available,
  // Chapter 14.4: local replay storage for the transmitted packet.
  input  logic                replay_space,
  // The transmit path, this cycle.
  input  logic                tx_ready,
  // Credit plumbing for the NP pools.
  input  logic                init_valid,
  input  logic [CRED_W-1:0]   init_nph_capacity,
  input  logic                init_nph_infinite,
  input  logic [CRED_W-1:0]   init_npd_capacity,
  input  logic                init_npd_infinite,
  input  logic                nph_return_valid,
  input  logic [CRED_W-1:0]   nph_return_count,
  input  logic                npd_return_valid,
  input  logic [CRED_W-1:0]   npd_return_count,
 
  // ---- Outputs ------------------------------------------------------------
  output logic                launch,          // ctx alloc + credit consume
  output logic [CRED_W-1:0]   nph_available,
  output logic [CRED_W-1:0]   npd_available,
 
  // WHICH resource is missing. Section 11's first debugging question, and
  // without these the answer costs a simulation run.
  output logic                blocked_on_ctx,
  output logic                blocked_on_nph,
  output logic                blocked_on_npd,
  output logic                blocked_on_replay,
  output logic                blocked_on_tx,
  output logic                np_error
);
 
  logic uses_nph, uses_npd, cost_err, credit_eligible, pair_err;
  logic [COST_W-1:0] nph_cost, npd_cost;
 
  np_credit_cost #(.LEN_W(LEN_W), .COST_W(COST_W)) u_cost (
    .pkt_kind, .payload_bytes,
    .uses_nph, .nph_cost, .uses_npd, .npd_cost, .cost_error(cost_err)
  );
 
  // ATOMIC ACROSS THE NP POOLS (Chapter 16.1 section 9). For a Memory Read
  // only the header pool is engaged, and the data pool must be neither
  // charged nor consulted -- a read blocked by a full NPD pool would be a
  // read blocked by a resource it does not use.
  credit_pair_gate #(.CRED_W(CRED_W), .COST_W(COST_W)) u_pair (
    .clk, .rst_n,
    .pkt_valid(local_read_valid),
    .needs_header(uses_nph), .header_cost(nph_cost),
    .needs_data(uses_npd),   .data_cost(npd_cost),
    .send_fire(launch),
    .hdr_return_valid(nph_return_valid), .hdr_return_count(nph_return_count),
    .dat_return_valid(npd_return_valid), .dat_return_count(npd_return_count),
    .init_valid,
    .init_hdr_capacity(init_nph_capacity),
    .init_hdr_infinite(init_nph_infinite),
    .init_dat_capacity(init_npd_capacity),
    .init_dat_infinite(init_npd_infinite),
    .eligible(credit_eligible),
    .hdr_available(nph_available), .dat_available(npd_available),
    .pool_error(pair_err)
  );
 
  // =====================================================================
  // THE CONJUNCTION. All four, in one cycle, or nothing.
  //
  // ACCEPTANCE IS LAUNCH: local_read_ready is exactly the condition under
  // which the packet also leaves. There is no window between accepting the
  // request and committing its resources, so there is no reservation state
  // and no release path to get wrong (section 8's callout).
  // =====================================================================
  wire all_ready = credit_eligible && ctx_available && replay_space && tx_ready;
 
  assign local_read_ready = all_ready;
  assign launch           = local_read_valid && all_ready;
 
  // Reported only while a request is actually waiting.
  assign blocked_on_ctx    = local_read_valid && !ctx_available;
  assign blocked_on_nph    = local_read_valid && uses_nph
                                              && (nph_available < CRED_W'(nph_cost));
  assign blocked_on_npd    = local_read_valid && uses_npd
                                              && (npd_available < CRED_W'(npd_cost));
  assign blocked_on_replay = local_read_valid && !replay_space;
  assign blocked_on_tx     = local_read_valid && !tx_ready;
  assign np_error          = cost_err | pair_err;
 
endmodule

// VERIFICATION-ONLY. Independent reference for the Non-Posted credit cost,
// written from section 1's table rather than from section 7's structure.
typedef struct { int nph; int npd; } np_cost_t;
 
function automatic np_cost_t ref_np_cost(string kind, int payload_bytes);
  np_cost_t c;
  c.nph = 1;                                   // every NP request, always
  case (kind)
    "MEM_READ", "IO_READ", "CFG_READ" : c.npd = 0;
    "IO_WRITE", "CFG_WRITE"           : c.npd = 1;
    "ATOMIC"                          : begin
      // Counted, not divided -- deliberately a different algorithm from
      // section 7, so a rounding bug cannot be present in both.
      c.npd = 0;
      while (payload_bytes > 0) begin
        c.npd = c.npd + 1;
        payload_bytes = payload_bytes - 16;
      end
    end
    default                           : begin c.nph = 0; c.npd = 0; end
  endcase
  return c;
endfunction
 
// The independent local-resource model. It tracks contexts from OBSERVED
// launches and OBSERVED completions -- never from the DUT's ctx_available.
class np_resource_model;
  int contexts_free;
  int nph, npd;
  function void on_launch(np_cost_t c);
    contexts_free--; nph -= c.nph; npd -= c.npd;
  endfunction
  // A COMPLETION returns a CONTEXT. It returns NO credit (section 4).
  function void on_completion();
    contexts_free++;
  endfunction
  // An UPDATE returns CREDIT. It returns NO context.
  function void on_nph_return(int n); nph += n; endfunction
endclass

// SVA over np_credit_cost and np_read_admission, composed with Chapter
// 16.1's primitives and bound against Chapter 12.1's context table.
// These assert the VERIFIED NP costs and the local admission contract.
// Nothing here asserts credit-return timing or completion timing (both
// environment properties -- Chapter 16.1 section 15), the Completion rows
// (16.4), spend policy (16.5), or the update protocol (16.6).
 
// ---- ENVIRONMENT ------------------------------------------------------
// A1: pkt_kind is Chapter 11.7's normalized class, not re-decoded here.
assume property (@(posedge clk) disable iff (!rst_n)
  local_read_valid |-> (pkt_kind != NP_NOT_NP));
// A2: the request is stable while offered and not accepted.
assume property (@(posedge clk) disable iff (!rst_n)
  (local_read_valid && !local_read_ready)
    |=> ($stable(pkt_kind) && $stable(payload_bytes)));
 
// ---- COST -------------------------------------------------------------
 
// P1: EVERY Non-Posted request costs exactly one header credit.
property p_nph_cost_is_one;
  @(posedge clk) disable iff (!rst_n)
  uses_nph |-> (nph_cost == COST_W'(1));
endproperty
a_nph_one : assert property (p_nph_cost_is_one);
 
// P2: A MEMORY READ CONSUMES NO DATA CREDIT -- the chapter's headline
// cost, and the one a mirror of Chapter 16.2's deriver gets wrong.
// Asserted for ALL payload_bytes values, including large ones: a read's
// Length describes REQUESTED data, not carried data (section 3).
property p_read_costs_no_npd;
  @(posedge clk) disable iff (!rst_n)
  (pkt_kind inside {NP_MEM_READ, NP_IO_READ, NP_CFG_READ})
    |-> (!uses_npd && (npd_cost == '0));
endproperty
a_read_no_npd : assert property (p_read_costs_no_npd);
 
// P3: an I/O or Configuration Write costs exactly one NPD -- never n.
property p_io_cfg_write_one_npd;
  @(posedge clk) disable iff (!rst_n)
  (pkt_kind inside {NP_IO_WRITE, NP_CFG_WRITE})
    |-> (uses_npd && (npd_cost == COST_W'(1)));
endproperty
a_io_npd : assert property (p_io_cfg_write_one_npd);
 
// P4: the AtomicOp data cost matches an INDEPENDENT model, and is a
// CEILING (Chapter 16.2 section 11's pair, applied to the one NP kind that
// needs a division).
property p_atomic_npd_ceiling;
  @(posedge clk) disable iff (!rst_n)
  ((pkt_kind == NP_ATOMIC) && (payload_bytes != '0))
    |-> ((COST_W'(npd_cost) * 16 >= payload_bytes)
      && ((COST_W'(npd_cost) - 1) * 16 < payload_bytes));
endproperty
a_atomic_ceiling : assert property (p_atomic_npd_ceiling);
 
// ---- ADMISSION --------------------------------------------------------
 
// P5: no NP request launches without sufficient NPH.
property p_no_launch_without_nph;
  @(posedge clk) disable iff (!rst_n)
  (launch && uses_nph) |-> (nph_available >= CRED_W'(nph_cost));
endproperty
a_nph_gate : assert property (p_no_launch_without_nph);
 
// P6: ALL FOUR RESOURCES, or none. The chapter's central admission
// property -- a launch that satisfied three of four would either overflow
// the receiver, lose replayability, or strand a Completion with no context.
property p_launch_needs_all_four;
  @(posedge clk) disable iff (!rst_n)
  launch |-> (credit_eligible && ctx_available && replay_space && tx_ready);
endproperty
a_conjunction : assert property (p_launch_needs_all_four);
 
// P7: NO RESOURCE IS TAKEN WITHOUT A LAUNCH. There is exactly one path
// that changes state (section 8).
property p_no_resource_without_launch;
  @(posedge clk) disable iff (!rst_n)
  (local_read_valid && !launch)
    |=> ($stable(nph_available) && $stable(npd_available)
      && $stable(dut_ctx_table.allocated_count));
endproperty
a_no_phantom : assert property (p_no_resource_without_launch);
 
// P8: ATOMICITY across the NP pools -- a failed NPD leaves NPH untouched.
property p_failed_npd_leaves_nph;
  @(posedge clk) disable iff (!rst_n)
  (local_read_valid && uses_npd && (npd_available < CRED_W'(npd_cost)))
    |=> $stable(nph_available);
endproperty
a_atomic : assert property (p_failed_npd_leaves_nph);
 
// P9: a Memory Read is never blocked by the NPD pool -- it does not use it.
property p_read_not_blocked_by_npd;
  @(posedge clk) disable iff (!rst_n)
  ((pkt_kind == NP_MEM_READ) && local_read_valid) |-> !blocked_on_npd;
endproperty
a_read_free_of_npd : assert property (p_read_not_blocked_by_npd);
 
// P10: a starved request is STABLE -- metadata unchanged while it waits.
property p_starved_stable;
  @(posedge clk) disable iff (!rst_n)
  (local_read_valid && !local_read_ready)
    |=> (local_read_valid && $stable(pkt_kind) && $stable(payload_bytes));
endproperty
a_stable : assert property (p_starved_stable);
 
// ---- CREDIT AND CONTEXT ARE DIFFERENT RESOURCES (section 4) ------------
 
// P11: THE CORRUPTION PROPERTY. An NPH return NEVER frees a requester
// context. A design that released a Tag on a credit return would free a
// context whose Completion has not arrived -- and that Completion would
// later match a Tag reallocated to a different read.
property p_credit_return_frees_no_context;
  @(posedge clk) disable iff (!rst_n)
  (nph_return_valid && !dut_cpl_arrives)
    |=> $stable(dut_ctx_table.allocated_count);
endproperty
a_no_ctx_from_credit : assert property (p_credit_return_frees_no_context);
 
// P12: and the mirror -- a Completion returns a context, never credit.
property p_completion_returns_no_credit;
  @(posedge clk) disable iff (!rst_n)
  (dut_cpl_arrives && !nph_return_valid && !npd_return_valid)
    |=> ($stable(nph_available) && $stable(npd_available));
endproperty
a_no_credit_from_cpl : assert property (p_completion_returns_no_credit);
 
// P13: context and credit are committed TOGETHER on launch. Catches the
// drift bug: allocate at acceptance, consume at send (section 8).
property p_ctx_and_credit_commit_together;
  @(posedge clk) disable iff (!rst_n)
  launch |=> ((dut_ctx_table.allocated_count == $past(dut_ctx_table.allocated_count) + 1)
           && (nph_available == $past(nph_available) - $past(nph_cost)));
endproperty
a_together : assert property (p_ctx_and_credit_commit_together);
 
// ---- CLASS ISOLATION --------------------------------------------------
 
// P14: a Posted packet never consumes NP credit through this engine.
property p_posted_never_spends_np;
  @(posedge clk) disable iff (!rst_n)
  (dut_posted_engine.send_fire && !launch)
    |=> ($stable(nph_available) && $stable(npd_available));
endproperty
a_class_isolation : assert property (p_posted_never_spends_np);
 
// P15: NPH exhaustion never blocks Posted traffic.
property p_np_starvation_does_not_block_posted;
  @(posedge clk) disable iff (!rst_n)
  ((nph_available == '0) && dut_posted_engine.credit_eligible
                         && dut_posted_engine.pkt_valid)
    |-> dut_posted_engine.pkt_ready;
endproperty
a_no_cross_block : assert property (p_np_starvation_does_not_block_posted);
 
// P16: 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(nph_available) && $stable(npd_available));
endproperty
a_not_replay : assert property (p_replay_is_not_credit);