Posted Credits — One Header, and a Ceiling Division

PH cost:   1                              a CONSTANT
PD cost:   Roundup(bytes / 16)            a CEILING DIVISION

step             1     2     3     4     5     6     7
pkt_valid        1     1     1     1     1     1     0
pkt_bytes       64    17    64    64    64     -     -
pd_cost          4     2     4     4     4     -     -
 
ph_available     4     3     2     1     1     1     2
pd_available     8     4     2     2     2     6     6
 
eligible         1     1     0     0     1     0     -
send_fire        1     1     0     0     1     0     -
 
pd_return        0     0     0     0     0     4     0

// SYNTHESIZABLE. Derive Posted flow-control cost from a normalized packet
// descriptor.
// 1 PH per Posted TLP, and n PD where n = Roundup(Length / FC unit size)
// with the data unit 4 DW: NORMATIVE (section 1). The descriptor shape and
// the illegal-length report: ILLUSTRATIVE.
package posted_fc_pkg;
 
  // VERIFIED (section 1): the data credit unit is 4 DW = 16 bytes.
  localparam int FC_DATA_UNIT_BYTES = 16;
 
  // Normalized packet class, from Chapter 11.7's decode. NOT re-derived
  // from Fmt/Type here (section 3).
  typedef enum logic [1:0] {
    PKT_MEM_WRITE       = 2'd0,   // Posted:     1 PH + n PD
    PKT_MSG_NO_DATA     = 2'd1,   // Posted:     1 PH
    PKT_MSG_WITH_DATA   = 2'd2,   // Posted:     1 PH + n PD
    PKT_NOT_POSTED      = 2'd3    // uses the NP pools -- Chapter 16.3
  } posted_kind_e;
 
  // CEILING DIVISION, in the only form that is correct at every boundary.
  //
  //   bytes/16          under-charges by 1 unless bytes is a multiple of 16
  //   bytes/16 + 1      over-charges by 1 on exact multiples
  //   (bytes+16)/16     over-charges by 1 on exact multiples
  //   (bytes+15)/16     CORRECT                                (section 4)
  //
  // COMPILE-TIME SAFE: the addition is performed at a width that cannot
  // wrap, then the result is narrowed once the division has shrunk it.
  function automatic logic [11:0]
      pd_credit_cost(input logic [13:0] payload_bytes);
    logic [14:0] widened;              // one bit wider than the input, so
    widened = {1'b0, payload_bytes}    // + (UNIT-1) cannot overflow
            + 15'(FC_DATA_UNIT_BYTES - 1);
    return 12'(widened / 15'(FC_DATA_UNIT_BYTES));
  endfunction
 
endpackage

import posted_fc_pkg::*;
 
