Completion Logic — The Memory of a Transaction You Already Sent

a live (Requester ID, Tag) is UNIQUE among contexts
FREE + LIVE == CONTEXTS, always

mark the context terminal        -- no further payload accounting
release the context exactly once -- via the SAME path as success
publish the error to the requester -- as a result, like any other

// SYNTHESIZABLE. Completion context types.
// The identity is the PAIR (Chapter 21.4 §3). §12 Model 8: matching on
// Tag alone misattributed 39.7% of completions; the pair, 0.
package cplctx_pkg;
 
  parameter int CONTEXTS = 8;
  parameter int CTX_W    = (CONTEXTS <= 1) ? 1 : $clog2(CONTEXTS);
  parameter int RID_W    = 16;
  parameter int TAG_W    = 8;
  parameter int LEN_W    = 13;
  parameter int ADDR_W   = 64;
 
  typedef struct packed {
    logic [RID_W-1:0] requester_id;
    logic [TAG_W-1:0] tag;
  } txn_id_t;
 
  typedef enum logic [2:0] {
    C_FREE=3'd0, C_ALLOC=3'd1, C_WAIT=3'd2,
    C_ASSEMBLE=3'd3, C_TERMINAL=3'd4, C_REPORT=3'd5
  } ctx_state_e;
 
  typedef enum logic [2:0] {
    ST_NONE=3'd0, ST_OK=3'd1, ST_CPL_ERROR=3'd2,
    ST_TIMEOUT=3'd3, ST_OVERRUN=3'd4, ST_RESET=3'd5
  } outcome_e;
 
  typedef struct packed {
    ctx_state_e        st;
    txn_id_t           id;
    logic [ADDR_W-1:0] local_addr;      // where the answer belongs (20.6 §9)
    logic [LEN_W-1:0]  requested;
    logic [LEN_W-1:0]  received;
    outcome_e          outcome;
  } ctx_t;
 
  function automatic bit id_match(input txn_id_t a, input txn_id_t b);
    return (a.requester_id == b.requester_id) && (a.tag == b.tag);
  endfunction
 
  function automatic bit ctx_live(input ctx_state_e s);
    return (s != C_FREE);
  endfunction
 
endpackage

import cplctx_pkg::*;
 
