Credits — Backpressure Across a Wire You Cannot Reach

                 Header          Data
Posted           PH              PD
Non-Posted       NPH             NPD
Completion       CPLH            CPLD

step             1    2    3    4    5    6    7    8
init_valid       1    0    0    0    0    0    0    0
init_capacity    8    -    -    -    -    -    -    -
 
consume_valid    0    1    1    1    1    1    0    0
consume_cost     -    3    3    3    2    2    -    -
 
return_valid     0    0    0    0    1    0    1    0
return_count     -    -    -    -    4    -    2    -
 
available        0    8    5    2    2    4    2    4
can_consume      0    1    1    0    1    1    1    1

// SYNTHESIZABLE. One normalized credit pool: advertised capacity, local
// accounting, eligibility.
// That a transmitter holds a local count, gates on it, and deducts as it
// sends is NORMATIVE (section 1). That zero means INFINITE at
// initialisation is NORMATIVE (section 1, Table 6 note). The error
// outputs, the same-cycle contract and the capacity ceiling are
// ILLUSTRATIVE IMPLEMENTATION POLICY.
module credit_account #(
  // Widths are chosen by the instantiating pool. Header pools are small;
  // data pools are not (section 1: PD's minimum advertisement is the
  // largest supported MPS divided by the FC unit size).
  parameter int CRED_W = 12,
  parameter int COST_W = 12
) (
  input  logic clk,
  input  logic rst_n,
 
  // ---- Initial advertisement, from InitFC (section 1) -------------------
  input  logic                init_valid,
  input  logic [CRED_W-1:0]   init_capacity,
  // NORMATIVE: an advertisement of zero means INFINITE, not empty. It must
  // be a distinct STATE, or the pool blocks that class forever (section 6).
  input  logic                init_infinite,
 
  // ---- Return, from Chapter 15.2's decoded update events ----------------
  input  logic                return_valid,
  input  logic [CRED_W-1:0]   return_count,
 
  // ---- Consumption, on the caller's irrevocable send event --------------
  input  logic                consume_valid,
  input  logic [COST_W-1:0]   consume_cost,
 
  // ---- Outputs ----------------------------------------------------------
  output logic [CRED_W-1:0]   available,
  output logic                can_consume,     // is consume_cost affordable?
  output logic                initialised,
  output logic                underflow_error, // consumed without capacity
  output logic                overflow_error   // returned beyond capacity
);
 
  // =====================================================================
  // THE SAME-CYCLE CONTRACT -- declared, because leaving it implicit is
  // how two blocks end up disagreeing about one cycle.
  //
  //   effective   = available + returned-this-cycle
  //   can_consume = effective >= cost
  //   next        = effective - consumed-this-cycle
  //
  // A return arriving THIS cycle IS usable by a consumption THIS cycle.
  // That is a choice, and the alternative -- returns visible only next
  // cycle -- is equally defensible and costs one cycle of latency per
  // return. What is NOT defensible is deciding eligibility from the old
  // value and then applying both, which can consume capacity that was
  // never available.
  // =====================================================================
 
  // WIDENED ARITHMETIC. available + returned can exceed CRED_W bits, and
  // effective - cost must be evaluated where a negative result is
  // REPRESENTABLE rather than wrapped to a huge positive one.
  localparam int ACC_W = ((CRED_W > COST_W) ? CRED_W : COST_W) + 2;
 
  logic [CRED_W-1:0] avail_q;
  logic [CRED_W-1:0] cap_q;          // the advertised ceiling, for checking
  logic              init_q, inf_q;
  logic              uf_q, of_q;
 
  assign available       = avail_q;
  assign initialised     = init_q;
  assign underflow_error = uf_q;
  assign overflow_error  = of_q;
 
  wire [ACC_W-1:0] avail_x  = ACC_W'(avail_q);
  wire [ACC_W-1:0] ret_x    = (return_valid && init_q && !inf_q)
                                ? ACC_W'(return_count) : '0;
  wire [ACC_W-1:0] cost_x   = ACC_W'(consume_cost);
  wire [ACC_W-1:0] cap_x    = ACC_W'(cap_q);
 
  // Effective capacity for THIS cycle's decision.
  wire [ACC_W-1:0] effective = avail_x + ret_x;
 
  // ELIGIBILITY. An infinite pool is always eligible -- it is not a large
  // number, it is the absence of a limit (section 6).
  assign can_consume = init_q && (inf_q || (effective >= cost_x));
 
  wire do_consume = consume_valid && can_consume;
 
  // Computed once, in one widened expression, from the same `effective`
  // the eligibility decision used. Two separate expressions could disagree.
  wire [ACC_W-1:0] next_x = effective - (do_consume ? cost_x : '0);
 
  // A return that would push a pool past its advertised ceiling is a
  // protocol or decode fault, not capacity (Chapter 15.2 section 6's
  // plausibility argument, applied to the accumulated value).
  wire ret_overflows = return_valid && init_q && !inf_q && (effective > cap_x);
 
  // THE CLAMP APPLIES TO THE NEXT STATE, NOT TO THE RETURN.
  // Clamping to cap_q whenever `effective` exceeded the ceiling would
  // DISCARD a consumption happening in the same cycle -- the packet leaves,
  // its cost is never deducted, and the pool is left at the full ceiling.
  // That INVENTS credit (up to one packet's cost) at the exact moment the
  // receiver has one more packet in it, which is the direction that
  // overflows. Clamp `next_x` instead: it is already the post-consumption
  // value, so the deduction survives the clamp.
  wire next_exceeds_cap = (next_x > cap_x);
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      avail_q <= '0; cap_q <= '0;
      init_q  <= 1'b0; inf_q <= 1'b0;
      uf_q    <= 1'b0; of_q  <= 1'b0;
    end else begin
      if (init_valid && !init_q) begin
        init_q  <= 1'b1;
        inf_q   <= init_infinite;
        cap_q   <= init_infinite ? '0 : init_capacity;
        avail_q <= init_infinite ? '0 : init_capacity;
      end else if (init_q && !inf_q) begin
        // Clamped at the ceiling rather than allowed to run away, and the
        // clamp is REPORTED so it can never be mistaken for normal.
        avail_q <= next_exceeds_cap ? cap_q : CRED_W'(next_x);
      end
 
      if (ret_overflows)                     of_q <= 1'b1;
      // A consumption offered without capacity must be REFUSED by the
      // caller, not absorbed here. If it is asserted anyway, that is a
      // contract violation and it is reported rather than silently wrapped.
      if (consume_valid && !can_consume)     uf_q <= 1'b1;
    end
  end
 
endmodule

// SYNTHESIZABLE. One traffic class, two pools, ATOMIC consumption.
// That a TLP consumes header and (when present) data credits together
// follows from section 1's consumption model. The joint-commit structure
// is the design consequence (section 9's callout).
module credit_pair_gate #(
  parameter int CRED_W = 12,
  parameter int COST_W = 12
) (
  input  logic clk,
  input  logic rst_n,
 
  // ---- Packet descriptor, from the cost deriver -------------------------
  input  logic                pkt_valid,
  input  logic                needs_header,
  input  logic [COST_W-1:0]   header_cost,
  input  logic                needs_data,
  input  logic [COST_W-1:0]   data_cost,
 
  // ---- The irrevocable send event ---------------------------------------
  // The caller asserts this ONLY when the packet is actually leaving. If
  // the transmit path can still stall after this point, the caller has the
  // wrong boundary -- see section 10.
  input  logic                send_fire,
 
  // ---- Pool interfaces ---------------------------------------------------
  input  logic                hdr_return_valid,
  input  logic [CRED_W-1:0]   hdr_return_count,
  input  logic                dat_return_valid,
  input  logic [CRED_W-1:0]   dat_return_count,
 
  input  logic                init_valid,
  input  logic [CRED_W-1:0]   init_hdr_capacity,
  input  logic                init_hdr_infinite,
  input  logic [CRED_W-1:0]   init_dat_capacity,
  input  logic                init_dat_infinite,
 
  // ---- Outputs -----------------------------------------------------------
  output logic                eligible,
  output logic [CRED_W-1:0]   hdr_available,
  output logic [CRED_W-1:0]   dat_available,
  output logic                pool_error
);
 
  logic hdr_ok_raw, dat_ok_raw;
  logic hdr_uf, hdr_of, dat_uf, dat_of;
  logic hdr_init, dat_init;
 
  // JOINT ELIGIBILITY, computed BEFORE either consume input is asserted.
  // A pool the packet does not need is trivially satisfied -- a header-only
  // packet must not be blocked by, or charged to, the data pool.
  wire hdr_ok = !needs_header || hdr_ok_raw;
  wire dat_ok = !needs_data   || dat_ok_raw;
 
  assign eligible = hdr_init && dat_init && hdr_ok && dat_ok;
 
  // ATOMIC COMMIT. Both consume strobes are driven from the SAME condition,
  // so there is no ordering between them and no state in which one pool has
  // been charged and the other has not.
  wire commit = pkt_valid && eligible && send_fire;
 
  credit_account #(.CRED_W(CRED_W), .COST_W(COST_W)) u_hdr (
    .clk, .rst_n,
    .init_valid, .init_capacity(init_hdr_capacity),
    .init_infinite(init_hdr_infinite),
    .return_valid(hdr_return_valid), .return_count(hdr_return_count),
    .consume_valid(commit && needs_header), .consume_cost(header_cost),
    .available(hdr_available), .can_consume(hdr_ok_raw),
    .initialised(hdr_init),
    .underflow_error(hdr_uf), .overflow_error(hdr_of)
  );
 
  credit_account #(.CRED_W(CRED_W), .COST_W(COST_W)) u_dat (
    .clk, .rst_n,
    .init_valid, .init_capacity(init_dat_capacity),
    .init_infinite(init_dat_infinite),
    .return_valid(dat_return_valid), .return_count(dat_return_count),
    .consume_valid(commit && needs_data), .consume_cost(data_cost),
    .available(dat_available), .can_consume(dat_ok_raw),
    .initialised(dat_init),
    .underflow_error(dat_uf), .overflow_error(dat_of)
  );
 
  assign pool_error = hdr_uf | hdr_of | dat_uf | dat_of;
 
