Completion Flow — The Return Path Is Its Own Pipeline

target read completes
   → response data and status become available          ← boundary 1
   → a Completion descriptor is constructed             ← boundary 2
   → the descriptor is queued for transmission          ← boundary 3
   → the packet is transmitted                          ← boundary 4

Completion arrives
   → CORRELATE: which read does this belong to?          (identity, not order)
   → ACCOUNT:   how much of the expected extent has now arrived?
   → DECIDE:    is this read finished, or is more owed?

// SYNTHESIZABLE. Turn accepted target-response events into queued Completion
// descriptors. Decoupling the resource from the outbound link: an
// ARCHITECTURAL requirement (section 3). The descriptor fields, the depth,
// and final_for_request: ILLUSTRATIVE internal metadata.
package cpl_flow_pkg;
 
  // NORMALIZED INTERNAL DESCRIPTOR — NOT a wire-format Completion.
  typedef struct packed {
    logic [15:0] requester_id;   // return route, copied from the Request
    logic [15:0] corr;           // correlation field, copied from the Request
    logic [10:0] dw;             // DW carried by this response chunk
    logic        has_data;       // status-only vs. with-data (section 2)
    logic        err;            // ABSTRACTED status. Module 13 owns the
                                 // actual Completion Status encodings.
    logic        final_for_request;  // INTERNAL teaching metadata only
  } cpl_desc_t;
 
endpackage

import cpl_flow_pkg::*;
 
