DDR vs HBM

   STAGE ONE -- FEASIBILITY (a geometry question)
     can the chosen SURFACE host enough connections to carry the
     required bandwidth, at a manufacturable pitch, for a die of
     the size the capability requires?

     if no: the technology is not slow for this application. It is
     IMPOSSIBLE for it, and no signalling improvement changes that
     -- §4 is why the exponent cannot be argued away.

   STAGE TWO -- COST (everything else)
     interposer, assembly, yield, repairability, capacity
     granularity, and the controller replication of §7.

   connections per unit of capability  =  4L / L²  =  4 / L

   DERIVED, recomputed:
       307.2 GB/s  /  1024 signals   =  0.300 GB/s per signal
   and per-pin rate:
       307.2e9 B/s x 8 bits/B / 1024 =  2.40 Gbit/s per signal

   bandwidth       =  W x R / 8   bytes per second
   per signal      =  (W x R / 8) / W  =  R / 8   bytes per second

   DERIVED, and read it before substituting anything: the per-signal
   figure does not depend on W at all. It is the TRANSFER RATE
   divided by eight, and nothing else.

   ILLUSTRATIVE R = 3200 MT/s:
       per signal  =  3200e6 / 8  =  0.400 GB/s per signal
       per-pin rate = 3.20 Gbit/s per signal

   INPUTS
     B_req    required bandwidth
     L        die side implied by the capability to be fed
     pitch    manufacturable connection pitch on the chosen surface
     r_sig    achievable per-signal rate on that surface
     f_sig    fraction of connections that carry a SIGNAL rather than
              power or ground -- 26.2 §6 owns that this fraction is
              well below one, and this chapter does not invent it

   PERIMETER SURFACE
     available  =  (4 x L / pitch) x f_sig
     carried    =  available x r_sig
     FEASIBLE iff carried >= B_req

   FACE SURFACE
     available  =  (L^2 / pitch^2) x f_sig
     carried    =  available x r_sig
     FEASIBLE iff carried >= B_req

   DERIVED, and the whole content is the exponent: the perimeter's
   available count is LINEAR in L and the face's is QUADRATIC. So
   the face's advantage GROWS with the die, and the technology
   becomes more attractive exactly as the problem gets harder.

   DERIVED, reusing 31.1 §10's per-bank state figure of 30 bits
   (row_open, row_known, row_idx, since_act, since_pre) and an
   ILLUSTRATIVE 8 banks per channel:

     per channel   =  8 banks x 30 bits  =  240 bits

     1 channel     =    240 bits
     8 channels    =  1,920 bits
    16 channels    =  3,840 bits

   plus, and this is the term that is NOT linear:

     a cross-channel distributor and its balance accounting, whose
     cost grows with the number of destinations it must choose
     among -- and 26.1 §10's pseudo-channel arbiter exists because
     the channels are SEMI-independent, so the shared parts need
     arbitrating rather than merely replicating.

   a request's burst covers  BURST_SPAN  contiguous bytes.
   the channel decode picks a channel from some address field.
   the field's weight determines the INTERLEAVE GRANULARITY --
   how many contiguous bytes land on one channel before the
   next channel takes over.

   the requirement, stated as an inequality:

       INTERLEAVE_GRAN  >=  BURST_SPAN

   if it holds : every burst lies entirely within one channel.
   if it fails : a single burst STRADDLES two channels, and one
                 request becomes two channel transactions that
                 must be split, tracked and rejoined.

