Split Completions — Accounting for a Byte Range, Not Counting Packets

Chapter 12.1 said a read may be answered by more than one Completion and moved on. Chapter 12.3 built the progress accounting that survives it. Chapter 13.2 decoded the outcome of each one.

None of them said where a returned chunk belongs.

How can one Memory Read Request be resolved by multiple Completion-with-Data packets, what information lets the Requester reconstruct the original byte range, and what RTL state must survive until every required byte is accounted for?

1. Packet Count Is Not Progress

The wrong model is seductive because it is arithmetic:

requested 256 B, MPS is 128 B
   → expect two Completions
   → count to two
   → done

Every step of that is wrong except the first.

The Completer is not obliged to use the largest payload it may. It may return 256 B as two chunks, or four, or five unequal ones — and the constraint on where it may cut is RCB (§5), not MPS alone.

So a design that counts packets is guessing, and it guesses wrong the first time it meets a Completer with different internal buffering, a different RCB, or a request that does not start on a boundary.

The right model is coverage:

requested byte extent
   → zero or more returned partial extents, each placed by its own fields
   → complete when the required extent is fully accounted for

§4's Byte Count field makes that computable directly, which is the whole reason it exists.

2. The Verified Fields and Rules

3. Why Splitting Happens

Several influences, and no single mandatory cause. A design that assumes one reason will be surprised by a Completer that had another.

4. Byte Count Counts Down, Not Up

The single most misread field in the Completion header.

Byte Count is the number of bytes still required to complete the Request, including this Completion's own payload.

It is not "bytes in this packet." That quantity is expressed separately, by the packet's own length.

And note the cross-check it gives you for free. The Byte Count of the first Completion must equal the requested extent. A mismatch there means the Completion does not belong to the Request you matched it to — a correlation error, detectable on the first packet rather than at the end.

5. Lower Address Says Where the Data Starts

Byte Count says how much remains. Lower Address says where this piece begins.

Lower Address is the 7 least significant bits of the address from which the first byte in this Completion was read.

Seven bits reaches 128 bytes, which is exactly the largest RCB — and that is not a coincidence. Given RCB-aligned cuts, seven bits is precisely enough to locate the start of any Completion within its boundary-aligned region.

And note what Lower Address is not. It is not the BAR offset, not the full address, and not an index into the Requester's buffer. It is address bits, and turning them into a destination offset is §10's arithmetic and the Requester's own business.

6. RCB — Where the Completer May Cut

RCB is a boundary constraint, not a size. It does not say how large a Completion is; it says which addresses a division may fall on.

RCB = 128 bytes
   → a multi-Completion response may be divided only at
     naturally aligned 128-byte boundaries
   → the first piece may start anywhere (wherever the request did)
   → the last piece may end anywhere (wherever the request did)
   → every interior cut is on a boundary

Which is why the first and last Completions are the odd-sized ones in §5's tables, and every interior one is exactly RCB bytes.

7. What the Ordering Rule Does and Does Not Give You

One rule, taken from Chapter 13.4's territory because this chapter cannot work without it:

Completions with the same Transaction ID must not pass each other.

What that gives you. The pieces of one Request arrive in the order the Completer emitted them. Since the Completer walks the requested range, that is increasing address order for the pieces of a single read.

What it explicitly does not give you. The same source states the rule adds no requirement between the Completions of different transactions. So:

8. A Worked Split

Setup. Memory Read for 256 bytes starting at 0x8000_1030. The path's RCB is 128 bytes. Correlation index 3; the Requester's destination buffer starts at local offset 0.

Check the arithmetic. 80 + 128 + 48 = 256 ✓. Byte Count decreases by exactly each Completion's payload: 256 − 80 = 176 ✓, 176 − 128 = 48 ✓. The last Completion's Byte Count equals its own payload, which is the retirement condition (§4).

Check the cuts. The first piece runs from the request's start to the next 128-byte boundary — 80 bytes, not a round number, because the request did not start on one. The interior piece is exactly RCB. The last piece is whatever remains.

And the destination offsets are derived, not carried. The Completion says where the data came from (Lower Address, plus the address bits the Requester already knows); the Requester computes where it goes locally. §10 is that computation, and §11's range checks are what stop it going wrong.

9. The Lifecycle

