Non-Posted Transactions — Ownership That Ends on the Return Path

Chapter 10.3 took the zero in "a single Request and zero or more Completions." This chapter takes the one or more, and the difference between them is not vocabulary.

What makes a Request non-posted, what state must the Requester retain while it is outstanding, and how does Completion-based resolution change RTL architecture and verification?

1. Which Requests Are Non-Posted

The per-space table is the one to memorise, and the Memory row is the odd one out.

Five of the six operations require a Completion. Only the Memory Write does not. So the accurate summary is not "reads are non-posted, writes are posted" — it is:

Every Read is non-posted. Every Write is non-posted except a Memory Write.

Why the exception exists where it does. Memory writes are the bulk-traffic case: a DMA engine streaming into host memory, a host filling a device's buffer. Requiring a Completion for each one would double the transaction count and force the Requester to hold state proportional to the traffic. I/O and Configuration writes are neither bulk nor frequent — a configuration write during enumeration is one of a handful — and both are cases where the software issuing them genuinely needs to know the write landed before it proceeds.

Which means the classification is a deliberate engineering trade, not an accident of history. Bulk traffic gets throughput; control traffic gets confirmation.

2. The Lifetime

A posted Request has one interesting moment: the handoff. A non-posted Request has six.

1. a local operation exists and asks to be issued
2. correlation state is allocated                ← ownership begins
3. the Request is launched onto the outbound path
4. the operation is OUTSTANDING — state retained, Requester free to do other work
5. a Completion returns and is matched against the retained state
6. the result is delivered locally and the state is freed   ← ownership ends

Stages 2 and 6 are the boundaries this chapter is about. Everything between them is a resource held, and the resource is finite.

Put this figure beside Chapter 10.3 §2's and the whole chapter is visible in one comparison. The posted figure ends at the third message. This one has three more, and every one of them is a reason for state to exist.

3. Launched Is Not Completed

4. Outstanding Depth Is a Hardware Resource

A Requester may have several non-posted operations in flight at once. Each one holds things.

So "how many operations may be outstanding" is a design parameter with area attached, and it is not free to increase. §13 explains why it is also the parameter that sets the throughput ceiling.

What this chapter does not state is any specific number. How many Tags a Function may use, and the rules governing them, are Module 11's; how many outstanding operations a given implementation supports is that implementation's choice.

5. Correlation ID Reuse — the Central Hazard

This is the bug that this chapter exists to prevent, and it has a clean statement.

A correlation identifier must not be reused while an earlier Request carrying it is still outstanding.

What happens if it is. Operation A is launched with ID 5 and is slow. The Requester decides A is finished — or simply runs out of IDs and recycles — and launches operation B with ID 5. A's Completion then arrives and resolves B's entry. A's data is delivered to B's consumer, B's operation is marked resolved having never been answered, and B's real Completion arrives later as an orphan.

One reuse, three corrupted operations, and none of them reports an error.

6. Microarchitecture — A Lifetime Controller

Chapter 10.2 §10 built the table that remembers. This chapter builds the thing that decides when to allocate, when to launch, and when to release — and those three decisions are where the hazards live.

Three responsibilities, deliberately in three blocks:

Identifier allocation owns the pool of correlation IDs: which are in use, which may be handed out, and the guarantee that one in use is never handed out again. §8.

The lifetime controller owns the request path, the completion path, and the coupling between them: allocate exactly when launching, retain while outstanding, resolve on a matching Completion, deliver the result, free exactly once. §9.

Supervision owns the question "has this operation been outstanding too long," which is a different question from "has it resolved" and must not be allowed to answer it. §11.

7. RTL — The Correlation Identifier Pool