module cpl_gen_queue #(
  parameter int DEPTH  = 4,
  parameter int DATA_W = 128
) (
  input  logic clk,
  input  logic rst_n,
 
  // ---- Accepted target-response event ----------------------------------
  // Context and data arrive TOGETHER, for Chapter 12.2 section 4's reason:
  // a response whose identity and payload can drift apart is a response that
  // can be delivered to the wrong Requester.
  input  logic                 rsp_valid,
  output logic                 rsp_ready,
  input  cpl_desc_t            rsp_desc,
  input  logic [DATA_W-1:0]    rsp_data,
 
  // ---- Queued descriptor out, to the return TX path --------------------
  output logic                 cpl_valid,
  input  logic                 cpl_ready,
  output cpl_desc_t            cpl_desc,
  output logic [DATA_W-1:0]    cpl_data
);
 
  generate
    if (DEPTH < 1) $error("DEPTH must be at least 1");
  endgenerate
 
  localparam int IDX_W = (DEPTH <= 1) ? 1 : $clog2(DEPTH);
  localparam int CNT_W = $clog2(DEPTH + 1);
 
  typedef struct packed {
    cpl_desc_t         desc;
    logic [DATA_W-1:0] data;
  } entry_t;
 
  entry_t           mem_q [DEPTH];
  logic [IDX_W-1:0] wr_q, rd_q;
  logic [CNT_W-1:0] cnt_q;
 
  wire full  = (cnt_q == CNT_W'(DEPTH));
  wire empty = (cnt_q == '0);
 
  assign cpl_valid = !empty;
 
  wire pop = cpl_valid && cpl_ready;
 
  // EFFECTIVE capacity — the slot a pop vacates is usable this cycle.
  // Refusing a response at full-with-pop would stall the target resource at
  // exactly the moment the queue was draining (Chapter 12.1's fixed bug,
  // and the same shape).
  assign rsp_ready = !full || pop;
 
  wire push = rsp_valid && rsp_ready;
 
  // Outputs from STORED state. There is no bypass, so a response cannot be
  // presented from a live input while an earlier one is still queued.
  assign cpl_desc = mem_q[rd_q].desc;
  assign cpl_data = mem_q[rd_q].data;
 
  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;
    end else begin
      if (push) begin
        mem_q[wr_q].desc <= rsp_desc;
        mem_q[wr_q].data <= rsp_data;
        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
    end
  end
 
endmodule

// SYNTHESIZABLE. Per-read progress accounting on the Requester side.
// That a read may require more than one Completion: NORMATIVE consequence of
// MPS bounding Completion payloads (section 2).
// The accounting scheme, the retire condition and the error outputs:
// ILLUSTRATIVE IMPLEMENTATION ACCOUNTING — this does NOT model the PCIe rules
// governing how a Completer may legally divide a response (Module 13).
module cpl_progress_tracker #(
  parameter int CTXS  = 8,
  parameter int LEN_W = 11,
  parameter int IDX_W = (CTXS <= 1) ? 1 : $clog2(CTXS)
) (
  input  logic clk,
  input  logic rst_n,
 
  // ---- A read becomes outstanding --------------------------------------
  input  logic               open_valid,
  input  logic [IDX_W-1:0]   open_id,
  input  logic [LEN_W-1:0]   open_expected_dw,
 
  // ---- A correlated Completion chunk arrives ---------------------------
  // Correlation has ALREADY happened upstream. This block accounts; it does
  // not identify (section 5).
  input  logic               chunk_valid,
  input  logic [IDX_W-1:0]   chunk_id,
  input  logic [LEN_W-1:0]   chunk_dw,
 
  // ---- Decisions -------------------------------------------------------
  output logic               chunk_credited,   // counted toward this read
  output logic               read_retire,      // extent complete THIS cycle
  output logic [LEN_W-1:0]   remaining_dw,     // for the credited read
 
  // ---- Reported conditions ---------------------------------------------
  output logic               unknown_ctx_error,
  output logic               overrun_error,
  output logic               reopen_error,
  // An identifier outside 0..CTXS-1 was presented. Distinct from
  // unknown_ctx_error, which means "in range but not active".
  output logic               illegal_id_error
);
 
  logic [LEN_W-1:0] remain_q [CTXS];
  logic [CTXS-1:0]  active_q;
 
  // ---- 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 the interface can present
  // 5, 6 or 7 — indices that do not exist. Every array access below is
  // therefore GUARDED, and the guard comes first.
  // Compared one bit wider than the identifier, so CTXS is representable
  // even when it is an exact power of two. A same-width comparison would
  // truncate CTXS to zero at CTXS = 8 and reject every legal identifier.
  localparam int CHK_W = IDX_W + 1;
  wire open_id_legal  = (CHK_W'(open_id)  < CHK_W'(CTXS));
  wire chunk_id_legal = (CHK_W'(chunk_id) < CHK_W'(CTXS));
 
  // Guarded reads. The defaults are chosen so that an illegal identifier
  // looks INACTIVE and EMPTY — it can therefore never satisfy `hit`, never
  // be credited, and never retire anything.
  logic             chunk_active;
  logic [LEN_W-1:0] chunk_remaining;
  logic             open_active;
 
  always_comb begin
    chunk_active    = 1'b0;
    chunk_remaining = '0;
    open_active     = 1'b0;
 
    if (chunk_id_legal) begin
      chunk_active    = active_q[chunk_id];
      chunk_remaining = remain_q[chunk_id];
    end
    if (open_id_legal)
      open_active = active_q[open_id];
  end
 
  // Every downstream decision now reads the GUARDED values, never the
  // arrays directly.
  wire hit = chunk_valid && chunk_id_legal && chunk_active;
 
  // Progress can never exceed what is still expected. An overrun is a
  // reported condition, NOT a saturating subtraction — silently clamping
  // would let a too-large chunk retire a read that is not complete.
  wire overrun = hit && (chunk_dw > chunk_remaining);
  wire credit  = hit && !overrun && (chunk_dw != '0);
 
  assign chunk_credited = credit;
  assign remaining_dw   = chunk_remaining;
 
  // RETIRE only when the chunk completes the expected extent. A partial
  // return NEVER retires — section 5, and the single most important line
  // in this module.
  assign read_retire    = credit && (chunk_dw == chunk_remaining);
 
  // Allocation is likewise gated on legality.
  wire do_open = open_valid && open_id_legal && !open_active;
 
  logic unk_q, ovr_q, reo_q, ill_q;
  assign unknown_ctx_error = unk_q;
  assign overrun_error     = ovr_q;
  assign reopen_error      = reo_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++) remain_q[i] <= '0;
      active_q <= '0;
      unk_q <= 1'b0; ovr_q <= 1'b0; reo_q <= 1'b0; ill_q <= 1'b0;
    end else begin
      // Both write paths are gated on legality, so no out-of-range index
      // ever reaches an array. This is STRUCTURAL prevention — the module
      // does not rely on any language behaviour for illegal indices.
      if (do_open) begin
        remain_q[open_id] <= open_expected_dw;
        active_q[open_id] <= 1'b1;
      end
 
      if (credit) begin
        remain_q[chunk_id] <= chunk_remaining - chunk_dw;
        if (chunk_dw == chunk_remaining)
          active_q[chunk_id] <= 1'b0;
      end
 
      // Reported, never acted on. None of these writes any entry.
      // Note the ordering of the two "unknown" cases: an out-of-range
      // identifier is illegal_id_error, not unknown_ctx_error, because
      // they call for different investigations (section 8a).
      if (chunk_valid && !chunk_id_legal)                  ill_q <= 1'b1;
      if (open_valid  && !open_id_legal)                   ill_q <= 1'b1;
      if (chunk_valid &&  chunk_id_legal && !chunk_active) unk_q <= 1'b1;
      if (overrun)                                         ovr_q <= 1'b1;
      if (open_valid  &&  open_id_legal  &&  open_active)  reo_q <= 1'b1;
    end
  end
 
endmodule

// SYNTHESIZABLE. Deliver credited Completion data to the correct local
// destination, decoupled from the local consumer's readiness.
// The separation of protocol resolution from local delivery: ARCHITECTURAL
// (Chapter 12.1 section 12). The interface and depth: ILLUSTRATIVE.
module cpl_result_router #(
  parameter int DEPTH  = 4,
  parameter int DEST_W = 8,
  parameter int DATA_W = 128
) (
  input  logic clk,
  input  logic rst_n,
 
  // ---- A credited chunk, with the destination from RETAINED context -----
  // dest comes from the context entry, never from the arriving packet and
  // never from arrival order (Chapter 12.1 section 11).
  input  logic                 in_valid,
  input  logic [DEST_W-1:0]    in_dest,
  input  logic [DATA_W-1:0]    in_data,
  input  logic [DATA_W/8-1:0]  in_byte_valid,
  input  logic                 in_err,
  input  logic                 in_final,      // this chunk retired the read
 
  // ---- To the local consumer -------------------------------------------
  output logic                 out_valid,
  input  logic                 out_ready,
  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_err,
  output logic                 out_final,
 
  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;
    logic                fin;
  } 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;
 
  // Same effective-capacity rule as section 7. The input here CANNOT be
  // backpressured meaningfully — the data has already arrived from the
  // fabric — so refusing it at full-with-pop would discard a chunk the
  // buffer had room for.
  wire can_accept = !full || pop;
  wire push       = in_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_err        = mem_q[rd_q].err;
  assign out_final      = mem_q[rd_q].fin;
  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 <= in_dest;
        mem_q[wr_q].data <= in_data;
        mem_q[wr_q].bv   <= in_byte_valid;
        mem_q[wr_q].err  <= in_err;
        mem_q[wr_q].fin  <= in_final;
        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
 
      // Genuinely no room: full, nothing leaving, something arriving.
      if (in_valid && full && !pop) ovf_q <= 1'b1;
    end
  end
 