endmodule

// SYNTHESIZABLE. Hold a packet until every resource it needs is available.
// Credit eligibility is section 9's. The OTHER resources are named here so
// the multi-resource nature of a launch is visible in one place; Chapter
// 16.3 section 12 builds the Memory Read case fully.
// The set of resources modelled: ILLUSTRATIVE.
module credit_resource_gate (
  input  logic clk,
  input  logic rst_n,
 
  // ---- The waiting packet ------------------------------------------------
  input  logic       pkt_valid,
  output logic       pkt_ready,
 
  // ---- Resources, each owned by a different chapter -----------------------
  input  logic       credit_eligible,   // section 9      -- REMOTE capacity
  input  logic       replay_space,      // Chapter 14.4   -- LOCAL storage
  input  logic       tx_path_ready,     // the transmit path this cycle
 
  output logic       send_fire,
  // Which resource is missing. Not decoration: section 13's first
  // debugging question is exactly this, and without it the answer needs a
  // simulation run.
  output logic       blocked_on_credit,
  output logic       blocked_on_replay,
  output logic       blocked_on_path
);
 
  // ALL OF THEM, ALWAYS. A launch that satisfied two of three would either
  // overflow the receiver, or transmit a packet that could never be
  // replayed if the Link lost it (Chapter 14.1 section 2).
  wire all_ready = credit_eligible && replay_space && tx_path_ready;
 
  assign pkt_ready = all_ready;
  assign send_fire = pkt_valid && all_ready;
 
  // Reported only while a packet is actually waiting -- an idle gate is not
  // "blocked", and a flag that asserts when nothing wants to send is noise.
  assign blocked_on_credit = pkt_valid && !credit_eligible;
  assign blocked_on_replay = pkt_valid && !replay_space;
  assign blocked_on_path   = pkt_valid && !tx_path_ready;
 
