Payload Size Effects — Two Controls, Two Sides of the Transaction

packets = ceil(T / P)              [dimensionless]

chunk = (remaining < max_payload) ? remaining : max_payload;   // INCOMPLETE

chunk = min( remaining ,
             configured_limit ,
             bytes_to_next_boundary ,
             local_buffer_headroom )        [bytes]

// COMPILE-TIME / VERIFICATION. Packetization arithmetic.
// Integer only; no `real`. Used by the estimator and by the DV model.
package pktsize_pkg;
 
  parameter int ADDR_W  = 64;
  parameter int LEN_W   = 24;                  // bytes in one transfer
  parameter int PAY_W   = 13;                  // bytes in one packet
  parameter int CNT_W   = 24;
 
  // ==================================================================
  // ceil(T / P) WITH THE ZERO GUARD. The naive ((T-1)/P)+1 underflows at
  // T = 0 and, in unsigned 32-bit arithmetic, returns 16,777,216 packets
  // for a 256-byte limit (§12 Model 6). It is correct for every non-zero
  // input, which is exactly why it survives testing.
  // ==================================================================
  function automatic logic [CNT_W-1:0] packet_count(input logic [LEN_W-1:0] total,
                                                    input logic [PAY_W-1:0] pay);
    if (total == '0) return '0;                                    // THE GUARD
    if (pay   == '0) return '0;                                    // no divide by zero
    return CNT_W'((total + LEN_W'(pay) - LEN_W'(1)) / LEN_W'(pay));
  endfunction
 
  // Bytes from `addr` to the next `bnd`-aligned boundary. bnd is a power of
  // two supplied as a mask to keep this a pure AND/subtract.
  function automatic logic [PAY_W-1:0] bytes_to_boundary(input logic [ADDR_W-1:0] addr,
                                                         input logic [PAY_W-1:0]  bnd);
    if (bnd == '0) return '1;                    // no boundary constraint
    return PAY_W'(bnd - PAY_W'(addr & ADDR_W'(bnd - 1)));
  endfunction
 
  function automatic logic [PAY_W-1:0] min3(input logic [PAY_W-1:0] a, b, c);
    logic [PAY_W-1:0] m;
    m = (a < b) ? a : b;
    return (m < c) ? m : c;
  endfunction
 
endpackage

import pktsize_pkg::*;
 
// SYNTHESIZABLE. Generic request chunker (§6).
// The chunk is the MINIMUM of every active constraint. Taking fewer of
// them is the bug: §12 Model 1 ran 13,563,622 packets with 0 violations.
module request_chunker (
  input  logic [ADDR_W-1:0] addr,
  input  logic [LEN_W-1:0]  remaining,
  input  logic [PAY_W-1:0]  max_payload,      // MPS or MRRS, already snapshotted
  input  logic [PAY_W-1:0]  boundary_mask,    // 0 = unconstrained (§1)
  input  logic [PAY_W-1:0]  buffer_headroom,
 
  output logic [PAY_W-1:0]  chunk_bytes,
  output logic [ADDR_W-1:0] next_addr,
  output logic              last,
  output logic              stuck             // would emit zero with bytes left
);
  logic [PAY_W-1:0] to_bnd, lim, rem_clip;
 
  always_comb begin
    to_bnd   = bytes_to_boundary(addr, boundary_mask);
    // Clip `remaining` into the packet-size domain without truncating a
    // large remainder down to a small (or zero) value.
    rem_clip = (remaining > LEN_W'({PAY_W{1'b1}})) ? {PAY_W{1'b1}}
                                                   : PAY_W'(remaining);
    lim      = (max_payload == '0) ? PAY_W'(1) : max_payload;   // never zero
    chunk_bytes = (remaining == '0) ? '0
                                    : min3(min3(rem_clip, lim, to_bnd),
                                           (buffer_headroom == '0) ? PAY_W'(1)
                                                                   : buffer_headroom,
                                           {PAY_W{1'b1}});
    next_addr = addr + ADDR_W'(chunk_bytes);
    last      = (remaining != '0) && (LEN_W'(chunk_bytes) == remaining);
    stuck     = (remaining != '0) && (chunk_bytes == '0);       // P1's escape hatch
  end
endmodule

import pktsize_pkg::*;
 
// SYNTHESIZABLE. MPS-aware write packetizer (§3, §8).
// Progress advances ONLY on the accepted transfer, and the packet's size
// comes from a SNAPSHOT taken when the descriptor was accepted -- a live
// register violated the packet's own contract in 15.3% of stalled cases.
module write_packetizer (
  input  logic clk,
  input  logic rst_n,
 
  input  logic              desc_valid,
  output logic              desc_ready,
  input  logic [ADDR_W-1:0] desc_addr,
  input  logic [LEN_W-1:0]  desc_bytes,
 
  input  logic [PAY_W-1:0]  mps_live,          // may change at ANY time
  input  logic [PAY_W-1:0]  boundary_mask,
 
  output logic              pkt_valid,
  input  logic              pkt_ready,
  output logic [ADDR_W-1:0] pkt_addr,
  output logic [PAY_W-1:0]  pkt_bytes,
  output logic              pkt_last,
  output logic [CNT_W-1:0]  pkt_index,
 
  output logic              busy,
  output logic              err_stuck          // sticky
);
  logic [ADDR_W-1:0] addr_q;
  logic [LEN_W-1:0]  rem_q;
  logic [PAY_W-1:0]  mps_snap_q;               // IMPLEMENTATION POLICY (§8)
  logic [CNT_W-1:0]  idx_q;
  logic              busy_q, err_q;
 
  logic [PAY_W-1:0]  chunk; logic [ADDR_W-1:0] nxt; logic lastc, stuck;
 
  request_chunker u_chunk (
    .addr(addr_q), .remaining(rem_q), .max_payload(mps_snap_q),
    .boundary_mask(boundary_mask), .buffer_headroom({PAY_W{1'b1}}),
    .chunk_bytes(chunk), .next_addr(nxt), .last(lastc), .stuck(stuck)
  );
 
  assign busy       = busy_q;
  assign desc_ready = !busy_q;
  assign pkt_valid  = busy_q && (rem_q != '0);
  assign pkt_addr   = addr_q;
  assign pkt_bytes  = chunk;
  assign pkt_last   = lastc;
  assign pkt_index  = idx_q;
  assign err_stuck  = err_q;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      addr_q<='0; rem_q<='0; mps_snap_q<='0; idx_q<='0; busy_q<=1'b0; err_q<=1'b0;
    end else begin
      if (busy_q && stuck) err_q <= 1'b1;       // report rather than hang silently
 
      if (!busy_q) begin
        if (desc_valid && (desc_bytes != '0)) begin
          addr_q     <= desc_addr;
          rem_q      <= desc_bytes;
          mps_snap_q <= mps_live;               // THE SNAPSHOT, taken once
          idx_q      <= '0;
          busy_q     <= 1'b1;
        end
        // A zero-length descriptor is consumed and emits NO packet (P14).
      end else if (pkt_valid && pkt_ready) begin
        // Progress on the TRANSFER only. Under stall nothing below runs, so
        // addr/rem/size are stable by construction (P7, P8).
        addr_q <= nxt;
        rem_q  <= rem_q - LEN_W'(chunk);
        idx_q  <= idx_q + CNT_W'(1);
        if (lastc) busy_q <= 1'b0;
      end
    end
  end
endmodule

import pktsize_pkg::*;
 
// SYNTHESIZABLE. MRRS-aware read request generator (§4, §5, §7).
// Tracks requested and returned bytes SEPARATELY. Completing on
// requests-issued is a data-corruption bug: at that instant only 40.3% of
// the transfer had returned on average, and 38.6% had received nothing
// (§12 Model 4).
module read_request_generator (
  input  logic clk,
  input  logic rst_n,
 
  input  logic              job_valid,
  output logic              job_ready,
  input  logic [ADDR_W-1:0] job_addr,
  input  logic [LEN_W-1:0]  job_bytes,
 
  input  logic [PAY_W-1:0]  mrrs_live,
  input  logic [PAY_W-1:0]  boundary_mask,
  input  logic              tag_available,
 
  output logic              rq_valid,
  input  logic              rq_ready,
  output logic [ADDR_W-1:0] rq_addr,
  output logic [PAY_W-1:0]  rq_bytes,
 
  // Returned EXTENT, not packet count -- Chapter 13.3's coverage model (§5).
  input  logic              cpl_valid,
  input  logic [PAY_W-1:0]  cpl_bytes,
 
  output logic [LEN_W-1:0]  requested_bytes,
  output logic [LEN_W-1:0]  returned_bytes,
  output logic              job_done,          // returned, NOT requested
  output logic              err_overreturn     // sticky
);
  logic [ADDR_W-1:0] addr_q;
  logic [LEN_W-1:0]  rem_q, total_q, req_q, ret_q;
  logic [PAY_W-1:0]  mrrs_snap_q;
  logic              busy_q, err_q;
  logic [PAY_W-1:0]  chunk; logic [ADDR_W-1:0] nxt; logic lastc, stuck;
 
  request_chunker u_chunk (
    .addr(addr_q), .remaining(rem_q), .max_payload(mrrs_snap_q),
    .boundary_mask(boundary_mask), .buffer_headroom({PAY_W{1'b1}}),
    .chunk_bytes(chunk), .next_addr(nxt), .last(lastc), .stuck(stuck)
  );
 
  assign job_ready       = !busy_q;
  assign rq_valid        = busy_q && (rem_q != '0) && tag_available;
  assign rq_addr         = addr_q;
  assign rq_bytes        = chunk;
  assign requested_bytes = req_q;
  assign returned_bytes  = ret_q;
  assign job_done        = busy_q && (ret_q >= total_q) && (total_q != '0);
  assign err_overreturn  = err_q;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      addr_q<='0; rem_q<='0; total_q<='0; req_q<='0; ret_q<='0;
      mrrs_snap_q<='0; busy_q<=1'b0; err_q<=1'b0;
    end else begin
      if (!busy_q) begin
        if (job_valid && (job_bytes != '0)) begin
          addr_q<=job_addr; rem_q<=job_bytes; total_q<=job_bytes;
          req_q<='0; ret_q<='0; mrrs_snap_q<=mrrs_live; busy_q<=1'b1;
        end
      end else begin
        if (rq_valid && rq_ready) begin
          addr_q <= nxt;
          rem_q  <= rem_q - LEN_W'(chunk);
          req_q  <= req_q + LEN_W'(chunk);      // REQUESTED advances here
        end
        if (cpl_valid) begin
          if ((ret_q + LEN_W'(cpl_bytes)) > total_q) err_q <= 1'b1;
          else ret_q <= ret_q + LEN_W'(cpl_bytes);   // RETURNED advances here
        end
        // The job retires on RETURNED coverage, never on requests issued.
        if ((ret_q >= total_q) && (total_q != '0)) busy_q <= 1'b0;
      end
    end
  end
endmodule

import pktsize_pkg::*;
 
// SYNTHESIZABLE. Configuration snapshot register (§8).
// IMPLEMENTATION POLICY, not a specification requirement. The pending
// value is visible so software can tell that its write has been observed
// but is not yet in force -- silence here is what makes the bug invisible.
module cfg_snapshot #(parameter int W = PAY_W) (
  input  logic clk,
  input  logic rst_n,
  input  logic [W-1:0] cfg_live,
  input  logic         take,            // an ownership boundary occurred
  input  logic         owned,           // a transaction currently holds the value
 
  output logic [W-1:0] cfg_effective,
  output logic [W-1:0] cfg_pending,
  output logic         cfg_stale        // live differs from effective
);
  logic [W-1:0] eff_q;
  assign cfg_effective = eff_q;
  assign cfg_pending   = cfg_live;
  assign cfg_stale     = owned && (cfg_live != eff_q);
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) eff_q <= '0;
    else if (take && !owned) eff_q <= cfg_live;   // ONLY at the boundary
  end
endmodule

// ==================================================================
// CHUNKING (§6) -- progress, and every constraint.
// ==================================================================
 
// P1: never zero while bytes remain. A zero chunk is a HANG, not a
// slow transfer -- nothing else will make progress on its behalf.
property p_chunk_nonzero_when_remaining;
  @(posedge clk) disable iff (!rst_n)
    (remaining != '0) |-> (chunk_bytes != '0);
endproperty
 
// P2: never more than remains.
property p_chunk_le_remaining;
  @(posedge clk) disable iff (!rst_n)
    (remaining != '0) |-> (LEN_W'(chunk_bytes) <= remaining);
endproperty
 
// P3: never more than the configured maximum (MPS or MRRS, snapshotted).
property p_chunk_le_configured;
  @(posedge clk) disable iff (!rst_n)
    (remaining != '0) && (max_payload != '0) |-> (chunk_bytes <= max_payload);
endproperty
 
// P4: never crosses the modelled boundary. §12 Model 1: 0 crossings over
// 13,563,622 packets.
property p_chunk_no_boundary_cross;
  @(posedge clk) disable iff (!rst_n)
    (remaining != '0) && (boundary_mask != '0) |->
      ((addr & ADDR_W'(boundary_mask - 1)) + ADDR_W'(chunk_bytes)
        <= ADDR_W'(boundary_mask));
endproperty
 
// P5: the address advances by exactly the chunk emitted.
property p_addr_advance_exact;
  @(posedge clk) disable iff (!rst_n)
    (pkt_valid && pkt_ready) |=> (pkt_addr == $past(pkt_addr) + ADDR_W'($past(pkt_bytes)));
endproperty
 
// P6: `last` marks the chunk that exactly closes the transfer -- the final
// short packet is neither dropped nor padded.
property p_last_is_exact_end;
  @(posedge clk) disable iff (!rst_n)
    last |-> (LEN_W'(chunk_bytes) == remaining);
endproperty
 
// ==================================================================
// STREAM DISCIPLINE (§9) -- valid/ready, ownership moves once.
// ==================================================================
 
// P7: the packet descriptor is STABLE under stall.
property p_packet_stable_under_stall;
  @(posedge clk) disable iff (!rst_n)
    (pkt_valid && !pkt_ready) |=>
      ($stable(pkt_addr) && $stable(pkt_bytes) && $stable(pkt_last));
endproperty
 
// P8: progress advances ONLY on the accepted transfer.
property p_progress_on_transfer_only;
  @(posedge clk) disable iff (!rst_n)
    (pkt_valid && !pkt_ready) |=> ($stable(pkt_index) && $stable(pkt_addr));
endproperty
 
// P9: the packet index increments exactly once per accepted packet -- no
// duplication, no loss.
property p_index_once_per_packet;
  @(posedge clk) disable iff (!rst_n)
    (pkt_valid && pkt_ready && !pkt_last) |=> (pkt_index == $past(pkt_index) + CNT_W'(1));
endproperty
 
// P10: the engine goes idle only after the LAST packet is accepted.
property p_busy_clears_on_last_only;
  @(posedge clk) disable iff (!rst_n)
    $fell(busy) |-> $past(pkt_valid && pkt_ready && pkt_last);
endproperty
 
// ==================================================================
// READ ACCOUNTING (§5, §7) -- requested and returned are different.
// ==================================================================
 
// P11: requested advances on an accepted REQUEST.
property p_requested_on_request;
  @(posedge clk) disable iff (!rst_n)
    (requested_bytes != $past(requested_bytes)) |-> $past(rq_valid && rq_ready);
endproperty
 
// P12: the job retires on RETURNED coverage, never on requests issued.
// §12 Model 4: at last-issue only 40.3% had returned; 38.6% had nothing.
property p_done_requires_returned;
  @(posedge clk) disable iff (!rst_n)
    job_done |-> (returned_bytes >= requested_bytes) || (returned_bytes != '0);
endproperty
 
// P13: returned never exceeds the transfer extent -- an over-return is an
// error, not arithmetic to absorb.
property p_no_overreturn;
  @(posedge clk) disable iff (!rst_n)
    (returned_bytes + LEN_W'(cpl_bytes) > total_q) && cpl_valid |=> err_overreturn;
endproperty
 
// P14: a Completion count is never used as a completion criterion --
// the coverage model of Chapter 13.3 §1, asserted structurally.
property p_extent_not_packet_count;
  @(posedge clk) disable iff (!rst_n)
    job_done |-> (returned_bytes >= total_q);
endproperty
 
// ==================================================================
// CONFIGURATION SNAPSHOT (§8) -- IMPLEMENTATION POLICY.
// ==================================================================
 
// P15: the effective value is stable while a transaction owns it.
property p_snapshot_stable_while_owned;
  @(posedge clk) disable iff (!rst_n)
    owned |=> $stable(cfg_effective);
endproperty
 
// P16: the effective value changes only at an ownership boundary.
property p_snapshot_changes_only_at_boundary;
  @(posedge clk) disable iff (!rst_n)
    (cfg_effective != $past(cfg_effective)) |-> $past(take && !owned);
endproperty
 
// P17: a divergence between live and effective is REPORTED, not hidden.
property p_stale_reported;
  @(posedge clk) disable iff (!rst_n)
    (owned && (cfg_live != cfg_effective)) |-> cfg_stale;
endproperty
 
// P18: a packet never exceeds the snapshot that governed it -- the
// property a live register cannot satisfy (15.3%, §12 Model 5).
property p_packet_within_its_own_snapshot;
  @(posedge clk) disable iff (!rst_n)
    pkt_valid |-> (pkt_bytes <= mps_snap_q);
endproperty
 
// ==================================================================
// PARAMETER SAFETY AND RESET (§10).
// ==================================================================
 
// P19: reset clears ownership and emits nothing.
property p_reset_clears_owned;
  @(posedge clk)
    (!rst_n) |=> (!busy && !pkt_valid);
endproperty
 
// P20: a zero-length descriptor is consumed and produces NO packet.
// §12 Model 6: the naive ceil helper produces 16,777,216 packets here.
property p_zero_length_no_packet;
  @(posedge clk) disable iff (!rst_n)
    (desc_valid && desc_ready && (desc_bytes == '0)) |=> !pkt_valid;
endproperty
 
// P21: a zero configured maximum never produces a zero chunk -- the
// minimum legal packet is one byte, not a divide-by-zero.
property p_zero_limit_safe;
  @(posedge clk) disable iff (!rst_n)
    (remaining != '0) && (max_payload == '0) |-> (chunk_bytes != '0);
endproperty
 
// P22: the estimator agrees with the runtime packet count under the same
// simplified assumptions (no boundary constraint, no headroom limit).
property p_estimator_matches_runtime;
  @(posedge clk) disable iff (!rst_n)
    (pkt_valid && pkt_ready && pkt_last && (boundary_mask == '0)) |->
      (pkt_index + CNT_W'(1) == packet_count(total_q, mps_snap_q));
endproperty