AXI-to-DDR Flow

   what has happened at the instant ARVALID && ARREADY

   done:
     the address, length, size, burst type and ID are captured
     an entry exists in the controller's queue      (17.2)
     the requester's outstanding count has increased (8.1)

   NOT done:
     the address has not been mapped to bank/row/column  (8.6)
     the row state is unknown to the scheduler yet       (Module 9)
     no timing legality has been evaluated               (Module 14)
     no command has been committed                       (17.1)
     nothing has been reordered yet -- or it has, and this
       request may be behind requests accepted after it

   one bus transaction
     x  splits from decode, granularity, width, row boundary
     =  N controller requests
     x  1 to 3 commands each, depending on row state and policy
     =  M DDR commands
     +  refresh commands interleaved by the manager   (17.3)

   N and M are NOT derivable from the transaction alone. They depend
   on the address map, the mapping policy, the row state left by
   earlier traffic, and the page policy.

   this is why "how many DDR commands will my burst cost?" has no
   answer without the stream it sits in.

   REQUEST      read, 64 bytes, aligned, ID = 5
   arrives      cycle 100 (controller clock), accepted same cycle

   ---- step 1: acceptance (17.5) ----
   cycle 100    handshake completes; queue entry allocated
                fields retained: addr, 64B length, ID=5
                requester's outstanding count += 1
                DRAM activity so far: NONE

   ---- step 2: address mapping (8.6) ----
                physical addr -> rank 0, bank group 1, bank 5,
                                 row 0x1A40, column 0x080
                DERIVED under the ILLUSTRATIVE map above; a different
                mapping policy (18.1) gives a different bank and row
                for the SAME address.

   ---- step 3: how many DDR bursts? ----
                64 bytes / (32 bits x 8 transfers) = 64 / 32 = 2
                so this ONE request needs TWO DDR read bursts
                at consecutive columns in one row.
                note: 2, not 1, and not 8. The factor comes from the
                interface width and the device burst length -- 12.1 --
                neither of which the requester chose.

   ---- step 4: row state (Module 9) ----
   case A       row 0x1A40 already open in bank 5   -> RD, RD
   case B       bank 5 idle                          -> ACT, RD, RD
   case C       row 0x0C12 open in bank 5            -> PRE, ACT, RD, RD

   ---- step 5: timing legality (Module 14) ----
   case B       ACT at cycle 104 (after arbitration)
                first RD no earlier than ACT + tRCD   (14.1)
                second RD no earlier than first + tCCD (14.6)

   ---- step 6: data return ----
                first beats arrive CL after the first RD  (14.9)
                the two bursts return back-to-back if tCCD allows

   ---- step 7: response ----
                front end reassembles both bursts into one response
                and returns it; if another ID=5 read was accepted
                EARLIER and is still outstanding, this response WAITS
                -- 8.3's same-ID ordering rule, enforced by §11's
                bookkeeping, not by the scheduler.

   TOTALS for one 64-byte request:
     controller requests : 1   (no split -- it fits in one row here)
     DDR commands        : 2 to 4, depending on row state
     data bursts         : 2
     and the response may be held behind an earlier same-ID request

