DDR5 Bank-Group Enhancements

   page size  =  2^(column address bits)  x  device width

   x4  :  2^11 x  4 bits  =  8192 bits  =  1 KB     published 1 KB
   x8  :  2^10 x  8 bits  =  8192 bits  =  1 KB     published 1 KB
   x16 :  2^10 x 16 bits  = 16384 bits  =  2 KB     published 2 KB

   page crossings        1,024
   bank crossings            0
   bank-group crossings      0

   x8  :  32 pieces of 1 KB
   x16 :  16 pieces of 2 KB
                                both total 32,768 B

// ---------------------------------------------------------------------
// ddr5_bank_organisation -- holds a DDR5 die's organisation and proves
// at elaboration that the fields, the page size, the bank count and
// the density all agree.
//
// CLASSIFICATION: educational, synthesisable.
//
// WHY ELABORATION AND NOT RUNTIME: 4.6 §5 established the principle --
// an architectural rule belongs where a violation cannot build. A
// runtime check would let a mis-parameterised design elaborate and
// then mis-address silently, which is the failure this prevents.
//
// WHAT IT DOES NOT MODEL:
//   - the array, any timing parameter, or the shared column data path
//     (5.3 owns that mechanism; 14.6 and 14.7 own its timing)
//   - any access. It describes a device, it does not serve requests.
//   - DDR5 timing values, which 16.3 §4 could not retrieve and this
//     chapter did not either. NOTHING here depends on one.
//
// THE FIGURES IT DEFAULTS TO ARE DEVICE-VERIFIED for a named 16Gb
// DDR5 die at x8 (§1). Other widths are legal parameterisations and
// the checks below are what keep them honest.
// ---------------------------------------------------------------------
module ddr5_bank_organisation #(
  parameter int DEVICE_WIDTH = 8,        // 4, 8 or 16
  parameter int BANK_GROUPS  = 8,        // 8 at x4/x8, 4 at x16
  parameter int BANKS_PER_BG = 4,        // constant at every width
  parameter int ROW_BITS     = 16,       // R0-R15
  parameter int COL_BITS     = 10,       // C0-C9 at x8/x16, C0-C10 at x4
  parameter int DENSITY_GB   = 16,       // gigabits on the label

  // ── Derived, not supplied. A caller that could override these
  //    could break the agreement the module exists to enforce.
  parameter int BANKS        = BANK_GROUPS * BANKS_PER_BG,
  parameter int PAGE_BITS    = (2 ** COL_BITS) * DEVICE_WIDTH,
  // Field widths. BG indexes into BANK_GROUPS, so clog2(BANK_GROUPS).
  parameter int BG_BITS      = (BANK_GROUPS  <= 1) ? 1 : $clog2(BANK_GROUPS),
  parameter int BA_BITS      = (BANKS_PER_BG <= 1) ? 1 : $clog2(BANKS_PER_BG),
  parameter int BANK_BITS    = BG_BITS + BA_BITS,
  // A COUNT of banks up to BANKS needs clog2(BANKS+1), not clog2(BANKS).
  parameter int BANKCNT_W    = $clog2(BANKS + 1)
) (
  input  logic                 clk,
  input  logic                 rst_n,

  // ── Query interface. A bank address in, its decomposition out.
  input  logic                 q_valid,
  input  logic [BANK_BITS-1:0] q_bank,

  output logic [BG_BITS-1:0]   q_group,
  output logic [BA_BITS-1:0]   q_bank_in_group,
  output logic                 q_in_range,

  // ── The organisation, published so a consumer need not recompute it.
  output logic [BANKCNT_W-1:0] n_banks,
  output logic [BG_BITS:0]     n_groups,
  output logic [31:0]          page_bytes,
  output logic [31:0]          rows_per_bank,
  output logic [63:0]          per_bank_bits,

  // §5: how much of the address space one bank spans. The quantity
  // that makes "more banks" cost something.
  output logic [63:0]          bank_span_bits,

  output logic                 err_bank_out_of_range,
  output logic                 any_error
);

  // ── The organisation invariant, as elaboration checks. Each one is
  //    a check §2 or §3 performed by hand on the datasheet's table.
  initial begin
    if (!(DEVICE_WIDTH inside {4, 8, 16}))
      $fatal(1, "ddr5_bank_organisation: DEVICE_WIDTH must be 4, 8 or 16 (got %0d)",
             DEVICE_WIDTH);
    if (BANKS_PER_BG != 4)
      // DEVICE-VERIFIED constant at every width (§1). A different
      // value is not a DDR5 organisation.
      $fatal(1, "ddr5_bank_organisation: BANKS_PER_BG must be 4 (got %0d)",
             BANKS_PER_BG);
    if (!(BANK_GROUPS inside {4, 8}))
      $fatal(1, "ddr5_bank_organisation: BANK_GROUPS must be 4 or 8 (got %0d)",
             BANK_GROUPS);
    // §1: the x16 organisation has FOUR groups and the narrower
    // widths have eight. A x16 part with eight groups is not a
    // device this addendum describes.
    if ((DEVICE_WIDTH == 16) && (BANK_GROUPS != 4))
      $fatal(1, "ddr5_bank_organisation: x16 has 4 bank groups, not %0d",
             BANK_GROUPS);
    if ((DEVICE_WIDTH != 16) && (BANK_GROUPS != 8))
      $fatal(1, "ddr5_bank_organisation: x4/x8 have 8 bank groups, not %0d",
             BANK_GROUPS);
    // Powers of two, with the >= 2 lower bound the shift arithmetic
    // needs. A power-of-two test ALONE accepts 0 and 1, both of which
    // would make a clog2 zero and the field width wrong.
    if (BANK_GROUPS < 2 || (BANK_GROUPS & (BANK_GROUPS - 1)) != 0)
      $fatal(1, "ddr5_bank_organisation: BANK_GROUPS must be a power of two >= 2");
    if (BANKS < 2 || (BANKS & (BANKS - 1)) != 0)
      $fatal(1, "ddr5_bank_organisation: BANKS must be a power of two >= 2");
    if (BANK_BITS != $clog2(BANKS))
      // The field widths must address exactly the stated bank count --
      // §2's check that the feature list and the addressing table agree.
      $fatal(1, "ddr5_bank_organisation: BG+BA bits (%0d) do not address %0d banks",
             BANK_BITS, BANKS);
    if (ROW_BITS < 1 || COL_BITS < 1)
      $fatal(1, "ddr5_bank_organisation: field widths must be positive");
    // §3's whole-die check: rows x page x banks must equal the density.
    if (((2 ** ROW_BITS) * PAGE_BITS * BANKS) != (DENSITY_GB * (1024 ** 3)))
      $fatal(1,
        "ddr5_bank_organisation: rows(%0d) x page(%0d bits) x banks(%0d) != %0d Gb",
        2 ** ROW_BITS, PAGE_BITS, BANKS, DENSITY_GB);
    if ((PAGE_BITS % 8) != 0)
      $fatal(1, "ddr5_bank_organisation: page must be a whole number of bytes");
  end

  logic e_range;

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

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

  // Field split follows the datasheet's own decomposition: the group
  // field is the high part and the bank-within-group the low part.
  // 8.4 owns extracting these from a full address; this is the
  // device-side decomposition of an already-formed bank number.
  assign q_group         = q_bank[BANK_BITS-1 -: BG_BITS];
  assign q_bank_in_group = q_bank[BA_BITS-1 : 0];
  assign q_in_range      = in_rng;

  assign n_banks       = BANKCNT_W'(BANKS);
  assign n_groups      = (BG_BITS+1)'(BANK_GROUPS);
  assign page_bytes    = 32'(PAGE_BITS / 8);
  assign rows_per_bank = 32'(2 ** ROW_BITS);
  assign per_bank_bits = 64'(2 ** ROW_BITS) * 64'(PAGE_BITS);
  // §5: one bank spans this much of the address space, so a
  // sequential walk crosses a bank boundary every this-many bits.
  assign bank_span_bits = 64'(2 ** ROW_BITS) * 64'(PAGE_BITS);

  assign err_bank_out_of_range = e_range;
  assign any_error = e_range;