// ---------------------------------------------------------------------
// channel_decode_replicate -- the comparative block of §10.
//
// CLASSIFICATION: synthesisable, ILLUSTRATIVE parameter values, and
// CORRECT as written. The intentionally defective block is §11.
//
// WHAT IT IS: an address decoder plus per-channel obligation state,
// parameterised on the channel count. NUM_CH = 1 or 2 is the
// few-wide configuration; 8 or 16 the many-narrow one. §7's
// multiplication is the `for` loop over channels; §8's inequality is
// the elaboration guard.
//
// WHY IT EXISTS HERE: §7 claims the difficult decision MOVES
// UPSTREAM from the scheduler to the distributor as the channel
// count rises. This block is both halves of that claim in one place,
// so the reader can see that the per-channel state is a loop and the
// decode is a design decision.
//
// HOW TO RUN IT: elaborate at NUM_CH = 1 and at NUM_CH = 16 and
// compare state-element counts; then present a request whose burst
// span exceeds the interleave granularity.
// EXPECTED RESULT: the second case is REFUSED AT ELABORATION by the
// guard below, which is the correct place to refuse it -- §8's
// inequality is a static property of the configuration, not a
// runtime condition.
//
// SYNTHESIS: NUM_CH x BANKS_PER_CH per-bank records, plus a decode
// that is combinational and a one-hot channel select.
//
// LIMITATIONS: models the DECODE and the per-channel OBLIGATION
// STATE. It does not model the shared command bus between the two
// halves of a channel -- 26.1 §5 owns why the halves share it and
// 26.1 §10 owns the arbiter that follows, and duplicating that here
// would rebuild another chapter's subject. Balance across channels
// is measured, not enforced: §13.
// ---------------------------------------------------------------------
module channel_decode_replicate #(
  parameter int NUM_CH          = 16,
  parameter int BANKS_PER_CH    = 8,
  parameter int ADDR_W          = 34,
  parameter int ROW_W           = 15,

  // §8's two quantities. BURST_SPAN is the contiguous byte run one
  // burst covers; INTERLEAVE_GRAN is how many contiguous bytes land
  // on one channel before the next takes over.
  parameter int BURST_SPAN      = 64,
  parameter int INTERLEAVE_GRAN = 256,

  // ILLUSTRATIVE timing. 14.1 to 14.3 own the real values.
  parameter int TRCD            = 14,
  parameter int TRP             = 14,
  parameter int TRAS            = 34,

  // COUNT, not INDEX: each counter must REPRESENT its threshold, so
  // it needs $clog2(threshold + 1) bits. TRAS is the largest.
  parameter int CNT_W           = $clog2(TRAS + 1),
  parameter int CH_W            = (NUM_CH > 1) ? $clog2(NUM_CH) : 1,
  parameter int BANK_W          = $clog2(BANKS_PER_CH),

  // The bit position the channel field starts at. DERIVED from the
  // granularity rather than chosen, so the two cannot disagree.
  parameter int CH_SHIFT        = $clog2(INTERLEAVE_GRAN)
)(
  input  logic                clk,
  input  logic                rst_n,

  input  logic                req_valid,
  input  logic [ADDR_W-1:0]   req_addr,
  input  logic [ROW_W-1:0]    req_row,

  output logic [CH_W-1:0]     sel_ch,
  output logic [NUM_CH-1:0]   ch_onehot,
  output logic                straddles,
  output logic [NUM_CH-1:0]   ch_legal,
  output logic [15:0]         state_bits_reported
);
  initial begin
    if (NUM_CH < 1) $fatal(1, "channel_decode_replicate: NUM_CH >= 1");
    if (NUM_CH > 1 && (NUM_CH & (NUM_CH - 1)) != 0)
      $fatal(1, "channel_decode_replicate: NUM_CH must be a power of two for a bit-field decode");
    if (BURST_SPAN < 1) $fatal(1, "channel_decode_replicate: BURST_SPAN >= 1");
    if ((INTERLEAVE_GRAN & (INTERLEAVE_GRAN - 1)) != 0)
      $fatal(1, "channel_decode_replicate: INTERLEAVE_GRAN must be a power of two");

    // §8's inequality, enforced AT ELABORATION. This is the correct
    // place for it: the relationship between the burst span and the
    // interleave granularity is a static property of the
    // configuration, so a design that violates it should not
    // elaborate rather than failing a runtime check on the one
    // access that happens to straddle.
    if (INTERLEAVE_GRAN < BURST_SPAN)
      $fatal(1, "channel_decode_replicate: INTERLEAVE_GRAN (%0d) < BURST_SPAN (%0d): a burst would straddle two channels (§8)",
             INTERLEAVE_GRAN, BURST_SPAN);

    if (CH_SHIFT + CH_W > ADDR_W)
      $fatal(1, "channel_decode_replicate: channel field falls outside the address");
  end

  // ---- The decode. One line of logic, and §7's argument is that
  //      this line is where the difficulty went.
  generate
  if (NUM_CH > 1) begin : g_multi
    assign sel_ch = req_addr[CH_SHIFT + CH_W - 1 : CH_SHIFT];
  end else begin : g_single
    assign sel_ch = '0;
  end
  endgenerate

  always_comb begin
    ch_onehot = '0;
    if (req_valid) ch_onehot[sel_ch] = 1'b1;
  end

  // ---- The straddle check, retained as a RUNTIME output even though
  //      the elaboration guard makes it unreachable. It is not
  //      redundant: it is the observable that proves the guard was
  //      the right guard, and 30.5 §11's lesson is that a guard which
  //      another guard always shadows is UNTESTED rather than
  //      working. §14's cover watches this signal for exactly that
  //      reason.
  logic [ADDR_W-1:0] span_end;
  always_comb begin
    span_end  = req_addr + BURST_SPAN[ADDR_W-1:0] - 1;
    straddles = req_valid &&
                (span_end[CH_SHIFT + CH_W - 1 : CH_SHIFT] != sel_ch);
  end

  // ===================================================================
  // §7's MULTIPLICATION. The obligations are identical in kind to
  // 31.1 §5's thirteen; what changes is that there are NUM_CH of
  // every one of them. Written as a loop precisely to make the point
  // that replication is CHEAP TO WRITE and expensive to verify.
  // ===================================================================
  logic             row_open  [NUM_CH][BANKS_PER_CH];
  logic             row_known [NUM_CH][BANKS_PER_CH];
  logic [ROW_W-1:0] row_idx   [NUM_CH][BANKS_PER_CH];
  logic [CNT_W-1:0] since_act [NUM_CH][BANKS_PER_CH];
  logic [CNT_W-1:0] since_pre [NUM_CH][BANKS_PER_CH];

  logic [BANK_W-1:0] req_bank;
  assign req_bank = req_addr[CH_SHIFT + CH_W + BANK_W - 1 : CH_SHIFT + CH_W];

  always_ff @(posedge clk) begin
    if (!rst_n) begin
      for (int c = 0; c < NUM_CH; c++)
        for (int b = 0; b < BANKS_PER_CH; b++) begin
          row_open[c][b]  <= 1'b0;
          row_known[c][b] <= 1'b0;
          row_idx[c][b]   <= '0;
          since_act[c][b] <= '0;
          since_pre[c][b] <= '0;
        end
    end else begin
      for (int c = 0; c < NUM_CH; c++)
        for (int b = 0; b < BANKS_PER_CH; b++) begin
          if (since_act[c][b] != {CNT_W{1'b1}}) since_act[c][b] <= since_act[c][b] + 1'b1;
          if (since_pre[c][b] != {CNT_W{1'b1}}) since_pre[c][b] <= since_pre[c][b] + 1'b1;
        end
      // Only the selected channel's record advances on a command. The
      // per-channel independence of the OBLIGATIONS is real even
      // though the channels are only SEMI-independent at the command
      // bus (26.1 §6) -- the timing state is per resource and the
      // resources are distinct.
      if (req_valid && ch_legal[sel_ch]) begin
        row_open[sel_ch][req_bank]  <= 1'b1;
        row_known[sel_ch][req_bank] <= 1'b1;
        row_idx[sel_ch][req_bank]   <= req_row;
        since_act[sel_ch][req_bank] <= '0;
      end
    end
  end

  // ---- Per-channel legality. NUM_CH independent copies of the same
  //      maximum-over-rules test that 13.3 owns.
  always_comb begin
    for (int c = 0; c < NUM_CH; c++) begin
      ch_legal[c] = row_open[c][req_bank]
                  ? (since_act[c][req_bank] >= TRCD[CNT_W-1:0])
                  : (since_pre[c][req_bank] >= TRP[CNT_W-1:0]);
    end
  end

  // §7's count, reported so the comparison is measured and not
  // claimed. 30 bits per bank, from 31.1 §10's figure.
  assign state_bits_reported = NUM_CH * BANKS_PER_CH * 30;
endmodule

// ---------------------------------------------------------------------
// channel_distributor -- INTENTIONALLY DEFECTIVE, for review (§11).
//
// CLASSIFICATION: synthesisable, ILLUSTRATIVE, and CONTAINS A BUG.
//
// WHAT IT IS MEANT TO DO: the five-clause contract above -- spread a
// request stream across NUM_CH channels, splitting any request whose
// burst would straddle a channel boundary.
//
// WHY IT EXISTS HERE: §8 establishes that the interleave-versus-burst
// inequality holds WITHOUT ANYONE CHECKING IT at the few-wide
// configuration and becomes a real constraint at the many-narrow
// one. This block is that configuration dependence, and it is the
// third instance in this module of the same bug class: code correct
// under one parameterisation, reused under another without
// re-deriving the requirement (31.1 §12, 31.2 §12).
//
// HOW TO RUN IT: elaborate with NUM_CH = 16 and INTERLEAVE_GRAN = 32
// against BURST_SPAN = 64, then present an aligned request.
// EXPECTED RESULT under clause 3: the request is SPLIT, and
// `split_req` is asserted.
// EXPECTED TRACE: a burst covering bytes 0 to 63 with a 32-byte
// granularity must produce two sub-requests, to channels 0 and 1.
//
// SYNTHESIS: one combinational decode plus a one-hot expander.
//
// LIMITATIONS: models the DECODE only. Return-path rejoining is the
// other half of clause 3 and is out of scope here -- 10.5 §9 owns
// the association problem -- and that omission is STATED rather than
// hidden. It is not what the bug is.
// ---------------------------------------------------------------------
module channel_distributor #(
  parameter int NUM_CH          = 16,
  parameter int ADDR_W          = 34,
  parameter int BURST_SPAN      = 64,
  parameter int INTERLEAVE_GRAN = 32,
  parameter int CH_W            = (NUM_CH > 1) ? $clog2(NUM_CH) : 1,
  parameter int CH_SHIFT        = $clog2(INTERLEAVE_GRAN)
)(
  input  logic               clk,
  input  logic               rst_n,

  input  logic               req_valid,
  input  logic [ADDR_W-1:0]  req_addr,

  output logic [CH_W-1:0]    sel_ch,
  output logic [NUM_CH-1:0]  ch_onehot,
  output logic               split_req,
  output logic [7:0]         sub_req_count
);
  initial begin
    if (NUM_CH < 1) $fatal(1, "channel_distributor: NUM_CH >= 1");
    if ((INTERLEAVE_GRAN & (INTERLEAVE_GRAN - 1)) != 0)
      $fatal(1, "channel_distributor: INTERLEAVE_GRAN must be a power of two");
    if (CH_SHIFT + CH_W > ADDR_W)
      $fatal(1, "channel_distributor: channel field falls outside the address");
    // NOTE: §10's guard on INTERLEAVE_GRAN >= BURST_SPAN is ABSENT
    // here, and deliberately so -- this block is supposed to SUPPORT
    // the straddling configuration by splitting (clause 3), so
    // refusing to elaborate would defeat its purpose. §12 is about
    // what was removed along with it.
  end

  // Clause 1 and 4: decode to one channel, one-hot.
  assign sel_ch = (NUM_CH > 1) ? req_addr[CH_SHIFT + CH_W - 1 : CH_SHIFT]
                               : '0;

  always_comb begin
    ch_onehot = '0;
    if (req_valid) ch_onehot[sel_ch] = 1'b1;
  end

  // Clause 3: decide whether a split is needed.
  assign split_req     = 1'b0;                          // <-- THE DEFECT
  assign sub_req_count = req_valid ? 8'd1 : 8'd0;
endmodule

   ILLUSTRATIVE NUM_CH = 16, INTERLEAVE_GRAN = 32, BURST_SPAN = 64.
   CH_SHIFT = 5, CH_W = 4, so the channel field is addr[8:5].

   a request at address 0, burst covering bytes 0..63:

       byte  0..31  ->  addr[8:5] = 0  ->  channel 0
       byte 32..63  ->  addr[8:5] = 1  ->  channel 1

   contract clause 3 : SPLIT into two sub-requests
   this block        : sel_ch = 0, sub_req_count = 1, split_req = 0

   so channel 0 is asked for 64 bytes. It has 32. It returns 64 --
   the second 32 coming from whatever is at the next address WITHIN
   channel 0, which is byte offset 512 of the interleaved space.

   the requester receives 64 contiguous-looking bytes of which the
   second half belongs to a different address entirely.

  // CORRECTED. Clause 3: compute the channel of the burst's LAST
  // byte as well as its first, and split when they differ. Note that
  // the general case can span MORE than two channels when the burst
  // span exceeds twice the granularity, so the count is derived
  // rather than fixed at two -- a two-way split would be a second
  // bug of the same family, right for one ratio and wrong for
  // another.
  logic [ADDR_W-1:0] span_end;
  logic [CH_W-1:0]   end_ch;
  always_comb begin
    span_end = req_addr + BURST_SPAN[ADDR_W-1:0] - 1;
    end_ch   = span_end[CH_SHIFT + CH_W - 1 : CH_SHIFT];

    split_req = req_valid && (end_ch != sel_ch);

    // The number of channels the burst touches. DERIVED from the
    // aligned span rather than from the channel indices, because the
    // indices WRAP and a difference computed on them is wrong at the
    // wrap point -- which would be a third bug of the same family.
    sub_req_count = req_valid
      ? 8'( ((req_addr[CH_SHIFT-1:0] + BURST_SPAN - 1) >> CH_SHIFT) + 1 )
      : 8'd0;
  end

// ---------------------------------------------------------------------
// channel_balance_monitor -- verification/telemetry, CORRECT as written.
//
// CLASSIFICATION: synthesisable telemetry. Drives nothing.
//
// WHAT IT DOES: counts requests per channel over a window and
// reports the imbalance, plus how many cycles each channel was
// blocked while another had work available.
//
// WHY IT EXISTS HERE: §7 argues the distributor is the new hard
// problem, and §11's defect is one way it goes wrong. This block
// catches the OTHER way, which produces no wrong data at all: a
// decode that is correct per request and systematically unbalanced
// across the stream, so the many-channel memory delivers the
// bandwidth of a few-channel one. 30.8's ladder names that exactly
// -- rung 1 moved and rung 4 did not.
//
// HOW TO RUN IT: run the real access pattern and read `imbalance`.
// EXPECTED RESULT: a stride that is a multiple of NUM_CH x
// INTERLEAVE_GRAN concentrates on one channel and imbalance
// approaches its maximum -- 18.2's mapping-for-performance problem
// at channel granularity.
//
// SYNTHESIS: NUM_CH counters plus a max/min tracker. No divider.
//
// LIMITATIONS: measures DISTRIBUTION, not correctness. §11's defect
// produces a perfectly balanced stream of wrong data, so this block
// cannot see it -- which is why §14 asserts correctness separately
// and this block's LIMITATIONS say so rather than implying coverage
// it does not give (27.3's independence discipline).
// ---------------------------------------------------------------------
module channel_balance_monitor #(
  parameter int NUM_CH = 16,
  parameter int WIN    = 65536,
  // COUNT, not INDEX: each per-channel counter must be able to
  // represent a window in which EVERY request went to one channel,
  // so it needs $clog2(WIN + 1) bits. Sized $clog2(WIN / NUM_CH) --
  // the "fair share" -- it would saturate in exactly the imbalanced
  // case it exists to detect, and report perfect balance.
  parameter int CNT_W  = $clog2(WIN + 1)
)(
  input  logic                clk,
  input  logic                rst_n,

  input  logic                req_fire,
  input  logic [$clog2(NUM_CH > 1 ? NUM_CH : 2)-1:0] req_ch,
  input  logic [NUM_CH-1:0]   ch_has_work,
  input  logic [NUM_CH-1:0]   ch_blocked,
  input  logic                win_tick,

  output logic [CNT_W-1:0]    r_max_ch,
  output logic [CNT_W-1:0]    r_min_ch,
  output logic [CNT_W-1:0]    r_imbalance,
  output logic [CNT_W-1:0]    r_starved_cycles,
  output logic                result_valid
);
  initial begin
    if (NUM_CH < 1) $fatal(1, "channel_balance_monitor: NUM_CH >= 1");
    if (WIN < NUM_CH)
      $fatal(1, "channel_balance_monitor: WIN must be >= NUM_CH or balance is meaningless");
  end

  logic [CNT_W-1:0] cnt [NUM_CH];
  logic [CNT_W-1:0] starved;

  always_ff @(posedge clk) begin
    if (!rst_n) begin
      for (int c = 0; c < NUM_CH; c++) cnt[c] <= '0;
      starved          <= '0;
      r_max_ch         <= '0;
      // AND-accumulator discipline: a minimum tracker must start at
      // all-ones or the first sample never wins and the reported
      // minimum stays zero forever -- which would report maximum
      // imbalance on every window regardless of the traffic.
      r_min_ch         <= '1;
      r_imbalance      <= '0;
      r_starved_cycles <= '0;
      result_valid     <= 1'b0;
    end else if (win_tick) begin
      begin
        logic [CNT_W-1:0] mx, mn;
        mx = '0;
        mn = '1;
        for (int c = 0; c < NUM_CH; c++) begin
          if (cnt[c] > mx) mx = cnt[c];
          if (cnt[c] < mn) mn = cnt[c];
        end
        r_max_ch    <= mx;
        r_min_ch    <= mn;
        // Reported as a DIFFERENCE with both endpoints, not as a
        // ratio. 27.5 refuses a single percentage and 30.8 §11
        // requires a derived statistic's range to be asserted; a
        // difference with its endpoints lets the consumer see the
        // denominator and own the rounding.
        r_imbalance <= mx - mn;
      end
      r_starved_cycles <= starved;
      result_valid     <= 1'b1;
      for (int c = 0; c < NUM_CH; c++) cnt[c] <= '0;
      starved          <= '0;
    end else begin
      result_valid <= 1'b0;
      if (req_fire && cnt[req_ch] != {CNT_W{1'b1}})
        cnt[req_ch] <= cnt[req_ch] + 1'b1;

      // A starved cycle: some channel had work and was blocked while
      // at least one other channel was idle with nothing to do. That
      // is the distributor's failure signature rather than the
      // scheduler's -- 30.5 §3's four-stage attribution, applied
      // across channels instead of within one.
      if (((ch_has_work & ch_blocked) != '0)
          && ((~ch_has_work) != '0)
          && starved != {CNT_W{1'b1}})
        starved <= starved + 1'b1;
    end
  end
endmodule

  // Offered as "proves the distributor decodes correctly".
  // Clause 1 and 4. Correct, non-vacuous, and PASSES on the
  // defective block.
  property p_channel_select_is_onehot;
    @(posedge clk) disable iff (!rst_n)
      req_valid |-> $onehot(ch_onehot);
  endproperty
  assert property (p_channel_select_is_onehot)
    else $error("channel select was not one-hot for a valid request");

  // Clause 2. It names BURST_SPAN, which is the quantity the
  // defective block never computes. Variety 2's repair: make the
  // property mention the thing whose corruption it must catch.
  property p_burst_lies_within_one_channel;
    @(posedge clk) disable iff (!rst_n)
      (req_valid && !split_req) |->
        (((req_addr + BURST_SPAN - 1) >> CH_SHIFT) ==
          (req_addr >> CH_SHIFT));
  endproperty
  assert property (p_burst_lies_within_one_channel)
    else $error("an unsplit burst crosses a channel boundary");

  // Clause 3, the other direction: when the span DOES cross, a split
  // must be signalled. Stating both directions separately matters --
  // a design that always splits satisfies the property above and
  // wastes half the channel bandwidth, and a design that never
  // splits satisfies this one vacuously.
  property p_crossing_burst_is_split;
    @(posedge clk) disable iff (!rst_n)
      (req_valid &&
       (((req_addr + BURST_SPAN - 1) >> CH_SHIFT) != (req_addr >> CH_SHIFT)))
      |-> split_req;
  endproperty
  assert property (p_crossing_burst_is_split)
    else $error("a crossing burst was not split");

  // Clause 3's arithmetic. The sub-request count must equal the
  // number of channels the span actually touches -- a COMPARATIVE
  // obligation, so it is checked against an independently computed
  // expectation rather than against the design's own derivation.
  // 30.6 §11: "best" and "correct count" obligations need a model,
  // and 27.3's independence requirement says the model must not
  // reuse the design's expression.
  property p_sub_req_count_matches_span;
    @(posedge clk) disable iff (!rst_n)
      req_valid |-> (sub_req_count == ref_channels_touched(req_addr, BURST_SPAN));
  endproperty
  assert property (p_sub_req_count_matches_span)
    else $error("sub-request count disagrees with the reference model");

  // Clause 5: the decode must be stable while a request is in
  // flight, or a return cannot be attributed. 10.5 §9's association
  // problem, at channel granularity.
  property p_decode_stable_in_flight;
    @(posedge clk) disable iff (!rst_n)
      (req_valid && !req_fire) |=> $stable(sel_ch);
  endproperty
  assert property (p_decode_stable_in_flight)
    else $error("channel decode changed while a request was pending");

  // The elaboration-time fact, restated as a runtime invariant for
  // the block that KEEPS the guard (§10). It must be unreachable
  // there, and 30.5 §11's lesson applies: a guard another guard
  // always shadows is untested, so the cover below must be watched.
  property p_no_straddle_when_guarded;
    @(posedge clk) disable iff (!rst_n)
      (INTERLEAVE_GRAN >= BURST_SPAN) -> !straddles;
  endproperty
  assert property (p_no_straddle_when_guarded)
    else $error("a straddle occurred in a configuration that forbids it");

  // ---- Covers. The configuration covers are mandatory here for the
  //      same reason as in 31.1 §14 and 31.2 §14: the defect lives
  //      in a configuration, so coverage must be per configuration.
  // The GRANULARITY regimes -- the two sides of §8's inequality.
  cover property (@(posedge clk) disable iff (!rst_n)
                  req_valid && (INTERLEAVE_GRAN >= BURST_SPAN));
  cover property (@(posedge clk) disable iff (!rst_n)
                  req_valid && (INTERLEAVE_GRAN < BURST_SPAN));
  // An actual crossing burst, which is the antecedent of
  // p_crossing_burst_is_split. A zero here means the fine-grained
  // configuration ran and never presented the case -- which random
  // aligned traffic will do, because aligned bursts do not cross.
  cover property (@(posedge clk) disable iff (!rst_n)
                  req_valid &&
                  (((req_addr + BURST_SPAN - 1) >> CH_SHIFT) != (req_addr >> CH_SHIFT)));
  // A burst spanning MORE than two channels, which is where the
  // naive two-way split in §12's discussion would itself fail.
  cover property (@(posedge clk) disable iff (!rst_n)
                  req_valid && (sub_req_count > 8'd2));
  // §10's shadowed guard, watched. This cover must go DEAD in the
  // guarded configuration and be LIVE in the unguarded one -- two
  // different instruments, and 30.10 §12's point that knowing which
  // kind you are writing is the senior move.
  cover property (@(posedge clk) disable iff (!rst_n) straddles);
  // The channel-concentration case, so §13's imbalance measurement
  // is known to have been exercised at its extreme.
  cover property (@(posedge clk) disable iff (!rst_n)
                  result_valid && (r_min_ch == '0) && (r_max_ch != '0));

  // ---- ISOLATION. The property that only exists once a design is
  //      replicated, and the one that catches the classic
  //      replication bug: an index computed from the wrong variable.
  //      A command to one channel must not disturb any other
  //      channel's obligation state. For NUM_CH = 1 this is
  //      vacuously true, which is exactly why a design scaled up
  //      from one channel has never had it checked.
  property p_channel_state_isolation;
    @(posedge clk) disable iff (!rst_n)
      (req_valid && ch_legal[sel_ch]) |=>
        (foreach_other_channel_stable(sel_ch));
  endproperty
  assert property (p_channel_state_isolation)
    else $error("a command to one channel disturbed another channel's state");

  // Written concretely for a bounded channel count, because the
  // helper above hides the thing worth seeing -- that the check is
  // over every OTHER index, and that "every other" is what the
  // buggy version gets wrong.
  generate
  for (genvar c = 0; c < NUM_CH; c++) begin : g_iso
    property p_other_channel_untouched;
      @(posedge clk) disable iff (!rst_n)
        (req_valid && ch_legal[sel_ch] && (sel_ch != c)) |=>
          ($stable(row_open[c]) && $stable(row_idx[c]) && $stable(row_known[c]));
    endproperty
    assert property (p_other_channel_untouched)
      else $error("channel %0d's state changed on a command to another channel", c);
  end
  endgenerate

  // ---- Per-channel legality must be computed from that channel's
  //      OWN state. A single shared counter feeding every channel's
  //      test would pass every timing property and be wrong for
  //      fifteen of sixteen channels -- and it would pass because
  //      the timing arithmetic is right, which is 30.5 §11's
  //      "shape versus content" distinction at replication scale.
  generate
  for (genvar c = 0; c < NUM_CH; c++) begin : g_leg
    property p_legality_uses_own_state;
      @(posedge clk) disable iff (!rst_n)
        ch_legal[c] |-> (row_open[c][req_bank]
                          ? (since_act[c][req_bank] >= TRCD)
                          : (since_pre[c][req_bank] >= TRP));
    endproperty
    assert property (p_legality_uses_own_state)
      else $error("channel %0d's legality was computed from foreign state", c);
  end
  endgenerate

  // ---- The elaboration guard's runtime shadow. §10 keeps the guard,
  //      so `straddles` must be unreachable there. This is the
  //      assertion form of 30.5 §11's warning: a guard that another
  //      guard always shadows is UNTESTED, so the claim that it is
  //      unreachable should be asserted rather than assumed.
  property p_straddle_unreachable_when_guarded;
    @(posedge clk) disable iff (!rst_n)
      !straddles;
  endproperty
  assert property (p_straddle_unreachable_when_guarded)
    else $error("a straddle occurred despite the elaboration guard");

  // ---- The reported state count must match the configuration, so
  //      that §7's measured multiplication cannot silently disagree
  //      with the parameters. An INVARIANT, and the cheapest
  //      possible check that the configuration which elaborated is
  //      the one intended -- 31.1 §13's argument, reused.
  property p_state_count_matches_config;
    @(posedge clk) disable iff (!rst_n)
      state_bits_reported == (NUM_CH * BANKS_PER_CH * 30);
  endproperty
  assert property (p_state_count_matches_config)
    else $error("reported state bits disagree with the channel configuration");

  // ---- Covers. The replication regimes, because a property proved
  //      at one channel count says nothing about another -- variety
  //      10 again, with the channel count as the parameter.
  cover property (@(posedge clk) disable iff (!rst_n)
                  req_valid && (NUM_CH == 1));
  cover property (@(posedge clk) disable iff (!rst_n)
                  req_valid && (NUM_CH > 1));
  // Every channel must have been SELECTED at least once, or the
  // isolation properties above held only for the indices the
  // stimulus happened to reach. This is the replication analogue of
  // 31.2 §14's duration cover: the coverage item must be on the
  // dimension the defect scales with, and here that dimension is
  // the index space.
  generate
  for (genvar c = 0; c < NUM_CH; c++) begin : g_cov
    cover property (@(posedge clk) disable iff (!rst_n)
                    req_valid && (sel_ch == c));
  end
  endgenerate