Credit Bottlenecks — A Healthy Link That Cannot Legally Transmit

// SYNTHESIZABLE. Credit classes and cost derivation.
// SOURCED via Chapter 16.1 §1: six tracked types; the data credit unit is
// 4 DW = 16 bytes; n = Roundup(Length / FC unit size).
package credit_pkg;
 
  parameter int N_CLASS      = 3;                    // P, NP, Cpl (VC0 only, §1)
  parameter int CLASS_W      = (N_CLASS <= 1) ? 1 : $clog2(N_CLASS);
  parameter int CREDIT_BYTES = 16;                   // SOURCED: 4 DW
  parameter int CRED_W       = 12;                   // credit counter width
  parameter int LEN_W        = 16;                   // payload bytes
  parameter int N_PROD       = 3;                    // producers contending
  parameter int PROD_W       = (N_PROD <= 1) ? 1 : $clog2(N_PROD);
 
  typedef enum logic [CLASS_W-1:0] {
    CL_POSTED = '0,
    CL_NONPOSTED = CLASS_W'(1),
    CL_COMPLETION = CLASS_W'(2)
  } tlp_class_e;
 
  // =================================================================
  // THE CEIL DIVISION, WITH THE ZERO GUARD.
  // A header-only TLP carries no data and therefore needs NO data
  // credit. The naive form ((bytes-1)/U)+1 UNDERFLOWS at bytes = 0 and
  // in unsigned 32-bit arithmetic returns 268,435,456 units (§11
  // Model 12) -- a number large enough to look like "plenty available".
  // It is correct for every non-zero input, which is why it survives
  // every test that does not include a header-only packet.
  // =================================================================
  function automatic logic [CRED_W-1:0] data_credits(input logic [LEN_W-1:0] bytes);
    if (bytes == '0) return '0;                                  // THE GUARD
    return CRED_W'((bytes + LEN_W'(CREDIT_BYTES - 1)) / CREDIT_BYTES);
  endfunction
 
  // One header credit per TLP, per Chapter 16.1's header-unit definition.
  function automatic logic [CRED_W-1:0] header_credits(input logic has_tlp);
    return has_tlp ? CRED_W'(1) : CRED_W'(0);
  endfunction
 
  typedef struct packed {
    logic             valid;
    tlp_class_e       tlp_class;
    logic             has_data;
    logic [LEN_W-1:0] payload_bytes;
    logic [CRED_W-1:0] need_hdr;
    logic [CRED_W-1:0] need_data;
  } pkt_cost_t;
 
endpackage

import credit_pkg::*;
 
// SYNTHESIZABLE. Packet credit calculator (§9).
// Header and data are computed INDEPENDENTLY -- a packet may need header
// credit and zero data credit, and collapsing them is mutation 27.
module packet_credit_cost (
  input  logic             pkt_valid,
  input  tlp_class_e       pkt_class,
  input  logic             pkt_has_data,
  input  logic [LEN_W-1:0] pkt_bytes,
  output pkt_cost_t        cost
);
  always_comb begin
    cost.valid         = pkt_valid;
    cost.tlp_class     = pkt_class;
    cost.has_data      = pkt_has_data;
    cost.payload_bytes = pkt_bytes;
    cost.need_hdr      = header_credits(pkt_valid);
    // has_data gates the computation as well as the guard inside it --
    // belt and braces, because this is the corner that ships broken.
    cost.need_data     = (pkt_valid && pkt_has_data) ? data_credits(pkt_bytes)
                                                     : CRED_W'(0);
  end
endmodule

import credit_pkg::*;
 