endmodule

// ---------------------------------------------------------------------
// same_group_opportunity_monitor -- measures the observed same-group
// fraction of a request stream against the structural baseline §4
// derives from the organisation alone.
//
// CLASSIFICATION: educational, synthesisable.
//
// WHY IT COMPARES AGAINST A BASELINE: §4 computes that a random pair
// of distinct banks shares a group 3/31 of the time at x8 and 3/15 at
// x16. That is what a RANDOM stream would produce. A real stream that
// does better has a mapping working for it; one that does worse has a
// mapping working against it -- and neither is visible from the
// same-group count alone.
//
// WHAT IT DOES NOT MODEL:
//   - the shared column path (5.3), or any timing (14.6, 14.7, 16.3)
//   - ANY PENALTY. §4's callout: DDR5's same-group cost is not
//     verified anywhere in this chapter, so this block reports
//     FREQUENCY and never converts it to cycles.
//
// NO DIVISION: the observed fraction and the baseline are compared by
// CROSS-MULTIPLICATION, and both are published as numerator and
// denominator pairs so the caller states its own denominator.
// ---------------------------------------------------------------------
module same_group_opportunity_monitor #(
  parameter int BANK_GROUPS  = 8,
  parameter int BANKS_PER_BG = 4,
  parameter int BANKS        = BANK_GROUPS * BANKS_PER_BG,
  parameter int BG_BITS      = (BANK_GROUPS <= 1) ? 1 : $clog2(BANK_GROUPS),
  parameter int BANK_BITS    = $clog2(BANKS),
  parameter int CNT_W        = 32
) (
  input  logic                 clk,
  input  logic                 rst_n,

  input  logic                 req_valid,
  input  logic [BANK_BITS-1:0] req_bank,

  // ── Observed, as a pair. Consecutive DISTINCT banks only: a repeat
  //    of the same bank is neither a same-group nor a different-group
  //    pair, and counting it as either would bias the fraction.
  output logic [CNT_W-1:0]     n_pairs,
  output logic [CNT_W-1:0]     n_same_group,
  output logic [CNT_W-1:0]     n_diff_group,
  output logic [CNT_W-1:0]     n_same_bank,

  // ── The structural baseline of §4: (BANKS_PER_BG-1)/(BANKS-1).
  output logic [CNT_W-1:0]     base_num,
  output logic [CNT_W-1:0]     base_den,

  // Verdict by cross-multiplication, never by dividing. A mapping is
  // "better than random" when observed/pairs < base_num/base_den.
  output logic                 better_than_random,
  output logic                 worse_than_random,
  output logic                 at_baseline,

  output logic                 err_bank_out_of_range,
  output logic                 any_saturated
);

  initial begin
    if (BANKS_PER_BG < 2)
      $fatal(1, "same_group_opportunity_monitor: BANKS_PER_BG must be >= 2");
    if (BANKS <= BANKS_PER_BG)
      // With one group every pair is same-group and the baseline is 1,
      // which makes the comparison meaningless rather than extreme.
      $fatal(1, "same_group_opportunity_monitor: need more than one bank group");
    if (BANK_BITS != $clog2(BANKS))
      $fatal(1, "same_group_opportunity_monitor: BANK_BITS must address BANKS");
  end

  logic [CNT_W-1:0]     c_pair, c_same, c_diff, c_reps;
  logic                 have_prev, sat, e_rng;
  logic [BANK_BITS-1:0] prev_bank;

  // Declared above the continuous assigns that read them.
  logic [BG_BITS-1:0] this_grp, prev_grp;
  assign this_grp = req_bank[BANK_BITS-1 -: BG_BITS];
  assign prev_grp = prev_bank[BANK_BITS-1 -: BG_BITS];

  logic in_rng;
  assign in_rng = ({{(32-BANK_BITS){1'b0}}, req_bank} < 32'(BANKS));

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      c_pair <= '0; c_same <= '0; c_diff <= '0; c_reps <= '0;
      have_prev <= 1'b0; prev_bank <= '0; sat <= 1'b0; e_rng <= 1'b0;
    end else begin
      e_rng <= 1'b0;
      if (req_valid) begin
        if (!in_rng) begin
          // Out of range: reported, and NOT folded into the counts. A
          // bad bank number classified as either kind would corrupt
          // the fraction the block exists to report.
          e_rng <= 1'b1;
        end else begin
          if (have_prev) begin
            if (req_bank == prev_bank) begin
              // Same bank is neither pair kind -- counted separately.
              if (c_reps != {CNT_W{1'b1}}) c_reps <= c_reps + CNT_W'(1);
            end else begin
              if (c_pair == {CNT_W{1'b1}}) sat <= 1'b1;
              else begin
                c_pair <= c_pair + CNT_W'(1);
                if (this_grp == prev_grp) c_same <= c_same + CNT_W'(1);
                else                      c_diff <= c_diff + CNT_W'(1);
              end
            end
          end
          prev_bank <= req_bank;
          have_prev <= 1'b1;
        end
      end
    end
  end

  assign n_pairs      = c_pair;
  assign n_same_group = c_same;
  assign n_diff_group = c_diff;
  assign n_same_bank  = c_reps;
  assign base_num     = CNT_W'(BANKS_PER_BG - 1);
  assign base_den     = CNT_W'(BANKS - 1);

  // observed(c_same/c_pair) vs baseline(base_num/base_den), compared
  // as c_same*base_den vs base_num*c_pair. No divide.
  assign better_than_random =
    (c_pair != '0) && ((c_same * CNT_W'(BANKS - 1)) <  (CNT_W'(BANKS_PER_BG - 1) * c_pair));
  assign worse_than_random =
    (c_pair != '0) && ((c_same * CNT_W'(BANKS - 1)) >  (CNT_W'(BANKS_PER_BG - 1) * c_pair));
  assign at_baseline =
    (c_pair != '0) && ((c_same * CNT_W'(BANKS - 1)) == (CNT_W'(BANKS_PER_BG - 1) * c_pair));

  assign err_bank_out_of_range = e_rng;
  assign any_saturated = sat;
endmodule

// ---------------------------------------------------------------------
// page_granularity_accountant -- counts page and bank crossings for a
// stream, which is what §5 says "more banks" costs.
//
// CLASSIFICATION: educational, synthesisable.
//
// WHAT IT ADDS: §5 argues that DDR5's smaller banks put boundaries
// twice as close together at x8, so a sequential walk crosses them
// twice as often. That is a claim about a STREAM, not about a device,
// so it needs measuring rather than deriving.
//
// WHAT IT DOES NOT MODEL: energy, bandwidth, any timing parameter, or
// the row buffer's contents. 23.3 owns row-buffer locality and what a
// hit is worth; this counts boundary crossings and nothing more.
// ---------------------------------------------------------------------
module page_granularity_accountant #(
  parameter int ADDR_W    = 36,
  parameter int PAGE_BYTES = 1024,           // DEVICE-VERIFIED at x8 (§1)
  parameter int BANKS      = 32,
  parameter int ROWS       = 65536,
  parameter int PAGE_SH    = $clog2(PAGE_BYTES),
  parameter int CNT_W      = 32
) (
  input  logic              clk,
  input  logic              rst_n,

  input  logic              acc_valid,
  input  logic [ADDR_W-1:0] acc_addr,
  input  logic [15:0]       acc_bytes,

  // ── Crossings.
  output logic [CNT_W-1:0]  n_accesses,
  output logic [CNT_W-1:0]  n_page_crossings,
  output logic [CNT_W-1:0]  n_within_page,
  // An access that itself spans a page boundary -- distinct from two
  // consecutive accesses landing in different pages.
  output logic [CNT_W-1:0]  n_self_spanning,

  // ── Span facts, published so a caller need not recompute them.
  output logic [31:0]       page_span_bytes,
  output logic [63:0]       bank_span_bytes,

  output logic              err_zero_length,
  output logic              err_access_exceeds_page,
  output logic              any_saturated
);

  initial begin
    if (PAGE_BYTES < 2 || (PAGE_BYTES & (PAGE_BYTES - 1)) != 0)
      // The lower bound matters: a power-of-two test alone accepts 0
      // and 1, either of which makes PAGE_SH zero and every shift a
      // no-op.
      $fatal(1, "page_granularity_accountant: PAGE_BYTES must be a power of two >= 2");
    if (BANKS < 1 || ROWS < 1)
      $fatal(1, "page_granularity_accountant: BANKS and ROWS must be positive");
    if (PAGE_SH >= ADDR_W)
      $fatal(1, "page_granularity_accountant: page field exceeds ADDR_W");
  end

  logic [CNT_W-1:0]   c_acc, c_cross, c_within, c_span;
  logic               have_prev, sat, e_zero, e_big;
  logic [ADDR_W-1:0]  prev_page;

  // Declared above the continuous assigns that read them.
  logic [ADDR_W-1:0] this_page, end_page;
  assign this_page = acc_addr >> PAGE_SH;
  // The page the LAST byte of this access falls in. Equal to
  // this_page unless the access itself straddles a boundary.
  assign end_page  = (acc_bytes == '0) ? this_page
                   : ((acc_addr + ADDR_W'(acc_bytes) - ADDR_W'(1)) >> PAGE_SH);

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      c_acc <= '0; c_cross <= '0; c_within <= '0; c_span <= '0;
      have_prev <= 1'b0; prev_page <= '0; sat <= 1'b0;
      e_zero <= 1'b0; e_big <= 1'b0;
    end else begin
      e_zero <= 1'b0; e_big <= 1'b0;
      if (acc_valid) begin
        if (acc_bytes == '0) begin
          e_zero <= 1'b1;
        end else begin
          if (c_acc == {CNT_W{1'b1}}) sat <= 1'b1;
          else begin
            c_acc <= c_acc + CNT_W'(1);
            if (have_prev) begin
              if (this_page != prev_page) c_cross  <= c_cross  + CNT_W'(1);
              else                        c_within <= c_within + CNT_W'(1);
            end
            if (end_page != this_page) c_span <= c_span + CNT_W'(1);
          end
          if ({{(32-16){1'b0}}, acc_bytes} > 32'(PAGE_BYTES))
            // Larger than a page: legal to request and it guarantees
            // a crossing, so it is reported rather than silently
            // inflating the crossing count.
            e_big <= 1'b1;
          prev_page <= this_page;
          have_prev <= 1'b1;
        end
      end
    end
  end

  assign n_accesses       = c_acc;
  assign n_page_crossings = c_cross;
  assign n_within_page    = c_within;
  assign n_self_spanning  = c_span;
  assign page_span_bytes  = 32'(PAGE_BYTES);
  // §5: one bank spans rows x page bytes of the address space.
  assign bank_span_bytes  = 64'(ROWS) * 64'(PAGE_BYTES);
  assign err_zero_length          = e_zero;
  assign err_access_exceeds_page  = e_big;
  assign any_saturated = sat;
endmodule

// Bind unit note: P1-P5 reference ddr5_bank_organisation's internals,
// P6-P10 same_group_opportunity_monitor's, P11-P14
// page_granularity_accountant's. Each is written as though bound into
// its own module.

// P1 -- the decomposition is exact: recombining the group and the
// bank-within-group reproduces the queried bank.
property p_decomposition_is_lossless;
  @(posedge clk) disable iff (!rst_n)
    q_in_range |-> ({q_group, q_bank_in_group} == q_bank);
endproperty
assert property (p_decomposition_is_lossless);

// P2 -- the published bank count always equals the parameterised
// organisation. Guards the COUNT-vs-INDEX trap: a too-narrow
// BANKCNT_W would silently truncate 32 to 0.
property p_bank_count_matches_organisation;
  @(posedge clk) disable iff (!rst_n)
    (n_banks == BANKCNT_W'(BANK_GROUPS * BANKS_PER_BG));
endproperty
assert property (p_bank_count_matches_organisation);

// P3 -- §3's whole-die identity, as a runtime invariant as well as an
// elaboration check: rows x page x banks is the density.
property p_die_identity_holds;
  @(posedge clk) disable iff (!rst_n)
    ((per_bank_bits * 64'(BANKS)) == (64'(DENSITY_GB) * 64'(1024*1024*1024)));
endproperty
assert property (p_die_identity_holds);

// P4 -- FORBIDDEN. A bank number outside the organisation 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-BANK_BITS){1'b0}}, q_bank} >= 32'(BANKS)))
      |-> (!q_in_range ##1 err_bank_out_of_range);
endproperty
assert property (p_out_of_range_never_accepted);

// P5 -- §2's page derivation, as an invariant: page bytes is
// 2^colbits x width / 8.
property p_page_size_derivation;
  @(posedge clk) disable iff (!rst_n)
    (page_bytes == 32'(((2 ** COL_BITS) * DEVICE_WIDTH) / 8));
endproperty
assert property (p_page_size_derivation);

// P6 -- the three pair outcomes partition every classified request
// after the first. Nothing is double-counted or lost.
property p_pair_outcomes_partition;
  @(posedge clk) disable iff (!rst_n)
    ((n_same_group + n_diff_group) == n_pairs);
endproperty
assert property (p_pair_outcomes_partition);

// P7 -- FORBIDDEN. A repeated bank never counts as a pair. §11: it is
// neither same-group nor different-group, and counting it as either
// would bias the fraction toward "better than random".
property p_repeat_is_never_a_pair;
  @(posedge clk) disable iff (!rst_n)
    (req_valid && (req_bank == $past(req_bank, 1)) && $past(req_valid, 1))
      |=> (n_pairs == $past(n_pairs, 1));
endproperty
assert property (p_repeat_is_never_a_pair);

// P8 -- FORBIDDEN. An out-of-range bank is never folded into any
// pair count. A bad bank number classified either way corrupts the
// measurement the block exists to produce.
property p_bad_bank_never_counted;
  @(posedge clk) disable iff (!rst_n)
    err_bank_out_of_range |-> ((n_pairs      == $past(n_pairs, 1)) &&
                               (n_same_group == $past(n_same_group, 1)));
endproperty
assert property (p_bad_bank_never_counted);

// P9 -- the baseline is the structural fraction of §4 and does not
// depend on the stream at all.
property p_baseline_is_structural;
  @(posedge clk) disable iff (!rst_n)
    ((base_num == CNT_W'(BANKS_PER_BG - 1)) && (base_den == CNT_W'(BANKS - 1)));
endproperty
assert property (p_baseline_is_structural);

// P10 -- the three verdicts are mutually exclusive, and none holds
// before any pair has been seen. A verdict on zero samples would be
// an opinion rather than a measurement.
property p_verdict_exclusive_and_grounded;
  @(posedge clk) disable iff (!rst_n)
    ((n_pairs == '0) ? (!better_than_random && !worse_than_random && !at_baseline)
                     : $onehot({better_than_random, worse_than_random, at_baseline}));
endproperty
assert property (p_verdict_exclusive_and_grounded);

// P11 -- crossings and within-page accesses partition every access
// after the first.
property p_crossings_partition;
  @(posedge clk) disable iff (!rst_n)
    ((n_page_crossings + n_within_page) <= n_accesses);
endproperty
assert property (p_crossings_partition);

// P12 -- an access larger than a page is always flagged, and always
// self-spanning. It cannot fit, so it must straddle.
property p_oversize_access_spans;
  @(posedge clk) disable iff (!rst_n)
    (acc_valid && (acc_bytes != '0) &&
     ({{(32-16){1'b0}}, acc_bytes} > 32'(PAGE_BYTES)))
      |=> err_access_exceeds_page;
endproperty
assert property (p_oversize_access_spans);

// P13 -- FORBIDDEN. A zero-length access is never counted. It is not
// silently treated as one byte, which would invent a crossing.
property p_zero_length_not_counted;
  @(posedge clk) disable iff (!rst_n)
    (acc_valid && (acc_bytes == '0))
      |=> ((n_accesses == $past(n_accesses, 1)) && err_zero_length);
endproperty
assert property (p_zero_length_not_counted);

// P14 -- §5's span arithmetic: a bank covers rows x page bytes.
property p_bank_span_is_rows_times_page;
  @(posedge clk) disable iff (!rst_n)
    (bank_span_bytes == (64'(ROWS) * 64'(PAGE_BYTES)));
endproperty
assert property (p_bank_span_is_rows_times_page);

// ── Cover.
// Every bank group reached, and every bank within a group.
cover property (@(posedge clk) disable iff (!rst_n)
                  q_in_range && (q_group == '0));
cover property (@(posedge clk) disable iff (!rst_n)
                  q_in_range && (q_group == BG_BITS'(BANK_GROUPS - 1)));
cover property (@(posedge clk) disable iff (!rst_n)
                  q_in_range && (q_bank_in_group == BA_BITS'(BANKS_PER_BG - 1)));
// Each forbidden condition ATTEMPTED. A property forbidding something
// is vacuous until the testbench tries it.
cover property (@(posedge clk) disable iff (!rst_n) err_bank_out_of_range);
cover property (@(posedge clk) disable iff (!rst_n) err_zero_length);
cover property (@(posedge clk) disable iff (!rst_n) err_access_exceeds_page);
// A repeated bank actually driven -- P7 is vacuous without it.
cover property (@(posedge clk) disable iff (!rst_n)
                  req_valid && $past(req_valid,1) && (req_bank == $past(req_bank,1)));
// All three mapping verdicts reached. "At baseline" is the one a
// suite is likeliest to miss.
cover property (@(posedge clk) disable iff (!rst_n) better_than_random);
cover property (@(posedge clk) disable iff (!rst_n) worse_than_random);
cover property (@(posedge clk) disable iff (!rst_n) at_baseline);
// Both crossing kinds, and the distinction of §12.
cover property (@(posedge clk) disable iff (!rst_n)
                  acc_valid && (n_page_crossings != $past(n_page_crossings,1)));
cover property (@(posedge clk) disable iff (!rst_n) n_self_spanning != '0);
// Both verified organisations exercised: 32 banks and 16 banks.
cover property (@(posedge clk) disable iff (!rst_n) n_banks == BANKCNT_W'(32));
cover property (@(posedge clk) disable iff (!rst_n) n_banks == BANKCNT_W'(16));

// Independent organisation reference. Builds the bank list explicitly
// as a table of (group, bank-in-group) pairs rather than by field
// arithmetic, so agreement with the DUT is evidence rather than a
// restatement of the same shift. SIMULATION-ONLY.
class organisation_ref;
  int grp_of[$];          // grp_of[bank] = its group
  int idx_of[$];          // idx_of[bank] = its index within the group
  int groups, per_group;

  function void build(int n_groups, int banks_per_group);
    groups = n_groups; per_group = banks_per_group;
    grp_of.delete(); idx_of.delete();
    for (int g = 0; g < n_groups; g++)
      for (int b = 0; b < banks_per_group; b++) begin
        grp_of.push_back(g);
        idx_of.push_back(b);
      end
  endfunction

  function int n_banks(); return grp_of.size(); endfunction

  // The structural baseline of §4, as a pair -- never as a real.
  function void baseline(output int num, output int den);
    num = per_group - 1;
    den = grp_of.size() - 1;
  endfunction

  // Page size from the fields, computed independently of the DUT.
  function int page_bytes(int col_bits, int width);
    return ((1 << col_bits) * width) / 8;
  endfunction

  // §3's whole-die identity.
  function bit die_consistent(int row_bits, int col_bits, int width,
                              int density_gb);
    longint total;
    total = longint'(1 << row_bits) * longint'((1 << col_bits) * width)
            * longint'(grp_of.size());
    return total == longint'(density_gb) * 1024 * 1024 * 1024;
  endfunction
endclass

  THE STREAM THAT LOOKS LIKE A PERFECT MAPPING
    A request stream confined to a single bank, 100,000 accesses.

    n_pairs            0
    n_same_group       0
    n_diff_group       0
    n_same_bank   99,999

    verdict:      none asserted  (P10 holds: no pairs, no opinion)

    assertions:   P6  pair outcomes partition     PASS (0 + 0 == 0)
                  P7  repeat is never a pair      PASS
                  P9  baseline is structural      PASS
                  all 14 properties               PASS

    what a NAIVE monitor would have reported:
                  same-group fraction  0 / 99,999  =  0.000%
                  baseline             3 / 31       =  9.677%
                  verdict:  BETTER THAN RANDOM, by a wide margin

    diagnosis : the naive reading is exactly backwards. A stream with
      zero same-group pairs because it never leaves one bank has NO
      bank-level parallelism at all -- it is the worst possible
      stream, reported as the best.

    what makes it dangerous : the same-group count is the number a
      mapping study naturally optimises, and it is minimised by the
      degenerate stream. The metric and the goal diverge precisely
      where the design is worst.

    the fix : the three outcomes must PARTITION and the repeat count
      must be visible (§11). P10's refusal to render a verdict on
      zero pairs is what stops the degenerate case from being scored
      at all, and n_same_bank is what names it.