endmodule

// SVA over cpl_gen_queue, cpl_progress_tracker and cpl_result_router.
// LOCAL flow contracts plus the normative consequence that a read may need
// more than one Completion. NOT claims about how a Completer may legally
// divide a response (Module 13), and NOT claims about Completion packet
// legality.
 
// GENERATOR — P1: one accepted response event produces exactly one queued
// descriptor. (gen_in_count / gen_out_count are testbench counters.)
property p_one_descriptor_per_response;
  @(posedge clk) disable iff (!rst_n)
  (cpl_valid && cpl_ready) |-> (gen_out_count + 1 <= gen_in_count);
endproperty
a_one_desc : assert property (p_one_descriptor_per_response);
 
// GENERATOR — P2: the queued descriptor and its data are stable while the
// return TX path stalls. Identity and payload do not drift apart.
property p_desc_stable;
  @(posedge clk) disable iff (!rst_n)
  (cpl_valid && !cpl_ready) |=> (cpl_valid && $stable({cpl_desc, cpl_data}));
endproperty
a_desc_stable : assert property (p_desc_stable);
 
// GENERATOR — P3: a refused response is not consumed. The producer must be
// able to re-offer it — a lost response is a read that never resolves.
property p_refused_not_consumed;
  @(posedge clk) disable iff (!rst_n)
  (rsp_valid && !rsp_ready) |-> !push;