// SYNTHESIZABLE. Context allocator (§4). A live identity is UNIQUE, and
// FREE + LIVE == CONTEXTS at every cycle. One next-state expression, so a
// same-cycle free and allocate cannot lose either write.
module context_allocator (
  input  logic clk,
  input  logic rst_n,
 
  input  logic       alloc_req,          // a non-posted request TRANSFERRED
  input  txn_id_t    alloc_id,
  input  logic       release_req,
  input  logic [CTX_W-1:0] release_idx,
 
  input  logic [CONTEXTS-1:0] live_map,  // from the table
  input  txn_id_t             live_id [CONTEXTS],
 
  output logic             alloc_grant,
  output logic [CTX_W-1:0] alloc_idx,
  output logic             err_duplicate_identity,   // sticky
  output logic             err_release_of_free       // sticky
);
  logic [CONTEXTS-1:0] free_q;
  logic ed_q, er_q;
  logic [CTX_W-1:0] pick;
  logic found, dup;
 
  assign err_duplicate_identity = ed_q;
  assign err_release_of_free    = er_q;
 
  always_comb begin
    pick = '0; found = 1'b0;
    for (int i = CONTEXTS-1; i >= 0; i--) if (free_q[i]) begin pick = CTX_W'(i); found = 1'b1; end
    // A live identity must be unique -- it is what makes §3's "two matches"
    // an error rather than a tie to break.
    dup = 1'b0;
    for (int i = 0; i < CONTEXTS; i++)
      if (live_map[i] && id_match(live_id[i], alloc_id)) dup = 1'b1;
  end
 
  assign alloc_grant = alloc_req && found && !dup;
  assign alloc_idx   = pick;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin free_q <= {CONTEXTS{1'b1}}; ed_q <= 1'b0; er_q <= 1'b0; end
    else begin
      if (alloc_req && dup)                     ed_q <= 1'b1;
      if (release_req && free_q[release_idx])   er_q <= 1'b1;
      // ONE next-state expression (§4).
      free_q <= (free_q | (release_req ? (CONTEXTS'(1) << release_idx) : '0))
                        & ~(alloc_grant ? (CONTEXTS'(1) << pick) : '0);
    end
  end
endmodule

import cplctx_pkg::*;
 
// SYNTHESIZABLE. THE MATCHER. Three outcomes, and it NEVER defaults (§3).
// Defaulting to entry 0 is the natural output of a for-loop whose index is
// initialised to zero -- and it routes every orphan into slot 0's owner.
module completion_matcher (
  input  logic       cpl_valid,
  input  txn_id_t    cpl_id,
  input  ctx_t       ctx [CONTEXTS],
 
  output logic [CONTEXTS-1:0] match_vec,
  output logic                hit,
  output logic                unknown_id,
  output logic                ambiguous,
  output logic [CTX_W-1:0]    sel
);
  always_comb
    for (int i = 0; i < CONTEXTS; i++)
      match_vec[i] = ctx_live(ctx[i].st) && id_match(ctx[i].id, cpl_id);
 
  assign hit        = cpl_valid &&  $onehot(match_vec);
  assign unknown_id = cpl_valid &&  (match_vec == '0);
  assign ambiguous  = cpl_valid && !$onehot0(match_vec);
 
  // `sel` is meaningful ONLY when `hit`. Every consumer gates on `hit`, so
  // the zero default can never be acted upon (P5, P6).
  always_comb begin
    sel = '0;
    if (hit) for (int i = 0; i < CONTEXTS; i++) if (match_vec[i]) sel = CTX_W'(i);
  end
endmodule

import cplctx_pkg::*;
 
// SYNTHESIZABLE. Tag/data alignment through a synchronous lookup (§6).
// §12 Model 10: the RAM's answer belongs to a DIFFERENT tag than the
// completion now presented in 87.5% of cycles. The fix is to send the
// identity and the payload metadata DOWN THE SAME PIPELINE as the read.
module context_lookup_pipe (
  input  logic clk,
  input  logic rst_n,
 
  // stage 0 -- the completion arrives, the RAM read is launched
  input  logic             s0_valid,
  input  txn_id_t          s0_id,
  input  logic [LEN_W-1:0] s0_bytes,
  input  logic             s0_err,
  input  logic [CTX_W-1:0] s0_idx,
 
  // stage 1 -- the RAM answers
  input  ctx_t             ram_dout,
 
  output logic             s1_valid,
  output txn_id_t          s1_id,          // carried, NOT re-read
  output logic [LEN_W-1:0] s1_bytes,
  output logic             s1_err,
  output logic [CTX_W-1:0] s1_idx,
  output ctx_t             s1_ctx,
  output logic             err_skew        // sticky: identity mismatch
);
  logic             v_q, e_q, skew_q;
  txn_id_t          id_q;
  logic [LEN_W-1:0] b_q;
  logic [CTX_W-1:0] i_q;
 
  assign s1_valid = v_q;   assign s1_id    = id_q;
  assign s1_bytes = b_q;   assign s1_err   = e_q;
  assign s1_idx   = i_q;   assign s1_ctx   = ram_dout;
  assign err_skew = skew_q;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin v_q<=1'b0; id_q<='0; b_q<='0; e_q<=1'b0; i_q<='0; skew_q<=1'b0; end
    else begin
      v_q<=s0_valid; id_q<=s0_id; b_q<=s0_bytes; e_q<=s0_err; i_q<=s0_idx;
      // The context that emerged must be the one fetched for THIS identity.
      if (v_q && ctx_live(ram_dout.st) && !id_match(ram_dout.id, id_q)) skew_q <= 1'b1;
    end
  end
endmodule

import cplctx_pkg::*;
 
// SYNTHESIZABLE. THE FLAGSHIP BLOCK. Coverage accumulation, terminal
// handling, and result ownership. Three measured bugs are prevented here:
// retire-on-first-fragment (80.8% of fragments orphaned), free-under-a-
// stalled-result (75.9% corrupted), and absorbing an over-return.
module context_table (
  input  logic clk,
  input  logic rst_n,
 
  // allocation
  input  logic             alloc_grant,
  input  logic [CTX_W-1:0] alloc_idx,
  input  txn_id_t          alloc_id,
  input  logic [ADDR_W-1:0] alloc_local_addr,
  input  logic [LEN_W-1:0] alloc_requested,
  input  logic             request_sent,
 
  // matched completion (post-pipeline, §6)
  input  logic             cpl_hit,
  input  logic [CTX_W-1:0] cpl_idx,
  input  logic [LEN_W-1:0] cpl_bytes,
  input  logic             cpl_error,
  input  logic             timeout_event,        // input, never invented (§8)
  input  logic [CTX_W-1:0] timeout_idx,
 
  // result handoff
  input  logic             result_ready,
 
  output ctx_t             ctx [CONTEXTS],
  output logic [CONTEXTS-1:0] live_map,
  output txn_id_t          live_id [CONTEXTS],
  output logic             result_valid,
  output txn_id_t          result_id,
  output outcome_e         result_outcome,
  output logic [LEN_W-1:0] result_bytes,
  output logic [CTX_W-1:0] result_idx,
  output logic             release_req,
  output logic             err_overrun          // sticky
);
  ctx_t c_q [CONTEXTS];
  logic e_q;
  int   rep;
 
  always_comb begin
    for (int i = 0; i < CONTEXTS; i++) begin
      ctx[i]      = c_q[i];
      live_map[i] = ctx_live(c_q[i].st);
      live_id[i]  = c_q[i].id;
    end
    // The FIRST context in REPORT owns the result output.
    rep = -1;
    for (int i = CONTEXTS-1; i >= 0; i--) if (c_q[i].st == C_REPORT) rep = i;
  end
 
  assign result_valid   = (rep >= 0);
  assign result_id      = (rep >= 0) ? c_q[rep].id       : '0;
  assign result_outcome = (rep >= 0) ? c_q[rep].outcome  : ST_NONE;
  assign result_bytes   = (rep >= 0) ? c_q[rep].received : '0;
  assign result_idx     = (rep >= 0) ? CTX_W'(rep)       : '0;
  // RELEASE follows an ACCEPTED result, never the end of the transfer (§7).
  assign release_req    = result_valid && result_ready;
  assign err_overrun    = e_q;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      for (int i = 0; i < CONTEXTS; i++) c_q[i] <= '0;
      e_q <= 1'b0;
    end else begin
      if (alloc_grant)
        c_q[alloc_idx] <= '{st:C_ALLOC, id:alloc_id, local_addr:alloc_local_addr,
                            requested:alloc_requested, received:'0, outcome:ST_NONE};
      if (request_sent)
        for (int i = 0; i < CONTEXTS; i++)
          if (c_q[i].st == C_ALLOC) c_q[i].st <= C_WAIT;
 
      if (cpl_hit) begin
        automatic logic [LEN_W:0] tot = {1'b0, c_q[cpl_idx].received} + {1'b0, cpl_bytes};
        if (cpl_error) begin
          // TERMINAL: no further payload accounting (§8).
          c_q[cpl_idx].st      <= C_TERMINAL;
          c_q[cpl_idx].outcome <= ST_CPL_ERROR;
        end else if (c_q[cpl_idx].st == C_TERMINAL) begin
          // already decided -- ignore payload, do not "un-fail" the read
        end else if (tot > {1'b0, c_q[cpl_idx].requested}) begin
          e_q <= 1'b1;                                   // REPORT the over-return
          c_q[cpl_idx].st      <= C_TERMINAL;
          c_q[cpl_idx].outcome <= ST_OVERRUN;
        end else begin
          c_q[cpl_idx].received <= tot[LEN_W-1:0];
          // COVERAGE, not packet count (§5). Retiring on the first fragment
          // orphaned 80.8% of all fragments in §12 Model 9.
          if (tot >= {1'b0, c_q[cpl_idx].requested}) begin
            c_q[cpl_idx].st      <= C_REPORT;
            c_q[cpl_idx].outcome <= ST_OK;
          end else c_q[cpl_idx].st <= C_ASSEMBLE;
        end
      end
 
      if (timeout_event && ctx_live(c_q[timeout_idx].st)
                        && (c_q[timeout_idx].st != C_REPORT)) begin
        c_q[timeout_idx].st      <= C_TERMINAL;
        c_q[timeout_idx].outcome <= ST_TIMEOUT;
      end
 
      for (int i = 0; i < CONTEXTS; i++)
        if (c_q[i].st == C_TERMINAL) c_q[i].st <= C_REPORT;   // one path (§8)
 
      // The slot is freed ONLY after the result has been accepted (§7).
      if (release_req) c_q[result_idx] <= '0;
    end
  end
endmodule

import cplctx_pkg::*;
 
// VERIFICATION-ONLY. Independent oracle: a dictionary keyed by identity,
// deliberately NOT sharing the DUT's match function, so a shared
// misconception about identity cannot make both agree.
module completion_oracle #(parameter int MAX = 64) (
  input logic clk, rst_n,
  input logic       alloc, txn_id_t alloc_id, input logic [LEN_W-1:0] alloc_bytes,
  input logic       cpl,   txn_id_t cpl_id,   input logic [LEN_W-1:0] cpl_bytes,
  input logic       retire, txn_id_t retire_id, input logic [LEN_W-1:0] retire_bytes,
 
  output logic err_unknown, err_over, err_early, err_leak,
  output int    outstanding
);
  txn_id_t          k [MAX];
  logic [LEN_W-1:0] want [MAX], got [MAX];
  logic             used [MAX];
  int               n;
 
  assign outstanding = n;
 
  function automatic int find(input txn_id_t q);
    for (int i = 0; i < MAX; i++)
      if (used[i] && (k[i].requester_id == q.requester_id) && (k[i].tag == q.tag)) return i;
    return -1;
  endfunction
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      for (int i=0;i<MAX;i++) used[i]<=1'b0;
      n<=0; err_unknown<=1'b0; err_over<=1'b0; err_early<=1'b0; err_leak<=1'b0;
    end else begin
      if (alloc) for (int i=0;i<MAX;i++) if (!used[i]) begin
        used[i]<=1'b1; k[i]<=alloc_id; want[i]<=alloc_bytes; got[i]<='0; n<=n+1; break;
      end
      if (cpl) begin
        automatic int j = find(cpl_id);
        if (j < 0) err_unknown <= 1'b1;
        else begin
          got[j] <= got[j] + cpl_bytes;
          if ((got[j] + cpl_bytes) > want[j]) err_over <= 1'b1;
        end
      end
      if (retire) begin
        automatic int j = find(retire_id);
        if (j < 0) err_unknown <= 1'b1;
        else begin
          if (got[j] < want[j]) err_early <= 1'b1;      // retired before coverage
          used[j] <= 1'b0; n <= n-1;
        end
      end
    end
  end
endmodule

// ==================================================================
// ALLOCATION AND IDENTITY (§3, §4).
// ==================================================================
 
// P1: a context is allocated only on a request TRANSFER, never an offer.
property p_alloc_on_transfer;
  @(posedge clk) disable iff (!rst_n)
    alloc_grant |-> alloc_req;
endproperty
 
// P2: a live identity is UNIQUE. This is what makes "two matches" an
// error rather than a tie (§3).
property p_live_identity_unique;
  @(posedge clk) disable iff (!rst_n)
    (live_map[0] && live_map[1]) |-> !id_match(live_id[0], live_id[1]);
endproperty
 
// P3: allocating a duplicate identity is REFUSED and reported.
property p_duplicate_identity_refused;
  @(posedge clk) disable iff (!rst_n)
    (alloc_req && dup) |-> (!alloc_grant ##1 err_duplicate_identity);
endproperty
 
// P4: FREE + LIVE == CONTEXTS, always -- a leak is one read away.
property p_context_conservation;
  @(posedge clk) disable iff (!rst_n)
    ($countones(free_q) + $countones(live_map) == CONTEXTS);
endproperty
 
// ==================================================================
// MATCHING (§3) -- three outcomes, no default.
// ==================================================================
 
// P5: exactly one outcome per arriving completion.
property p_match_outcome_total;
  @(posedge clk) disable iff (!rst_n)
    cpl_valid |-> $onehot({hit, unknown_id, ambiguous});
endproperty
 
// P6: an unmatched completion applies NOTHING -- it does not default to
// slot 0. §12 Model 8: tag-only matching misattributed 39.7%.
property p_unknown_applies_nothing;
  @(posedge clk) disable iff (!rst_n)
    unknown_id |=> $stable(ctx[0].received);
endproperty
 
// P7: a hit names a context whose identity really matches.
property p_hit_identity_matches;
  @(posedge clk) disable iff (!rst_n)
    hit |-> id_match(ctx[sel].id, cpl_id);
endproperty
 
// P8: same-cycle release and allocate -- the freed slot is allocatable.
property p_same_cycle_release_alloc;
  @(posedge clk) disable iff (!rst_n)
    (release_req && alloc_req) |=> ($countones(free_q) + $countones(live_map) == CONTEXTS);
endproperty
 
// P9: an identity is not reused while its context is still live.
property p_no_identity_reuse_while_live;
  @(posedge clk) disable iff (!rst_n)
    (alloc_grant) |-> !live_map[alloc_idx];
endproperty
 
// ==================================================================
// COVERAGE (§5) -- bytes, never packets.
// ==================================================================
 
// P10: received bytes are monotonic.
property p_received_monotonic;
  @(posedge clk) disable iff (!rst_n)
    ctx_live(ctx[0].st) |-> (ctx[0].received >= $past(ctx[0].received));
endproperty
 
// P11: a context reports only when coverage is complete or terminal.
// §12 Model 9: retiring on the first fragment orphaned 80.8% of fragments.
property p_report_requires_coverage_or_terminal;
  @(posedge clk) disable iff (!rst_n)
    ((ctx[0].st == C_REPORT) && (ctx[0].outcome == ST_OK))
      |-> (ctx[0].received >= ctx[0].requested);
endproperty
 
// P12: received never exceeds requested; an over-return is REPORTED.
property p_no_overrun_absorbed;
  @(posedge clk) disable iff (!rst_n)
    ctx_live(ctx[0].st) |-> (ctx[0].received <= ctx[0].requested);
endproperty
 
// P13: a terminal context accumulates no further payload (§8).
property p_terminal_stops_accounting;
  @(posedge clk) disable iff (!rst_n)
    (ctx[0].st == C_TERMINAL) |=> $stable(ctx[0].received);
endproperty
 
// P14: TAG/DATA ALIGNMENT. The context that emerged from the RAM was
// fetched for the identity presented at the same stage. §12 Model 10:
// 87.5% of cycles are misaligned without this pipeline.
property p_lookup_alignment;
  @(posedge clk) disable iff (!rst_n)
    (s1_valid && ctx_live(s1_ctx.st)) |-> id_match(s1_ctx.id, s1_id);
endproperty
 
// P15: skew is reported stickily rather than silently applied.
property p_skew_reported;
  @(posedge clk) disable iff (!rst_n)
    (s1_valid && ctx_live(s1_ctx.st) && !id_match(s1_ctx.id, s1_id)) |=> err_skew;
endproperty
 
// ==================================================================
// RESULT OWNERSHIP (§7).
// ==================================================================
 
// P16: the context is released only after the result is ACCEPTED.
// §12 Model 11: freeing earlier corrupted 75.9% of stalled results.
property p_release_after_result_accepted;
  @(posedge clk) disable iff (!rst_n)
    release_req |-> (result_valid && result_ready);
endproperty
 
// P17: the result record is STABLE while stalled.
property p_result_stable_under_stall;
  @(posedge clk) disable iff (!rst_n)
    (result_valid && !result_ready) |=>
      (result_valid && $stable(result_id) && $stable(result_outcome)
                    && $stable(result_bytes));
endproperty
 
// P18: every outcome reaches REPORT by the same path -- success and error
// share one release route (§8).
property p_terminal_reaches_report;
  @(posedge clk) disable iff (!rst_n)
    (ctx[0].st == C_TERMINAL) |=> (ctx[0].st == C_REPORT);
endproperty
 
// P19: the result identity is the ORIGINAL request's identity.
property p_result_identity_original;
  @(posedge clk) disable iff (!rst_n)
    result_valid |-> id_match(result_id, ctx[result_idx].id);
endproperty
 
// P20: a released slot is not reported again -- exactly one result.
property p_single_result_per_transaction;
  @(posedge clk) disable iff (!rst_n)
    release_req |=> (ctx[$past(result_idx)].st == C_FREE);
endproperty
 
// ==================================================================
// RESET, RANGE AND NON-INTERFERENCE.
// ==================================================================
 
// P21: reset invalidates every context and publishes nothing.
property p_reset_clears_contexts;
  @(posedge clk)
    (!rst_n) |=> (!result_valid && (live_map == '0));
endproperty
 
// P22: a completion after reset finds no context and is reported unknown,
// rather than matching a stale entry.
property p_no_stale_match_after_reset;
  @(posedge clk) disable iff (!rst_n)
    ($past(!rst_n) && cpl_valid) |-> unknown_id;
endproperty
 
// P23: every index is in range -- CONTEXTS = 1 included.
property p_index_in_range;
  @(posedge clk) disable iff (!rst_n)
    (sel < CTX_W'(CONTEXTS)) && (alloc_idx < CTX_W'(CONTEXTS))
      && (result_idx < CTX_W'(CONTEXTS));
endproperty
 
// P24: releasing a free context is reported, never absorbed.
property p_release_of_free_flagged;
  @(posedge clk) disable iff (!rst_n)
    (release_req && free_q[release_idx]) |=> err_release_of_free;
endproperty
 
// P25: outstanding population equals the number of live contexts.
property p_population_consistent;
  @(posedge clk) disable iff (!rst_n)
    ($countones(live_map) == outstanding);
endproperty
 
// P26: a completion with zero payload bytes does not advance coverage.
property p_zero_byte_no_coverage;
  @(posedge clk) disable iff (!rst_n)
    (cpl_hit && (cpl_bytes == '0) && !cpl_error) |=> $stable(ctx[cpl_idx].received);
endproperty
 
// P27: the timeout input is treated as one terminal reason among others --
// no duration is computed here (§8).
property p_timeout_is_terminal_only;
  @(posedge clk) disable iff (!rst_n)
    (timeout_event && ctx_live(ctx[timeout_idx].st)
      && (ctx[timeout_idx].st != C_REPORT)) |=> (ctx[timeout_idx].st == C_TERMINAL);
endproperty
 
// P28: the oracle never drives the engine.
property p_oracle_non_functional;
  @(posedge clk) disable iff (!rst_n)
    $stable({cpl_hit, alloc_grant}) or !$stable(outstanding);
endproperty