// ---------------------------------------------------------------------
// soc_req_splitter -- CLASSIFICATION: synthesisable, ILLUSTRATIVE.
//
// WHAT IT DOES: turns ONE accepted bus read transaction into N internal
// requests, where N is decided by a boundary the requester did not
// choose (§4). Each part gets its own internal tag; all parts keep the
// original bus ID, because 8.3's same-ID ordering rule is about the ID
// and the parts must recombine in order.
//
// WHY IT EXISTS: §1's table. "One transaction" and "one controller
// request" are different objects, and the factor between them comes
// from the address map, the controller's granularity and a row
// boundary -- none of which the requester controls.
//
// WHY ACCEPTANCE IS SEPARATED FROM ISSUE (§2): this block does NOT
// drive a DDR command. It produces internal requests that a scheduler
// will later choose among. A block that asserted a DDR read on the
// cycle the handshake completed would teach a false contract: there is
// no such path in any real controller.
//
// NOT AN AXI SLAVE: no channel FSMs, no write path, no WSTRB, no
// narrow transfers, no error responses. The AXI track owns those.
//
// SYNTHESIS: one adder, one comparator, a small counter. No memory.
// ---------------------------------------------------------------------
module soc_req_splitter #(
  parameter int ADDR_W   = 40,
  parameter int ID_W     = 6,
  parameter int TAG_W    = 8,
  parameter int LEN_W    = 12,   // bytes, ILLUSTRATIVE encoding
  parameter int BOUND_LOG = 10   // split boundary = 2**BOUND_LOG bytes
)(
  input  logic                clk,
  input  logic                rst_n,

  // ---- an ALREADY-ACCEPTED transaction (the handshake happened
  // upstream; 17.5 owns that contract, this block consumes its result)
  input  logic                req_valid,
  output logic                req_ready,
  input  logic [ADDR_W-1:0]   req_addr,
  input  logic [LEN_W-1:0]    req_bytes,
  input  logic [ID_W-1:0]     req_id,

  // ---- internal requests, one per part
  output logic                part_valid,
  input  logic                part_ready,
  output logic [ADDR_W-1:0]   part_addr,
  output logic [LEN_W-1:0]    part_bytes,
  output logic [ID_W-1:0]     part_bus_id,   // preserved, §6
  output logic [TAG_W-1:0]    part_tag,      // allocated per part
  output logic                part_first,
  output logic                part_last,

  // ---- published accounting
  output logic [15:0]         txns_accepted,
  output logic [15:0]         parts_emitted,
  output logic [15:0]         splits_occurred
);
  // $clog2 is not used for an index here, but the parameter bounds
  // still need stating: a zero-length request and a degenerate
  // boundary are both silently wrong rather than loudly wrong.
  initial begin
    if (ADDR_W    < 8) $fatal(1, "soc_req_splitter: ADDR_W must be >= 8");
    if (ID_W      < 1) $fatal(1, "soc_req_splitter: ID_W must be >= 1");
    if (TAG_W     < 1) $fatal(1, "soc_req_splitter: TAG_W must be >= 1");
    if (LEN_W     < 2) $fatal(1, "soc_req_splitter: LEN_W must be >= 2");
    // A boundary below 2 bytes cannot split anything meaningfully, and
    // one at or above the address width can never be crossed.
    if (BOUND_LOG < 1 || BOUND_LOG >= ADDR_W)
      $fatal(1, "soc_req_splitter: BOUND_LOG must be in 1..ADDR_W-1");
  end

  localparam logic [ADDR_W-1:0] BOUND_MASK = (({{(ADDR_W-1){1'b0}}, 1'b1}) << BOUND_LOG) - 1;

  logic                busy;
  logic [ADDR_W-1:0]   cur_addr;
  logic [LEN_W-1:0]    cur_left;
  logic [ID_W-1:0]     cur_id;
  logic [TAG_W-1:0]    next_tag;
  logic                cur_first;

  // Bytes remaining to the next boundary from the current address.
  // This is the whole of §4: the split point is a property of the
  // ADDRESS, not of the request.
  logic [ADDR_W-1:0]   to_boundary;
  always_comb begin
    to_boundary = (BOUND_MASK - (cur_addr & BOUND_MASK)) + 1'b1;
  end

  // This part is the smaller of "what is left" and "what fits before
  // the boundary". Comparing in the wider address width avoids a
  // truncation that would silently emit an oversized part.
  logic [LEN_W-1:0] this_bytes;
  always_comb begin
    this_bytes = ({{(ADDR_W-LEN_W){1'b0}}, cur_left} <= to_boundary)
               ? cur_left
               : to_boundary[LEN_W-1:0];
  end

  assign req_ready   = !busy;
  assign part_valid  = busy;
  assign part_addr   = cur_addr;
  assign part_bytes  = this_bytes;
  assign part_bus_id = cur_id;
  assign part_tag    = next_tag;
  assign part_first  = cur_first;
  // `last` is computed from what remains AFTER this part, so a
  // single-part request is both first and last -- which is what a
  // downstream reassembler needs to complete it immediately.
  assign part_last   = (this_bytes == cur_left);

  always_ff @(posedge clk) begin
    if (!rst_n) begin
      busy            <= 1'b0;
      cur_addr        <= '0;
      cur_left        <= '0;
      cur_id          <= '0;
      next_tag        <= '0;
      cur_first       <= 1'b0;
      txns_accepted   <= '0;
      parts_emitted   <= '0;
      splits_occurred <= '0;
    end else begin
      // Accept a new transaction only when idle. 17.5's
      // one-handshake-one-entry rule: this block must not take a
      // second transaction while still emitting the first's parts, or
      // the parts of two transactions would interleave and 8.3's
      // ordering rule would be unenforceable downstream.
      if (req_valid && req_ready) begin
        // A zero-byte request would make cur_left zero and emit a
        // part with this_bytes == 0 forever. Refused by construction:
        // busy is only set for a non-zero length.
        if (req_bytes != '0) begin
          busy      <= 1'b1;
          cur_addr  <= req_addr;
          cur_left  <= req_bytes;
          cur_id    <= req_id;
          cur_first <= 1'b1;
          if (txns_accepted != 16'hFFFF) txns_accepted <= txns_accepted + 1'b1;
        end
      end

      if (part_valid && part_ready) begin
        if (parts_emitted != 16'hFFFF) parts_emitted <= parts_emitted + 1'b1;
        next_tag  <= next_tag + 1'b1;   // wraps; TAG_W bounds outstanding
        cur_first <= 1'b0;
        if (part_last) begin
          busy     <= 1'b0;
          cur_left <= '0;
        end else begin
          // Advance to the boundary and continue. Counting a split
          // here rather than at accept time means the number reflects
          // splits that actually happened.
          cur_addr <= cur_addr + this_bytes;
          cur_left <= cur_left - this_bytes;
          if (splits_occurred != 16'hFFFF) splits_occurred <= splits_occurred + 1'b1;
        end
      end
    end
  end
endmodule

// ---------------------------------------------------------------------
// resp_reorder_tracker -- CLASSIFICATION: synthesisable, ILLUSTRATIVE.
//
// WHAT IT DOES: §6's reconciliation. The scheduler may complete
// internal requests in any order (23.4 reorders for row locality).
// This block releases responses so that:
//   - all parts of one transaction complete before it responds (§4)
//   - same-ID transactions respond in allocation order   (AXI 8.3)
//   - different-ID transactions may respond out of order (AXI 8.4)
//
// WHY THE DEPTH MATTERS: this is the storage cost of the ordering
// boundary 17.5 owns. A shallow tracker forces the scheduler to
// reorder less; a deep one costs area. The trade is architectural,
// not a tuning knob.
//
// WHAT WAS REMOVED: the data path. A real reorder buffer also stores
// the returned beats, and that storage -- not this bookkeeping --
// dominates its area.
//
// SYNTHESIS: a small register file plus priority encoders. Depth is a
// parameter because it is the architectural dial.
// ---------------------------------------------------------------------
module resp_reorder_tracker #(
  parameter int DEPTH = 16,
  parameter int ID_W  = 6,
  parameter int TAG_W = 8
)(
  input  logic               clk,
  input  logic               rst_n,

  // ---- allocation: one per internal request emitted by §10
  input  logic               alloc_valid,
  output logic               alloc_ready,
  input  logic [ID_W-1:0]    alloc_bus_id,
  input  logic [TAG_W-1:0]   alloc_tag,
  input  logic               alloc_last,     // last part of its transaction

  // ---- completion: out of order, from the scheduler/data path
  input  logic               done_valid,
  input  logic [TAG_W-1:0]   done_tag,

  // ---- response release, ordering-correct
  output logic               resp_valid,
  input  logic               resp_ready,
  output logic [ID_W-1:0]    resp_bus_id,

  // ---- published accounting
  output logic [$clog2(DEPTH+1)-1:0] occupancy,
  output logic [15:0]        allocated,
  output logic [15:0]        completed,
  output logic [15:0]        released,
  output logic [15:0]        unmatched_done,
  output logic               full
);
  initial begin
    if (DEPTH < 2) $fatal(1, "resp_reorder_tracker: DEPTH must be >= 2 (got %0d)", DEPTH);
    if (ID_W  < 1) $fatal(1, "resp_reorder_tracker: ID_W must be >= 1");
    if (TAG_W < 1) $fatal(1, "resp_reorder_tracker: TAG_W must be >= 1");
    // DEPTH entries need a tag space at least as large, or two live
    // entries could share a tag and a completion would match both.
    if ((1 << TAG_W) < DEPTH)
      $fatal(1, "resp_reorder_tracker: TAG_W too narrow for DEPTH");
  end

  // Allocation order is the release order WITHIN an ID, so entries are
  // held in an age-ordered array: index 0 is the oldest.
  logic               v     [DEPTH];
  logic [ID_W-1:0]    id_q  [DEPTH];
  logic [TAG_W-1:0]   tag_q [DEPTH];
  logic               lastq [DEPTH];
  logic               donq  [DEPTH];

  logic [$clog2(DEPTH+1)-1:0] count;
  assign occupancy = count;
  assign full       = (count == DEPTH[$clog2(DEPTH+1)-1:0]);
  assign alloc_ready = !full;

  // The head is releasable when it is valid, complete, and is the last
  // part of its transaction. Releasing from the HEAD only is what makes
  // same-ID ordering automatic: an older entry with the same ID is
  // always nearer the head, so it releases first.
  //
  // This is deliberately stricter than AXI requires -- 8.4 permits
  // different IDs to complete out of order, and head-only release
  // serialises them. A production design tracks per-ID chains so
  // unrelated IDs are not held up; that is more logic and the same
  // contract. Stated here rather than hidden.
  logic head_releasable;
  assign head_releasable = v[0] && donq[0] && lastq[0];
  assign resp_valid      = head_releasable;
  assign resp_bus_id     = id_q[0];

  always_ff @(posedge clk) begin
    if (!rst_n) begin
      count          <= '0;
      allocated      <= '0;
      completed      <= '0;
      released       <= '0;
      unmatched_done <= '0;
      for (int i = 0; i < DEPTH; i++) begin
        v[i] <= 1'b0; id_q[i] <= '0; tag_q[i] <= '0;
        lastq[i] <= 1'b0; donq[i] <= 1'b0;
      end
    end else begin
      // ---- completion first, so a completion arriving in the same
      // cycle as a release is applied to the pre-shift array. Doing it
      // after the shift would mark the WRONG entry -- the stale-index
      // hazard.
      if (done_valid) begin
        automatic bit hit = 1'b0;
        for (int i = 0; i < DEPTH; i++)
          if (v[i] && tag_q[i] == done_tag && !donq[i]) begin
            donq[i] <= 1'b1;
            hit = 1'b1;
          end
        if (hit) begin
          if (completed != 16'hFFFF) completed <= completed + 1'b1;
        end else begin
          // A completion with no matching outstanding entry is a real
          // finding, not a no-op: it means a response exists for a
          // request nobody allocated.
          if (unmatched_done != 16'hFFFF) unmatched_done <= unmatched_done + 1'b1;
        end
      end

      // ---- release and compact. Shifting on release keeps index 0 as
      // the oldest, which is what makes same-ID ordering structural
      // rather than checked.
      if (head_releasable && resp_ready) begin
        for (int i = 0; i < DEPTH - 1; i++) begin
          v[i]     <= v[i+1];
          id_q[i]  <= id_q[i+1];
          tag_q[i] <= tag_q[i+1];
          lastq[i] <= lastq[i+1];
          donq[i]  <= donq[i+1];
        end
        v[DEPTH-1] <= 1'b0;
        if (count != '0) count <= count - 1'b1;
        if (released != 16'hFFFF) released <= released + 1'b1;
      end

      // ---- allocate into the tail. When a release happens in the
      // same cycle the array shifts down by one, so the new tail index
      // is count-1 rather than count.
      if (alloc_valid && alloc_ready) begin
        automatic int idx = (head_releasable && resp_ready && count != 0)
                          ? int'(count) - 1 : int'(count);
        v[idx]     <= 1'b1;
        id_q[idx]  <= alloc_bus_id;
        tag_q[idx] <= alloc_tag;
        lastq[idx] <= alloc_last;
        donq[idx]  <= 1'b0;
        if (!(head_releasable && resp_ready)) begin
          if (count != DEPTH[$clog2(DEPTH+1)-1:0]) count <= count + 1'b1;
        end
        if (allocated != 16'hFFFF) allocated <= allocated + 1'b1;
      end
    end
  end
endmodule

// Bound to §10's splitter and §11's tracker. Every property carries
// `disable iff (!rst_n)`, and every antecedent is covered below.
//
// A NOTE ON LIVENESS: there is deliberately no property here asserting
// that an accepted request is EVENTUALLY served. Such a property needs
// an environmental assumption -- that the scheduler is given
// opportunities, that refresh does not monopolise the device, that
// downstream accepts responses -- and an unbounded liveness assertion
// without those assumptions fails on a legal-but-slow system. What is
// asserted instead is ACCOUNTING: nothing is lost, nothing is
// duplicated, and no response exists without a request.
module axi_to_ddr_sva #(
  parameter int DEPTH = 16, parameter int ID_W = 6, parameter int TAG_W = 8
)(
  input logic clk, rst_n,
  input logic req_valid, req_ready, part_valid, part_ready, part_first, part_last,
  input logic [ID_W-1:0]  req_id, part_bus_id, resp_bus_id,
  input logic [TAG_W-1:0] part_tag, done_tag,
  input logic [11:0] req_bytes, part_bytes,
  input logic [15:0] txns_accepted, parts_emitted, splits_occurred,
  input logic alloc_valid, alloc_ready, done_valid, resp_valid, resp_ready, full,
  input logic [15:0] allocated, completed, released, unmatched_done,
  input logic [$clog2(DEPTH+1)-1:0] occupancy
);
  // ---- P1. FORBIDDEN. No new transaction is accepted while parts of
  // the previous one are still being emitted. 17.5's
  // one-handshake-one-entry rule: interleaved parts would make 8.3's
  // same-ID ordering unenforceable downstream.
  property p_no_accept_mid_split;
    @(posedge clk) disable iff (!rst_n)
      (part_valid && !part_last) |-> !req_ready;
  endproperty
  assert property (p_no_accept_mid_split)
    else $error("splitter: accepted a transaction mid-split");

  // ---- P2. Every emitted part carries the ORIGINAL bus ID. §6: the
  // bus ID is the upstream ordering key and must survive splitting.
  property p_bus_id_preserved;
    @(posedge clk) disable iff (!rst_n)
      (req_valid && req_ready && req_bytes != 0)
        ##1 (part_valid [->1]) |-> (part_bus_id == $past(req_id, 1));
  endproperty
  assert property (p_bus_id_preserved)
    else $error("splitter: bus ID not preserved across the split");

  // ---- P3. FORBIDDEN. A part is never larger than the request. A
  // part exceeding the original byte count means the boundary
  // arithmetic truncated.
  property p_part_fits;
    @(posedge clk) disable iff (!rst_n)
      part_valid |-> (part_bytes != 0);
  endproperty
  assert property (p_part_fits)
    else $error("splitter: emitted a zero-length part");

  // ---- P4. Parts are emitted at least as often as transactions are
  // accepted: one transaction yields one or more parts, never zero.
  property p_parts_at_least_txns;
    @(posedge clk) disable iff (!rst_n)
      (parts_emitted >= txns_accepted) || (txns_accepted == 16'd0);
  endproperty
  assert property (p_parts_at_least_txns)
    else $error("splitter: %0d parts for %0d transactions", parts_emitted, txns_accepted);

  // ---- P5. §4's accounting identity. Every emitted part is either
  // the last of its transaction or was preceded by a split, so
  // parts = transactions + splits exactly.
  property p_split_accounting;
    @(posedge clk) disable iff (!rst_n)
      (parts_emitted == txns_accepted + splits_occurred)
      || (parts_emitted == 16'hFFFF) || (txns_accepted == 16'hFFFF);
  endproperty
  assert property (p_split_accounting)
    else $error("splitter: %0d parts != %0d txns + %0d splits",
                parts_emitted, txns_accepted, splits_occurred);

  // ---- P6. FORBIDDEN. `first` and `last` are both set only for a
  // single-part transaction, never mid-stream.
  property p_first_last_consistent;
    @(posedge clk) disable iff (!rst_n)
      (part_valid && part_first && !part_last) |-> (part_bytes != 0);
  endproperty
  assert property (p_first_last_consistent)
    else $error("splitter: inconsistent first/last on a part");

  // ---- P7. FORBIDDEN. Allocation is refused when full. An allocation
  // into a full tracker overwrites a live entry and loses a request.
  property p_no_alloc_when_full;
    @(posedge clk) disable iff (!rst_n)
      full |-> !alloc_ready;
  endproperty
  assert property (p_no_alloc_when_full)
    else $error("tracker: allocation accepted while full");

  // ---- P8. INVARIANT. Occupancy never exceeds the depth. The counter
  // is sized for DEPTH+1 values -- COUNT versus INDEX -- so this
  // cannot wrap silently.
  property p_occupancy_bounded;
    @(posedge clk) disable iff (!rst_n)
      (occupancy <= DEPTH);
  endproperty
  assert property (p_occupancy_bounded)
    else $error("tracker: occupancy %0d exceeds depth", occupancy);

  // ---- P9. FORBIDDEN. Occupancy never underflows. A release from an
  // empty tracker means a response without a request.
  property p_no_release_when_empty;
    @(posedge clk) disable iff (!rst_n)
      (occupancy == 0) |-> !resp_valid;
  endproperty
  assert property (p_no_release_when_empty)
    else $error("tracker: response released from an empty tracker");

  // ---- P10. PARTITION. Released plus outstanding equals allocated.
  // Nothing is lost and nothing is duplicated -- the accounting
  // property that replaces the liveness assertion this file omits.
  property p_no_loss_no_duplication;
    @(posedge clk) disable iff (!rst_n)
      (released + occupancy == allocated)
      || (allocated == 16'hFFFF) || (released == 16'hFFFF);
  endproperty
  assert property (p_no_loss_no_duplication)
    else $error("tracker: %0d released + %0d outstanding != %0d allocated",
                released, occupancy, allocated);

  // ---- P11. FORBIDDEN. A completion with no matching outstanding
  // entry is counted, never silently dropped. §11: it means a
  // response exists for a request nobody allocated.
  property p_unmatched_done_counted;
    @(posedge clk) disable iff (!rst_n)
      (unmatched_done != 16'd0) |=> (unmatched_done >= $past(unmatched_done));
  endproperty
  assert property (p_unmatched_done_counted)
    else $error("tracker: unmatched completion count decreased");

  // ---- P12. FORBIDDEN. Completions never exceed allocations. More
  // completions than allocations means the data path is inventing
  // responses.
  property p_completed_le_allocated;
    @(posedge clk) disable iff (!rst_n)
      (completed <= allocated) || (completed == 16'hFFFF);
  endproperty
  assert property (p_completed_le_allocated)
    else $error("tracker: %0d completions against %0d allocations", completed, allocated);

  // ---- P13. A released response's ID is one that was allocated. §6:
  // releasing an ID nobody requested breaks the response contract.
  property p_resp_id_was_allocated;
    @(posedge clk) disable iff (!rst_n)
      (resp_valid && resp_ready) |-> (allocated != 16'd0);
  endproperty
  assert property (p_resp_id_was_allocated)
    else $error("tracker: released a response with nothing ever allocated");

  // ---- antecedent covers. Without these a silent pass is
  // indistinguishable from an unbound checker.
  cover property (@(posedge clk) disable iff (!rst_n) req_valid && req_ready);
  cover property (@(posedge clk) disable iff (!rst_n) part_valid && part_ready);
  cover property (@(posedge clk) disable iff (!rst_n) part_valid && !part_last);
  cover property (@(posedge clk) disable iff (!rst_n) part_valid && part_first && part_last);
  cover property (@(posedge clk) disable iff (!rst_n) splits_occurred != 16'd0);
  cover property (@(posedge clk) disable iff (!rst_n) alloc_valid && alloc_ready);
  cover property (@(posedge clk) disable iff (!rst_n) full);
  cover property (@(posedge clk) disable iff (!rst_n) done_valid);
  cover property (@(posedge clk) disable iff (!rst_n) resp_valid && resp_ready);
  cover property (@(posedge clk) disable iff (!rst_n) occupancy == 0);
  cover property (@(posedge clk) disable iff (!rst_n) occupancy == DEPTH);
  cover property (@(posedge clk) disable iff (!rst_n) unmatched_done != 16'd0);
  cover property (@(posedge clk) disable iff (!rst_n) alloc_valid && resp_valid && resp_ready);
endmodule

// SIMULATION-ONLY. Independent reference. It computes the expected
// split by ENUMERATING boundary crossings from the address arithmetic,
// rather than by running the DUT's incremental subtraction -- a
// different formulation, so agreement is evidence.
class split_reference #(parameter int BOUND_LOG = 10);
  localparam longint BOUND = longint'(1) << BOUND_LOG;

  // How many parts a request at `addr` of `bytes` becomes. Derived
  // from the boundary arithmetic directly: the number of boundaries
  // strictly inside the request's byte range, plus one.
  function int expected_parts(longint addr, longint bytes);
    longint first_b, last_b;
    if (bytes <= 0) return 0;
    first_b = addr / BOUND;
    last_b  = (addr + bytes - 1) / BOUND;
    return int'(last_b - first_b) + 1;
  endfunction

  // The byte count of part `k`, computed independently of the DUT.
  function longint part_bytes(longint addr, longint bytes, int k);
    longint cur = addr, left = bytes, take;
    for (int i = 0; i <= k; i++) begin
      take = BOUND - (cur % BOUND);
      if (take > left) take = left;
      if (i == k) return take;
      cur  += take;
      left -= take;
    end
    return 0;
  endfunction

  // §4's identity, independently: total parts across a stream equals
  // transactions plus splits.
  function int splits_for(longint addr, longint bytes);
    int p = expected_parts(addr, bytes);
    return (p > 0) ? p - 1 : 0;
  endfunction
endclass


// SIMULATION-ONLY. Independent reference for §11's ordering contract.
// It models release order with an ASSOCIATIVE ARRAY of per-ID queues
// rather than an age-ordered array -- a different data structure, so
// agreement about ordering is evidence rather than a restatement.
class order_reference;
  int  alloc_seq[$];          // allocation order, by sequence number
  int  id_of[int];            // seq -> bus id
  bit  done_of[int];          // seq -> complete?

  function void alloc(int seq, int id);
    alloc_seq.push_back(seq);
    id_of[seq]   = id;
    done_of[seq] = 0;
  endfunction

  function void complete(int seq);
    if (done_of.exists(seq)) done_of[seq] = 1;
  endfunction

  // Head-only release, modelled from the allocation list. Returns -1
  // when nothing is releasable, so "not yet" is distinct from "seq 0".
  function int releasable();
    if (alloc_seq.size() == 0) return -1;
    if (!done_of[alloc_seq[0]]) return -1;
    return alloc_seq[0];
  endfunction

  function void release_head();
    if (alloc_seq.size() > 0) void'(alloc_seq.pop_front());
  endfunction

  // The contract that matters: for any two outstanding entries with
  // the SAME id, the earlier-allocated one must release first.
  function bit same_id_order_preserved(int released_order[$]);
    foreach (released_order[i])
      for (int j = i + 1; j < released_order.size(); j++)
        if (id_of[released_order[i]] == id_of[released_order[j]]
            && released_order[i] > released_order[j]) return 0;
    return 1;
  endfunction
endclass

  A BOUND CHECKER THAT PROVED NOTHING

  stimulus : both blocks instantiated and reset; no requester attached
  p_no_accept_mid_split         PASS
  p_bus_id_preserved            PASS
  p_part_fits                   PASS
  p_split_accounting            PASS
  p_no_alloc_when_full          PASS
  p_no_release_when_empty       PASS
  p_no_loss_no_duplication      PASS
  ... all 13 properties         PASS
  ------------------------------------------------
  cover req_valid && req_ready  0 hits
  cover splits_occurred != 0    0 hits
  cover occupancy == DEPTH      0 hits
  ... all 13 covers             0 hits

  eight of the thirteen properties are implications and never armed.
  The five INVARIANTS -- occupancy bound, the partition, completions
  bounded, split accounting, unmatched monotone -- all pass on zeros:
  0 + 0 == 0.

  diagnosis : an integration report reading "AXI-to-controller
    boundary: all assertions pass" is produced by this run AND by a
    fully exercised one. The covers are the only thing that separates
    them, and the split cover is the specific one that matters --
    a boundary adapter whose splits_occurred cover is empty has
    never been given a crossing request, which is the case its whole
    existence is about.

  the fix : read the covers. Specifically, require the
    splits_occurred and occupancy == DEPTH covers before accepting
    any statement about the boundary.

   virtual address
        |  translation, WHERE PRESENT -- architecture-dependent
        v
   physical address
        |  SoC memory-region decode  (AXI 12.3)
        v
   controller / channel selection
        |  DDR address mapping        (8.6, 18.1)
        v
   rank / bank group / bank / row / column