Why HBM Exists

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

   1024 bits  x  2.4 Gb/s per pin  =  2457.6 Gb/s
                                    /  8 bits per byte
                                    =  307.2 GB/s        matches

   full channel     :  128 bits x BL2 x 2 edges  =  512 bits  =  64 B
   pseudo-channel   :   64 bits x BL4 x 2 edges  =  512 bits  =  64 B

// ---------------------------------------------------------------------
// hbm_channel_organisation -- holds the stack interface hierarchy and
// proves at elaboration that both decompositions reconstruct it.
//
// CLASSIFICATION: educational, synthesisable.
//
// PROVENANCE OF THE DEFAULTS:
//   TOTAL_BITS=1024, CHANNELS=8  -- CURRICULUM-DERIVED from 4.8 §2's
//     published set, which this curriculum verified.
//   PC_PER_CHANNEL=2             -- REPORTED (§3). NOT verified from a
//     primary source in this module. The block takes it as a
//     parameter precisely so the unverified part is visible and
//     replaceable rather than baked in.
//
// WHAT IT DOES NOT MODEL:
//   - the stack, the interposer, or TSVs (26.2 and 26.3)
//   - ANY physical dimension. §1's area-versus-perimeter arithmetic is
//     prose and stays prose: there is no millimetre in this file.
//   - any timing parameter, the array, or any access
//   - bandwidth. 4.8 §5's bandwidth_account owns that and is cited,
//     not reimplemented.
// ---------------------------------------------------------------------
module hbm_channel_organisation #(
  parameter int TOTAL_BITS     = 1024,   // CURRICULUM-DERIVED (4.8 §2)
  parameter int CHANNELS       = 8,      // CURRICULUM-DERIVED (4.8 §2)
  parameter int PC_PER_CHANNEL = 2,      // REPORTED (§3) -- see header

  // ── Derived. A caller that could override these could break the
  //    agreement the module exists to enforce.
  parameter int CH_BITS   = TOTAL_BITS / CHANNELS,
  parameter int PC_BITS   = CH_BITS / PC_PER_CHANNEL,
  parameter int PC_TOTAL  = CHANNELS * PC_PER_CHANNEL,
  // Indices into their own level.
  parameter int CH_IDX_W  = (CHANNELS <= 1) ? 1 : $clog2(CHANNELS),
  parameter int PC_IDX_W  = (PC_PER_CHANNEL <= 1) ? 1 : $clog2(PC_PER_CHANNEL),
  parameter int PCG_IDX_W = (PC_TOTAL <= 1) ? 1 : $clog2(PC_TOTAL),
  // A COUNT up to PC_TOTAL needs clog2(PC_TOTAL+1), not clog2(PC_TOTAL).
  parameter int PCCNT_W   = $clog2(PC_TOTAL + 1)
) (
  input  logic                  clk,
  input  logic                  rst_n,

  // ── Query: a global pseudo-channel index in, its coordinates out.
  input  logic                  q_valid,
  input  logic [PCG_IDX_W-1:0]  q_pc_global,

  output logic [CH_IDX_W-1:0]   q_channel,
  output logic [PC_IDX_W-1:0]   q_pc_in_channel,
  output logic                  q_in_range,

  // ── The organisation, published so consumers need not recompute it.
  output logic [15:0]           total_bits,
  output logic [7:0]            n_channels,
  output logic [PCCNT_W-1:0]    n_pseudo_channels,
  output logic [15:0]           channel_bits,
  output logic [15:0]           pc_bits,

  output logic                  err_pc_out_of_range,
  output logic                  any_error
);

  initial begin
    if (TOTAL_BITS < 2 || (TOTAL_BITS & (TOTAL_BITS - 1)) != 0)
      // The >= 2 bound matters: a power-of-two test ALONE accepts 0
      // and 1, either of which makes a clog2 zero and every field
      // width wrong. Module 24 shipped that hole once.
      $fatal(1, "hbm_channel_organisation: TOTAL_BITS must be a power of two >= 2");
    if (CHANNELS < 2 || (CHANNELS & (CHANNELS - 1)) != 0)
      $fatal(1, "hbm_channel_organisation: CHANNELS must be a power of two >= 2");
    if (PC_PER_CHANNEL < 1 || (PC_PER_CHANNEL & (PC_PER_CHANNEL - 1)) != 0)
      $fatal(1, "hbm_channel_organisation: PC_PER_CHANNEL must be a power of two >= 1");
    // §2's check: the channels must reconstruct the interface exactly.
    if ((CH_BITS * CHANNELS) != TOTAL_BITS)
      $fatal(1, "hbm_channel_organisation: %0d channels x %0d bits != %0d",
             CHANNELS, CH_BITS, TOTAL_BITS);
    // §3's check: so must the pseudo-channels.
    if ((PC_BITS * PC_TOTAL) != TOTAL_BITS)
      $fatal(1, "hbm_channel_organisation: %0d pseudo-channels x %0d bits != %0d",
             PC_TOTAL, PC_BITS, TOTAL_BITS);
    if ((PC_BITS * PC_PER_CHANNEL) != CH_BITS)
      $fatal(1, "hbm_channel_organisation: pseudo-channels do not tile a channel");
    if (PCG_IDX_W != $clog2(PC_TOTAL))
      $fatal(1, "hbm_channel_organisation: global index must address PC_TOTAL");
    if ((CH_IDX_W + PC_IDX_W) != PCG_IDX_W)
      // The global index must decompose losslessly into a channel
      // index and a within-channel index. P1 asserts it at runtime;
      // this is the width precondition that makes it possible.
      $fatal(1, "hbm_channel_organisation: index widths do not compose (%0d + %0d != %0d)",
             CH_IDX_W, PC_IDX_W, PCG_IDX_W);
  end

  logic e_range;

  // Declared above the continuous assigns that read it.
  logic in_rng;
  assign in_rng = q_valid &&
                  ({{(32-PCG_IDX_W){1'b0}}, q_pc_global} < 32'(PC_TOTAL));

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) e_range <= 1'b0;
    else        e_range <= q_valid && !in_rng;
  end

  // The channel is the high field and the within-channel index the
  // low field, so consecutive global indices stay within a channel.
  assign q_channel       = q_pc_global[PCG_IDX_W-1 -: CH_IDX_W];
  assign q_pc_in_channel = q_pc_global[PC_IDX_W-1 : 0];
  assign q_in_range      = in_rng;

  assign total_bits        = 16'(TOTAL_BITS);
  assign n_channels        = 8'(CHANNELS);
  assign n_pseudo_channels = PCCNT_W'(PC_TOTAL);
  assign channel_bits      = 16'(CH_BITS);
  assign pc_bits           = 16'(PC_BITS);

  assign err_pc_out_of_range = e_range;
  assign any_error = e_range;
endmodule

// ---------------------------------------------------------------------
// pseudo_channel_cmd_arbiter -- one command bus, two pseudo-channels
// that decode independently. Decides which one is issued to, and
// records what the other lost.
//
// CLASSIFICATION: educational, synthesisable.
//
// WHY THIS IS THE CHAPTER'S LOAD-BEARING BLOCK: §8's diagram shows
// every benefit of the pseudo-channel split arriving free and its
// entire cost arriving through one edge -- the shared command bus.
// This is that edge.
//
// THE ARRANGEMENT IS REPORTED, NOT VERIFIED (§3): two pseudo-channels
// sharing a channel's command bus and clock, decoding independently,
// with a bank-address bit selecting between them.
//
// WHAT IT DOES NOT MODEL:
//   - the device, any command encoding, or any timing parameter
//   - the banks, or what a command DOES once issued. §6: contention
//     is on command ISSUE, not on command EFFECT.
//   - the controller's scheduling POLICY. This block resolves a slot;
//     choosing which requester deserves it is a policy question
//     Module 23 owns for a different standard and 26.4 revisits.
// ---------------------------------------------------------------------
module pseudo_channel_cmd_arbiter #(
  parameter int PC_PER_CHANNEL = 2,      // REPORTED (§3)
  parameter int PC_IDX_W = (PC_PER_CHANNEL <= 1) ? 1 : $clog2(PC_PER_CHANNEL),
  parameter int CNT_W    = 24
) (
  input  logic                      clk,
  input  logic                      rst_n,

  // ── One request per pseudo-channel, asserted independently.
  input  logic [PC_PER_CHANNEL-1:0] pc_req,
  // Whether each pseudo-channel is able to accept a command now. A
  // pseudo-channel busy with its own banks cannot use a slot.
  input  logic [PC_PER_CHANNEL-1:0] pc_ready,

  // ── The single shared bus. One grant per slot, at most.
  output logic                      slot_granted,
  output logic [PC_IDX_W-1:0]       grant_pc,
  output logic [PC_PER_CHANNEL-1:0] grant_onehot,

  // ── What sharing costs, measured. §6: the controller never sees
  //    the command it was not given, so the loss must be counted
  //    here or it is invisible everywhere.
  output logic [CNT_W-1:0]          cnt_slots,
  output logic [CNT_W-1:0]          cnt_granted,
  output logic [CNT_W-1:0]          cnt_contended,
  output logic [CNT_W-1:0]          cnt_idle_slots,
  output logic [CNT_W-1:0]          cnt_deferred [PC_PER_CHANNEL],

  // Longest run of consecutive slots a pseudo-channel was denied --
  // the fairness quantity a round-robin is supposed to bound.
  output logic [15:0]               worst_starve_run,
  output logic                      fairness_bound_exceeded,

  output logic                      err_grant_to_unready,
  output logic                      err_multiple_grants,
  output logic                      any_error
);

  initial begin
    if (PC_PER_CHANNEL < 2)
      // With one pseudo-channel there is nothing to arbitrate, and a
      // block that "arbitrates" a single requester would imply a
      // contention cost that does not exist.
      $fatal(1, "pseudo_channel_cmd_arbiter: need at least 2 pseudo-channels");
    if (PC_IDX_W != $clog2(PC_PER_CHANNEL))
      $fatal(1, "pseudo_channel_cmd_arbiter: PC_IDX_W must address PC_PER_CHANNEL");
  end

  logic [PC_IDX_W-1:0]  rr_ptr;
  logic [CNT_W-1:0]     n_slot, n_grant, n_cont, n_idle;
  logic [CNT_W-1:0]     n_def [PC_PER_CHANNEL];
  logic [15:0]          run [PC_PER_CHANNEL];
  logic [15:0]          worst;
  logic                 e_unready, e_multi;

  // ── Only a pseudo-channel that is both requesting AND ready can be
  //    granted. Declared above the continuous assigns that read it.
  logic [PC_PER_CHANNEL-1:0] eligible;
  assign eligible = pc_req & pc_ready;

  // Round-robin from the pointer. Combinational so the grant is
  // available in the same slot the request is presented.
  logic [PC_IDX_W-1:0]       sel;
  logic                      have_sel;
  always_comb begin
    sel      = '0;
    have_sel = 1'b0;
    for (int k = 0; k < PC_PER_CHANNEL; k++) begin
      // Walk from rr_ptr forwards, wrapping, and take the first
      // eligible requester. Fixed priority would starve one half
      // indefinitely, which P7 forbids.
      int unsigned idx;
      idx = (int unsigned'(rr_ptr) + k) % PC_PER_CHANNEL;
      if (!have_sel && eligible[idx]) begin
        sel      = PC_IDX_W'(idx);
        have_sel = 1'b1;
      end
    end
  end

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      rr_ptr <= '0;
      n_slot <= '0; n_grant <= '0; n_cont <= '0; n_idle <= '0;
      worst <= '0; e_unready <= 1'b0; e_multi <= 1'b0;
      for (int i = 0; i < PC_PER_CHANNEL; i++) begin
        n_def[i] <= '0; run[i] <= '0;
      end
    end else begin
      e_unready <= 1'b0; e_multi <= 1'b0;

      if (n_slot != {CNT_W{1'b1}}) n_slot <= n_slot + CNT_W'(1);

      // More than one requester eligible in one slot is the
      // contention §6 names -- counted whether or not it is resolved.
      if ($countones(eligible) > 1) begin
        if (n_cont != {CNT_W{1'b1}}) n_cont <= n_cont + CNT_W'(1);
      end

      if (have_sel) begin
        if (n_grant != {CNT_W{1'b1}}) n_grant <= n_grant + CNT_W'(1);
        // Advance past the granted index so the next slot favours the
        // other half.
        rr_ptr <= PC_IDX_W'((int unsigned'(sel) + 1) % PC_PER_CHANNEL);
      end else begin
        if (n_idle != {CNT_W{1'b1}}) n_idle <= n_idle + CNT_W'(1);
      end

      // ── Per-pseudo-channel deferral and starvation runs.
      for (int i = 0; i < PC_PER_CHANNEL; i++) begin
        if (pc_req[i] && !(have_sel && (sel == PC_IDX_W'(i)))) begin
          if (n_def[i] != {CNT_W{1'b1}}) n_def[i] <= n_def[i] + CNT_W'(1);
          if (run[i] != 16'hFFFF) begin
            run[i] <= run[i] + 16'd1;
            // Compare the INCREMENTED value combinationally: run[i]'s
            // write lands on this edge, so reading run[i] here would
            // test the pre-increment value and under-report the peak
            // by one. This is the stale-register hazard Module 21 §10
            // and 25.2 §15 both name.
            if ((run[i] + 16'd1) > worst) worst <= run[i] + 16'd1;
          end
        end else if (have_sel && (sel == PC_IDX_W'(i))) begin
          run[i] <= '0;
        end
      end

      // A grant to a pseudo-channel that is not ready would be a
      // command the device cannot accept.
      if (have_sel && !pc_ready[sel]) e_unready <= 1'b1;
    end
  end

  assign slot_granted = have_sel;
  assign grant_pc     = sel;
  always_comb begin
    grant_onehot = '0;
    if (have_sel) grant_onehot[sel] = 1'b1;
  end

  assign cnt_slots     = n_slot;
  assign cnt_granted   = n_grant;
  assign cnt_contended = n_cont;
  assign cnt_idle_slots = n_idle;
  assign cnt_deferred  = n_def;
  assign worst_starve_run = worst;
  // A round-robin over N requesters should never defer one for more
  // than N-1 consecutive slots in which it was eligible.
  assign fairness_bound_exceeded = (worst > 16'(PC_PER_CHANNEL - 1));
  assign err_grant_to_unready = e_unready;
  assign err_multiple_grants  = e_multi;
  assign any_error = e_unready | e_multi;
endmodule

if ((run[i] + 16'd1) > worst) worst <= run[i] + 16'd1;

// ---------------------------------------------------------------------
// pc_stream_monitor -- how many pseudo-channels are actually carrying
// traffic, and how the idle ones are distributed.
//
// CLASSIFICATION: educational, synthesisable.
//
// WHY IT EXISTS: 4.8 §2 states that "307 GB/s requires traffic that
// keeps all eight channels busy" and that "one channel's worth of
// traffic gets one channel's worth of bandwidth". §4 doubles the
// relevant count to sixteen. That is a claim about a STREAM, so it
// needs measuring rather than deriving -- and 4.8's bandwidth_account
// computes the PEAK, which is exactly the number this does not.
//
// WHAT IT DOES NOT MODEL:
//   - bandwidth in bytes per second (4.8 §5 owns it, cited not rebuilt)
//   - any timing parameter, the array, or the interposer
//   - WHY a stream is idle. It attributes idleness to a
//     pseudo-channel; whether the cause is the requester, the
//     mapping or the arbiter is outside this block.
//
// NO DIVISION: occupancy is published as numerator and denominator so
// the caller states its own denominator.
// ---------------------------------------------------------------------
module pc_stream_monitor #(
  parameter int PC_TOTAL = 16,           // §3: 8 channels x 2
  parameter int CHANNELS = 8,            // CURRICULUM-DERIVED (4.8 §2)
  parameter int PC_IDX_W = (PC_TOTAL <= 1) ? 1 : $clog2(PC_TOTAL),
  // A COUNT up to PC_TOTAL needs clog2(PC_TOTAL+1).
  parameter int PCCNT_W  = $clog2(PC_TOTAL + 1),
  parameter int CHCNT_W  = $clog2(CHANNELS + 1),
  parameter int CNT_W    = 28
) (
  input  logic                  clk,
  input  logic                  rst_n,

  // One bit per pseudo-channel: carrying traffic this cycle.
  input  logic [PC_TOTAL-1:0]   pc_active,

  // ── Instantaneous.
  output logic [PCCNT_W-1:0]    n_active,
  output logic [PCCNT_W-1:0]    n_idle,
  // Channels with at least one active pseudo-channel. A channel whose
  // two halves are both idle is a wholly unused command bus.
  output logic [CHCNT_W-1:0]    n_channels_touched,

  // ── Occupancy, as a PAIR. Never a percentage.
  output logic [CNT_W-1:0]      pc_active_cycles,
  output logic [CNT_W-1:0]      pc_slot_cycles,

  // ── Peaks and the reachability question.
  output logic [PCCNT_W-1:0]    peak_active,
  output logic                  all_streams_seen,
  output logic [CNT_W-1:0]      cy_single_stream,
  output logic [CNT_W-1:0]      cy_fully_idle,

  // The failure 4.8 §2 describes: plenty of width, one stream using
  // it. Reported as a state rather than inferred from a ratio.
  output logic                  width_wasted_now,

  output logic                  err_active_out_of_range,
  output logic                  any_saturated
);

  initial begin
    if (PC_TOTAL < 2)
      $fatal(1, "pc_stream_monitor: need at least 2 pseudo-channels");
    if (CHANNELS < 1 || (PC_TOTAL % CHANNELS) != 0)
      // Pseudo-channels must tile the channels evenly, or "channels
      // touched" cannot be computed from the active mask at all.
      $fatal(1, "pc_stream_monitor: %0d pseudo-channels do not tile %0d channels",
             PC_TOTAL, CHANNELS);
    if (PCCNT_W <= PC_IDX_W)
      // COUNT vs INDEX: a count up to PC_TOTAL needs one more bit
      // than an index into it when PC_TOTAL is a power of two. Too
      // narrow and n_active can never represent "all of them", so
      // all_streams_seen becomes unreachable -- the silent form.
      $fatal(1, "pc_stream_monitor: PCCNT_W too narrow to count PC_TOTAL");
  end

  localparam int PC_PER_CH = PC_TOTAL / CHANNELS;

  logic [CNT_W-1:0]  c_act, c_slot, c_single, c_allidle;
  logic [PCCNT_W-1:0] pk;
  logic              seen_all, sat;
  logic              e_rng;

  // Declared above the continuous assigns that read them.
  logic [PCCNT_W-1:0] n_act_c;
  assign n_act_c = PCCNT_W'($countones(pc_active));

  logic [CHCNT_W-1:0] n_touch_c;
  always_comb begin
    n_touch_c = '0;
    for (int ch = 0; ch < CHANNELS; ch++) begin
      logic any_in_ch;
      any_in_ch = 1'b0;
      for (int k = 0; k < PC_PER_CH; k++)
        if (pc_active[ch*PC_PER_CH + k]) any_in_ch = 1'b1;
      if (any_in_ch) n_touch_c = n_touch_c + CHCNT_W'(1);
    end
  end

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      c_act <= '0; c_slot <= '0; c_single <= '0; c_allidle <= '0;
      pk <= '0; seen_all <= 1'b0; sat <= 1'b0; e_rng <= 1'b0;
    end else begin
      e_rng <= 1'b0;

      if (c_slot == {CNT_W{1'b1}}) sat <= 1'b1;
      else begin
        c_slot <= c_slot + CNT_W'(1);
        // Accumulate pseudo-channel-cycles, not cycles: the quantity
        // that matters is how much of the width was used.
        c_act  <= c_act + CNT_W'(n_act_c);
      end

      if (n_act_c > pk) pk <= n_act_c;
      if (n_act_c == PCCNT_W'(PC_TOTAL)) seen_all <= 1'b1;
      if (n_act_c == PCCNT_W'(1)) begin
        if (c_single != {CNT_W{1'b1}}) c_single <= c_single + CNT_W'(1);
      end
      if (n_act_c == '0) begin
        if (c_allidle != {CNT_W{1'b1}}) c_allidle <= c_allidle + CNT_W'(1);
      end
    end
  end

  assign n_active            = n_act_c;
  assign n_idle              = PCCNT_W'(PC_TOTAL) - n_act_c;
  assign n_channels_touched  = n_touch_c;
  assign pc_active_cycles    = c_act;
  // The denominator a caller needs: slots x pseudo-channels.
  assign pc_slot_cycles      = c_slot * CNT_W'(PC_TOTAL);
  assign peak_active         = pk;
  assign all_streams_seen    = seen_all;
  assign cy_single_stream    = c_single;
  assign cy_fully_idle       = c_allidle;
  // 4.8 §2's failure, named: traffic present, but on one stream.
  assign width_wasted_now    = (n_act_c == PCCNT_W'(1));
  assign err_active_out_of_range = e_rng;
  assign any_saturated = sat;
endmodule

// Bind unit note: P1-P4 reference hbm_channel_organisation's
// internals, P5-P9 pseudo_channel_cmd_arbiter's, P10-P14
// pc_stream_monitor's. Each is written as though bound into its
// own module.

// P1 -- the global index decomposes losslessly. §9's width check is
// the precondition; this is the property it enables.
property p_index_decomposition_is_lossless;
  @(posedge clk) disable iff (!rst_n)
    q_in_range |-> ({q_channel, q_pc_in_channel} == q_pc_global);
endproperty
assert property (p_index_decomposition_is_lossless);

// P2 -- §2 and §3's identities, as runtime invariants: both levels
// reconstruct the interface exactly.
property p_both_levels_reconstruct_the_interface;
  @(posedge clk) disable iff (!rst_n)
    ((16'(n_channels) * channel_bits == total_bits) &&
     (16'(n_pseudo_channels) * pc_bits == total_bits));
endproperty
assert property (p_both_levels_reconstruct_the_interface);

// P3 -- the pseudo-channel count is the channel count times the
// per-channel count. Guards the COUNT-vs-INDEX trap: a too-narrow
// PCCNT_W would wrap and silently report fewer streams.
property p_pc_count_is_the_product;
  @(posedge clk) disable iff (!rst_n)
    (n_pseudo_channels == PCCNT_W'(CHANNELS * PC_PER_CHANNEL));
endproperty
assert property (p_pc_count_is_the_product);

// P4 -- FORBIDDEN. An out-of-range index is never reported in range,
// and is always flagged.
property p_out_of_range_never_accepted;
  @(posedge clk) disable iff (!rst_n)
    (q_valid && ({{(32-PCG_IDX_W){1'b0}}, q_pc_global} >= 32'(PC_TOTAL)))
      |-> (!q_in_range ##1 err_pc_out_of_range);
endproperty
assert property (p_out_of_range_never_accepted);

// P5 -- FORBIDDEN. At most one pseudo-channel is granted per slot.
// §6: there is one bus and one slot, and two grants would model a
// bus that does not exist.
property p_at_most_one_grant_per_slot;
  @(posedge clk) disable iff (!rst_n)
    $onehot0(grant_onehot);
endproperty
assert property (p_at_most_one_grant_per_slot);

// P6 -- FORBIDDEN. A grant never goes to a pseudo-channel that is
// not both requesting and ready.
property p_grant_only_to_eligible;
  @(posedge clk) disable iff (!rst_n)
    slot_granted |-> ((pc_req[grant_pc]) && (pc_ready[grant_pc]));
endproperty
assert property (p_grant_only_to_eligible);

// P7 -- FORBIDDEN. No eligible pseudo-channel is deferred for more
// than PC_PER_CHANNEL-1 consecutive slots. §10: the fairness bound a
// round-robin exists to provide, and the property the stale-register
// bug would let pass at exactly the violating run length.
property p_round_robin_bounds_starvation;
  @(posedge clk) disable iff (!rst_n)
    !fairness_bound_exceeded;
endproperty
assert property (p_round_robin_bounds_starvation);

// P8 -- a slot with any eligible requester always produces a grant.
// Rules out an arbiter that idles a usable slot, which would waste
// the scarce resource §5 says the whole architecture conserves.
property p_eligible_slot_is_never_wasted;
  @(posedge clk) disable iff (!rst_n)
    (((pc_req & pc_ready) != '0) |-> slot_granted);
endproperty
assert property (p_eligible_slot_is_never_wasted);

// P9 -- every slot is accounted exactly once as granted or idle.
property p_slots_are_partitioned;
  @(posedge clk) disable iff (!rst_n)
    ((cnt_granted + cnt_idle_slots) == cnt_slots);
endproperty
assert property (p_slots_are_partitioned);

// P10 -- active and idle stream counts partition the pseudo-channels.
property p_stream_counts_partition;
  @(posedge clk) disable iff (!rst_n)
    ((n_active + n_idle) == PCCNT_W'(PC_TOTAL));
endproperty
assert property (p_stream_counts_partition);

// P11 -- channels touched never exceeds the channel count, and is
// zero exactly when nothing is active.
property p_channels_touched_is_consistent;
  @(posedge clk) disable iff (!rst_n)
    ((n_channels_touched <= CHCNT_W'(CHANNELS)) &&
     ((n_active == '0) == (n_channels_touched == '0)));
endproperty
assert property (p_channels_touched_is_consistent);

// P12 -- channels touched never exceeds active streams. Each active
// pseudo-channel touches exactly one channel, so the channel count
// cannot be the larger of the two.
property p_touched_never_exceeds_active;
  @(posedge clk) disable iff (!rst_n)
    (CHCNT_W'(n_channels_touched) <= CHCNT_W'(n_active));
endproperty
assert property (p_touched_never_exceeds_active);

// P13 -- the peak is monotone, and all_streams_seen is sticky once
// every stream has been simultaneously active.
property p_peak_and_seen_are_monotone;
  @(posedge clk) disable iff (!rst_n)
    ((peak_active >= $past(peak_active, 1)) &&
     ($past(all_streams_seen, 1) |-> all_streams_seen));
endproperty
assert property (p_peak_and_seen_are_monotone);

// P14 -- 4.8 §2's failure state, as an invariant: width_wasted_now
// holds exactly when precisely one stream is carrying traffic.
property p_width_wasted_means_one_stream;
  @(posedge clk) disable iff (!rst_n)
    (width_wasted_now == (n_active == PCCNT_W'(1)));
endproperty
assert property (p_width_wasted_means_one_stream);

// ── Cover.
// Every channel and every within-channel index reached.
cover property (@(posedge clk) disable iff (!rst_n)
                  q_in_range && (q_channel == '0));
cover property (@(posedge clk) disable iff (!rst_n)
                  q_in_range && (q_channel == CH_IDX_W'(CHANNELS - 1)));
cover property (@(posedge clk) disable iff (!rst_n)
                  q_in_range && (q_pc_in_channel == PC_IDX_W'(PC_PER_CHANNEL - 1)));
// Each forbidden condition ATTEMPTED -- vacuous otherwise.
cover property (@(posedge clk) disable iff (!rst_n) err_pc_out_of_range);
cover property (@(posedge clk) disable iff (!rst_n) err_grant_to_unready);
// CONTENTION actually occurring: both halves eligible in one slot.
// §6 says this is the entire cost of the split, so a suite that never
// reaches it has not exercised the chapter's subject.
cover property (@(posedge clk) disable iff (!rst_n) cnt_contended != '0);
cover property (@(posedge clk) disable iff (!rst_n)
                  $countones(pc_req & pc_ready) == PC_PER_CHANNEL);
// A requester deferred, and then served -- the round-robin working.
cover property (@(posedge clk) disable iff (!rst_n)
                  (cnt_deferred[0] != '0) && (cnt_deferred[1] != '0));
// An idle slot with a request pending but not ready.
cover property (@(posedge clk) disable iff (!rst_n)
                  (pc_req != '0) && ((pc_req & pc_ready) == '0) && !slot_granted);
// THE REACHABILITY COVERS. All sixteen streams simultaneously active,
// and the one-stream waste 4.8 §2 warns about.
cover property (@(posedge clk) disable iff (!rst_n) all_streams_seen);
cover property (@(posedge clk) disable iff (!rst_n) width_wasted_now);
cover property (@(posedge clk) disable iff (!rst_n) cy_fully_idle != '0);
// Eight active streams spread across eight channels versus concentrated
// in four -- the same count, different command-bus pressure (§15).
cover property (@(posedge clk) disable iff (!rst_n)
                  (n_active == PCCNT_W'(8)) && (n_channels_touched == CHCNT_W'(8)));
cover property (@(posedge clk) disable iff (!rst_n)
                  (n_active == PCCNT_W'(8)) && (n_channels_touched == CHCNT_W'(4)));

// Independent hierarchy reference. Builds the pseudo-channel list
// explicitly as a table of (channel, index-within-channel) pairs
// rather than by field arithmetic, so agreement with the DUT is
// evidence rather than a restatement of the same shift.
// SIMULATION-ONLY.
class hbm_hierarchy_ref;
  int ch_of[$];        // ch_of[global] = its channel
  int idx_of[$];       // idx_of[global] = its index within that channel
  int total_bits, channels, pc_per_ch;

  function void build(int bits, int n_ch, int n_pc);
    total_bits = bits; channels = n_ch; pc_per_ch = n_pc;
    ch_of.delete(); idx_of.delete();
    for (int c = 0; c < n_ch; c++)
      for (int p = 0; p < n_pc; p++) begin
        ch_of.push_back(c);
        idx_of.push_back(p);
      end
  endfunction

  function int n_pseudo(); return ch_of.size(); endfunction
  function int channel_bits(); return total_bits / channels; endfunction
  function int pc_bits(); return channel_bits() / pc_per_ch; endfunction

  // §2 and §3's identities, computed independently of the DUT.
  function bit levels_reconstruct();
    return (channel_bits() * channels == total_bits) &&
           (pc_bits() * ch_of.size() == total_bits);
  endfunction

  // §4's granularity identity, as a pair rather than a single number.
  function int access_bits(int width, int burst_len);
    return width * burst_len * 2;          // both clock edges
  endfunction

  function bit granularity_is_preserved();
    return access_bits(channel_bits(), 2) == access_bits(pc_bits(), 4);
  endfunction
endclass

  TWO WAYS TO PASS EVERYTHING AND BE WRONG

  (A) the starvation counter that is always one short
      Replace the combinational compare with  run[i] > worst.

      stimulus : both halves eligible every slot, fixed-priority
                 arbiter substituted so half 1 is never granted.
      true worst starvation run          : 2 consecutive slots
      worst_starve_run reports           : 1
      fairness_bound_exceeded (> N-1 = 1): FALSE

      P7 round_robin_bounds_starvation   : PASS
      every other property               : PASS

      diagnosis : the bound is N-1 = 1, the real run is 2, and the
        counter reports 1. The property is evaluated against a value
        that is wrong by exactly the margin that would have failed
        it. A starvation bound off by one is not a small error --
        it is the difference between detecting unfairness and
        certifying it.

  (B) sixteen streams "active", four command buses idle
      stimulus : 8 pseudo-channels active, but both halves of only
                 four channels.

      n_active                 8
      n_channels_touched       4     <-- half the command buses unused
      peak_active              8
      all_streams_seen         0
      every property           PASS

      diagnosis : nothing is illegal. Eight streams are running, and
        4.8 §2's advice to "keep the channels busy" appears
        satisfied by a count of eight. But four of eight command
        buses are idle while the other four carry two halves each --
        maximum contention on half the resource and none on the
        rest.

      what makes it dangerous : the stream count is the number a
        tuning exercise naturally watches, and it is identical to
        the healthy case. Only n_channels_touched distinguishes
        them, and a design that does not publish it cannot see the
        difference.