module posted_credit_cost #(
  parameter int LEN_W  = 14,        // payload bytes; 14 bits covers 4096
  parameter int COST_W = 12
) (
  input  posted_kind_e        pkt_kind,
  input  logic [LEN_W-1:0]    payload_bytes,
 
  output logic                uses_ph,
  output logic [COST_W-1:0]   ph_cost,
  output logic                uses_pd,
  output logic [COST_W-1:0]   pd_cost,
 
  // A Posted packet claiming payload it cannot have, or a non-Posted kind
  // reaching this deriver at all. Reported rather than silently costed.
  output logic                cost_error
);
 
  wire is_posted = (pkt_kind != PKT_NOT_POSTED);
  wire has_data  = (pkt_kind == PKT_MEM_WRITE)
                || (pkt_kind == PKT_MSG_WITH_DATA);
 
  // THE HEADER COST IS A CONSTANT (section 4). There is nothing to compute
  // and therefore nothing to get wrong -- the unit is sized for the largest
  // header plus Digest, so a 3DW and a 4DW header both cost one.
  assign uses_ph = is_posted;
  assign ph_cost = is_posted ? COST_W'(1) : '0;
 
  // A ZERO-LENGTH payload consumes NO data credits. Charging one would
  // drain PD against packets that store nothing.
  wire data_present = has_data && (payload_bytes != '0);
 
  assign uses_pd = data_present;
  assign pd_cost = data_present
                     ? COST_W'(pd_credit_cost(14'(payload_bytes)))
                     : '0;
 
  assign cost_error = (!is_posted)
                   || (!has_data && (payload_bytes != '0));
 
endmodule

import posted_fc_pkg::*;
 
// SYNTHESIZABLE. Compose the cost deriver with Chapter 16.1's atomic pair
// and multi-resource gate for one Posted transmit path.
// The PH/PD costs are NORMATIVE (section 1). The composition, the reason
// flags and the consume-on-send boundary are Chapter 16.1's ILLUSTRATIVE
// implementation policy.
module posted_issue_gate #(
  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 Posted transmit queue --------------------------------
  input  logic                pkt_valid,
  input  posted_kind_e        pkt_kind,
  input  logic [LEN_W-1:0]    payload_bytes,
  output logic                pkt_ready,
 
  // ---- Other launch resources (Chapter 16.1 section 10) -----------------
  input  logic                replay_space,
  input  logic                tx_path_ready,
 
  // ---- Credit plumbing ---------------------------------------------------
  input  logic                init_valid,
  input  logic [CRED_W-1:0]   init_ph_capacity,
  input  logic                init_ph_infinite,
  input  logic [CRED_W-1:0]   init_pd_capacity,
  input  logic                init_pd_infinite,
  input  logic                ph_return_valid,
  input  logic [CRED_W-1:0]   ph_return_count,
  input  logic                pd_return_valid,
  input  logic [CRED_W-1:0]   pd_return_count,
 
  // ---- Outputs ------------------------------------------------------------
  output logic                send_fire,
  output logic [CRED_W-1:0]   ph_available,
  output logic [CRED_W-1:0]   pd_available,
  output logic                blocked_on_ph,
  output logic                blocked_on_pd,
  output logic                blocked_on_replay,
  output logic                blocked_on_path,
  output logic                posted_error
);
 
  logic uses_ph, uses_pd, cost_err, credit_eligible;
  logic [COST_W-1:0] ph_cost, pd_cost;
 
  posted_credit_cost #(.LEN_W(LEN_W), .COST_W(COST_W)) u_cost (
    .pkt_kind, .payload_bytes,
    .uses_ph, .ph_cost, .uses_pd, .pd_cost, .cost_error(cost_err)
  );
 
  // ATOMIC ACROSS BOTH POOLS (Chapter 16.1 section 9). Eligibility is
  // evaluated for PH and PD together, and the two consume strobes come from
  // one commit -- so a short PD pool can never leak a PH credit.
  logic pair_err;
  credit_pair_gate #(.CRED_W(CRED_W), .COST_W(COST_W)) u_pair (
    .clk, .rst_n,
    .pkt_valid,
    .needs_header(uses_ph), .header_cost(ph_cost),
    .needs_data(uses_pd),   .data_cost(pd_cost),
    .send_fire,
    .hdr_return_valid(ph_return_valid), .hdr_return_count(ph_return_count),
    .dat_return_valid(pd_return_valid), .dat_return_count(pd_return_count),
    .init_valid,
    .init_hdr_capacity(init_ph_capacity),
    .init_hdr_infinite(init_ph_infinite),
    .init_dat_capacity(init_pd_capacity),
    .init_dat_infinite(init_pd_infinite),
    .eligible(credit_eligible),
    .hdr_available(ph_available), .dat_available(pd_available),
    .pool_error(pair_err)
  );
 
  // CREDIT IS ONE INPUT TO A LAUNCH, NOT THE WHOLE OF IT.
  credit_resource_gate u_gate (
    .clk, .rst_n,
    .pkt_valid, .pkt_ready,
    .credit_eligible, .replay_space, .tx_path_ready,
    .send_fire,
    .blocked_on_credit(), .blocked_on_replay, .blocked_on_path
  );
 
  // Split the credit reason by pool. "Blocked on credit" is not actionable;
  // "blocked on PD" tells an engineer which pool to watch (section 11).
  assign blocked_on_ph = pkt_valid && uses_ph && (ph_available < CRED_W'(ph_cost));
  assign blocked_on_pd = pkt_valid && uses_pd && (pd_available < CRED_W'(pd_cost));
  assign posted_error  = cost_err | pair_err;
 
endmodule

remote receiver stops draining
   → PD credits stop returning
   → head-of-queue write is ineligible
   → posted queue stops dequeuing
   → queue fills
   → local producer sees its own ready go low
   → the producer stalls

// VERIFICATION-ONLY. Independent reference for the Posted credit cost.
// Deliberately NOT the same algorithm as section 6: this counts units,
// section 6 divides. Two implementations of one rule, and a mismatch means
// one of them is wrong.
function automatic int ref_pd_cost(int payload_bytes);
  int n, remaining;
  n = 0;
  remaining = payload_bytes;
  while (remaining > 0) begin
    n = n + 1;
    remaining = remaining - 16;      // 4 DW, verified (section 1)
  end
  return n;                          // zero-length yields 0
endfunction
 
function automatic int ref_ph_cost(bit is_posted);
  return is_posted ? 1 : 0;          // a constant, verified (section 1)
endfunction

in-flight posted bytes  ≤  PD credits available × 16 bytes

// SVA over posted_credit_cost and posted_issue_gate, composed with Chapter
// 16.1's primitives. These assert the VERIFIED Posted costs and the local
// issue contract. Nothing here asserts credit-return timing (an environment
// property), the NP or Completion rows (Chapters 16.3-16.4), spend policy
// (16.5), or the update protocol (16.6).
 
// ---- ENVIRONMENT ------------------------------------------------------
// A1: pkt_kind is the NORMALIZED class from Chapter 11.7, not re-decoded.
assume property (@(posedge clk) disable iff (!rst_n)
  pkt_valid |-> (pkt_kind != PKT_NOT_POSTED));
// A2: payload_bytes is stable while the packet is offered.
assume property (@(posedge clk) disable iff (!rst_n)
  (pkt_valid && !pkt_ready) |=> $stable(payload_bytes));
 
// ---- COST -------------------------------------------------------------
 
// P1: THE HEADER COST IS EXACTLY ONE, always (section 1). No length
// dependence, no header-size dependence.
property p_ph_cost_is_one;
  @(posedge clk) disable iff (!rst_n)
  uses_ph |-> (ph_cost == COST_W'(1));
endproperty
a_ph_one : assert property (p_ph_cost_is_one);
 
// P2: THE CHAPTER'S CENTRAL PROPERTY. The data cost equals an INDEPENDENT
// model (section 9's counting loop, not section 6's division). A shared
// rounding bug cannot satisfy this.
property p_pd_cost_matches_reference;
  @(posedge clk) disable iff (!rst_n)
  uses_pd |-> (pd_cost == COST_W'(ref_pd_cost(int'(payload_bytes))));
endproperty
a_pd_ref : assert property (p_pd_cost_matches_reference);
 
// P2b: CEILING, NOT FLOOR -- stated directly, so the failure names itself.
// n*16 must COVER the payload, and (n-1)*16 must not.
property p_pd_cost_is_ceiling;
  @(posedge clk) disable iff (!rst_n)
  (uses_pd && (payload_bytes != '0))
    |-> ((COST_W'(pd_cost) * 16 >= payload_bytes)
      && ((COST_W'(pd_cost) - 1) * 16 < payload_bytes));
endproperty
a_ceiling : assert property (p_pd_cost_is_ceiling);
 
// P3: a Posted packet with no payload consumes NO data credits.
property p_no_payload_no_pd;
  @(posedge clk) disable iff (!rst_n)
  (pkt_kind == PKT_MSG_NO_DATA) |-> (!uses_pd && (pd_cost == '0));
endproperty
a_no_pd : assert property (p_no_payload_no_pd);
 
// ---- ISSUE ------------------------------------------------------------
 
// P4: no Posted packet issues without sufficient PH.
property p_no_issue_without_ph;
  @(posedge clk) disable iff (!rst_n)
  (send_fire && uses_ph) |-> (ph_available >= CRED_W'(ph_cost));
endproperty
a_ph_gate : assert property (p_no_issue_without_ph);
 
// P5: no payload-carrying Posted packet issues without sufficient PD.
property p_no_issue_without_pd;
  @(posedge clk) disable iff (!rst_n)
  (send_fire && uses_pd) |-> (pd_available >= CRED_W'(pd_cost));
endproperty
a_pd_gate : assert property (p_no_issue_without_pd);
 
// P6: ATOMICITY. A failed PD eligibility consumes NO PH -- the leak in
// Chapter 16.1 section 9, in its Posted form.
property p_failed_pd_leaves_ph;
  @(posedge clk) disable iff (!rst_n)
  (pkt_valid && uses_pd && (pd_available < CRED_W'(pd_cost)))
    |=> $stable(ph_available);
endproperty
a_atomic : assert property (p_failed_pd_leaves_ph);
 
// P7: and the mirror -- a failed PH eligibility consumes no PD.
property p_failed_ph_leaves_pd;
  @(posedge clk) disable iff (!rst_n)
  (pkt_valid && uses_ph && (ph_available < CRED_W'(ph_cost)))
    |=> $stable(pd_available);
endproperty
a_atomic_mirror : assert property (p_failed_ph_leaves_pd);
 
// P8: a header-only Posted packet never touches PD.
property p_header_only_leaves_pd;
  @(posedge clk) disable iff (!rst_n)
  (send_fire && !uses_pd) |=> $stable(pd_available);
endproperty
a_isolation : assert property (p_header_only_leaves_pd);
 
// P9: CREDIT IS CONSUMED EXACTLY ONCE PER ISSUED PACKET. Ghost counters
// are testbench state.
property p_consumed_once;
  @(posedge clk) disable iff (!rst_n)
  send_fire |=> ((g_ph_spent == $past(g_ph_spent) + $past(ph_cost))
              && (g_pd_spent == $past(g_pd_spent) + $past(pd_cost)));
endproperty
a_once : assert property (p_consumed_once);
 
// P10: no credit consumed without an issue (Chapter 16.1 P8, Posted form).
property p_no_phantom_consumption;
  @(posedge clk) disable iff (!rst_n)
  (pkt_valid && !send_fire)
    |=> ($stable(ph_available) && $stable(pd_available));
endproperty
a_no_phantom : assert property (p_no_phantom_consumption);
 
// P11: a credit-starved packet is STABLE and still offered.
property p_starved_stable;
  @(posedge clk) disable iff (!rst_n)
  (pkt_valid && !pkt_ready)
    |=> (pkt_valid && $stable(pkt_kind) && $stable(payload_bytes));
endproperty
a_stable : assert property (p_starved_stable);
 
// ---- CROSS-POOL NON-INTERFERENCE --------------------------------------
 
// P12: A NON-POSTED PACKET NEVER CONSUMES POSTED CREDIT through this
// engine (section 3). The mutation that drains PH with I/O writes.
property p_np_never_spends_posted;
  @(posedge clk) disable iff (!rst_n)
  (dut_np_engine.send_fire && !send_fire)
    |=> ($stable(ph_available) && $stable(pd_available));
endproperty
a_class_isolation : assert property (p_np_never_spends_posted);
 
// P13: a PD return never lands in the PH pool, and vice versa.
property p_returns_do_not_cross;
  @(posedge clk) disable iff (!rst_n)
  (pd_return_valid && !ph_return_valid) |=> $stable(ph_available);
endproperty
a_return_pool : assert property (p_returns_do_not_cross);
 
// P14: 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(ph_available) && $stable(pd_available));
endproperty
a_not_replay : assert property (p_replay_is_not_credit);