endproperty
a_not_consumed : assert property (p_refused_not_consumed);
 
// GENERATOR — P4: full + pop accepts. The target must not stall at the
// full-rate steady state.
property p_full_pop_accepts;
  @(posedge clk) disable iff (!rst_n)
  (full && pop) |-> rsp_ready;
endproperty
a_full_pop : assert property (p_full_pop_accepts);
 
// TRACKER — P5: THE CENTRAL PROPERTY. A partial return NEVER retires a read.
property p_partial_does_not_retire;
  @(posedge clk) disable iff (!rst_n)
  (chunk_credited && (chunk_dw < remaining_dw)) |-> !read_retire;
endproperty
a_no_partial_retire : assert property (p_partial_does_not_retire);
 
// TRACKER — P6: and the converse. The chunk that completes the extent DOES
// retire it. Together P5 and P6 pin the retire condition exactly.
property p_complete_retires;
  @(posedge clk) disable iff (!rst_n)
  (chunk_credited && (chunk_dw == remaining_dw)) |-> read_retire;
endproperty
a_complete_retires : assert property (p_complete_retires);
 
// TRACKER — P7: CONSERVATION. Progress never exceeds the expected extent.
property p_progress_bounded;
  @(posedge clk) disable iff (!rst_n)
  chunk_credited |-> (chunk_dw <= remaining_dw);
endproperty
a_bounded : assert property (p_progress_bounded);
 
// TRACKER — P8: an oversized chunk is REPORTED, not clamped. A saturating
// subtraction would zero the remainder and retire a short read.
// NOTE the guarded signals: the properties read chunk_active/chunk_remaining,
// never the arrays, for the same reason the RTL does.
property p_overrun_reported_not_absorbed;
  @(posedge clk) disable iff (!rst_n)
  (chunk_valid && chunk_id_legal && chunk_active
                && (chunk_dw > chunk_remaining))
    |-> (!chunk_credited && !read_retire) ##1 overrun_error;
endproperty
a_overrun : assert property (p_overrun_reported_not_absorbed);
 
// TRACKER — P9: ISOLATION. A chunk for an in-range but inactive context
// changes nothing. (remain_snapshot / active_snapshot are testbench copies.)
property p_inactive_ctx_harmless;
  @(posedge clk) disable iff (!rst_n)
  (chunk_valid && chunk_id_legal && !chunk_active)
    |=> ((remain_q == $past(remain_snapshot))
      && (active_q == $past(active_snapshot))
      && unknown_ctx_error);
endproperty
a_isolated : assert property (p_inactive_ctx_harmless);
 
// RANGE — P9a: THE STRUCTURAL PROPERTY. An out-of-range identifier changes
// NOTHING in the table. This is the one that fails for a design which
// indexes before it checks, at any non-power-of-two CTXS.
property p_illegal_id_changes_nothing;
  @(posedge clk) disable iff (!rst_n)
  ((chunk_valid && !chunk_id_legal) || (open_valid && !open_id_legal))
    |=> ((remain_q == $past(remain_snapshot))
      && (active_q == $past(active_snapshot))
      && illegal_id_error);
endproperty
a_illegal_inert : assert property (p_illegal_id_changes_nothing);
 
// RANGE — P9b: an illegal open never allocates.
property p_illegal_open_never_allocates;
  @(posedge clk) disable iff (!rst_n)
  (open_valid && !open_id_legal) |=> (active_q == $past(active_snapshot));
endproperty
a_illegal_open : assert property (p_illegal_open_never_allocates);
 
// RANGE — P9c: an illegal chunk is never credited and never retires.
property p_illegal_chunk_never_credited;
  @(posedge clk) disable iff (!rst_n)
  (chunk_valid && !chunk_id_legal) |-> (!chunk_credited && !read_retire);
endproperty
a_illegal_chunk : assert property (p_illegal_chunk_never_credited);
 
// RANGE — P9d: the two "unknown" conditions are DISJOINT (section 8a).
// An identifier is out of range or it is in range; it is never both, and a
// design that raised both would have made the distinction useless.
property p_error_kinds_disjoint;
  @(posedge clk) disable iff (!rst_n)
  chunk_valid |-> !($rose(illegal_id_error) && $rose(unknown_ctx_error));