// SYNTHESIZABLE. A pool of internal correlation identifiers, implemented as
// an explicit FREE LIST with a busy bitmap for legality checking.
// The requirement (never confuse two outstanding operations) is NORMATIVE.
// The structure, the width, and the allocation order are ILLUSTRATIVE.
module corr_id_alloc #(
  parameter int IDS  = 8,
  // Derived. Never zero-width, including at IDS == 1.
  parameter int ID_W = (IDS <= 1) ? 1 : $clog2(IDS)
) (
  input  logic              clk,
  input  logic              rst_n,
 
  // ---- Allocate --------------------------------------------------------
  input  logic              alloc_req,
  output logic              alloc_gnt,
  output logic [ID_W-1:0]   alloc_id,
  output logic              pool_full,     // nothing available
 
  // ---- Free ------------------------------------------------------------
  input  logic              free_valid,
  input  logic [ID_W-1:0]   free_id,
  // Freeing an identifier that is not busy. Reported and IGNORED — see below.
  output logic              free_error,
 
  // ---- Visibility, for composition and for checking --------------------
  output logic [IDS-1:0]    busy_mask,
  output logic [ID_W:0]     busy_count
);
 
  generate
    if (IDS < 1) $error("IDS must be at least 1");
  endgenerate
 
  // The free list: identifiers currently available, in a small circular
  // buffer. Popping is O(1) regardless of pool size, unlike the priority
  // scan Chapter 10.2's table uses — a deliberately different structure for
  // a deliberately different job, and the trade-off is discussed below.
  logic [ID_W-1:0] flist_q [IDS];
  logic [ID_W-1:0] head_q, tail_q;
  logic [ID_W:0]   avail_q;      // 0..IDS, so ID_W+1 bits
 
  // The busy bitmap is NOT redundant with the free list. It is what makes a
  // double free detectable: without it, freeing the same identifier twice
  // pushes it onto the list twice, and the pool later hands one identifier
  // to two live operations — the exact catastrophe of section 5, produced by
  // the allocator itself.
  logic [IDS-1:0]  busy_q;
 
  localparam logic [ID_W:0] IDS_C = IDS[ID_W:0];
 
  assign busy_mask  = busy_q;
  assign busy_count = IDS_C - avail_q;
  assign pool_full  = (avail_q == '0);
 
  assign alloc_gnt  = alloc_req && !pool_full;
  assign alloc_id   = flist_q[head_q];
 
  // A free of an identifier that is not busy changes nothing. Silently
  // accepting it would corrupt the free list; silently dropping it would
  // hide a real bug. Reporting and ignoring does neither.
  wire do_free  = free_valid && busy_q[free_id];
  assign free_error = free_valid && !busy_q[free_id];
  wire do_alloc = alloc_gnt;
 
  function automatic logic [ID_W-1:0] nxt(input logic [ID_W-1:0] p);
    return (p == ID_W'(IDS-1)) ? '0 : (p + 1'b1);
  endfunction
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      // Every identifier starts available. Cheap for the small pools this
      // structure suits; a large pool would initialise lazily instead.
      for (int i = 0; i < IDS; i++) flist_q[i] <= ID_W'(i);
      head_q  <= '0;
      tail_q  <= '0;
      avail_q <= IDS_C;
      busy_q  <= '0;
    end else begin
      if (do_alloc) begin
        busy_q[alloc_id] <= 1'b1;
        head_q           <= nxt(head_q);
      end
      if (do_free) begin
        busy_q[free_id]  <= 1'b0;
        flist_q[tail_q]  <= free_id;
        tail_q           <= nxt(tail_q);
      end
 
      case ({do_alloc, do_free})
        2'b10:   avail_q <= avail_q - 1'b1;
        2'b01:   avail_q <= avail_q + 1'b1;
        default: avail_q <= avail_q;
      endcase
    end
  end
 
endmodule

Classification: synthesizable.

Semantics — every dimension:

What it teaches — three things:

1. The busy bitmap is a safety mechanism, not bookkeeping. It is the only thing standing between a double free and a free list containing the same identifier twice — which converts a software or logic bug into silent cross-talk between two live operations.
2. busy_count is derived, not counted separately. IDS − avail_q cannot disagree with the pool's actual state, whereas a second independently-maintained counter can. §12's P8 checks it against the bitmap anyway, because "cannot disagree" deserves an assertion.
3. Allocation order is not part of the contract. After recycling, identifiers come back in the order they were freed. Any design or test that depends on getting identifier 0 first is depending on something this module does not promise.

Deliberately simplified: one allocate and one free port per cycle; a flat array sized for a small pool; no reservation or rollback path (§6's second contract would add one); no aging.

Production implication: a design with a large identifier space uses RAM for the list and a wider free/alloc interface; must respect the rules governing the standardised Tag it maps onto (Module 11); and typically supports flushing the pool as part of a broader reset or error-recovery flow whose semantics later chapters own.

8. RTL — The Request Lifetime Controller

// SYNTHESIZABLE. Owns a non-posted operation from admission to resolution.
// "Not complete until the Completion returns" is NORMATIVE; the interface,
// the depth-one result stage, and the descriptor are ILLUSTRATIVE. No packet
// field is constructed or decoded here — Module 11 owns that.
module nonposted_engine #(
  parameter int IDS    = 8,
  parameter int ID_W   = (IDS <= 1) ? 1 : $clog2(IDS),
  parameter int ADDR_W = 64,
  parameter int TOK_W  = 12          // the producer's own handle
) (
  input  logic               clk,
  input  logic               rst_n,
 
  // ---- Local operation in ----------------------------------------------
  input  logic               req_valid,
  output logic               req_ready,
  input  logic [ADDR_W-1:0]  req_addr,
  input  logic [TOK_W-1:0]   req_token,
 
  // ---- Outbound Request ------------------------------------------------
  output logic               tx_valid,
  input  logic               tx_ready,
  output logic [ADDR_W-1:0]  tx_addr,
  output logic [ID_W-1:0]    tx_corr_id,
  output logic               tx_needs_completion,   // constant 1
 
  // ---- Identifier pool (section 7) -------------------------------------
  output logic               alloc_req,
  input  logic               alloc_gnt,
  input  logic [ID_W-1:0]    alloc_id,
  input  logic               pool_full,
  input  logic [IDS-1:0]     busy_mask,
  output logic               free_valid,
  output logic [ID_W-1:0]    free_id,
 
  // ---- Decoded Completion metadata in ----------------------------------
  input  logic               cpl_valid,
  output logic               cpl_ready,
  input  logic [ID_W-1:0]    cpl_id,
  input  logic               cpl_last,     // terminates the Sequence
  input  logic               cpl_error,    // ABSTRACT status — Chapter 13.2 owns the real one
  input  logic [31:0]        cpl_data,
 
  // ---- Local result out -------------------------------------------------
  output logic               res_valid,
  input  logic               res_ready,
  output logic [TOK_W-1:0]   res_token,
  output logic               res_error,
  output logic [31:0]        res_data,
 
  // ---- Diagnostics ------------------------------------------------------
  output logic               orphan_cpl,
  output logic               launch                 // observable, for checking
);
 
  // Retained context. Written at launch, read at resolution, never between.
  logic [TOK_W-1:0] token_q [IDS];
 
  // ---- Launch ----------------------------------------------------------
  // tx_valid asserts because an operation exists AND an identifier exists.
  // It never consults tx_ready.
  assign tx_valid           = req_valid && !pool_full;
  assign tx_addr            = req_addr;
  assign tx_corr_id         = alloc_id;
  assign tx_needs_completion = 1'b1;
 
  // req_ready depends on STATE (pool_full) and downstream ready only — never
  // on req_valid. A producer is admitted because a slot and a path exist.
  assign req_ready = !pool_full && tx_ready;
 
  // ALLOCATION COMMITS EXACTLY AT LAUNCH (section 6). alloc_req is driven by
  // the launch handshake itself, so an allocation without a launch has no
  // signal path and a reserved-but-unlaunched identifier is unrepresentable.
  assign launch    = req_valid && req_ready;   // == tx_valid && tx_ready
  assign alloc_req = launch;
 
  // ---- Result stage: one operation's answer, held under back-pressure ----
  logic             res_valid_q;
  logic [TOK_W-1:0] res_token_q;
  logic             res_err_q;
  logic [31:0]      res_data_q;
 
  // cpl_ready depends on STATE and the local consumer only — never on
  // cpl_valid, so an orphan is consumed rather than deadlocking the return
  // path, and a Completion is never dropped because the core is stalled.
  assign cpl_ready = !res_valid_q || res_ready;
 
  wire cpl_xfer = cpl_valid && cpl_ready;
  // busy_mask is the pool's registered state, so this asks "is this
  // identifier outstanding right now" — the only safe question to ask of a
  // returning Completion.
  wire cpl_hit  = cpl_xfer &&  busy_mask[cpl_id];
  assign orphan_cpl = cpl_xfer && !busy_mask[cpl_id];
 
  // FREE ON END OF SEQUENCE ONLY, and never on the launch path. A Completion
  // may "partially terminate" a Sequence (Chapter 10.2 section 7).
  assign free_valid = cpl_hit && cpl_last;
  assign free_id    = cpl_id;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      res_valid_q <= 1'b0;
      res_token_q <= '0;
      res_err_q   <= 1'b0;
      res_data_q  <= 32'h0;
      for (int i = 0; i < IDS; i++) token_q[i] <= '0;
    end else begin
      // Context is captured at launch. Nothing on the completion path may
      // write it, which is what makes it trustworthy for the whole lifetime.
      if (launch) token_q[alloc_id] <= req_token;
 
      // Drain first, then refill, so a taken result and a newly matched
      // Completion may share a cycle.
      if (res_valid_q && res_ready) res_valid_q <= 1'b0;
 
      if (cpl_hit) begin
        res_valid_q <= 1'b1;
        res_token_q <= token_q[cpl_id];   // from RETAINED state, not from the Completion
        res_err_q   <= cpl_error;
        res_data_q  <= cpl_data;
      end
    end
  end
 
  assign res_valid = res_valid_q;
  assign res_token = res_token_q;
  assign res_error = res_err_q;
  assign res_data  = res_data_q;
 
endmodule

Classification: synthesizable.

Semantics — every dimension:

Trace one operation, cycle by cycle.

Cycle 0. The producer asserts req_valid with an address and its own token. The pool has identifiers, so pool_full is low and tx_valid is high with tx_corr_id = alloc_id. Suppose tx_ready is low: req_ready is low, nothing happens, and everything holds.

Cycle 1. tx_ready rises. req_ready rises, launch asserts, and three things happen together: the Request is taken by the outbound path, alloc_req commits the identifier in the pool, and token_q[alloc_id] captures the producer's handle. The operation is now outstanding.

Cycles 2..N. busy_mask[id] is set. The producer may issue more operations; the engine may launch them with different identifiers. Nothing about this operation changes.

Cycle N+1. A Completion arrives with cpl_id = id and cpl_last high. cpl_ready is high because the result stage is empty, so cpl_hit asserts. The result stage loads the retained token, the error flag and the data; free_valid releases the identifier in the pool.

Cycle N+2. res_valid is high with the producer's original token. When the consumer takes it, the stage empties. The identifier became available again at N+2 — one cycle after the free — because the pool's state is registered.

What it teaches — five things:

1. Nothing frees on the launch path. Search the module for free_valid and it appears once, gated on a matched terminating Completion. §3's failure is not merely avoided; it has no signal path.
2. Allocation and launch are the same event. One assign makes the two inseparable, so §6's leak cannot occur.
3. The result's destination comes from retained state. res_token_q is loaded from token_q, not from anything the Completion carried — Chapter 10.2 §9's rule, now inside the controller that owns the lifetime.
4. Back-pressure runs backwards along the whole chain. A stalled consumer holds the result stage, which deasserts cpl_ready, which — in a real design — stops Completion credits being returned and eventually throttles the Completer. A slow local consumer becomes a system-wide limit, and this is the mechanism.
5. An orphan is consumed, reported, and inert. It does not free, does not deliver, and does not stall. Any other choice turns a diagnosable anomaly into either corruption or a hang.

Deliberately simplified: one result in flight at a time; one 32-bit data beat per Completion; no accumulation across a multi-Completion Sequence beyond the free-on-last contract; a single outbound Request type; no flow-control accounting; and no ordering awareness.

Production implication: a real engine buffers several results, accumulates the fragments of a split response (Chapter 13.3), interprets the real Completion Status (Chapter 13.2), obeys the ordering rules (Chapter 13.4), checks flow-control credit before launching (Module 16), and implements the Completion Timeout mechanism (Chapter 25.7).

9. RTL — Supervision, and Why It Is Not Resolution

// SYNTHESIZABLE. Per-identifier elapsed-time supervision.
// GENERIC IMPLEMENTATION WATCHDOG — not the PCIe Completion Timeout
// mechanism, and LIMIT has no PCIe meaning whatsoever.
module outstanding_watchdog #(
  parameter int IDS   = 8,
  parameter int LIMIT = 1024,
  parameter int ID_W  = (IDS   <= 1) ? 1 : $clog2(IDS),
  parameter int CNT_W = (LIMIT <= 1) ? 1 : $clog2(LIMIT + 1)
) (
  input  logic             clk,
  input  logic             rst_n,
 
  input  logic [IDS-1:0]   busy_mask,    // from the pool
  input  logic             start_valid,  // an identifier has just been allocated
  input  logic [ID_W-1:0]  start_id,
 
  // An identifier that is still outstanding after LIMIT cycles. An
  // OBSERVATION, not a resolution — see below.
  output logic [IDS-1:0]   expired_mask
);
 
  generate
    if (LIMIT < 1) $error("LIMIT must be at least 1");
  endgenerate
 
  logic [CNT_W-1:0] cnt_q [IDS];
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      for (int i = 0; i < IDS; i++) cnt_q[i] <= '0;
    end else begin
      for (int i = 0; i < IDS; i++) begin
        if (start_valid && (start_id == ID_W'(i)))
          cnt_q[i] <= CNT_W'(LIMIT);
        else if (busy_mask[i] && (cnt_q[i] != '0))
          cnt_q[i] <= cnt_q[i] - 1'b1;
      end
    end
  end
 
  // Expiry is a pure function of "still outstanding" and "counter drained".
  // Note what it does NOT do: it does not free the identifier, it does not
  // deliver a result, and it does not touch the engine's state.
  always_comb begin
    for (int i = 0; i < IDS; i++)
      expired_mask[i] = busy_mask[i] && (cnt_q[i] == '0);
  end
 
endmodule

Classification: synthesizable.

Cost, stated honestly. This is IDS × CNT_W flip-flops — for eight identifiers and a 1024-cycle limit, eighty-eight. Acceptable for a small pool and clearly not for a large one. Production alternatives include a single free-running timestamp with a per-entry capture and a comparison against an aging window, or a coarse epoch scheme that sweeps entries periodically and accepts a wider timing tolerance. Both trade precision for area, and both are the right answer above some pool size.

10. Assertions

// SVA over corr_id_alloc, nonposted_engine and outstanding_watchdog composed
// into one instance. Implementation invariants for THESE designs plus the
// normative requirements they serve — not claims about any PCIe field.
 
// ENVIRONMENT ASSUMPTIONS. The producer and the Completion source both owe
// valid- and payload-stability. The liveness property additionally needs
// downstream and consumer fairness; none of this is provable from inside.
assume property (@(posedge clk) disable iff (!rst_n)
  (req_valid && !req_ready) |=> (req_valid && $stable(req_addr)
                                 && $stable(req_token)));
assume property (@(posedge clk) disable iff (!rst_n)
  (cpl_valid && !cpl_ready) |=> (cpl_valid && $stable(cpl_id)
                                 && $stable(cpl_last) && $stable(cpl_data)));
// FAIRNESS, required for P13 only.
assume property (@(posedge clk) disable iff (!rst_n) s_eventually (tx_ready));
assume property (@(posedge clk) disable iff (!rst_n) s_eventually (res_ready));
 
// OWNERSHIP — P1: a Request is never launched without an identifier
// committed for it. The allocate-at-launch contract of section 6.
property p_no_launch_without_id;
  @(posedge clk) disable iff (!rst_n)
  launch |-> alloc_gnt;
endproperty
a_launch_has_id : assert property (p_no_launch_without_id);
 
// OWNERSHIP — P2: and no identifier is committed without a launch, so
// nothing can be reserved and leaked.
property p_no_alloc_without_launch;
  @(posedge clk) disable iff (!rst_n)
  alloc_gnt |-> launch;
endproperty
a_no_orphan_alloc : assert property (p_no_alloc_without_launch);
 
// OWNERSHIP — P3: THE CENTRAL PROPERTY. Nothing is freed because a Request
// was transmitted. Freeing happens only on a matched terminating Completion.
property p_never_free_on_launch;
  @(posedge clk) disable iff (!rst_n)
  free_valid |-> (cpl_hit && cpl_last);
endproperty
a_free_needs_completion : assert property (p_never_free_on_launch);
 
// UNIQUENESS — P4: an identifier freed this cycle is not allocated this
// cycle. Structural in section 7, asserted so that an optimisation which
// bypasses a free straight to a waiting allocation fails loudly.
property p_no_same_cycle_reuse;
  @(posedge clk) disable iff (!rst_n)
  (do_alloc && do_free) |-> (alloc_id != free_id);
endproperty
a_no_immediate_reuse : assert property (p_no_same_cycle_reuse);
 
// UNIQUENESS — P5: an identifier handed out is not already busy. Section 5's
// hazard, made unrepresentable.
property p_alloc_not_already_busy;
  @(posedge clk) disable iff (!rst_n)
  alloc_gnt |-> !busy_mask[alloc_id];
endproperty
a_no_double_alloc : assert property (p_alloc_not_already_busy);
 
// UNIQUENESS — P6: an identifier stays busy for the whole time between its
// allocation and its free. Written per identifier, because the claim is
// about each one rather than about whichever is being handled.
generate for (genvar k = 0; k < IDS; k++) begin : g_busy_span
  property p_busy_until_freed;
    @(posedge clk) disable iff (!rst_n)
    (busy_mask[k] && !(do_free && (free_id == k[ID_W-1:0]))) |=> busy_mask[k];
  endproperty
  a_busy_held : assert property (p_busy_until_freed);
end endgenerate
 
// LEGALITY — P7: freeing an identifier that is not busy changes nothing.
// Double-free protection, and the guard on the free list's integrity.
property p_double_free_inert;
  @(posedge clk) disable iff (!rst_n)
  free_error |-> (!do_free && $stable(avail_q));
endproperty
a_no_double_free : assert property (p_double_free_inert);
 
// CONSERVATION — P8: busy_count agrees with the bitmap. "Allocated minus
// freed equals outstanding", checkable without a shadow model.
property p_count_matches_bitmap;
  @(posedge clk) disable iff (!rst_n)
  busy_count == $countones(busy_mask);
endproperty
a_count_exact : assert property (p_count_matches_bitmap);
 
// CONSERVATION — P9: an exhausted pool blocks launching. The back-pressure
// that stops a Requester issuing an operation it could not track.
property p_full_blocks_launch;
  @(posedge clk) disable iff (!rst_n)
  pool_full |-> (!launch && !req_ready);
endproperty
a_full_blocks : assert property (p_full_blocks_launch);
 
// CORRECTNESS — P10: a delivered result carries the token retained at
// launch for that identifier — never anything the Completion supplied.
property p_result_uses_retained_token;
  @(posedge clk) disable iff (!rst_n)
  cpl_hit |=> (res_token == $past(token_q[cpl_id]));
endproperty
a_token_from_state : assert property (p_result_uses_retained_token);
 
// LEGALITY — P11: a Completion whose identifier is not outstanding resolves
// nothing, frees nothing and delivers nothing.
property p_orphan_inert;
  @(posedge clk) disable iff (!rst_n)
  orphan_cpl |-> (!free_valid && !cpl_hit);
endproperty
a_orphan_inert : assert property (p_orphan_inert);
 
// STABILITY — P12: a held result is stable until its consumer takes it, and
// an outbound Request is stable while the path is stalled.
property p_result_stable_under_stall;
  @(posedge clk) disable iff (!rst_n)
  (res_valid && !res_ready) |=> (res_valid && $stable(res_token)
                                 && $stable(res_error) && $stable(res_data));
endproperty
a_result_held : assert property (p_result_stable_under_stall);
 
property p_request_stable_under_stall;
  @(posedge clk) disable iff (!rst_n)
  (tx_valid && !tx_ready) |=> (tx_valid && $stable(tx_addr)
                               && $stable(tx_corr_id));
endproperty
a_request_held : assert property (p_request_stable_under_stall);
 
// LIVENESS — P13: an admitted operation is eventually launched. DEPENDS ON
// the fairness assumptions above and on identifiers being returned; without
// them an operation legitimately waits forever and this is unprovable.
property p_admitted_eventually_launched;
  @(posedge clk) disable iff (!rst_n)
  (req_valid && !pool_full) |-> s_eventually (launch);
endproperty
a_eventually_launched : assert property (p_admitted_eventually_launched);
 
// SUPERVISION — P14: expiry observes and does nothing else. The watchdog
// must not free an identifier or resolve an operation (section 9).
property p_watchdog_does_not_free;
  @(posedge clk) disable iff (!rst_n)
  (|expired_mask) && !cpl_hit |-> !free_valid;
endproperty
a_watchdog_inert : assert property (p_watchdog_does_not_free);
 
// SUPERVISION — P15: only an outstanding identifier can expire.
property p_expiry_implies_busy;
  @(posedge clk) disable iff (!rst_n)
  (expired_mask & ~busy_mask) == '0;
endproperty
a_expiry_scoped : assert property (p_expiry_implies_busy);
 
// RESET — P16: reset clears local ownership. LOCAL BLOCK behaviour only.
property p_reset_clears;
  @(posedge clk) !rst_n |=> ((busy_count == '0) && !res_valid && !tx_valid);
endproperty
a_reset_clears : assert property (p_reset_clears);
 
// SAFETY — P17: no interface output is ever unknown.
property p_outputs_never_unknown;
  @(posedge clk) disable iff (!rst_n)
  !$isunknown({req_ready, tx_valid, cpl_ready, res_valid, free_valid,
               alloc_req, orphan_cpl, pool_full, free_error});
endproperty
a_no_x : assert property (p_outputs_never_unknown);

P3 is the chapter's thesis and the property most worth writing first. "Nothing is freed merely because a Request was transmitted" is exactly §3's rule, and a design that violated it would pass most of the rest of this list — allocation would be correct, uniqueness would hold, conservation would balance — while delivering no results at all. P3 fails on the first launch.

P1 and P2 are a pair and neither is sufficient alone. P1 stops a Request going out untracked. P2 stops an identifier being consumed by something that did not go out. Together they make allocation and launch the same event, which is §6's contract; separately, either allows a leak in one direction.

P6 is the property that catches the subtle version of §5's hazard. P5 says an identifier is not handed out while busy — true of any allocator that reads its own bitmap correctly. P6 says busy stays set until an explicit free, which catches a design where something else clears the bit: an error path, a flush, a watchdog wired to the pool. That last one is the realistic failure, and P14 exists to catch it from the other side.

P13 carries its assumptions in plain sight, and one of them is not about fairness. Eventual launch needs tx_ready to assert and the pool to be non-empty — which depends on Completions returning and freeing identifiers. So the liveness of the request path depends on the health of the return path, which is the formal statement of §12's second debugging scenario. Writing the property honestly makes that dependency visible instead of leaving it as folklore.

11. Verification

Monitors observe: the request handshake with its address and token; launch, alloc_req, alloc_gnt and alloc_id; busy_mask and busy_count; free_valid and free_error; the Completion interface; the result handshake; orphan_cpl; and expired_mask.

Lifetime basics

• One operation, launched and completed. Verify the identifier is allocated at launch and not before, busy_mask sets, the result carries the original token, and the identifier is released exactly once.
• Several operations outstanding at once. Verify each gets a distinct identifier, each result carries its own token, and busy_count tracks the number in flight.
• Completions in launch order. Verify each resolves its own operation.
• Completions in the reverse order. The test a position-based design fails (Chapter 10.2 §4). Verify correlation is unaffected.
• A non-terminating Completion followed by a terminating one. Verify the result is delivered for each, the identifier is held through the first, and released only on the second (P3).
• Two operations carrying the same producer token but different identifiers. Verify results are not confused — this catches a design that keyed anything on the token instead of on the identifier.

Pool pressure

• Launch until the pool is exhausted. Verify pool_full, req_ready low, tx_valid low, and that no Request is emitted (P9).
• Exhaust, then complete one operation. Verify the identifier becomes available and a waiting Request launches — on the cycle after the free, not the same cycle (P4).
• Sustained launch and completion at the pool's capacity. Verify no identifier is ever allocated while busy (P5) and the count never exceeds IDS.
• Identifier recycling under pressure. Run long enough that every identifier is reused many times. Verify no result is ever delivered with a token from a previous use of that identifier — the direct test for §5's hazard.

Negative tests

• A Completion with an identifier that is not outstanding. Verify orphan_cpl pulses, nothing is freed, nothing is delivered, and the return path does not stall (P11).
• A duplicate terminating Completion. Complete an operation, then present the same identifier again. Verify the second is an orphan. Run it twice: once with the identifier still free, and once after it has been reallocated to a new operation — only the second version can corrupt anything, and it is the one that matters.
• A stale Completion after a full recycle. Launch, complete, and cycle the identifier through several more operations, then inject a Completion carrying the original operation's data. Verify it resolves whatever is currently outstanding — and that the scoreboard flags the resulting token mismatch. This test demonstrates the hazard rather than proving its absence, which is the honest thing a test can do here: the protection is the reuse rule, not the hardware.
• A double free. Drive free_valid twice for one identifier. Verify free_error pulses, the available count does not rise twice (P7), and the free list is not corrupted — check by continuing to allocate and confirming no identifier is ever handed out twice.
• A free of a never-allocated identifier. Verify the same.
• Result consumer stalled indefinitely. Verify the result is held stable (P12), cpl_ready deasserts, Completions stop being accepted, identifiers stop being freed, the pool exhausts, and launching stops. Verify the whole chain, because that chain is §12's second scenario and this is where it is proven to exist.
• Reset with operations outstanding. Verify local state clears (P16), and that a Completion arriving afterwards for a pre-reset identifier is an orphan rather than resolving a new operation.
• Watchdog expiry. With LIMIT small, launch an operation and never complete it. Verify expired_mask sets, and — critically — verify nothing else happens: no free, no result, no reissue (P14, P15).

Parameter corners

• IDS = 1. Verify ID_W is 1, no zero-width vector, and that a second operation cannot launch until the first completes.
• IDS = 3 — non-power-of-two. Verify the free-list wrap is correct and no identifier outside 0..IDS-1 is ever produced.
• LIMIT = 1 on the watchdog. Verify CNT_W is at least 1 and expiry occurs on the expected cycle.
• IDS large enough that busy_count needs its extra bit. Verify the count reaches IDS without wrapping.

Coverage should include: every identifier allocated at least once and recycled at least once; the pool at empty, one-below-full and full; Completions in launch order, reverse order, and interleaved; cpl_last set and clear on matched Completions; simultaneous allocate and free; the result consumer continuously ready, continuously stalled and randomly toggled; and every diagnostic output asserted at least once.

12. Debugging

Symptom: the Requester stops issuing even though the Link is idle

An idle Link with a stalled Requester means the Requester is blocked on something internal. For a non-posted engine there are only a few candidates, and they form a chain.

1. Is the pool exhausted? pool_full high with busy_count at IDS. If so, the Requester is not broken — it is out of identifiers, and the question becomes why they are not coming back.
2. Are Completions arriving? Watch cpl_valid. If nothing is returning, this is a return-path problem and the Requester is a victim. Where the Completions have gone is a fabric or Completer question.
3. Are arriving Completions matching? If orphan_cpl is pulsing, Completions are returning and finding nothing outstanding — so identifiers are being freed too early, or the decoded identifier is wrong. Nothing will be freed by these, so the pool stays exhausted.
4. Is cpl_last ever asserting? A cpl_last stuck low means every Completion is treated as non-terminating: results are delivered, nothing is freed, and the pool drains to empty and stays there. The signature is unmistakable — results arriving normally while busy_count never falls.
5. Is the result consumer draining? If res_valid is high with res_ready low for a long time, the result stage is stuck, cpl_ready is low, Completions are not being accepted, and identifiers are not being freed. The root cause is a stalled local consumer and the visible symptom is an idle Link three steps away. This is the most commonly misdiagnosed failure in the chapter.
6. Are identifiers leaking? busy_count rising monotonically over a long run with results being delivered normally means frees are being lost somewhere — P7's free_error and P3's gating are the places to look.
7. Is the design simply at its outstanding limit? A pool at capacity with identifiers turning over steadily is not a fault. It is §13's ceiling.

The distinguishing observation: plot busy_count against time. Rising to IDS and flat with no frees is a leak or a blockage (3, 4, 5, 6). Oscillating near IDS with steady frees is saturation (7). They look identical at the request interface and demand opposite responses, and this is the same diagnostic shape Chapter 10.2 §15 and Chapter 10.3 §12 both end on — because it is the general shape of a resource-pool failure.

Symptom: read data is delivered to the wrong consumer

The data is valid, so transport is fine. The association is wrong, and there are exactly three places it can be wrong.

1. The identifier was reused while the first operation was outstanding. §5's hazard. The signature is that the receiving consumer's token does not match any operation it issued — and the token that did arrive belongs to an operation completed earlier. Check whether the same identifier appears on two launches with no intervening free. P5 and P6 make this unrepresentable inside the design, so if it is happening the identifier came from somewhere else, or something outside the pool cleared a busy bit.
2. The retained token was read from the wrong entry. An indexing error between the launch write and the completion read of token_q. P10 catches it; by hand, compare the token recorded at launch for an identifier against the token delivered when that identifier completes.
3. The result was built from the Completion rather than from retained state. The architectural error of Chapter 10.2 §9. The signature is that the delivered token correlates with something about the Completion rather than with the operation that was issued.

The measurement that partitions them. Log (identifier, token) at every launch and (identifier, token) at every result. If an identifier appears twice in the launch log with no free between, it is (1). If the pairs disagree, it is (2) or (3), and P10 separates those.

And a free-list-specific cause worth naming. If a double free ever corrupted the pool — pushing one identifier onto the list twice — the allocator would hand it to two live operations and produce (1) with no reuse bug anywhere in the engine. §7's busy bitmap is what prevents it, and free_error is where it would have been visible.

Symptom: two outstanding operations carry the same identifier

Stop and treat this as a correlation-safety failure, not a performance anomaly. It is the precondition for every corruption in this chapter, and it is worth an immediate assertion rather than an investigation.

Where it can come from, given §7's structure:

• A double free corrupted the free list — the identifier was pushed twice and handed out twice. free_error should have fired; if it did not, the busy bitmap was already wrong.
• Something outside the pool cleared a busy bit. An error path, a flush, or — the realistic one — a watchdog wired to free on expiry, which §9 explicitly forbids and P14 catches.
• Two allocators, or a reset that cleared one structure and not the other. A local reset that clears the pool while the engine keeps its retained tokens leaves the two disagreeing about what is outstanding.

The immediate check. $countones(busy_mask) against the number of launches minus frees, and against busy_count (P8). Any disagreement localises the fault to the pool. If they agree and two operations still share an identifier, the identifier did not come from this pool.

13. Outstanding Depth Is the Throughput Ceiling

Chapter 10.3 §11 established that posted throughput is limited by forward-path resources. Non-posted throughput has a second limit, and it is usually the binding one.

The mechanism. Each outstanding operation holds an identifier from launch until its Completion returns. If the round trip takes L cycles and the pool holds N identifiers, then at most N operations are in flight during any L-cycle window — regardless of how fast the Requester can generate them or how much bandwidth the Link has.

The other side of the same coin. Return-path pressure limits the request path, and §10's P13 makes the dependency formal: eventual launch requires identifiers to come back, which requires Completions to be accepted, which requires the local consumer to keep draining. A slow consumer of read data throttles read issuance, through a chain with no explicit feedback signal anywhere in it.

14. Posted and Non-Posted, Side by Side

Every row is scoped deliberately; the absolutes people reach for are wrong in both directions.

15. Common Misconceptions

• "Non-posted means the Request waits on the wire until the response comes back." It does not. The Request is transmitted and the fabric is free; what waits is state at the Requester, not the link. That is what "split transaction" means.
• "Non-posted means only one Request may be outstanding." Outstanding depth is an implementation parameter, and §13 explains why keeping only one outstanding wastes most of the available throughput.
• "Non-posted means synchronous software execution." It is a protocol-level property. Whether the software issuing the operation blocks is a driver and operating-system design choice at a completely different level.
• "Every write is posted, so no write can be non-posted." I/O Writes and Configuration Writes are non-posted and require Completion (§1). Only Memory Writes among the writes are posted.
• "The Requester can free its context once the Request is accepted downstream." Acceptance transfers ownership of the packet. The operation is "not considered complete until after the Completion returns" (§3), and freeing early loses the result or corrupts an unrelated operation.
• "A correlation identifier can be reused as soon as the Request has been transmitted." It may be reused only once no Completion carrying it can still arrive (§5). Transmission is the moment the risk begins, not the moment it ends.
• "A timeout means it is safe to resend the Request." A timed-out operation has an unknown outcome, and a reissue is "a distinct Request" with "no relationship" to the original. Whether it may safely be repeated is knowledge that lives above this layer (§9).
• "Completions can be matched by arrival order." Completions for distinct Requests may return in a different order than the Requests were issued (Chapter 10.2 §4). Matching is by identity.
• "Outstanding capacity is unrelated to performance." It is the primary throughput limit for non-posted traffic, together with round-trip latency (§13). A design that under-provisions it will look bandwidth-limited when it is not.
• "Non-posted traffic has no payload." A Configuration Write and an I/O Write are non-posted and carry data outbound; a Read carries data back in its Completion. Direction and classification are independent properties.

16. Understanding Check

17. What's Next

Module 10 now has its semantics complete. 10.1 established what a Request is and who may issue one. 10.2 built the return half and the correlation that makes it work. 10.3 and this chapter split the Request population into the two lifetimes — ownership that ends going out, and ownership that ends coming back.

Chapter 10.5 — Transaction Flow puts them together and follows one complete request-to-Completion exchange across the fabric: every hop, every boundary, and every place the transaction changes hands, with all of this module's vocabulary already in place.

Then Module 11 opens the packet. Everything this module has called a category — the operation, the routing information, the identity, the correlation, the length, the byte-valid information — becomes a field with a position and an encoding. Module 12 takes memory transactions in detail, and Module 13 takes Completions in the depth this chapter kept deferring: their types, their status, the rules for splitting one response across several, and the ordering that governs them all.

The idea to carry forward: a non-posted Request is not finished when it is sent — and every piece of state, every property, and every debugging ladder in this chapter exists because of that one fact.