Host Memory Access — Writes That Vanish and Reads That Come Back in Pieces

device → host memory                    host memory → device
────────────────────                    ────────────────────
Memory WRITE                            Memory READ Request
posted                                  non-posted
payload travels WITH the request        request carries NO data
no Completion, ever                     Completion(s) return the data
fire and forget                         outstanding state until data lands

descriptor snapshot (20.2 §6)
      ↓
chunk: address, length          bounded by MPS and the address boundary (§7)
      ↓
Memory Write TLP: addr + payload
      ↓
transmit path                   credits, arbitration, LTSSM (20.1 §7)
      ↓
host memory

descriptor snapshot
      ↓
chunk: address, length                bounded by max read request and boundary (§7)
      ↓
allocate a TAG                        §9 -- BEFORE the request goes out
      ↓
create a read CONTEXT                 §11 -- where does this data go?
      ↓
Memory Read Request TLP
      ↓
        ... time passes, other requests are issued ...
      ↓
Completion with Data arrives          carries a Tag (§12)
      ↓
match to context, accumulate bytes    §13
      ↓
when expected bytes received:  retire context, FREE the Tag

valid            is this Tag in use?
descriptor_id    which transfer does it belong to?
local_offset     where in the device buffer does this data land?
expected_bytes   how much did we ask for?
received_bytes   how much has arrived?
status           did anything fail?

bytes_to_boundary = 4096 - (addr & 0xFFF)

chunk = min(remaining, max_request, bytes_to_boundary)

one Completion  ≠  one read request completed
all requests issued  ≠  all bytes returned

cycle              1     2     3     4     5     6     7     8     9    10
desc_active        0     1     1     1     1     1     1     1     1     0
 
memrd_valid        0     1     1     0     0     0     0     0     0     0
memrd_ready        0     0     1     0     0     0     0     0     0     0
read_tag          --     3     3    --    --    --    --    --    --    --
tag_busy[3]        0     0     1     1     1     1     1     1     0     0
 
cpl_valid          0     0     0     0     0     1     0     1     0     0
cpl_tag           --    --    --    --    --     3    --     3    --    --
cpl_bytes         --    --    --    --    --   256    --   256    --    --
 
expected           0     0   512   512   512   512   512   512     0     0
received           0     0     0     0     0   256   256   512     0     0
read_done          0     0     0     0     0     0     0     1     0     0

// SYNTHESIZABLE. Normalized host-access types.
// TAG WIDTH is the sourced part (section 1): a 5-bit Tag field gives 32
// outstanding identifiers, 8 bits gives 256 with Extended Tag enabled.
// Everything else is internal normalization.
package host_access_pkg;
 
  parameter int ADDR_W = 64;
  parameter int LEN_W  = 24;
  parameter int TAG_W  = 5;                 // section 1: 5-bit Tag field
  parameter int N_TAGS = (1 << TAG_W);
 
  // The address boundary a single request must not span.
  parameter int BOUNDARY = 4096;
  parameter int BND_W    = $clog2(BOUNDARY);   // 12
 
  typedef enum logic [1:0] {
    CPL_OK      = 2'd0,
    CPL_ERR     = 2'd1,      // normalized failure -- Chapter 13.2 owns encodings
    CPL_UNKNOWN = 2'd2       // no matching outstanding request (section 11)
  } cpl_status_e;
 
  function automatic logic [BND_W:0] bytes_to_boundary(input logic [ADDR_W-1:0] a);
    return (BND_W+1)'(BOUNDARY) - {1'b0, a[BND_W-1:0]};
  endfunction
 
endpackage

import host_access_pkg::*;
 