endmodule

// SVA over credit_account, credit_pair_gate and credit_resource_gate.
// These assert the local accounting contract and the declared same-cycle
// semantics. They assert NOTHING about credit-return timing (an
// environment property, not a design one), nothing about the per-class
// consumption table (Chapters 16.2-16.4), nothing about spend policy
// (Chapter 16.5), and nothing about the update protocol (Chapter 16.6).
 
// ---- ENVIRONMENT ------------------------------------------------------
// A1: returns are decoded DIFFERENCES from Chapter 15.2, not totals.
assume property (@(posedge clk) disable iff (!rst_n)
  return_valid |-> (return_count != '0));
// A2: send_fire is IRREVOCABLE -- the packet really leaves (section 10).
assume property (@(posedge clk) disable iff (!rst_n)
  send_fire |-> pkt_valid);
 
// ---- CONSERVATION AND RANGE -------------------------------------------
 
// P1: available NEVER underflows. The property a narrow-arithmetic design
// fails by wrapping to a huge positive value.
property p_no_underflow;
  @(posedge clk) disable iff (!rst_n)
  initialised |-> (available <= cap_q);
endproperty
a_range : assert property (p_no_underflow);
 
// P2: THE CONSERVATION IDENTITY. A verification accounting statement, NOT
// PCIe wire state: everything advertised and returned is either still
// available or was spent. Ghost counters are testbench state.
property p_conservation;
  @(posedge clk) disable iff (!rst_n)
  (initialised && !inf_q)
    |-> ((g_initial + g_returned - g_consumed) == available);
endproperty
a_conserve : assert property (p_conservation);
 
// P3: AN INFINITE POOL NEVER BLOCKS. Zero at initialisation means
// unlimited, not empty (section 6). A design that missed this stalls that
// class forever, and the symptom looks like a dead receiver.
property p_infinite_never_blocks;
  @(posedge clk) disable iff (!rst_n)
  (initialised && inf_q) |-> can_consume;
endproperty
a_infinite : assert property (p_infinite_never_blocks);
 
// P4: nothing is consumable before initialisation. A transmitter with no
// information must assume NO capacity (section 2).
property p_no_credit_before_init;
  @(posedge clk) disable iff (!rst_n)
  !initialised |-> !can_consume;
endproperty
a_uninit : assert property (p_no_credit_before_init);
 
// ---- THE SAME-CYCLE CONTRACT ------------------------------------------
 
// P5: eligibility uses EFFECTIVE capacity -- available plus this cycle's
// return (section 8's declared contract). Restated independently, so a
// design that decided from the stale value fails.
property p_effective_eligibility;
  @(posedge clk) disable iff (!rst_n)
  (initialised && !inf_q)
    |-> (can_consume ==
         ((available + (return_valid ? return_count : '0)) >= consume_cost));
endproperty
a_effective : assert property (p_effective_eligibility);
 
// P6: return and consume in the SAME cycle both apply, exactly once each.
property p_simultaneous_applies_both;
  @(posedge clk) disable iff (!rst_n)
  (return_valid && consume_valid && can_consume && !inf_q)
    |=> (available == ($past(available) + $past(return_count)
                                        - $past(consume_cost)));
endproperty
a_simul : assert property (p_simultaneous_applies_both);
 
// P7: a return is applied EXACTLY ONCE -- not twice, not zero times.
property p_return_applied_once;
  @(posedge clk) disable iff (!rst_n)
  (return_valid && !consume_valid && !inf_q && !ret_overflows)
    |=> (available == ($past(available) + $past(return_count)));
endproperty
a_return_once : assert property (p_return_applied_once);
 
// ---- OWNERSHIP --------------------------------------------------------
 
// P8: NO CREDIT IS CONSUMED MERELY BECAUSE A PACKET IS VALID. The single
// most common credit bug (section 13).
property p_no_consume_without_send;
  @(posedge clk) disable iff (!rst_n)
  (pkt_valid && !send_fire) |=> ($stable(hdr_available) && $stable(dat_available));
endproperty
a_no_phantom : assert property (p_no_consume_without_send);
 
// P9: A FAILED MULTI-RESOURCE ELIGIBILITY CHANGES NO POOL. The leak in
// section 9's callout, asserted directly.
property p_failed_eligibility_is_free;
  @(posedge clk) disable iff (!rst_n)
  (pkt_valid && !eligible)
    |=> ($stable(hdr_available) && $stable(dat_available));
endproperty
a_atomic : assert property (p_failed_eligibility_is_free);
 
// P10: ATOMICITY. Either both needed pools moved, or neither did.
property p_pair_atomic;
  @(posedge clk) disable iff (!rst_n)
  (commit && needs_header && needs_data)
    |=> (!$stable(hdr_available) && !$stable(dat_available));
endproperty
a_pair : assert property (p_pair_atomic);
 
// P11: ISOLATION. A packet that needs no data credit never touches the
// data pool -- it is neither charged nor blocked by it.
property p_header_only_leaves_data_alone;
  @(posedge clk) disable iff (!rst_n)
  (commit && needs_header && !needs_data) |=> $stable(dat_available);
endproperty
a_isolation : assert property (p_header_only_leaves_data_alone);
 
// P12: a credit-starved packet is STABLE. Not dropped, not mutated.
property p_starved_packet_stable;
  @(posedge clk) disable iff (!rst_n)
  (pkt_valid && !pkt_ready)
    |=> (pkt_valid && $stable(header_cost) && $stable(data_cost));
endproperty
a_stable : assert property (p_starved_packet_stable);
 
// ---- CROSS-RESOURCE NON-INTERFERENCE ----------------------------------
 
// P13: REPLAY STORAGE IS NOT CREDIT (section 3). A full replay buffer
// blocks the launch and must not alter any credit counter.
property p_replay_does_not_touch_credit;
  @(posedge clk) disable iff (!rst_n)
  !replay_space |=> ($stable(hdr_available) && $stable(dat_available));
endproperty
a_not_replay : assert property (p_replay_does_not_touch_credit);
 
// P14: an ACK returns replay storage, never credit (Chapter 14.2).
property p_ack_returns_no_credit;
  @(posedge clk) disable iff (!rst_n)
  (dut_retire_window.retire_valid && !return_valid)
    |=> ($stable(hdr_available) && $stable(dat_available));
endproperty
a_ack_not_credit : assert property (p_ack_returns_no_credit);
 
// P15: reset and initialisation are explicit.
property p_reset_clears;
  @(posedge clk)
  !rst_n |=> (!initialised && !can_consume && (available == '0));
endproperty
a_reset : assert property (p_reset_clears);