endproperty
a_disjoint : assert property (p_error_kinds_disjoint);
 
// RANGE — P9e: state changes only ever occur for a LEGAL selected index.
// The generate loop makes it per-entry, so a write to a neighbouring entry
// cannot hide inside an aggregate comparison.
generate for (genvar g = 0; g < CTXS; g++) begin : g_legal_write
  a_write_needs_legal : assert property (@(posedge clk) disable iff (!rst_n)
    (!$stable(active_q[g]) || !$stable(remain_q[g]))
      |-> ($past(do_open && (open_id == IDX_W'(g)))
        || $past(credit  && (chunk_id == IDX_W'(g)))
        || $past(!rst_n)));
end endgenerate
 
// TRACKER — P10: retirement happens at most once per read. read_retire is a
// single-cycle pulse and cannot repeat without a reopen.
property p_retire_once;
  @(posedge clk) disable iff (!rst_n)
  read_retire |=> !active_q[$past(chunk_id)] until_with
                  (do_open && (open_id == $past(chunk_id)));
endproperty
 
// TRACKER — P11: an active context is never silently reopened.
property p_no_silent_reopen;
  @(posedge clk) disable iff (!rst_n)
  (open_valid && open_id_legal && open_active) |=> reopen_error;
endproperty
a_reopen : assert property (p_no_silent_reopen);
 
// ROUTER — P12: the destination is carried per entry. Data credited to one
// read never emerges against another read's destination.
// (exp_dest is a testbench map keyed by a shadow chunk ID.)
property p_dest_preserved;
  @(posedge clk) disable iff (!rst_n)
  (out_valid && out_ready) |-> (out_dest == exp_dest[out_seq]);
endproperty
a_dest : assert property (p_dest_preserved);
 
// ROUTER — P13: the result is stable while the local consumer stalls.
property p_result_stable;
  @(posedge clk) disable iff (!rst_n)
  (out_valid && !out_ready)
    |=> (out_valid && $stable({out_dest, out_data, out_byte_valid,
                               out_err, out_final}));
endproperty
a_result_stable : assert property (p_result_stable);
 
// ROUTER — P14: full + pop + push is accepted, not overflow.
property p_router_full_pop_push;
  @(posedge clk) disable iff (!rst_n)
  (in_valid && full && pop) |-> (push && !$rose(overflow_error));
endproperty
a_router_full_pop : assert property (p_router_full_pop_push);
 
// ROUTER — P15: a chunk is never silently lost.
property p_no_silent_loss;
  @(posedge clk) disable iff (!rst_n)
  (in_valid && full && !pop) |=> overflow_error;
endproperty
a_no_loss : assert property (p_no_silent_loss);
 
// RESET — P16: reset clears local flow state in all three blocks. This is a
// LOCAL TEACHING-MODEL contract, not a statement about PCIe system reset.
property p_reset_clears_flow;
  @(posedge clk)
  !rst_n |=> ((cnt_q == '0) && (active_q == '0) && !out_valid && !cpl_valid);
endproperty
// And every remaining count, per entry — an aggregate check on active_q alone
// would pass a design that cleared the bitmap and left stale expectations.
generate for (genvar g = 0; g < CTXS; g++) begin : g_reset_remain
  a_reset_remain : assert property (@(posedge clk)
    !rst_n |=> (remain_q[g] == '0));
end endgenerate
a_reset : assert property (p_reset_clears_flow);

// A1: the return TX path eventually accepts a queued Completion.
assume property (@(posedge clk) disable iff (!rst_n)
  cpl_valid |-> s_eventually cpl_ready);
// A2: the local consumer eventually accepts a presented result.
assume property (@(posedge clk) disable iff (!rst_n)
  out_valid |-> s_eventually out_ready);
// A3: every outstanding read eventually receives its full extent. PCIe does
// NOT guarantee this — it is precisely why Completion timeout exists.
assume property (@(posedge clk) disable iff (!rst_n)
  open_valid |-> s_eventually read_retire);
 
// L1: under A1-A3, an opened read eventually delivers its final chunk.
property p_read_eventually_delivered;
  @(posedge clk) disable iff (!rst_n)
  open_valid |-> s_eventually (out_valid && out_ready && out_final);
endproperty
a_liveness : assert property (p_read_eventually_delivered);