// SYNTHESIZABLE. Choose one legal request size.
// TWO INDEPENDENT BOUNDS (section 7): a configured maximum, and the
// address boundary. Section 17 verified 0 boundary crossings and 0
// oversize chunks across 5,680 fully-walked transfers.
//
// SOURCED WORKED CASE: 4096 bytes at max_request 512 -> 8 requests, which
// matches section 1's vendor text exactly.
module host_req_chunker (
  input  logic [ADDR_W-1:0] addr,
  input  logic [LEN_W-1:0]  remaining,
  input  logic [LEN_W-1:0]  max_request,     // MRRS for reads, MPS for writes (§8)
 
  output logic [LEN_W-1:0]  chunk_bytes,
  output logic [ADDR_W-1:0] next_addr,
  output logic              chunk_valid
);
 
  wire [BND_W:0] to_bnd = bytes_to_boundary(addr);
 
  always_comb begin
    logic [LEN_W-1:0] c;
    c = remaining;
    if (max_request != '0 && c > max_request) c = max_request;
    // ==============================================================
    // THE BOUNDARY BOUND. Without it, a maximum-size request from a
    // misaligned address spans a boundary -- section 7's worked case
    // 0x1000_0004 with 4096 bytes at max 4096, which must become
    // [4092, 4] rather than one illegal request.
    // ==============================================================
    if (LEN_W'(to_bnd) < c) c = LEN_W'(to_bnd);
    chunk_bytes = c;
  end
 
  // Never zero while bytes remain -- a zero chunk is an infinite loop
  // (section 18, mutation 13). to_bnd is at least 1 by construction.
  assign chunk_valid = (remaining != '0) && (chunk_bytes != '0);
  assign next_addr   = addr + ADDR_W'(chunk_bytes);
 
endmodule

import host_access_pkg::*;
 
// SYNTHESIZABLE. Device -> host: posted Memory Write (section 3).
// NO COMPLETION EVER RETURNS. The retirement boundary used here is
// acceptance by the transmit path, and it is DECLARED (section 3).
module host_write_owner (
  input  logic clk,
  input  logic rst_n,
 
  input  logic              active,
  input  logic [ADDR_W-1:0] cur_addr,
  input  logic [LEN_W-1:0]  chunk_bytes,
  input  logic              chunk_valid,
  input  logic              payload_ready,     // the data for this chunk exists
 
  output logic              tx_valid,
  output logic [ADDR_W-1:0] tx_addr,
  output logic [LEN_W-1:0]  tx_len,
  input  logic              tx_ready,
  input  logic              link_ok,
 
  output logic              issue_fire,
  output logic [LEN_W-1:0]  issue_bytes
);
  // Offered only when the payload exists -- a stall must never strand a
  // half-built request (mutation 15).
  assign tx_valid = active && chunk_valid && payload_ready && link_ok;
  assign tx_addr  = cur_addr;
  assign tx_len   = chunk_bytes;
 
  // ==================================================================
  // PROGRESS ON THE HANDSHAKE ONLY. Chapter 20.1 section 19 measured
  // advancing on `valid`: bytes_issued exceeded the total in 79.5% of
  // randomized cases, so the descriptor "completed" with data never sent.
  // ==================================================================
  assign issue_fire  = tx_valid && tx_ready;
  assign issue_bytes = chunk_bytes;
 
  // NOTE what is absent: any completion input. A posted write has none
  // (section 3), and a design that waited for one hangs (mutation 3).
endmodule

import host_access_pkg::*;
 
// SYNTHESIZABLE. Tag lease management (section 9).
// A TAG IS ALLOCATED BEFORE THE REQUEST IS OFFERED and freed only at
// CONTEXT RETIREMENT. Section 18's counterexample is the version that
// frees at transmission.
//
// DELIBERATELY SMALL. Section 1 sources 32 or 256 Tags; scaling the pool
// and the outstanding-request depth belongs to Chapter 20.5.
module tag_allocator #(
  parameter int TAGS  = 8,
  parameter int TAG_IDX_W = (TAGS <= 1) ? 1 : $clog2(TAGS)
) (
  input  logic clk,
  input  logic rst_n,
 
  input  logic                 alloc_req,
  output logic                 alloc_valid,
  output logic [TAG_IDX_W-1:0] alloc_tag,
 
  input  logic                 free_req,
  input  logic [TAG_IDX_W-1:0] free_tag,
 
  output logic                 no_tags_available,
  output logic                 err_double_free,
  output logic [TAGS-1:0]      busy_map        // lab observability (§19)
);
  generate if (TAGS < 1) $error("TAGS must be at least 1"); endgenerate
 
  logic [TAGS-1:0] busy_q;
  logic            dfree_q;
  assign busy_map          = busy_q;
  assign err_double_free   = dfree_q;
  assign no_tags_available = (&busy_q);
 
  // Lowest free index. Deterministic, so a failing test is reproducible.
  logic [TAG_IDX_W-1:0] first_free;
  logic                 any_free;
  always_comb begin
    first_free = '0; any_free = 1'b0;
    for (int i = TAGS-1; i >= 0; i--)
      if (!busy_q[i]) begin first_free = TAG_IDX_W'(i); any_free = 1'b1; end
  end
  assign alloc_valid = alloc_req && any_free;
  assign alloc_tag   = first_free;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin busy_q <= '0; dfree_q <= 1'b0; end
    else begin
      // ==============================================================
      // ALLOCATE AND FREE IN THE SAME CYCLE is legal and must be handled:
      // a context retiring while a new request is issued is the steady
      // state of a busy engine (section 16). Free is applied first so the
      // freed Tag is immediately re-allocatable.
      // ==============================================================
      if (free_req) begin
        if (free_tag < TAG_IDX_W'(TAGS) && busy_q[free_tag]) busy_q[free_tag] <= 1'b0;
        else dfree_q <= 1'b1;      // double free or out of range -- REPORTED
      end
      if (alloc_valid && !(free_req && (free_tag == alloc_tag)))
        busy_q[alloc_tag] <= 1'b1;
      else if (alloc_valid)
        busy_q[alloc_tag] <= 1'b1; // re-allocated the just-freed Tag
    end
  end
endmodule

import host_access_pkg::*;
 
// SYNTHESIZABLE. One context per outstanding read (section 5).
// THIS TABLE IS WHY OUT-OF-ORDER AND SPLIT COMPLETIONS ARE SURVIVABLE:
// the returning data carries no information about where it belongs
// (section 5) -- only the context does.
module read_context_table #(
  parameter int TAGS = 8,
  parameter int TAG_IDX_W = (TAGS <= 1) ? 1 : $clog2(TAGS)
) (
  input  logic clk,
  input  logic rst_n,
 
  // ---- Create, at the request handshake ----------------------------------
  input  logic                 create,
  input  logic [TAG_IDX_W-1:0] create_tag,
  input  logic [15:0]          create_desc_id,
  input  logic [LEN_W-1:0]     create_offset,
  input  logic [LEN_W-1:0]     create_bytes,
 
  // ---- Completion arrival -------------------------------------------------
  input  logic                 cpl_valid,
  input  logic [TAG_IDX_W-1:0] cpl_tag,
  input  logic [LEN_W-1:0]     cpl_bytes,
  input  cpl_status_e          cpl_status,
 
  // ---- Retirement ---------------------------------------------------------
  output logic                 retire_valid,
  output logic [TAG_IDX_W-1:0] retire_tag,
  output logic [15:0]          retire_desc_id,
  output logic [LEN_W-1:0]     retire_bytes,
  output cpl_status_e          retire_status,
 
  output logic                 err_unknown_tag,
  output logic                 err_overrun
);
  logic [TAGS-1:0]      v_q;
  logic [15:0]          did_q  [TAGS];
  logic [LEN_W-1:0]     off_q  [TAGS], exp_q [TAGS], rcv_q [TAGS];
  cpl_status_e          st_q   [TAGS];
  logic                 unk_q, ovr_q;
 
  assign err_unknown_tag = unk_q;
  assign err_overrun     = ovr_q;
 
  // ==================================================================
  // THE MATCH IS BY TAG AGAINST THE OUTSTANDING SET, never against
  // "the descriptor we are currently on" (section 6). Section 18's third
  // counterexample is that design, and it writes B's data into A's buffer.
  // ==================================================================
  wire in_range   = (cpl_tag < TAG_IDX_W'(TAGS));
  wire matched    = cpl_valid && in_range && v_q[cpl_tag];
  // NEXT value, not current -- section 18's second counterexample measured
  // the alternative at 100.0% failure to retire.
  wire [LEN_W-1:0] next_rcv = matched ? (rcv_q[cpl_tag] + cpl_bytes) : '0;
  wire overrun    = matched && (next_rcv > exp_q[cpl_tag]);
  wire complete   = matched && !overrun && (next_rcv == exp_q[cpl_tag]);
  wire failed     = matched && (cpl_status != CPL_OK);
 
  assign retire_valid   = matched && (complete || failed || overrun);
  assign retire_tag     = cpl_tag;
  assign retire_desc_id = did_q[cpl_tag];
  assign retire_bytes   = overrun ? rcv_q[cpl_tag] : next_rcv;
  assign retire_status  = (failed || overrun) ? CPL_ERR : CPL_OK;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      v_q <= '0; unk_q <= 1'b0; ovr_q <= 1'b0;
    end else begin
      if (create) begin
        v_q[create_tag]   <= 1'b1;
        did_q[create_tag] <= create_desc_id;
        off_q[create_tag] <= create_offset;   // WHERE the data goes (§5)
        exp_q[create_tag] <= create_bytes;
        rcv_q[create_tag] <= '0;
        st_q[create_tag]  <= CPL_OK;
      end
 
      if (cpl_valid) begin
        if (!matched) begin
          // Section 1: "User should signal if a completion is received but
          // the tag does not match any outstanding requests." REPORTED --
          // never aliased onto context 0 (mutation 11).
          unk_q <= 1'b1;
        end else if (overrun) begin
          ovr_q <= 1'b1;
          v_q[cpl_tag] <= 1'b0;
        end else begin
          rcv_q[cpl_tag] <= next_rcv;
          // Retire on the byte count, never on a Completion count (§10).
          if (complete || failed) v_q[cpl_tag] <= 1'b0;
        end
      end
    end
  end
endmodule

// SVA over the host-access blocks. LOCAL contract only. Nothing asserts
// that Completions arrive, that Tags become available, or that the Link
// permits traffic.
 
// ---- CHUNKING ---------------------------------------------------------
 
// P1: A CHUNK NEVER CROSSES THE BOUNDARY. Section 17 verified 0 crossings
// across 5,680 fully-walked transfers.
property p_no_boundary_cross;
  @(posedge clk) disable iff (!rst_n)
  chunk_valid |-> ((addr[ADDR_W-1:BND_W]) == ((addr + chunk_bytes - 1) >> BND_W));
endproperty
a_bnd : assert property (p_no_boundary_cross);
 
// P2: bounded by the configured maximum and by what remains, and never
// zero while bytes remain (mutation 13 loops forever).
property p_chunk_bounded;
  @(posedge clk) disable iff (!rst_n)
  chunk_valid |-> ((chunk_bytes != '0) && (chunk_bytes <= remaining)
                && ((max_request == '0) || (chunk_bytes <= max_request)));
endproperty
a_chunk : assert property (p_chunk_bounded);
 
// ---- WRITE PATH -------------------------------------------------------
 
// P3: the write request is stable under stall.
property p_wr_stable;
  @(posedge clk) disable iff (!rst_n)
  (tx_valid && !tx_ready) |=> (tx_valid && $stable(tx_addr) && $stable(tx_len));
endproperty
a_wr : assert property (p_wr_stable);
 
// P4: progress advances only on the handshake.
property p_wr_fire;
  @(posedge clk) disable iff (!rst_n) issue_fire |-> (tx_valid && tx_ready);
endproperty
a_wrfire : assert property (p_wr_fire);
 
// P5: THE WRITE PATH NEVER WAITS FOR A COMPLETION -- structurally, it has
// no completion input (section 3, mutation 3).
property p_wr_no_cpl_wait;
  @(posedge clk) disable iff (!rst_n)
  (active && chunk_valid && payload_ready && link_ok) |-> tx_valid;
endproperty
a_nowait : assert property (p_wr_no_cpl_wait);
 
// ---- TAGS -------------------------------------------------------------
 
// P6: A TAG IS ALLOCATED BEFORE THE REQUEST IS OFFERED.
property p_tag_before_request;
  @(posedge clk) disable iff (!rst_n)
  (memrd_valid) |-> busy_map[read_tag];
endproperty
a_tagfirst : assert property (p_tag_before_request);
 
// P7: NO DOUBLE ALLOCATION -- an allocated Tag is not handed out again
// until it is freed.
property p_no_double_alloc;
  @(posedge clk) disable iff (!rst_n)
  (alloc_valid && !(free_req && (free_tag == alloc_tag))) |-> !busy_map[alloc_tag];
endproperty
a_dblalloc : assert property (p_no_double_alloc);
 
// P8: THE TAG IS NOT FREED UNTIL ITS CONTEXT RETIRES. Section 18's first
// counterexample is the version freed at transmission.
property p_tag_lease;
  @(posedge clk) disable iff (!rst_n)
  (busy_map[t] && !$past(retire_valid && (retire_tag == TAG_IDX_W'(t))))
    |=> (busy_map[t] || $past(!rst_n));
endproperty
a_lease : assert property (p_tag_lease);
 
// P9: freeing an unallocated or out-of-range Tag is REPORTED.
property p_bad_free;
  @(posedge clk) disable iff (!rst_n)
  (free_req && ((free_tag >= TAG_IDX_W'(TAGS)) || !busy_map[free_tag]))
    |=> err_double_free;
endproperty
a_badfree : assert property (p_bad_free);
 
// ---- COMPLETION MATCHING AND ACCUMULATION -----------------------------
 
// P10: A COMPLETION IS MATCHED BY TAG, and an unmatched one is reported
// rather than aliased (section 1's sourced requirement).
property p_unknown_reported;
  @(posedge clk) disable iff (!rst_n)
  (cpl_valid && ((cpl_tag >= TAG_IDX_W'(TAGS)) || !ctx_valid[cpl_tag]))
    |=> (err_unknown_tag && !retire_valid);
endproperty
a_unk : assert property (p_unknown_reported);
 
// P11: RECEIVED BYTES NEVER EXCEED EXPECTED.
property p_no_overrun;
  @(posedge clk) disable iff (!rst_n)
  ctx_valid[t] |-> (ctx_received[t] <= ctx_expected[t]);
endproperty
a_over : assert property (p_no_overrun);
 
// P12: RETIREMENT ON THE EXACT BYTE COUNT, using the NEXT value.
// Section 17 measured the current-value comparison at 100.0% failure.
property p_retire_exact;
  @(posedge clk) disable iff (!rst_n)
  (retire_valid && (retire_status == CPL_OK))
    |-> (retire_bytes == $past(ctx_expected[cpl_tag]));
endproperty
a_exact : assert property (p_retire_exact);
 
// P12b: and ONE retirement per context -- a split Completion does not
// retire on its first fragment (mutation 10).
property p_retire_once;
  @(posedge clk) disable iff (!rst_n)
  (retire_valid) |=> !ctx_valid[$past(cpl_tag)];
endproperty
a_once : assert property (p_retire_once);
 
// P13: A COMPLETION CANNOT UPDATE A CONTEXT OTHER THAN ITS OWN. The
// property section 18's third counterexample violates.
property p_no_cross_context;
  @(posedge clk) disable iff (!rst_n)
  (cpl_valid && (cpl_tag != TAG_IDX_W'(t))) |=> $stable(ctx_received[t]);
endproperty
a_cross : assert property (p_no_cross_context);
 
// P14: AN ERROR COMPLETION IS NOT COUNTED AS GOOD DATA.
property p_error_not_success;
  @(posedge clk) disable iff (!rst_n)
  (cpl_valid && (cpl_status != CPL_OK) && ctx_valid[cpl_tag])
    |=> (retire_status == CPL_ERR);
endproperty
a_err : assert property (p_error_not_success);
 
// P15: THE READ PATH NEVER RETIRES ON ISSUANCE (20.1 §19: 99.5% early).
property p_read_not_on_issued;
  @(posedge clk) disable iff (!rst_n)
  retire_valid |-> $past(cpl_valid);
endproperty
a_notissued : assert property (p_read_not_on_issued);
 
// P16: CONSERVATION -- requested bytes are either outstanding or returned.
property p_conservation;
  @(posedge clk) disable iff (!rst_n)
  ctx_valid[t] |-> ((ctx_expected[t] - ctx_received[t]) + ctx_received[t]
                    == ctx_expected[t]);
endproperty
a_cons : assert property (p_conservation);
 
// P17: reset clears every outstanding context and Tag -- no stale
// transaction state survives (section 20).
property p_reset;
  @(posedge clk)
  !rst_n |=> ((busy_map == '0) && (ctx_valid == '0) && !retire_valid);
endproperty
a_reset : assert property (p_reset);