The two amber steps are the chapter. Valid data has arrived and the read is not finished. A design that retires there frees the correlation index while two Completions are still in flight — Chapter 12.1 §8's catastrophe, now with a mechanism that makes the correct condition computable.

10. RTL — Split Read Progress Table

// SYNTHESIZABLE. Per-read coverage accounting for a split Completion
// response. Byte Count semantics (remaining INCLUDING this packet) and
// Lower Address semantics (7 LSBs of this packet's first byte address):
// NORMATIVE (section 2). The table structure, the offset derivation and the
// error outputs: ILLUSTRATIVE implementation.
//
// COVERAGE MODEL A — ordered, non-overlapping chunks. Valid because
// Completions with the same Transaction ID must not pass each other
// (section 7). A design that cannot rely on that needs Model B, a coverage
// bitmap; section 12 sketches it as a verification model.
module split_read_progress #(
  parameter int CTXS   = 8,
  parameter int BC_W   = 13,          // byte count, up to 4096
  parameter int OFF_W  = 13,          // offset within one request
  parameter int DEST_W = 8,
  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 [BC_W-1:0]    open_total_bytes,   // the requested extent
  input  logic [6:0]         open_lower_addr,    // 7 LSBs of the request address
  input  logic [DEST_W-1:0]  open_dest,
 
  // ---- A correlated Completion chunk -----------------------------------
  // Correlation happened upstream (Chapter 12.3 section 5). This block
  // accounts and places; it does not identify.
  input  logic               chunk_valid,
  input  logic [IDX_W-1:0]   chunk_id,
  input  logic [BC_W-1:0]    chunk_byte_count,   // NORMATIVE: remaining incl. this
  input  logic [6:0]         chunk_lower_addr,   // NORMATIVE: 7 LSBs of first byte
  input  logic [OFF_W-1:0]   chunk_bytes,        // this packet's payload bytes
 
  // ---- Placement and completion ----------------------------------------
  output logic               chunk_accept,
  output logic [OFF_W-1:0]   chunk_dest_offset,  // where this data goes locally
  output logic [DEST_W-1:0]  chunk_dest,
  output logic               read_complete,      // coverage complete THIS cycle
 
  // ---- Reported conditions ---------------------------------------------
  output logic               illegal_id_error,
  output logic               unknown_ctx_error,
  output logic               range_error,        // would fall outside the request
  output logic               sequence_error,     // gap, overlap or duplicate
  output logic               byte_count_error    // inconsistent with our record
);
 
  // ---- Range safety, before any array access ---------------------------
  // IDX_W = $clog2(CTXS) can express values >= CTXS at any non-power-of-two
  // CTXS. Compared one bit wider so CTXS stays representable at powers of
  // two (Chapter 12.3 section 8a).
  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));
 
  typedef struct packed {
    logic              active;
    logic [BC_W-1:0]   total_bytes;    // requested extent
    logic [BC_W-1:0]   remaining;      // still owed
    logic [OFF_W-1:0]  next_offset;    // Model A cursor
    logic [6:0]        base_lower;     // request's own 7 LSBs
    logic [DEST_W-1:0] dest;
  } read_t;
 
  read_t ctx_q [CTXS];
 
  // ---- Guarded reads ---------------------------------------------------
  logic              c_active;
  logic [BC_W-1:0]   c_total, c_remaining;
  logic [OFF_W-1:0]  c_next_off;
  logic [6:0]        c_base_lower;
  logic [DEST_W-1:0] c_dest;
  logic              o_active;
 
  always_comb begin
    c_active = 1'b0; c_total = '0; c_remaining = '0;
    c_next_off = '0; c_base_lower = '0; c_dest = '0;
    o_active = 1'b0;
    if (chunk_id_legal) begin
      c_active     = ctx_q[chunk_id].active;
      c_total      = ctx_q[chunk_id].total_bytes;
      c_remaining  = ctx_q[chunk_id].remaining;
      c_next_off   = ctx_q[chunk_id].next_offset;
      c_base_lower = ctx_q[chunk_id].base_lower;
      c_dest       = ctx_q[chunk_id].dest;
    end
    if (open_id_legal) o_active = ctx_q[open_id].active;
  end
 
  wire hit = chunk_valid && chunk_id_legal && c_active;
 
  // ---- EXTENDED-WIDTH RANGE CHECK --------------------------------------
  // Computed one bit wider than either operand. A same-width
  // (offset + length <= size) wraps on overflow and then passes, which is
  // exactly how an oversized chunk gets written past the end of a buffer.
  wire [OFF_W:0] end_off_ext = {1'b0, c_next_off} + {1'b0, chunk_bytes};
  wire in_range = hit && (end_off_ext <= {1'b0, OFF_W'(c_total)});
 
  // ---- Byte Count consistency ------------------------------------------
  // NORMATIVE semantics applied as a check, not merely consumed: the
  // arriving Byte Count must equal what we still expect, because it counts
  // remaining bytes INCLUDING this packet (section 4).
  wire bc_ok = hit && (chunk_byte_count == c_remaining);
 
  // ---- Model A sequence check ------------------------------------------
  // The chunk must start exactly where the previous one ended. Because
  // Lower Address is only 7 bits it cannot by itself locate a chunk within a
  // request larger than 128 bytes, so it is used as a CONSISTENCY CHECK on
  // the cursor rather than as the placement source (section 5).
  wire [6:0] expected_lower = c_base_lower + 7'(c_next_off);
  wire seq_ok = hit && (chunk_lower_addr == expected_lower);
 
  wire nonzero = hit && (chunk_bytes != '0);
 
  assign chunk_accept      = hit && in_range && bc_ok && seq_ok && nonzero;
  assign chunk_dest_offset = c_next_off;
  assign chunk_dest        = c_dest;
 
  // RETIRE only when this chunk completes the coverage. Expressed in the
  // protocol's own terms: Byte Count equals this packet's payload means
  // nothing remains after it (section 4).
  assign read_complete = chunk_accept && (chunk_byte_count == BC_W'(chunk_bytes));
 
  logic ill_q, unk_q, rng_q, seq_q, bc_q;
  assign illegal_id_error  = ill_q;
  assign unknown_ctx_error = unk_q;
  assign range_error       = rng_q;
  assign sequence_error    = seq_q;
  assign byte_count_error  = bc_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;
      ill_q <= 1'b0; unk_q <= 1'b0; rng_q <= 1'b0;
      seq_q <= 1'b0; bc_q  <= 1'b0;
    end else begin
      if (open_valid && open_id_legal && !o_active) begin
        ctx_q[open_id].active      <= 1'b1;
        ctx_q[open_id].total_bytes <= open_total_bytes;
        ctx_q[open_id].remaining   <= open_total_bytes;
        ctx_q[open_id].next_offset <= '0;
        ctx_q[open_id].base_lower  <= open_lower_addr;
        ctx_q[open_id].dest        <= open_dest;
      end
 
      if (chunk_accept) begin
        ctx_q[chunk_id].next_offset <= c_next_off + chunk_bytes;
        ctx_q[chunk_id].remaining   <= c_remaining - BC_W'(chunk_bytes);
        // Freed ONLY on complete coverage. Never on a packet count.
        if (chunk_byte_count == BC_W'(chunk_bytes))
          ctx_q[chunk_id].active <= 1'b0;
      end
 
      // Reported, never acted on. None of these writes any entry, and each
      // names a DIFFERENT investigation (section 15).
      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 && !c_active) unk_q <= 1'b1;
      if (hit && !in_range)                           rng_q <= 1'b1;
      if (hit &&  in_range && !bc_ok)                 bc_q  <= 1'b1;
      if (hit &&  in_range &&  bc_ok && !seq_ok)      seq_q <= 1'b1;
    end
  end
 
endmodule

Classification: synthesizable.

Architecture. One cursor and one remaining-byte counter per outstanding read, with three independent consistency checks — range, Byte Count, sequence — each with its own reported condition.

State. Per entry: active, requested extent, remaining bytes, next expected offset, the request's own low address bits, and the local destination. Five sticky error flags.

Cycle behaviour. A chunk is accepted only if it is in range, its Byte Count matches what is still owed, it starts where the last one ended, and it is non-empty. read_complete pulses on the chunk whose Byte Count equals its own payload — the protocol's own retirement condition, not a counter.

Contract. Upstream guarantees chunk_id came from a correlation lookup. The environment must deliver the chunks of one read in ascending order — §7's rule, stated as p_env_chunks_in_order in §11 rather than assumed silently.

Why Lower Address is a check and not the placement source. It is 7 bits, so it cannot locate a chunk within a request larger than 128 bytes. Placement comes from the cursor; Lower Address confirms the cursor is where the Completer thinks it is — which catches a dropped or duplicated chunk on the packet after the fault, rather than at the end of the read.

Failure — six. Retiring on packet count rather than on Byte Count is §1's error. Computing in_range at native width lets an oversized chunk wrap and pass (§11's P4). Using Lower Address directly as the destination offset places every chunk within 128 bytes of the buffer start. Treating Byte Count as bytes in this packet makes the remaining count diverge immediately. Accepting a chunk without the sequence check lets a duplicate advance the cursor twice. And indexing the table before the legality check breaks at non-power-of-two CTXS.

Deliberately simplified: Model A only; a single request extent within OFF_W; no status interaction (Chapter 13.2); no timeout; one chunk per cycle.

Production implication: a real design also applies the status rules, the timeout, and whatever additional legality checks the specification requires. The accounting is unchanged.

11. RTL — Reassembly Buffer with Range Enforcement

// SYNTHESIZABLE. Place an accepted chunk into a per-read reassembly region
// and refuse anything that would fall outside it.
// The range-safety discipline is a LOCAL REASSEMBLY CHECK, not automatically
// a PCIe malformed-TLP definition. The buffer organisation is ILLUSTRATIVE —
// a register array at teaching scale, not production DMA memory.
module read_reassembly #(
  parameter int REGION_BYTES = 512,       // bytes reserved per read
  parameter int BEAT_BYTES   = 16,        // bytes written per beat
  parameter int OFF_W        = 13
) (
  input  logic clk,
  input  logic rst_n,
 
  input  logic                    wr_valid,
  input  logic [OFF_W-1:0]        wr_offset,       // byte offset within the read
  input  logic [OFF_W-1:0]        wr_bytes,        // bytes in this beat
  input  logic [BEAT_BYTES*8-1:0] wr_data,
 
  // A region is claimed at open and released at retirement.
  input  logic                    region_open,
  input  logic                    region_close,
 
  output logic                    wr_accept,
  // The write would fall outside the region, or into bytes already written.
  output logic                    wr_range_error,
  output logic                    wr_overwrite_error
);
 
  generate
    if (REGION_BYTES < 1) $error("REGION_BYTES must be at least 1");
    if (BEAT_BYTES  < 1)  $error("BEAT_BYTES must be at least 1");
  endgenerate
 
  logic [7:0] mem_q [REGION_BYTES];
  // One written-bit per byte. At teaching scale this is affordable and it is
  // what makes overwrite detectable at all; a production design would use a
  // cursor and rely on the ordering rule, as section 10 does.
  logic [REGION_BYTES-1:0] written_q;
  logic                    open_q;
 
  // EXTENDED-WIDTH BOUNDS. One bit wider than either operand, so the sum
  // cannot wrap into a value that passes the comparison.
  wire [OFF_W:0] end_ext = {1'b0, wr_offset} + {1'b0, wr_bytes};
  wire in_region = open_q
                && (end_ext <= {1'b0, OFF_W'(REGION_BYTES)})
                && (wr_bytes != '0)
                && (wr_bytes <= OFF_W'(BEAT_BYTES));
 
  // Overlap detection over the bytes this beat would write.
  logic overlaps;
  always_comb begin
    overlaps = 1'b0;
    for (int b = 0; b < REGION_BYTES; b++)
      if ((OFF_W'(b) >= wr_offset) && ({1'b0, OFF_W'(b)} < end_ext)
          && written_q[b])
        overlaps = 1'b1;
  end
 
  assign wr_accept          = wr_valid && in_region && !overlaps;
  assign wr_range_error     = wr_valid && open_q && !in_region;
  assign wr_overwrite_error = wr_valid && in_region && overlaps;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      written_q <= '0; open_q <= 1'b0;
      for (int i = 0; i < REGION_BYTES; i++) mem_q[i] <= '0;
    end else begin
      // close has priority over open: a same-cycle retire-and-reopen ends
      // with a CLEAN region rather than one carrying the previous read's
      // written bits.
      if (region_close) begin
        open_q    <= 1'b0;
        written_q <= '0;
      end
      if (region_open) begin
        open_q    <= 1'b1;
        written_q <= '0;
      end
 
      if (wr_accept)
        for (int b = 0; b < REGION_BYTES; b++)
          if ((OFF_W'(b) >= wr_offset) && ({1'b0, OFF_W'(b)} < end_ext)) begin
            mem_q[b]     <= wr_data[8*(b - int'(wr_offset)) +: 8];
            written_q[b] <= 1'b1;
          end
    end
  end
 
endmodule

Classification: synthesizable at teaching scale.

Architecture. A byte-addressed region with a per-byte written bitmap — the Model B coverage idea, applied to one read's buffer rather than to the whole table. It exists so overwrite is detectable, which a cursor alone cannot do.

State. The data region, the written bitmap, the open flag.

Cycle behaviour. region_close has priority over region_open, so a same-cycle retire-and-reopen leaves a clean region rather than one carrying the previous read's bits.

Contract. The caller supplies offsets already validated by §10. This block validates them again — deliberately, because a reassembly buffer is the last place a bad offset can be stopped before it becomes silent corruption.

Failure — three. Native-width bounds arithmetic lets offset + bytes wrap and pass. Clearing written_q on open but not on close leaves a stale bitmap if a read is abandoned. And giving region_open priority over region_close on a same-cycle event opens a region that is about to be cleared.

Deliberately simplified: one region rather than one per context; a register array rather than RAM; per-byte bits, which do not scale — a production design relies on §7's ordering rule and a cursor, and uses the bitmap only in verification (§13).

12. Assertions

// SVA over split_read_progress and read_reassembly. These assert the
// NORMATIVE Byte Count and Lower Address semantics of section 2 plus LOCAL
// reassembly safety. They do NOT assert the rules governing when a Completer
// may split, and they do NOT define PCIe malformed-TLP conditions.
 
// ENVIRONMENT — the ordering assumption Model A depends on, stated as an
// assumption rather than left implicit (section 7).
assume property (@(posedge clk) disable iff (!rst_n)
  chunk_accept |=> !(chunk_valid && chunk_id_legal && c_active
                     && (chunk_lower_addr != (c_base_lower + 7'(c_next_off)))));
 
// COVERAGE — P1: THE CENTRAL PROPERTY. A chunk that does not complete the
// coverage NEVER retires the read.
property p_partial_never_completes;
  @(posedge clk) disable iff (!rst_n)
  (chunk_accept && (chunk_byte_count != BC_W'(chunk_bytes))) |-> !read_complete;
endproperty
a_partial : assert property (p_partial_never_completes);
 
// COVERAGE — P2: and the converse. The chunk that completes the coverage
// DOES retire it. P1 alone is satisfied by a design that never retires.
property p_final_completes;
  @(posedge clk) disable iff (!rst_n)
  (chunk_accept && (chunk_byte_count == BC_W'(chunk_bytes))) |-> read_complete;
endproperty
a_final : assert property (p_final_completes);
 
// COVERAGE — P3: a retired read has zero remaining coverage.
property p_retire_zero_remaining;
  @(posedge clk) disable iff (!rst_n)
  read_complete |=> !ctx_q[$past(chunk_id)].active;
endproperty
a_retire_clean : assert property (p_retire_zero_remaining);
 
// RANGE — P4: THE OVERFLOW-SAFETY PROPERTY. No accepted chunk can extend
// beyond the requested extent. Written with extended-width arithmetic in the
// property too, so a wrapping implementation cannot satisfy it by agreeing
// with a wrapping check.
property p_never_out_of_range;
  @(posedge clk) disable iff (!rst_n)
  chunk_accept |-> (({1'b0, chunk_dest_offset} + {1'b0, chunk_bytes})
                    <= {1'b0, OFF_W'(c_total)});
endproperty
a_in_range : assert property (p_never_out_of_range);
 
// BYTE COUNT — P5: the NORMATIVE semantics, asserted rather than assumed.
// The arriving Byte Count must equal what is still owed.
property p_byte_count_is_remaining;
  @(posedge clk) disable iff (!rst_n)
  chunk_accept |-> (chunk_byte_count == c_remaining);
endproperty
a_bc : assert property (p_byte_count_is_remaining);
 
// BYTE COUNT — P6: it decreases by exactly this chunk's payload.
property p_remaining_decrements_exactly;
  @(posedge clk) disable iff (!rst_n)
  (chunk_accept && !read_complete)
    |=> (ctx_q[$past(chunk_id)].remaining
         == $past(c_remaining) - BC_W'($past(chunk_bytes)));
endproperty
a_bc_step : assert property (p_remaining_decrements_exactly);
 
// SEQUENCE — P7: a duplicate or overlapping chunk is never accepted. Model
// A's cursor makes this checkable: a repeat arrives with a stale Byte Count
// and a stale Lower Address, and fails both checks.
property p_no_duplicate_accepted;
  @(posedge clk) disable iff (!rst_n)
  (chunk_valid && chunk_id_legal && c_active
               && (chunk_lower_addr != (c_base_lower + 7'(c_next_off))))
    |-> (!chunk_accept ##1 sequence_error);
endproperty
a_no_dup : assert property (p_no_duplicate_accepted);
 
// ISOLATION — P8: one chunk updates at most one context, and only the one it
// named. Per-entry, so a write to a neighbour cannot hide in an aggregate.
generate for (genvar g = 0; g < CTXS; g++) begin : g_one_ctx
  a_single_ctx : assert property (@(posedge clk) disable iff (!rst_n)
    !$stable(ctx_q[g])
      |-> ($past(open_valid && open_id_legal && (open_id == IDX_W'(g)))
        || $past(chunk_accept && (chunk_id == IDX_W'(g)))
        || $past(!rst_n)));
end endgenerate
 
// RANGE — P9: an out-of-range identifier changes nothing.
property p_illegal_id_inert;
  @(posedge clk) disable iff (!rst_n)
  ((chunk_valid && !chunk_id_legal) || (open_valid && !open_id_legal))
    |=> ((ctx_q == $past(ctx_snapshot)) && illegal_id_error);
endproperty
a_illegal : assert property (p_illegal_id_inert);
 
// LIFETIME — P10: a correlation index stays unavailable until the read is
// fully resolved. The property that prevents Chapter 12.1 section 8's
// catastrophe from the split side.
property p_id_held_until_complete;
  @(posedge clk) disable iff (!rst_n)
  (chunk_accept && !read_complete) |=> ctx_q[$past(chunk_id)].active;
endproperty
a_id_held : assert property (p_id_held_until_complete);
 
// REASSEMBLY — P11: no accepted write falls outside the region.
property p_write_in_region;
  @(posedge clk) disable iff (!rst_n)
  wr_accept |-> (({1'b0, wr_offset} + {1'b0, wr_bytes})
                 <= {1'b0, OFF_W'(REGION_BYTES)});
endproperty
a_wr_range : assert property (p_write_in_region);
 
// REASSEMBLY — P12: no accepted write touches a byte already written.
property p_no_silent_overwrite;
  @(posedge clk) disable iff (!rst_n)
  wr_accept |-> !overlaps;
endproperty
a_no_overwrite : assert property (p_no_silent_overwrite);
 
// REASSEMBLY — P13: same-cycle close and open leaves a CLEAN region.
property p_close_open_clean;
  @(posedge clk) disable iff (!rst_n)
  (region_close && region_open) |=> ((written_q == '0) && open_q);
endproperty
a_clean_reopen : assert property (p_close_open_clean);
 
// RESET — P14: reset clears every context, per entry.
generate for (genvar g = 0; g < CTXS; g++) begin : g_reset
  a_reset : assert property (@(posedge clk) !rst_n |=> !ctx_q[g].active);
end endgenerate

P1 and P2 are the pair that defines "finished", and both are needed. P1 forbids early retirement — the catastrophe. P2 forbids the opposite: a read whose final chunk arrives and which never retires, holding a correlation index forever. A design satisfying only P1 by never retiring anything is not correct, and only P2 says so.

P4 is written with extended-width arithmetic in the property, deliberately. A property that computed the bound at native width would wrap exactly where the implementation wraps, agree with it, and pass. The property has to be arithmetically stronger than the code it checks, or it is checking that the code agrees with itself.

P5 is the normative semantics turned into a check. Byte Count could simply be consumed; asserting it against the Requester's own remaining count means a Completion belonging to a different Request fails on the first packet rather than corrupting the read and being discovered at the end.

P7 is what Model A buys. A duplicate chunk arrives with a stale Byte Count and a stale Lower Address, so it fails both consistency checks — and the cursor never advances twice. Without the sequence check, a duplicate would advance the cursor and the read would finish short with no error.

The environment assumption is stated as an assume, not buried in prose. Model A is correct only if the chunks of one read arrive in ascending order (§7). A design deployed where that does not hold needs Model B, and the assumption is where a reviewer finds that out.

13. Verification

Monitors observe: the open interface; the chunk interface with Byte Count, Lower Address and payload size; the placement outputs; every reported condition; and the reassembly writes.

The scoreboard maintains an independent byte-range coverage model.

// VERIFICATION-ONLY. The reference model. Coverage is tracked as a BITMAP
// per read — Model B — deliberately independent of the DUT's cursor. A
// scoreboard that mirrored the cursor could not detect a cursor bug.
typedef struct {
  bit               active;
  int               total_bytes;
  int               start_addr;
  bit [4095:0]      covered;      // one bit per byte of the request
  int               dest;
} sb_read_t;
 
// On each observed chunk:
//   1. validate the context is active                (independent map)
//   2. compute the expected offset from the ADDRESS, not from a cursor
//   3. assert no bit in [offset, offset+bytes) is already set  -> overlap
//   4. assert every bit in range is within total_bytes         -> range
//   5. set the bits
//   6. compare returned bytes against an independent memory model
//   7. read is complete iff ALL bits in [0, total_bytes) are set

Point 7 is the reason for the bitmap. The DUT decides completion from a remaining counter; the scoreboard decides it from coverage. A design that decremented twice, or accepted a duplicate, reaches zero remaining with gaps still uncovered — and only a coverage model sees the gap. A scoreboard reading remaining would agree with the bug.

Never use the DUT's next_offset, remaining, or chunk_dest_offset as the oracle. Compute the expected offset from the address the Completion reports.

Split shapes

• One CplD covering the whole read. The unsplit case.
• A two-way split at exactly RCB.
• The §8 example — 80 / 128 / 48 with RCB 128, request not boundary-aligned. Verify every Byte Count and Lower Address.
• The same request with RCB 64 — five chunks, Lower Address alternating 0x00 and 0x40. The test that catches "zero after the first" (§5).
• A minimum first chunk: request starting one byte below a boundary, so the first chunk is 1 byte.
• A minimum final chunk: request ending one byte past a boundary.
• Many small chunks — the maximum the model supports.
• A request that starts and ends on RCB boundaries. Every chunk exactly RCB.

Multiple reads

• Two reads outstanding, chunks interleaved. Verify each read's coverage advances independently.
• Read B completes entirely between two of read A's chunks (§7 permits it). Verify A is unaffected.
• Three reads, all multi-chunk, fully interleaved. The strongest test available.

Negative

• A duplicate chunk. Verify sequence_error, no acceptance, cursor unchanged (P7).
• An overlapping chunk — same context, offset before the cursor.
• A gap — a chunk starting past the cursor. Verify rejection.
• A chunk that would extend past the requested extent. Verify range_error (P4).
• An oversized chunk chosen to wrap offset + bytes at native width. The test that only fails a native-width check — pick chunk_bytes so the untruncated sum exceeds 2^OFF_W.
• A zero-length chunk.
• A Byte Count inconsistent with the record. Verify byte_count_error.
• A first chunk whose Byte Count ≠ the requested extent — the correlation cross-check of §4.
• An unknown context, and an out-of-range identifier. Verify they are reported differently (P9).
• A context reused before its final chunk. Verify the open is refused.
• Result-buffer stall across a retirement.
• Reset mid-read, and same-cycle close-and-open (P13).

Which mutation which test kills

Coverage should include: RCB 64 and 128; aligned and unaligned request starts and ends; chunk counts from 1 to the model's maximum; every reported condition; two and three interleaved reads; and CTXS at 1, a power of two and a non-power of two.

14. Debugging

The first half of the data is correct; the second half repeats the first half

Placement, not accounting — the bytes arrived, they went to the wrong place.

The dominant cause is using Lower Address as the destination offset. It is 7 bits. For a request larger than 128 bytes it cannot express an offset beyond 127, so every chunk after the first lands within the first 128 bytes of the buffer — overwriting what is already there. The symptom is exactly "the later data replaced the earlier data."

Two others. The cursor did not advance — check whether next_offset moves on every acceptance. Or the reassembly write used the wrong base.

The one observation: print chunk_dest_offset for each chunk of one read. It must be the running sum of the payload sizes. If it tracks chunk_lower_addr instead, that is the bug.

A read retires, then a later CplD arrives as an orphan

Premature retirement, and the orphan is the evidence.

Three causes. The retirement condition counts packets rather than testing Byte Count against the payload (§1). remaining was decremented by the wrong amount, reaching zero early. Or the first chunk's Byte Count was not the full requested extent — meaning the Completion belonged to a different Request and the correlation is wrong.

Distinguish them by summing. Add up the payload bytes actually delivered before the retirement. Short of the requested extent → the accounting retired early. Equal to it → the read really was complete and the orphan belongs to something else — which points at correlation (Chapter 12.3 §5), not at this chapter.

The read never retires even though every byte appears in the buffer

Coverage bookkeeping — the data arrived and the accounting did not agree.

Check remaining against the sum of accepted payloads. If remaining is larger than it should be, a chunk was rejected: look at sequence_error, byte_count_error and range_error, which name three different reasons.

And check the final chunk specifically. The retirement condition tests Byte Count == payload bytes; a final chunk whose Byte Count is off by any amount will be accepted and will not retire. remaining reaching a small non-zero value and stopping is that signature.

One chunk of read A is credited to read B

Correlation, not accounting — and this chapter's checks are what caught it.

byte_count_error on B is the tell. A's chunk carries A's remaining count, which will not match B's record except by coincidence. That is P5 doing its job, and it fires on the packet rather than at the end of either read.

Look upstream at the correlation lookup and at whether a context was reused early (Chapter 12.1 §9a). This block cannot fix it and should not try — it reports and refuses.

15. Common Misconceptions

• "One Memory Read always produces one CplD." It may produce any legal number. The Requester must handle all of them (§3).
• "Packet count tells you how much of the read is complete." Coverage does. Byte Count is the field that makes coverage computable (§1, §4).
• "MRRS and MPS are the same." MRRS bounds the request; the payload limit bounds each Completion (Chapter 12.5 §9).
• "RCB and MPS are the same." RCB constrains where a division may fall; the payload limit constrains how large a piece may be. Independent (§6).
• "RCB tracks the host cache line size." It is a PCIe element property — 64 or 128 for a Root Complex, reported in Link Control; 128 for all other elements (§2).
• "Lower Address is the BAR offset." It is the 7 least significant bits of the address the data was read from (§5).
• "Lower Address is zero on every Completion after the first." Only when RCB is 128. At RCB 64 it alternates 0x00 and 0x40 (§5).
• "Byte Count is the payload bytes in this packet." It is the bytes remaining including this packet (§4).
• "The first CplD means the Request can be freed." The correlation index stays owned until coverage is complete (§12, P10).
• "Split pieces can be reconstructed by arrival order." The pieces of one read are ordered relative to each other, but the stream is a merge of many reads. Placement comes from the fields (§7).
• "The context identity alone says where inside the read the data belongs." Identity says which read; Lower Address and the cursor say where within it (§7).
• "Duplicate Completion data is harmless because it is the same bytes." It advances a naive cursor twice, so the read finishes short with a gap and reports success (§12, P7).
• "Splitting is a Requester implementation choice." The Requester chooses the request size. The division is the Completer's decision within the rules (§3).
• "A local result can be delivered before all required data is present." Not without an explicit streaming contract that the consumer agreed to. Absent one, partial delivery is delivering data the design has not established is complete (§12, P1).

16. Understanding Check

17. What's Next

This chapter made a split read computable. Byte Count counts down what is still owed and states the retirement condition in the protocol's own terms; Lower Address says where each piece was read from and confirms the cursor; RCB constrains where the Completer may cut; and the accounting — never the packet count — decides when a read is done.

It borrowed exactly one ordering rule, and only for the pieces of a single Request.

Chapter 13.4 — Ordering takes ordering properly: what may pass what across all transactions in flight, why the producer/consumer model depends on the defaults, and why "may pass" is a permission rather than a prediction. It closes Module 13.

Module 14 then leaves transaction semantics behind entirely and asks what makes a single Link reliable enough for any of this to work.

The idea to carry forward: a read is finished when its bytes are accounted for — and the packet already tells you how many are still owed.