// SYNTHESIZABLE. Multi-class credit ledger.
// Three states per class: AVAILABLE (may be reserved), RESERVED (owned by
// a specific packet), SPENT (transmitted, awaiting an FC update).
// Arithmetic is WIDENED and checked BEFORE commit -- unsigned underflow
// turns 0 minus 1 into the maximum value (§11 Model 18).
module credit_ledger (
  input  logic clk,
  input  logic rst_n,
 
  input  logic [CRED_W-1:0] advertised_hdr  [N_CLASS],
  input  logic [CRED_W-1:0] advertised_data [N_CLASS],
  input  logic              init_done,
 
  // reservation grant from the manager below -- never from a producer
  input  logic              resv_commit,
  input  tlp_class_e        resv_class,
  input  logic [CRED_W-1:0] resv_hdr,
  input  logic [CRED_W-1:0] resv_data,
 
  input  logic              resv_release,     // cancellation
  input  logic              resv_consume,     // transfer completed
 
  // normalized FC return (Chapter 16.6 owns the real DLLP path)
  input  logic              fc_valid,
  input  logic              fc_ready,
  input  tlp_class_e        fc_class,
  input  logic [CRED_W-1:0] fc_hdr_delta,
  input  logic [CRED_W-1:0] fc_data_delta,
 
  output logic [CRED_W-1:0] avail_hdr  [N_CLASS],
  output logic [CRED_W-1:0] avail_data [N_CLASS],
  output logic [CRED_W-1:0] reserved_hdr  [N_CLASS],
  output logic [CRED_W-1:0] reserved_data [N_CLASS],
  output logic              err_underflow,    // sticky
  output logic              err_overflow      // sticky
);
  logic [CRED_W-1:0] ah_q [N_CLASS], ad_q [N_CLASS];
  logic [CRED_W-1:0] rh_q [N_CLASS], rd_q [N_CLASS];
  logic uf_q, of_q;
 
  always_comb begin
    for (int c = 0; c < N_CLASS; c++) begin
      avail_hdr[c]     = ah_q[c];  avail_data[c]    = ad_q[c];
      reserved_hdr[c]  = rh_q[c];  reserved_data[c] = rd_q[c];
    end
  end
  assign err_underflow = uf_q;
  assign err_overflow  = of_q;
 
  // Widened by one bit so the borrow/carry is VISIBLE rather than wrapped.
  function automatic logic [CRED_W:0] wsub(input logic [CRED_W-1:0] a,
                                           input logic [CRED_W-1:0] b);
    return {1'b0, a} - {1'b0, b};
  endfunction
  function automatic logic [CRED_W:0] wadd(input logic [CRED_W-1:0] a,
                                           input logic [CRED_W-1:0] b);
    return {1'b0, a} + {1'b0, b};
  endfunction
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      for (int c = 0; c < N_CLASS; c++) begin
        ah_q[c] <= '0; ad_q[c] <= '0; rh_q[c] <= '0; rd_q[c] <= '0;
      end
      uf_q <= 1'b0; of_q <= 1'b0;                 // reset FABRICATES NOTHING
    end else begin
      if (init_done)
        for (int c = 0; c < N_CLASS; c++) begin
          if (ah_q[c] == '0 && ad_q[c] == '0 && rh_q[c] == '0 && rd_q[c] == '0) begin
            ah_q[c] <= advertised_hdr[c];
            ad_q[c] <= advertised_data[c];
          end
        end
 
      // ---- RESERVE: available -> reserved -------------------------
      if (resv_commit) begin
        automatic logic [CRED_W:0] nh = wsub(ah_q[resv_class], resv_hdr);
        automatic logic [CRED_W:0] nd = wsub(ad_q[resv_class], resv_data);
        if (nh[CRED_W] || nd[CRED_W]) uf_q <= 1'b1;      // BORROW -> report
        else begin
          ah_q[resv_class] <= nh[CRED_W-1:0];
          ad_q[resv_class] <= nd[CRED_W-1:0];
          rh_q[resv_class] <= rh_q[resv_class] + resv_hdr;
          rd_q[resv_class] <= rd_q[resv_class] + resv_data;
        end
      end
 
      // ---- RELEASE (cancel): reserved -> available -----------------
      if (resv_release) begin
        if (rh_q[resv_class] < resv_hdr || rd_q[resv_class] < resv_data)
          uf_q <= 1'b1;                                   // release without reserve
        else begin
          rh_q[resv_class] <= rh_q[resv_class] - resv_hdr;
          rd_q[resv_class] <= rd_q[resv_class] - resv_data;
          ah_q[resv_class] <= ah_q[resv_class] + resv_hdr;
          ad_q[resv_class] <= ad_q[resv_class] + resv_data;
        end
      end
 
      // ---- CONSUME (transferred): reserved -> spent -----------------
      // Credit stays SPENT. It returns only via an FC update (16.6 §1).
      if (resv_consume) begin
        if (rh_q[resv_class] < resv_hdr || rd_q[resv_class] < resv_data) uf_q <= 1'b1;
        else begin
          rh_q[resv_class] <= rh_q[resv_class] - resv_hdr;
          rd_q[resv_class] <= rd_q[resv_class] - resv_data;
        end
      end
 
      // ---- FC RETURN: applied ONCE, on the accepted beat ------------
      if (fc_valid && fc_ready) begin
        automatic logic [CRED_W:0] nh = wadd(ah_q[fc_class], fc_hdr_delta);
        automatic logic [CRED_W:0] nd = wadd(ad_q[fc_class], fc_data_delta);
        // Returning above what was advertised means the loop is broken.
        if ((nh + {1'b0, rh_q[fc_class]}) > {1'b0, advertised_hdr[fc_class]} ||
            (nd + {1'b0, rd_q[fc_class]}) > {1'b0, advertised_data[fc_class]})
          of_q <= 1'b1;
        else begin
          ah_q[fc_class] <= nh[CRED_W-1:0];
          ad_q[fc_class] <= nd[CRED_W-1:0];
        end
      end
    end
  end
endmodule

import credit_pkg::*;
 
// SYNTHESIZABLE. THE FLAGSHIP BLOCK. Centralized reservation.
// Producers may OBSERVE credit; only this block may GRANT it. Several
// producers each seeing "one credit available" and each deciding to send
// is the double-spend Chapter 16.5 §4 proves; §11 Model 14 measured that
// producers collectively want more than is available in 65.6% of cycles.
module reservation_manager (
  input  logic clk,
  input  logic rst_n,
 
  input  logic       [N_PROD-1:0] req_valid,
  input  tlp_class_e              req_class [N_PROD],
  input  logic [CRED_W-1:0]       req_hdr   [N_PROD],
  input  logic [CRED_W-1:0]       req_data  [N_PROD],
 
  input  logic [CRED_W-1:0]       avail_hdr  [N_CLASS],
  input  logic [CRED_W-1:0]       avail_data [N_CLASS],
 
  output logic [N_PROD-1:0]       grant,
  output logic                    commit,
  output tlp_class_e              commit_class,
  output logic [CRED_W-1:0]       commit_hdr,
  output logic [CRED_W-1:0]       commit_data,
  output logic [N_PROD-1:0]       blocked_by_credit
);
  logic [PROD_W-1:0] rr_q;
  logic [N_PROD-1:0] eligible;
 
  // Eligibility needs BOTH resources for the packet's own class (§2).
  always_comb
    for (int i = 0; i < N_PROD; i++)
      eligible[i] = req_valid[i]
                 && (avail_hdr [req_class[i]] >= req_hdr [i])
                 && (avail_data[req_class[i]] >= req_data[i]);
 
  // A producer is credit-blocked only if it HAS a request (§5).
  always_comb
    for (int i = 0; i < N_PROD; i++)
      blocked_by_credit[i] = req_valid[i] && !eligible[i];
 
  // EXACTLY ONE grant per cycle. This is the whole point: the decision is
  // made once, centrally, against one snapshot of the ledger.
  logic [PROD_W-1:0] pick; logic found;
  always_comb begin
    pick = '0; found = 1'b0;
    for (int k = N_PROD-1; k >= 0; k--) begin
      int idx = (int'(rr_q) + k) % N_PROD;
      if (eligible[idx]) begin pick = PROD_W'(idx); found = 1'b1; end
    end
    grant        = '0;
    if (found) grant[pick] = 1'b1;
    commit       = found;
    commit_class = req_class[pick];
    commit_hdr   = req_hdr[pick];
    commit_data  = req_data[pick];
  end
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) rr_q <= '0;
    else if (found) rr_q <= (pick == PROD_W'(N_PROD-1)) ? '0 : (pick + PROD_W'(1));
  end
endmodule

import credit_pkg::*;
 
// SYNTHESIZABLE. The reservation TRAVELS WITH THE PACKET (§9).
// Held stable under stall; terminated exactly once, by consume OR release.
module reservation_record (
  input  logic clk,
  input  logic rst_n,
  input  logic              grant_valid,
  input  tlp_class_e        grant_class,
  input  logic [CRED_W-1:0] grant_hdr,
  input  logic [CRED_W-1:0] grant_data,
 
  input  logic              tx_valid,
  input  logic              tx_ready,
  input  logic              tx_eop,
  input  logic              cancel,
 
  output logic              resv_valid,
  output tlp_class_e        resv_class,
  output logic [CRED_W-1:0] resv_hdr,
  output logic [CRED_W-1:0] resv_data,
  output logic              do_consume,
  output logic              do_release,
  output logic              err_double_terminate    // sticky
);
  logic v_q, e_q; tlp_class_e c_q; logic [CRED_W-1:0] h_q, d_q;
 
  assign resv_valid = v_q;   assign resv_class = c_q;
  assign resv_hdr   = h_q;   assign resv_data  = d_q;
  assign err_double_terminate = e_q;
 
  // Terminal events are mutually exclusive and require a live reservation.
  assign do_consume = v_q && tx_valid && tx_ready && tx_eop && !cancel;
  assign do_release = v_q && cancel;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin v_q<=1'b0; c_q<=CL_POSTED; h_q<='0; d_q<='0; e_q<=1'b0; end
    else begin
      if ((do_consume || do_release) && !v_q) e_q <= 1'b1;   // cannot happen: prove it
      if (do_consume || do_release) v_q <= 1'b0;
      else if (!v_q && grant_valid) begin
        v_q <= 1'b1; c_q <= grant_class; h_q <= grant_hdr; d_q <= grant_data;
      end
      // Under stall NOTHING above fires, so the record is stable by
      // construction -- P14 proves it rather than trusting it.
    end
  end
endmodule

import credit_pkg::*;
 
// SYNTHESIZABLE. Class-aware scheduler (§7). A class whose credits are
// exhausted must not block a class whose credits are healthy. This is
// LOCAL POLICY -- PCIe does not require separate queues; it makes them
// possible by flow-controlling the classes independently (16.1 §4).
// §11 Model 16: single FIFO lost 34.8% of issue opportunities, per-class
// queues 6.3% -- 28.4% of all cycles recovered by structure alone.
module class_scheduler (
  input  logic clk,
  input  logic rst_n,
  input  logic [N_CLASS-1:0] queue_valid,
  input  logic [N_CLASS-1:0] credits_ok,
  input  logic               tx_ready,
  input  logic               link_operational,
 
  output logic [N_CLASS-1:0] eligible,
  output logic               sel_valid,
  output tlp_class_e         sel_class,
  output logic [N_CLASS-1:0] blocked_pending    // pending AND not eligible (§5)
);
  logic [CLASS_W-1:0] rr_q;
 
  always_comb begin
    for (int c = 0; c < N_CLASS; c++) begin
      eligible[c]        = queue_valid[c] && credits_ok[c] && link_operational;
      blocked_pending[c] = queue_valid[c] && !credits_ok[c];   // qualified, §5
    end
  end
 
  logic [CLASS_W-1:0] pick; logic found;
  always_comb begin
    pick='0; found=1'b0;
    for (int k = N_CLASS-1; k >= 0; k--) begin
      int idx = (int'(rr_q) + k) % N_CLASS;
      if (eligible[idx]) begin pick = CLASS_W'(idx); found = 1'b1; end
    end
    sel_valid = found;
    sel_class = tlp_class_e'(pick);
  end
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) rr_q <= '0;
    else if (found && tx_ready)
      rr_q <= (pick == CLASS_W'(N_CLASS-1)) ? '0 : (pick + CLASS_W'(1));
  end
endmodule

import credit_pkg::*;
 
// SYNTHESIZABLE. Bottleneck attribution instrumentation (§4, §5).
// Per class, per resource, QUALIFIED BY PENDENCY. An unqualified counter
// inflated the credit-blocked total by 81.8% (§11 Model 17).
module credit_stall_counters (
  input  logic clk,
  input  logic rst_n,
  input  logic [N_CLASS-1:0] pending,
  input  logic [N_CLASS-1:0] hdr_short,      // pending packet needs more header
  input  logic [N_CLASS-1:0] data_short,
  input  logic               tags_short,     // §4: a different resource entirely
  input  logic               link_down,
  input  logic [CRED_W-1:0]  avail_hdr  [N_CLASS],
  input  logic [CRED_W-1:0]  avail_data [N_CLASS],
  input  logic               clear,
 
  output logic [31:0] hdr_block_cycles  [N_CLASS],
  output logic [31:0] data_block_cycles [N_CLASS],
  output logic [31:0] tag_block_cycles,
  output logic [31:0] link_block_cycles,
  output logic [CRED_W-1:0] min_hdr  [N_CLASS],   // watermarks, §9
  output logic [CRED_W-1:0] min_data [N_CLASS]
);
  logic [31:0] hb_q [N_CLASS], db_q [N_CLASS], tb_q, lb_q;
  logic [CRED_W-1:0] mh_q [N_CLASS], md_q [N_CLASS];
  logic init_q;
 
  always_comb begin
    for (int c = 0; c < N_CLASS; c++) begin
      hdr_block_cycles[c]  = hb_q[c];
      data_block_cycles[c] = db_q[c];
      min_hdr[c]  = mh_q[c];
      min_data[c] = md_q[c];
    end
    tag_block_cycles  = tb_q;
    link_block_cycles = lb_q;
  end
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n || clear) begin
      for (int c = 0; c < N_CLASS; c++) begin
        hb_q[c] <= '0; db_q[c] <= '0;
        mh_q[c] <= {CRED_W{1'b1}}; md_q[c] <= {CRED_W{1'b1}};  // start HIGH
      end
      tb_q <= '0; lb_q <= '0; init_q <= 1'b0;
    end else begin
      init_q <= 1'b1;
      // ---- FIRST BLOCKING RESOURCE, ranked (§4). A cycle blocked by
      // several resources indicts ONE, or the shares cannot be compared.
      if (link_down) begin
        if (!(&lb_q)) lb_q <= lb_q + 32'd1;
      end else begin
        for (int c = 0; c < N_CLASS; c++) begin
          if (pending[c] && hdr_short[c]) begin              // pendency, §5
            if (!(&hb_q[c])) hb_q[c] <= hb_q[c] + 32'd1;
          end else if (pending[c] && data_short[c]) begin
            if (!(&db_q[c])) db_q[c] <= db_q[c] + 32'd1;
          end
        end
        if (tags_short && !(&tb_q)) tb_q <= tb_q + 32'd1;
      end
 
      // ---- WATERMARKS: monotone DOWNWARD only, never re-raised.
      for (int c = 0; c < N_CLASS; c++) begin
        if (avail_hdr[c]  < mh_q[c]) mh_q[c] <= avail_hdr[c];
        if (avail_data[c] < md_q[c]) md_q[c] <= avail_data[c];
      end
    end
  end
endmodule

import credit_pkg::*;
 
// VERIFICATION-ONLY. Conservation monitor: per class, the three states
// plus what is awaiting an FC update must equal what was advertised.
// A SUMMED-ACROSS-CLASSES version of this check passes while two classes
// are wrong in opposite directions -- the lesson of Chapter 21.4 §7.
module credit_conservation_monitor (
  input logic [CRED_W-1:0] advertised [N_CLASS],
  input logic [CRED_W-1:0] avail      [N_CLASS],
  input logic [CRED_W-1:0] reserved   [N_CLASS],
  input logic [CRED_W-1:0] spent      [N_CLASS],
  output logic err_conservation
);
  always_comb begin
    err_conservation = 1'b0;
    for (int c = 0; c < N_CLASS; c++)
      if ((avail[c] + reserved[c] + spent[c]) != advertised[c])
        err_conservation = 1'b1;               // PER CLASS, deliberately
  end
endmodule

// ==================================================================
// COST DERIVATION (§9) -- the arithmetic that ships broken.
// ==================================================================
 
// P1: a header-only TLP requires ZERO data credit. §11 Model 12: the
// naive ceil form returns 268,435,456 units at bytes = 0.
property p_zero_bytes_zero_data_credit;
  @(posedge clk) disable iff (!rst_n)
    (cost.valid && !cost.has_data) |-> (cost.need_data == '0);
endproperty
 
// P2: the ceil relation holds exactly -- SOURCED n = Roundup(Length/unit).
property p_ceil_division_exact;
  @(posedge clk) disable iff (!rst_n)
    (cost.valid && cost.has_data && (cost.payload_bytes != '0)) |->
      (cost.need_data ==
        CRED_W'((cost.payload_bytes + LEN_W'(CREDIT_BYTES-1)) / CREDIT_BYTES));
endproperty
 
// P3: an exact multiple of the unit consumes no extra credit.
property p_exact_multiple_no_roundup;
  @(posedge clk) disable iff (!rst_n)
    (cost.valid && cost.has_data && ((cost.payload_bytes % CREDIT_BYTES) == '0)
      && (cost.payload_bytes != '0)) |->
      (cost.need_data == CRED_W'(cost.payload_bytes / CREDIT_BYTES));
endproperty
 
// P4: one byte past a unit boundary costs exactly one more credit.
property p_one_byte_over_costs_one_more;
  @(posedge clk) disable iff (!rst_n)
    (cost.valid && cost.has_data
      && ((cost.payload_bytes % CREDIT_BYTES) == LEN_W'(1))) |->
      (cost.need_data == CRED_W'(cost.payload_bytes / CREDIT_BYTES) + CRED_W'(1));
endproperty
 
// P5: every TLP costs header credit, whether or not it carries data.
property p_every_tlp_costs_header;
  @(posedge clk) disable iff (!rst_n)
    cost.valid |-> (cost.need_hdr == CRED_W'(1));
endproperty
 
// ==================================================================
// LEDGER ARITHMETIC (§9) -- no wrap, either direction.
// ==================================================================
 
// P6: credit never underflows. §11 Model 18: unsigned 0 minus 1 is 255,
// after which the engine believes it owns 255 credits.
property p_no_underflow;
  @(posedge clk) disable iff (!rst_n)
    (avail_hdr[0] <= advertised_hdr[0]) && (avail_data[0] <= advertised_data[0]);
endproperty
 
// P7: a reservation that would borrow is REFUSED and reported.
property p_borrow_refused_and_flagged;
  @(posedge clk) disable iff (!rst_n)
    (resv_commit && (resv_hdr > avail_hdr[resv_class])) |=> err_underflow;
endproperty
 
// P8: available + reserved never exceeds what was advertised.
property p_no_overflow_above_advertised;
  @(posedge clk) disable iff (!rst_n)
    ((avail_hdr[0] + reserved_hdr[0]) <= advertised_hdr[0]);
endproperty
 
// P9: per-class conservation. A summed version passes while two classes
// are wrong oppositely (Chapter 21.4 §7's lesson, applied to credit).
property p_conservation_per_class;
  @(posedge clk) disable iff (!rst_n)
    !err_conservation;
endproperty
 
// ==================================================================
// RESERVATION -- availability is not ownership (§9).
// ==================================================================
 
// P10: EXACTLY ONE grant per cycle. Two producers observing the same last
// credit is the double-spend of Chapter 16.5 §4.
property p_single_grant;
  @(posedge clk) disable iff (!rst_n)
    $onehot0(grant);
endproperty
 
// P11: a grant implies both resources sufficed for THAT producer's class.
property p_grant_implies_both_resources;
  @(posedge clk) disable iff (!rst_n)
    grant[0] |-> ((avail_hdr [req_class[0]] >= req_hdr [0])
               && (avail_data[req_class[0]] >= req_data[0]));
endproperty
 
// P12: header sufficiency alone never grants -- mutation 2.
property p_header_alone_insufficient;
  @(posedge clk) disable iff (!rst_n)
    (req_valid[0] && (avail_data[req_class[0]] < req_data[0])) |-> !grant[0];
endproperty
 
// P13: data sufficiency alone never grants -- mutation 1.
property p_data_alone_insufficient;
  @(posedge clk) disable iff (!rst_n)
    (req_valid[0] && (avail_hdr[req_class[0]] < req_hdr[0])) |-> !grant[0];
endproperty
 
// P14: no transmission without a live reservation.
property p_no_issue_without_reservation;
  @(posedge clk) disable iff (!rst_n)
    (tx_valid && tx_ready) |-> resv_valid;
endproperty
 
// P15: the reservation record is STABLE under stall. Availability may
// change underneath; ownership may not.
property p_reservation_stable_under_stall;
  @(posedge clk) disable iff (!rst_n)
    (resv_valid && !(tx_valid && tx_ready && tx_eop) && !cancel)
      |=> (resv_valid && $stable(resv_class)
                      && $stable(resv_hdr) && $stable(resv_data));
endproperty
 
// P16: the reserved class cannot change while the reservation is held --
// the scheduler may not swap the packet under its own reservation.
property p_class_cannot_change_under_stall;
  @(posedge clk) disable iff (!rst_n)
    (resv_valid && $past(resv_valid)) |-> $stable(resv_class);
endproperty
 
// P17: terminal events are mutually exclusive -- consume XOR release.
property p_terminal_exclusive;
  @(posedge clk) disable iff (!rst_n)
    !(do_consume && do_release);
endproperty
 
// P18: a reservation terminates AT MOST ONCE. Releasing twice returns
// credit that was never reserved and lifts the pool above advertised.
property p_single_termination;
  @(posedge clk) disable iff (!rst_n)
    (do_consume || do_release) |=> !(do_consume || do_release) until_with grant_valid;
endproperty
 
// P19: a terminal event requires a live reservation.
property p_terminate_requires_live;
  @(posedge clk) disable iff (!rst_n)
    (do_consume || do_release) |-> resv_valid;
endproperty
 
// P20: cancellation releases the reservation exactly once, and the credit
// returns to AVAILABLE rather than being lost.
property p_cancel_returns_credit;
  @(posedge clk) disable iff (!rst_n)
    do_release |=> (avail_hdr[$past(resv_class)]
                     == $past(avail_hdr[resv_class]) + $past(resv_hdr));
endproperty
 
// ==================================================================
// FC RETURN (§9).
// ==================================================================
 
// P21: an update is applied ONCE, on the accepted beat -- not on every
// cycle `fc_valid` is held.
property p_fc_applied_once;
  @(posedge clk) disable iff (!rst_n)
    (fc_valid && !fc_ready) |=> ($stable(avail_hdr[fc_class])
                              && $stable(avail_data[fc_class]));
endproperty
 
// P22: an update credits the class it names, and no other.
property p_fc_credits_named_class_only;
  @(posedge clk) disable iff (!rst_n)
    (fc_valid && fc_ready && (fc_class != CL_POSTED))
      |=> $stable(avail_hdr[CL_POSTED]);
endproperty
 
// P23: a same-cycle return and reservation are ordered -- the reservation
// may use the returned credit, never the stale value (§10).
property p_same_cycle_return_then_reserve;
  @(posedge clk) disable iff (!rst_n)
    (fc_valid && fc_ready && resv_commit && (fc_class == resv_class)) |=>
      (avail_hdr[resv_class]
        == $past(avail_hdr[resv_class]) + $past(fc_hdr_delta) - $past(resv_hdr));
endproperty
 
// ==================================================================
// RESET (§10) -- must not invent permission.
// ==================================================================
 
// P24: reset zeroes credit. It must NEVER fabricate the advertised total.
property p_reset_zeroes_credit;
  @(posedge clk)
    (!rst_n) |=> ((avail_hdr[0] == '0) && (avail_data[0] == '0));
endproperty
 
// P25: no reservation survives reset.
property p_reset_clears_reservations;
  @(posedge clk)
    (!rst_n) |=> (!resv_valid && (reserved_hdr[0] == '0));
endproperty
 
// ==================================================================
// CLASS INDEPENDENCE AND ATTRIBUTION (§5, §7).
// ==================================================================
 
// P26: a starved class does not block an eligible one. §11 Model 16:
// 28.4% of cycles recovered by queue structure alone.
property p_starved_class_does_not_block;
  @(posedge clk) disable iff (!rst_n)
    (queue_valid[1] && credits_ok[1] && link_operational) |-> sel_valid;
endproperty
 
// P27: exactly one class is selected.
property p_single_class_selected;
  @(posedge clk) disable iff (!rst_n)
    sel_valid |-> (eligible[sel_class]);
endproperty
 
// P28: a credit-stall counter advances only when a packet of that class
// is PENDING. §11 Model 17: unqualified counting inflated by 81.8%.
property p_stall_requires_pending;
  @(posedge clk) disable iff (!rst_n)
    (hdr_block_cycles[0] != $past(hdr_block_cycles[0]))
      |-> $past(pending[0] && hdr_short[0]);
endproperty
 
// P29: an idle class never accrues credit-stall cycles.
property p_no_work_never_counts_as_credit_stall;
  @(posedge clk) disable iff (!rst_n)
    (!pending[0]) |=> ($stable(hdr_block_cycles[0]) && $stable(data_block_cycles[0]));
endproperty
 
// P30: one blocking resource per cycle -- header and data stalls for the
// same class are not both counted (§4's ranking).
property p_one_blocking_resource_per_class;
  @(posedge clk) disable iff (!rst_n)
    (!link_down) |=>
      !((hdr_block_cycles[0]  != $past(hdr_block_cycles[0])) &&
        (data_block_cycles[0] != $past(data_block_cycles[0])));
endproperty
 
// P31: a down Link is attributed to the Link, never to credit (§3).
property p_link_down_outranks_credit;
  @(posedge clk) disable iff (!rst_n)
    link_down |=> ($stable(hdr_block_cycles[0]) && $stable(data_block_cycles[0]));
endproperty
 
// P32: the watermark is monotone DOWNWARD between clears -- it records
// the worst moment, and a recovery must not erase it.
property p_watermark_monotone_down;
  @(posedge clk) disable iff (!rst_n)
    (!clear) |=> (min_hdr[0] <= $past(min_hdr[0]));
endproperty
 
// P33: the watermark never claims less than was ever available.
property p_watermark_bounded_by_history;
  @(posedge clk) disable iff (!rst_n)
    (init_q && !clear) |-> (min_hdr[0] <= avail_hdr[0]);
endproperty
 
// P34: the diagnostic counters never drive the credit state or the
// scheduler -- a monitor that throttles is not a monitor.
property p_monitor_does_not_drive;
  @(posedge clk) disable iff (!rst_n)
    $stable({grant, commit, sel_valid}) or
      !$stable({hdr_block_cycles[0], min_hdr[0]});
endproperty