Memory Read — A Split Transaction, End to End

software load from 0x8000_0120
   → the Requester recognises a PCIe-space access
   → a Memory Read Request TLP is constructed and launched
   → address routing carries it to the Endpoint
   → the Endpoint's BAR decode matches, producing internal offset 0x120
   → the resource is read
   → a Completion with Data is constructed and routed back
   → the Requester correlates it to the original operation
   → the load's result is delivered

0x8000_0120  is placed in the Request's address field
   → each Switch compares it against its downstream Base/Limit windows
   → it falls inside the window covering this Endpoint's subtree
   → the Request is forwarded down that port
   → it reaches the Endpoint
   → the Endpoint's BAR decode matches: BAR base 0x8000_0000, so this is mine
   → internal offset = 0x8000_0120 - 0x8000_0000 = 0x120
   → the resource at offset 0x120 is read

// SYNTHESIZABLE. Accept a local read intent, allocate context, and emit a
// normalized Memory Read Request descriptor.
// Non-posted split semantics and MRRS bounding the request extent:
// NORMATIVE (section 3). The descriptor, the interface and the
// correlation-index scheme: ILLUSTRATIVE.
module mem_read_req_engine #(
  parameter int ADDR_W = 64,
  parameter int CTXS   = 8,      // outstanding reads supported
  parameter int LEN_W  = 11,     // DW count; 1..1024 needs 11 bits
  parameter int DEST_W = 8,      // opaque local destination token
  // In the PARAMETER LIST, not the body: it appears in the port list, and a
  // body localparam cannot be referenced there. Width-safe at CTXS == 1.
  parameter int IDX_W  = (CTXS <= 1) ? 1 : $clog2(CTXS)
) (
  input  logic clk,
  input  logic rst_n,
 
  // ---- Operative limit, from configuration at RUN TIME -----------------
  // DECODED byte limit from Device Control bits 14:12 (section 3). An input
  // rather than a parameter: software sets it after elaboration.
  input  logic [12:0]        mrrs_bytes,
  input  logic               mrrs_valid,
 
  // ---- Local read intent -----------------------------------------------
  input  logic               loc_valid,
  input  logic [ADDR_W-1:0]  loc_addr,
  input  logic [LEN_W-1:0]   loc_len_dw,
  input  logic [DEST_W-1:0]  loc_dest,
  output logic               loc_ready,
 
  // ---- Outbound Request descriptor -------------------------------------
  output logic               req_valid,
  output logic [ADDR_W-1:0]  req_addr,
  output logic [LEN_W-1:0]   req_len_dw,
  output logic [IDX_W-1:0]   req_ctx_id,     // INTERNAL index, NOT a Tag
  input  logic               req_ready,
 
  // ---- Context table interface -----------------------------------------
  input  logic               ctx_free_avail,
  input  logic [IDX_W-1:0]   ctx_free_id,
  output logic               ctx_reserve,     // FREE      -> RESERVED
  output logic [IDX_W-1:0]   ctx_reserve_id,
  output logic               ctx_launch,      // RESERVED  -> OUTSTANDING
  output logic [IDX_W-1:0]   ctx_launch_id,
 
  // ---- Reported conditions ---------------------------------------------
  output logic               oversize_error,  // asked beyond MRRS
  output logic               no_limit_error   // MRRS not known
);
 
  generate
    if (CTXS < 1)  $error("CTXS must be at least 1");
    if (LEN_W < 11) $error("LEN_W must hold 1024 DW");
  endgenerate
 
  // MRRS in DW. Four bytes per DW.
  wire [10:0] mrrs_dw   = mrrs_bytes[12:2];
  wire        limit_ok  = mrrs_valid && (mrrs_dw != 11'd0);
  wire        size_ok   = limit_ok && (loc_len_dw != '0)
                                   && (loc_len_dw <= LEN_W'(mrrs_dw));
 
  // ---- PENDING REQUEST STAGE ------------------------------------------
  // The descriptor offered downstream is REGISTERED, never a live view of a
  // combinational free-entry scan. Without this stage, req_ctx_id would be
  // driven straight from ctx_free_id — and a Completion freeing a
  // lower-numbered entry while req_ready is low would change the correlation
  // index of an offer already in progress. That is a valid/ready payload
  // stability violation, and it corrupts a Request nobody has sent yet.
  logic                 pend_valid_q;
  logic [IDX_W-1:0]     pend_ctx_q;
  logic [ADDR_W-1:0]    pend_addr_q;
  logic [LEN_W-1:0]     pend_len_q;
 
  wire launch = pend_valid_q && req_ready;
 
  // Accept a new local read when the pending stage is empty, or when the
  // pending Request is being launched this cycle (same-cycle replacement).
  assign loc_ready = (!pend_valid_q || req_ready)
                   && ctx_free_avail && size_ok;
 
  wire accept = loc_valid && loc_ready;
 
  // FREE -> RESERVED happens at local acceptance, so the chosen index is
  // removed from the free pool before the offer begins.
  assign ctx_reserve    = accept;
  assign ctx_reserve_id = ctx_free_id;
 
  // RESERVED -> OUTSTANDING happens on the downstream handshake.
  assign ctx_launch     = launch;
  assign ctx_launch_id  = pend_ctx_q;
 
  // The offer is driven entirely from registers. Nothing here can move
  // while req_ready is low.
  assign req_valid  = pend_valid_q;
  assign req_addr   = pend_addr_q;
  assign req_len_dw = pend_len_q;
  assign req_ctx_id = pend_ctx_q;
 
  logic osz_q, nol_q;
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      pend_valid_q <= 1'b0; pend_ctx_q <= '0;
      pend_addr_q  <= '0;   pend_len_q <= '0;
      osz_q <= 1'b0; nol_q <= 1'b0;
    end else begin
      // accept has priority over launch, so a same-cycle launch-and-accept
      // leaves the stage holding the NEW request rather than going empty.
      if (accept) begin
        pend_valid_q <= 1'b1;
        pend_ctx_q   <= ctx_free_id;
        pend_addr_q  <= loc_addr;
        pend_len_q   <= loc_len_dw;
      end else if (launch) begin
        pend_valid_q <= 1'b0;
      end
 
      // Reported, not silently clamped. A design that truncated an oversized
      // request to MRRS would return less data than the client asked for and
      // tell no one (section 9's principle, applied to size).
      if (loc_valid && !limit_ok)             nol_q <= 1'b1;
      if (loc_valid &&  limit_ok && !size_ok) osz_q <= 1'b1;
    end
  end
  assign oversize_error = osz_q;
  assign no_limit_error = nol_q;
 
endmodule

// SYNTHESIZABLE. Retain per-read state for the lifetime of an outstanding
// Memory Read, and match returning Completions against it.
// Retaining context across a split transaction: NORMATIVE consequence of
// non-posted semantics. The fields, the index scheme and the progress
// accounting: ILLUSTRATIVE implementation.
module read_ctx_table #(
  parameter int ADDR_W = 64,
  parameter int CTXS   = 8,
  parameter int LEN_W  = 11,
  parameter int DEST_W = 8,
  parameter int IDX_W  = (CTXS <= 1) ? 1 : $clog2(CTXS)
) (
  input  logic clk,
  input  logic rst_n,
 
  // ---- Reservation and launch, from the request engine ------------------
  // FREE -> RESERVED. The descriptor is captured here so the entry is
  // complete before the Request is ever offered downstream (section 9a).
  input  logic               reserve,
  input  logic [IDX_W-1:0]   reserve_id,
  input  logic [ADDR_W-1:0]  reserve_addr,
  input  logic [LEN_W-1:0]   reserve_len_dw,
  input  logic [DEST_W-1:0]  reserve_dest,
  // RESERVED -> OUTSTANDING, on the outbound handshake.
  input  logic               launch,
  input  logic [IDX_W-1:0]   launch_id,
 
  output logic               free_avail,
  output logic [IDX_W-1:0]   free_id,
  // Validity bitmap: an entry is OCCUPIED if reserved or outstanding.
  // Exposed so a reset assertion can cover EVERY entry (section 14, P13).
  output logic [CTXS-1:0]    ctx_occupied_mask,
 
  // ---- Returned Completion chunk ---------------------------------------
  input  logic               cpl_valid,
  input  logic [IDX_W-1:0]   cpl_ctx_id,
  input  logic [LEN_W-1:0]   cpl_dw,          // DW returned in this chunk
 
  // ---- Per-chunk outputs, for the assembler ----------------------------
  output logic               chunk_accept,
  output logic [DEST_W-1:0]  chunk_dest,
  output logic [ADDR_W-1:0]  chunk_addr,      // where this chunk belongs
  output logic               read_resolved,   // ALL expected data has arrived
 
  // ---- Reported conditions ---------------------------------------------
  output logic               unknown_ctx_error,
  output logic               overrun_error,
  // An identifier outside 0..CTXS-1 was presented. Distinct from
  // unknown_ctx_error, which means in-range but not outstanding.
  output logic               illegal_id_error
);
 
  typedef struct packed {
    logic                valid;        // RESERVED or OUTSTANDING
    logic                outstanding;  // launched; Completions may arrive
    logic [DEST_W-1:0]   local_dest;
    logic [LEN_W-1:0]    remaining_dw;
    logic [ADDR_W-1:0]   start_addr;
    logic [LEN_W-1:0]    received_dw;
  } read_ctx_t;
 
  read_ctx_t ctx_q [CTXS];
 
  always_comb
    for (int i = 0; i < CTXS; i++) ctx_occupied_mask[i] = ctx_q[i].valid;
 
  // ---- RANGE SAFETY ----------------------------------------------------
  // IDX_W = $clog2(CTXS) can express values >= CTXS whenever CTXS is not a
  // power of two: at CTXS = 5, IDX_W is 3 and 5, 6 and 7 are presentable
  // but do not exist. Every array access below is guarded. The comparison
  // is one bit wider than the identifier so CTXS stays representable when
  // it IS a power of two — a same-width compare truncates CTXS to zero at
  // CTXS = 8 and rejects every legal index.
  localparam int CHK_W = IDX_W + 1;
  wire cpl_id_legal     = (CHK_W'(cpl_ctx_id) < CHK_W'(CTXS));
  wire reserve_id_legal = (CHK_W'(reserve_id) < CHK_W'(CTXS));
  wire launch_id_legal  = (CHK_W'(launch_id)  < CHK_W'(CTXS));
 
  // Guarded reads. Defaults make an illegal index look absent, so it can
  // never satisfy ctx_hit and never be credited.
  logic             cpl_entry_valid, cpl_entry_outstanding;
  logic [LEN_W-1:0] cpl_entry_remaining, cpl_entry_received;
  logic [DEST_W-1:0]  cpl_entry_dest;
  logic [ADDR_W-1:0]  cpl_entry_start;
 
  always_comb begin
    cpl_entry_valid       = 1'b0;
    cpl_entry_outstanding = 1'b0;
    cpl_entry_remaining   = '0;
    cpl_entry_received    = '0;
    cpl_entry_dest        = '0;
    cpl_entry_start       = '0;
    if (cpl_id_legal) begin
      cpl_entry_valid       = ctx_q[cpl_ctx_id].valid;
      cpl_entry_outstanding = ctx_q[cpl_ctx_id].outstanding;
      cpl_entry_remaining   = ctx_q[cpl_ctx_id].remaining_dw;
      cpl_entry_received    = ctx_q[cpl_ctx_id].received_dw;
      cpl_entry_dest        = ctx_q[cpl_ctx_id].local_dest;
      cpl_entry_start       = ctx_q[cpl_ctx_id].start_addr;
    end
  end
 
  // Free-entry search over the occupancy bitmap. A RESERVED entry is already
  // valid, so it is never offered again — which is what keeps the offered
  // req_ctx_id from being re-pointed mid-offer (section 9a). Linear for
  // clarity at teaching scale; a real design uses a free-list.
  logic             fa;
  logic [IDX_W-1:0] fid;
  always_comb begin
    fa = 1'b0; fid = '0;
    for (int i = CTXS - 1; i >= 0; i--)
      if (!ctx_q[i].valid) begin fa = 1'b1; fid = IDX_W'(i); end
  end
  assign free_avail = fa;
  assign free_id    = fid;
 
  // Completion matching. A chunk is accepted only for an OUTSTANDING context
  // — an unknown identifier, or one that is merely RESERVED, must never
  // disturb any entry. A Completion for a Request that has not launched is
  // by definition not ours.
  wire        ctx_hit  = cpl_valid && cpl_id_legal
                                   && cpl_entry_valid && cpl_entry_outstanding;
  wire [LEN_W-1:0] rem = cpl_entry_remaining;
  wire        overrun  = ctx_hit && (cpl_dw > rem);
  wire        fits     = ctx_hit && !overrun && (cpl_dw != '0);
 
  assign chunk_accept = fits;
  assign chunk_dest   = cpl_entry_dest;
  // Where this chunk belongs within the read: start + what already arrived.
  // Derived from RETAINED state, never from the packet's arrival order.
  assign chunk_addr   = cpl_entry_start
                      + ADDR_W'(cpl_entry_received) * ADDR_W'(4);
 
  // RESOLVED means every expected DW has arrived. It does NOT mean the local
  // client has taken the data — that is a separate event (section 14).
  assign read_resolved = fits && (cpl_dw == rem);
 
  logic unk_q, ovr_q, ill_q;
  assign unknown_ctx_error = unk_q;
  assign overrun_error     = ovr_q;
  assign illegal_id_error  = ill_q;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      for (int i = 0; i < CTXS; i++) ctx_q[i] <= '0;
      unk_q <= 1'b0; ovr_q <= 1'b0; ill_q <= 1'b0;
    end else begin
      // FREE -> RESERVED. The entry becomes occupied immediately, so the
      // free-entry search stops offering this index from the next cycle.
      // Gated on legality: no out-of-range index ever reaches the array.
      if (reserve && reserve_id_legal) begin
        ctx_q[reserve_id].valid        <= 1'b1;
        ctx_q[reserve_id].outstanding  <= 1'b0;
        ctx_q[reserve_id].local_dest   <= reserve_dest;
        ctx_q[reserve_id].remaining_dw <= reserve_len_dw;
        ctx_q[reserve_id].start_addr   <= reserve_addr;
        ctx_q[reserve_id].received_dw  <= '0;
      end
 
      // RESERVED -> OUTSTANDING. Only now may Completions match it.
      if (launch && launch_id_legal)
        ctx_q[launch_id].outstanding <= 1'b1;
 
      // `fits` already requires cpl_id_legal, so this write is guarded.
      if (fits) begin
        ctx_q[cpl_ctx_id].received_dw  <= cpl_entry_received + cpl_dw;
        ctx_q[cpl_ctx_id].remaining_dw <= rem - cpl_dw;
        // Freed ONLY when the whole extent has arrived. Freeing on the first
        // chunk is section 8's catastrophe.
        // Freed ONLY when the whole extent has arrived, and both bits clear
        // together so the entry cannot linger as outstanding-but-invalid.
        if (cpl_dw == rem) begin
          ctx_q[cpl_ctx_id].valid       <= 1'b0;
          ctx_q[cpl_ctx_id].outstanding <= 1'b0;
        end
      end
 
      // Reported, never acted on. A chunk for an unknown, out-of-range or
      // not-yet-launched context is dropped and flagged; it must not write
      // any entry. Out-of-range is reported separately because it points at
      // an upstream mapping bug rather than at context lifetime.
      if (cpl_valid && !cpl_id_legal)                    ill_q <= 1'b1;
      if (reserve   && !reserve_id_legal)                ill_q <= 1'b1;
      if (launch    && !launch_id_legal)                 ill_q <= 1'b1;
      if (cpl_valid &&  cpl_id_legal
                    && !(cpl_entry_valid
                      && cpl_entry_outstanding))         unk_q <= 1'b1;
      if (overrun)                                       ovr_q <= 1'b1;
    end
  end
 
endmodule

// SYNTHESIZABLE. Decouple protocol resolution from local delivery.
// The separation of the two events is an ARCHITECTURAL requirement
// (section 12); the queue depth, the status abstraction and the interface
// are ILLUSTRATIVE.
module read_result_buffer #(
  parameter int DEPTH  = 4,
  parameter int DEST_W = 8,
  parameter int DATA_W = 128
) (
  input  logic clk,
  input  logic rst_n,
 
  // ---- From the completion path — CANNOT be backpressured --------------
  input  logic               res_valid,
  input  logic [DEST_W-1:0]  res_dest,
  input  logic [DATA_W-1:0]  res_data,
  input  logic [DATA_W/8-1:0] res_byte_valid,
  input  logic               res_error,       // abstracted status
 
  // ---- To the local client — MAY backpressure --------------------------
  output logic               out_valid,
  output logic [DEST_W-1:0]  out_dest,
  output logic [DATA_W-1:0]  out_data,
  output logic [DATA_W/8-1:0] out_byte_valid,
  output logic               out_error,
  input  logic               out_ready,
 
  // Reported: a result arrived with no room. NOT silently dropped.
  output logic               overflow_error
);
 
  localparam int IDX_W = (DEPTH <= 1) ? 1 : $clog2(DEPTH);
  localparam int CNT_W = $clog2(DEPTH + 1);
 
  typedef struct packed {
    logic [DEST_W-1:0]   dest;
    logic [DATA_W-1:0]   data;
    logic [DATA_W/8-1:0] bv;
    logic                err;
  } res_t;
 
  res_t             mem_q [DEPTH];
  logic [IDX_W-1:0] wr_q, rd_q;
  logic [CNT_W-1:0] cnt_q;
  logic             ovf_q;
 
  wire full = (cnt_q == CNT_W'(DEPTH));
  wire pop  = out_valid && out_ready;
 
  // EFFECTIVE capacity, not instantaneous capacity. A slot being vacated
  // this cycle is available this cycle: full + pop + push replaces one
  // element and loses nothing. Gating push on `!full` alone would drop a
  // result at exactly the moment the consumer was draining the buffer —
  // the busiest moment, and the one a bench is least likely to hit.
  wire can_accept = !full || pop;
  wire push       = res_valid && can_accept;
 
  assign out_valid      = (cnt_q != '0);
  assign out_dest       = mem_q[rd_q].dest;
  assign out_data       = mem_q[rd_q].data;
  assign out_byte_valid = mem_q[rd_q].bv;
  assign out_error      = mem_q[rd_q].err;
  assign overflow_error = ovf_q;
 
  function automatic logic [IDX_W-1:0] next_idx (input logic [IDX_W-1:0] i);
    next_idx = (i == IDX_W'(DEPTH - 1)) ? '0 : (i + IDX_W'(1));
  endfunction
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      wr_q <= '0; rd_q <= '0; cnt_q <= '0; ovf_q <= 1'b0;
    end else begin
      if (push) begin
        mem_q[wr_q].dest <= res_dest;
        mem_q[wr_q].data <= res_data;
        mem_q[wr_q].bv   <= res_byte_valid;
        mem_q[wr_q].err  <= res_error;
        wr_q <= next_idx(wr_q);
      end
      if (pop) rd_q <= next_idx(rd_q);
 
      case ({push, pop})
        2'b10:   cnt_q <= cnt_q + CNT_W'(1);
        2'b01:   cnt_q <= cnt_q - CNT_W'(1);
        default: cnt_q <= cnt_q;
      endcase
 
      // Overflow is ONLY the genuinely-no-room case: full, nothing leaving,
      // and something arriving. A result that cannot be stored is a REPORTED
      // loss — dropping it silently would mean a read that resolved at the
      // protocol level and returned nothing.
      if (res_valid && full && !pop) ovf_q <= 1'b1;
    end
  end
 
endmodule

// SVA over mem_read_req_engine, read_ctx_table and read_result_buffer.
// LOCAL contracts plus the normative non-posted lifecycle of section 3.
// SAFETY properties first; LIVENESS is section 15 and is stated separately
// with its assumptions.
 
// REQUEST — P1: no Request is ever offered without a context RESERVED for it
// (section 9a). The offer and the reservation cannot diverge.
property p_no_offer_without_reservation;
  @(posedge clk) disable iff (!rst_n)
  req_valid |-> ctx_occupied_mask[req_ctx_id];
endproperty
a_offer_reserved : assert property (p_no_offer_without_reservation);
 
// REQUEST — P2: a reservation is made only for a request the stage takes
// ownership of, and it is released only by launch or reset. Together P1, P2
// and P13a make both the identifier leak AND the mid-offer index change
// unrepresentable.
property p_reserve_only_on_accept;
  @(posedge clk) disable iff (!rst_n)
  ctx_reserve |-> (loc_valid && loc_ready);
endproperty
a_reserve_on_accept : assert property (p_reserve_only_on_accept);
 
// REQUEST — P2a: launch happens only on the outbound handshake, and promotes
// the index that was actually offered.
property p_launch_on_handshake;
  @(posedge clk) disable iff (!rst_n)
  ctx_launch |-> (req_valid && req_ready && (ctx_launch_id == req_ctx_id));
endproperty
a_launch_handshake : assert property (p_launch_on_handshake);
 
// REQUEST — P3: the request extent never exceeds MRRS (section 3, 8).
property p_within_mrrs;
  @(posedge clk) disable iff (!rst_n)
  (req_valid && mrrs_valid) |-> (req_len_dw <= LEN_W'(mrrs_dw));
endproperty
a_mrrs : assert property (p_within_mrrs);
 
// REQUEST — P4: descriptor stable while the TX path stalls.
property p_req_stable_under_stall;
  @(posedge clk) disable iff (!rst_n)
  (req_valid && !req_ready)
    |=> (req_valid && $stable({req_addr, req_len_dw, req_ctx_id}));
endproperty
a_req_stable : assert property (p_req_stable_under_stall);
 
// CONTEXT — P5: UNIQUENESS. A correlation index is never reserved while it is
// already occupied — whether reserved or outstanding. THE property that
// prevents a straggling Completion from resolving against a later read
// (section 8), now covering the reservation window too.
property p_id_not_reused_while_owned;
  @(posedge clk) disable iff (!rst_n)
  reserve |-> !ctx_occupied_mask[reserve_id];
endproperty
a_unique_id : assert property (p_id_not_reused_while_owned);
 
// CONTEXT — P6: ISOLATION. A chunk for an unknown context disturbs nothing.
// (ctx_snapshot is a testbench copy of the whole table.)
property p_unknown_ctx_harmless;
  @(posedge clk) disable iff (!rst_n)
  (cpl_valid && cpl_id_legal && !(cpl_entry_valid && cpl_entry_outstanding))
    |=> (ctx_q == $past(ctx_snapshot)) && unknown_ctx_error;
endproperty
a_unknown_isolated : assert property (p_unknown_ctx_harmless);
 
// RANGE — P6a: an out-of-range identifier changes NOTHING in the table.
// The structural property; it fails for any design that indexes before it
// checks, at any non-power-of-two CTXS.
property p_illegal_id_inert;
  @(posedge clk) disable iff (!rst_n)
  ((cpl_valid && !cpl_id_legal) || (reserve && !reserve_id_legal)
                                || (launch  && !launch_id_legal))
    |=> ((ctx_q == $past(ctx_snapshot)) && illegal_id_error);
endproperty
a_illegal_inert : assert property (p_illegal_id_inert);
 
// RANGE — P6b: an out-of-range Completion is never accepted as progress.
property p_illegal_chunk_not_accepted;
  @(posedge clk) disable iff (!rst_n)
  (cpl_valid && !cpl_id_legal) |-> (!chunk_accept && !read_resolved);
endproperty
a_illegal_chunk : assert property (p_illegal_chunk_not_accepted);
 
// RANGE — P6c: per-entry write provenance. A table entry changes only when
// THAT entry was the legal selected index. An aggregate check would let a
// write to a neighbouring entry hide.
generate for (genvar g = 0; g < CTXS; g++) begin : g_write_prov
  a_write_provenance : assert property (@(posedge clk) disable iff (!rst_n)
    !$stable(ctx_q[g])
      |-> ($past(reserve && reserve_id_legal && (reserve_id == IDX_W'(g)))
        || $past(launch  && launch_id_legal  && (launch_id  == IDX_W'(g)))
        || $past(fits    && (cpl_ctx_id == IDX_W'(g)))
        || $past(!rst_n)));
end endgenerate
 
// CONTEXT — P7: CONSERVATION. Progress never exceeds the requested extent.
property p_progress_bounded;
  @(posedge clk) disable iff (!rst_n)
  chunk_accept |=> (ctx_q[$past(cpl_ctx_id)].received_dw
                    <= $past(ctx_q[$past(cpl_ctx_id)].received_dw)
                     + $past(ctx_q[$past(cpl_ctx_id)].remaining_dw));
endproperty
a_progress : assert property (p_progress_bounded);
 
// CONTEXT — P8: THE CENTRAL LIFETIME PROPERTY. A context is freed ONLY when
// the whole extent has arrived. A partial Completion must not free it.
property p_free_only_on_full_extent;
  @(posedge clk) disable iff (!rst_n)
  (chunk_accept && !read_resolved) |=> ctx_q[$past(cpl_ctx_id)].valid;
endproperty
a_no_early_free : assert property (p_free_only_on_full_extent);
 
// CONTEXT — P9: chunk placement comes from RETAINED progress, not from
// arrival order. States the in-read ordering assumption explicitly.
property p_chunk_addr_from_progress;
  @(posedge clk) disable iff (!rst_n)
  chunk_accept |-> (chunk_addr == cpl_entry_start
                  + ADDR_W'(cpl_entry_received) * ADDR_W'(4));
endproperty
a_placement : assert property (p_chunk_addr_from_progress);
 
// CONTEXT — P10: exactly one local completion event per resolved read.
property p_one_resolution_per_read;
  @(posedge clk) disable iff (!rst_n)
  read_resolved |=> !read_resolved until_with reserve;
endproperty
 
// DELIVERY — P11: the result is stable while the local client stalls. The
// property that makes section 12's decoupling real.
property p_result_stable_under_client_stall;
  @(posedge clk) disable iff (!rst_n)
  (out_valid && !out_ready)
    |=> (out_valid && $stable({out_dest, out_data, out_byte_valid, out_error}));
endproperty
a_result_stable : assert property (p_result_stable_under_client_stall);
 
// DELIVERY — P12: a result is never silently lost. Overflow is reported ONLY
// when there was genuinely no room: full, nothing leaving, something
// arriving.
property p_no_silent_result_loss;
  @(posedge clk) disable iff (!rst_n)
  (res_valid && full && !pop) |=> overflow_error;
endproperty
a_no_loss : assert property (p_no_silent_result_loss);
 
// DELIVERY — P12a: FULL + POP + PUSH IS NOT OVERFLOW. The slot being vacated
// this cycle is usable this cycle, so the result is accepted and occupancy
// is unchanged. Catches a `push = res_valid && !full` capacity test.
property p_full_pop_push_accepted;
  @(posedge clk) disable iff (!rst_n)
  (res_valid && full && pop) |-> (push && !$rose(overflow_error));
endproperty
a_full_pop_push : assert property (p_full_pop_push_accepted);
 
// DELIVERY — P12b: simultaneous push and pop conserves occupancy at every
// level, not only at full.
property p_simul_conserves;
  @(posedge clk) disable iff (!rst_n)
  (push && pop) |=> (cnt_q == $past(cnt_q));
endproperty
a_simul_res : assert property (p_simul_conserves);
 
// RESET — P13: reset clears EVERY context, the pending stage, and the result
// buffer. Written over the whole occupancy bitmap rather than over entry
// zero, so a design that clears only the entry it happens to index cannot
// pass. Defined explicitly because "what happens to reads outstanding at
// reset" is otherwise ambiguous.
property p_reset_clears_all;
  @(posedge clk)
  !rst_n |=> (!out_valid
           && (ctx_occupied_mask == '0)
           && !pend_valid_q
           && free_avail);
endproperty
a_reset : assert property (p_reset_clears_all);
 
// RESERVATION — P13a: THE STABILITY PROPERTY THIS ARCHITECTURE EXISTS FOR.
// The offered Request descriptor — including the correlation index — does
// not move while the outbound path stalls, no matter what Completions
// resolve underneath it.
property p_offer_stable_under_tx_stall;
  @(posedge clk) disable iff (!rst_n)
  (req_valid && !req_ready)
    |=> (req_valid && $stable({req_ctx_id, req_addr, req_len_dw}));
endproperty
a_offer_stable : assert property (p_offer_stable_under_tx_stall);
 
// RESERVATION — P13b: a reserved index is never offered as free again.
property p_reserved_not_reoffered;
  @(posedge clk) disable iff (!rst_n)
  (reserve) |=> (ctx_occupied_mask[$past(reserve_id)]);
endproperty
a_reserved_held : assert property (p_reserved_not_reoffered);
 
// RESERVATION — P13c: launch promotes exactly the reserved index, and only
// an index that was reserved.
property p_launch_promotes_reserved;
  @(posedge clk) disable iff (!rst_n)
  launch |-> (ctx_occupied_mask[launch_id] && !ctx_q[launch_id].outstanding);
endproperty
a_launch_promotes : assert property (p_launch_promotes_reserved);
 
// RESERVATION — P13d: the states are consistent for EVERY entry. An entry can
// never be outstanding without being occupied, which is what makes FREE /
// RESERVED / OUTSTANDING a partition rather than three independent bits.
// Written as a generate loop because the property is per-entry.
generate for (genvar g = 0; g < CTXS; g++) begin : g_state_excl
  a_state_partition : assert property (@(posedge clk) disable iff (!rst_n)
    ctx_q[g].outstanding |-> ctx_q[g].valid);
end endgenerate
 
// RESERVATION — P13e: a Completion for a merely-RESERVED context is rejected,
// not accepted as progress. A Request that has not launched cannot have an
// answer in flight.
property p_no_completion_for_unlaunched;
  @(posedge clk) disable iff (!rst_n)
  (cpl_valid && cpl_id_legal && cpl_entry_valid && !cpl_entry_outstanding)
    |-> !chunk_accept;
endproperty
a_unlaunched_rejected : assert property (p_no_completion_for_unlaunched);
 
// SAFETY — P14: no descriptor or result output is ever unknown.
property p_outputs_never_unknown;
  @(posedge clk) disable iff (!rst_n)
  (req_valid |-> !$isunknown({req_addr, req_len_dw, req_ctx_id}))
  && (out_valid |-> !$isunknown({out_dest, out_error}));
endproperty
a_no_x : assert property (p_outputs_never_unknown);

// LIVENESS. Valid ONLY under the environment assumptions below. State them
// as `assume` so the obligation sits on the environment, where it belongs.
 
// A1: the TX path eventually accepts an offered Request.
assume property (@(posedge clk) disable iff (!rst_n)
  req_valid |-> s_eventually req_ready);
 
// A2: a launched read is eventually answered in full by the remote system.
// This assumes a functioning fabric AND a functioning Completer — neither is
// guaranteed by PCIe, which is why Completion timeout mechanisms exist.
assume property (@(posedge clk) disable iff (!rst_n)
  (req_valid && req_ready) |-> s_eventually read_resolved);
 
// A3: the local client eventually accepts a presented result.
assume property (@(posedge clk) disable iff (!rst_n)
  out_valid |-> s_eventually out_ready);
 
// L1: under A1-A3, an accepted local read eventually delivers a result.
property p_read_eventually_delivers;
  @(posedge clk) disable iff (!rst_n)
  (loc_valid && loc_ready) |-> s_eventually (out_valid && out_ready);
endproperty
a_liveness : assert property (p_read_eventually_delivers);
 
// L2: a context entry is eventually released, so the design does not
// permanently lose concurrency.
property p_context_eventually_freed;
  @(posedge clk) disable iff (!rst_n)
  alloc |-> s_eventually free_avail;
endproperty
a_ctx_liveness : assert property (p_context_eventually_freed);

expected_dw(addr) = a decorrelated deterministic function of addr