2.5D Packaging for HBM

   continuous :  A / p²  =  L² / p²

   integer    :  floor(L/p)²

   face      L² / p²        L
   ────  =  ─────────  =  ────
   edge      4L / p         4p

   24 GB  /  12 core dies  =  2 GB per die  =  16 Gb per die

   check :  16 Gb x 12  /  8 bits per byte  =  24 GB     exact

// ---------------------------------------------------------------------
// bump_connection_budget -- converts an area and a pitch into a
// connection count, and checks a signal requirement against it.
//
// CLASSIFICATION: educational, synthesisable. COUNTING ONLY.
//
// WHAT IT DOES NOT MODEL -- and this list is the most important part
// of the block:
//   - capacitance, resistance, inductance. A pitch has electrical
//     consequences and NONE of them is computed here.
//   - thermal resistance, temperature, yield, assembly tolerance,
//     mechanical stress. 4.8 §3 owns the yield ARGUMENT; no block
//     may compute a yield.
//   - trace length or its energy consequence. §2: shortness is a
//     real benefit and it is not what this block is about.
// A PITCH ENTERS AS AN INTEGER AND IS USED ONLY TO COUNT. Converting
// it to an electrical result would be this module's fake-eye failure
// (22.3), and the discipline is absolute.
//
// UNITS: pitch in micrometres, side lengths in micrometres, areas in
// square micrometres. Integers throughout -- no fixed point, no
// division where a comparison will do.
// ---------------------------------------------------------------------
module bump_connection_budget #(
  // ILLUSTRATIVE defaults. No pitch or die size in this module
  // was verified from any source.
  parameter int DIE_SIDE_UM   = 10000,   // 10 mm, ILLUSTRATIVE
  parameter int PITCH_UM      = 45,      // ILLUSTRATIVE
  parameter int SIGNAL_BUMPS  = 1024,    // CURRICULUM-DERIVED (4.8 §2)
  // §6: power/ground bumps per signal bump, as a numerator over a
  // denominator so a caller can express 1:2 or 3:4 without a real.
  parameter int PG_NUM        = 2,
  parameter int PG_DEN        = 1,
  parameter int CNT_W         = 32
) (
  input  logic              clk,
  input  logic              rst_n,

  // ── Query a hypothetical pitch at runtime, so a design can budget
  //    more than one option without re-elaborating.
  input  logic              q_valid,
  input  logic [15:0]       q_pitch_um,

  // ── Counts at the ELABORATED pitch.
  output logic [CNT_W-1:0]  face_positions,
  output logic [CNT_W-1:0]  edge_positions,
  output logic [CNT_W-1:0]  total_bumps_needed,
  output logic [CNT_W-1:0]  spare_positions,
  output logic              requirement_fits,

  // §4's closed form, as a PAIR. face/edge = L/(4p), published as
  // numerator and denominator so no division happens here.
  output logic [CNT_W-1:0]  advantage_num,
  output logic [CNT_W-1:0]  advantage_den,

  // ── Runtime query result.
  output logic [CNT_W-1:0]  q_face_positions,
  output logic              q_fits,
  output logic              q_out_valid,

  output logic              err_pitch_zero,
  output logic              err_pitch_exceeds_die,
  output logic              any_error
);

  // Derived at elaboration. §3's model: a square grid over the face.
  localparam int POS_PER_SIDE = DIE_SIDE_UM / PITCH_UM;
  localparam int FACE_POS     = POS_PER_SIDE * POS_PER_SIDE;
  localparam int EDGE_POS     = (4 * DIE_SIDE_UM) / PITCH_UM;
  // §6: total = signals x (1 + PG_NUM/PG_DEN), computed without a
  // real by scaling the numerator.
  localparam int TOTAL_BUMPS  = (SIGNAL_BUMPS * (PG_DEN + PG_NUM)) / PG_DEN;

  initial begin
    if (PITCH_UM < 1)
      $fatal(1, "bump_connection_budget: PITCH_UM must be at least 1");
    if (DIE_SIDE_UM < 1)
      $fatal(1, "bump_connection_budget: DIE_SIDE_UM must be at least 1");
    if (PITCH_UM > DIE_SIDE_UM)
      // A pitch larger than the die holds zero positions, which is a
      // misparameterisation rather than a very sparse die.
      $fatal(1, "bump_connection_budget: PITCH_UM (%0d) exceeds DIE_SIDE_UM (%0d)",
             PITCH_UM, DIE_SIDE_UM);
    if (PG_DEN < 1 || PG_NUM < 0)
      $fatal(1, "bump_connection_budget: power/ground ratio must be non-negative over a positive denominator");
    if (SIGNAL_BUMPS < 1)
      $fatal(1, "bump_connection_budget: SIGNAL_BUMPS must be at least 1");
    if (POS_PER_SIDE < 1)
      $fatal(1, "bump_connection_budget: pitch leaves fewer than one position per side");
    // §6: the overhead must actually be counted. A block that
    // reported a signals-only total would understate the field by
    // whatever the power overhead is, which §6 says is the whole
    // reason the ratio is a required input.
    if (TOTAL_BUMPS < SIGNAL_BUMPS)
      $fatal(1, "bump_connection_budget: total (%0d) below signal count (%0d)",
             TOTAL_BUMPS, SIGNAL_BUMPS);
    // §5's observation, enforced: the requirement should fit with
    // room to spare at any sensible parameterisation. If it does not,
    // the caller has chosen a pitch or a die that cannot work, and
    // finding that at elaboration is the point.
    if (TOTAL_BUMPS > FACE_POS)
      $fatal(1, "bump_connection_budget: %0d bumps do not fit in %0d positions",
             TOTAL_BUMPS, FACE_POS);
  end

  logic              e_zero, e_big, qv;
  logic [CNT_W-1:0]  q_face;
  logic              q_ok;

  // Declared above the continuous assigns that read them.
  logic [CNT_W-1:0] q_per_side;
  assign q_per_side = (q_pitch_um == '0) ? '0
                    : CNT_W'(CNT_W'(DIE_SIDE_UM) / CNT_W'(q_pitch_um));

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      e_zero <= 1'b0; e_big <= 1'b0; qv <= 1'b0;
      q_face <= '0; q_ok <= 1'b0;
    end else begin
      e_zero <= 1'b0; e_big <= 1'b0; qv <= 1'b0;
      if (q_valid) begin
        if (q_pitch_um == '0) begin
          // A zero pitch is not an infinitely dense surface, it is a
          // division by zero. Reported, never computed.
          e_zero <= 1'b1;
        end else if ({{(32-16){1'b0}}, q_pitch_um} > CNT_W'(DIE_SIDE_UM)) begin
          e_big <= 1'b1;
        end else begin
          q_face <= q_per_side * q_per_side;
          q_ok   <= (q_per_side * q_per_side) >= CNT_W'(TOTAL_BUMPS);
          qv     <= 1'b1;
        end
      end
    end
  end

  assign face_positions     = CNT_W'(FACE_POS);
  assign edge_positions     = CNT_W'(EDGE_POS);
  assign total_bumps_needed = CNT_W'(TOTAL_BUMPS);
  assign spare_positions    = (FACE_POS >= TOTAL_BUMPS)
                            ? CNT_W'(FACE_POS - TOTAL_BUMPS) : '0;
  assign requirement_fits   = (FACE_POS >= TOTAL_BUMPS);
  // §4: face/edge = L/(4p). Published as the pair, never divided.
  assign advantage_num      = CNT_W'(DIE_SIDE_UM);
  assign advantage_den      = CNT_W'(4 * PITCH_UM);
  assign q_face_positions   = q_face;
  assign q_fits             = q_ok;
  assign q_out_valid        = qv;
  assign err_pitch_zero        = e_zero;
  assign err_pitch_exceeds_die = e_big;
  assign any_error = e_zero | e_big;
endmodule

// ---------------------------------------------------------------------
// hbm_stack_layer_map -- the stack's layer structure: one base die at
// the bottom, N core dies above it, N from the verified height set.
//
// CLASSIFICATION: educational, synthesisable.
//
// WHAT IT DOES NOT MODEL:
//   - the dies themselves, or anything physical. There is no
//     thickness, no thermal path and no assembly step here.
//   - the vertical connections (26.3 owns them entirely)
//   - the base die's CONTENTS. §9's callout: 4.8 deferred "the
//     stack's logic layer" to this module and this module could not
//     deliver it. The block models the base die's POSITION and its
//     SHARED status, which §9 derives from structure, and nothing
//     about what is inside it.
//
// HEIGHTS ARE CURRICULUM-DERIVED from 4.8 §2: 2, 4, 8 and 12. A
// height outside that set is refused rather than accommodated,
// because accommodating it would imply a generality the source does
// not support.
// ---------------------------------------------------------------------
module hbm_stack_layer_map #(
  parameter int CORE_DIES   = 12,        // CURRICULUM-DERIVED set (4.8 §2)
  parameter int GB_PER_DIE2 = 16,        // §8's inference: 16 Gb per core die
  // Layers = core dies + one base die.
  parameter int LAYERS      = CORE_DIES + 1,
  parameter int LAYER_IDX_W = $clog2(LAYERS),
  // A COUNT up to LAYERS needs clog2(LAYERS+1).
  parameter int LAYERCNT_W  = $clog2(LAYERS + 1),
  parameter int CAP_W        = 16
) (
  input  logic                    clk,
  input  logic                    rst_n,

  // ── Query a layer index.
  input  logic                    q_valid,
  input  logic [LAYER_IDX_W-1:0]  q_layer,

  output logic                    q_is_base,
  output logic                    q_is_core,
  output logic                    q_in_range,
  // Core dies are numbered from the bottom upward, above the base.
  output logic [LAYER_IDX_W-1:0]  q_core_index,

  // ── The structure, published.
  output logic [LAYERCNT_W-1:0]   n_layers,
  output logic [LAYERCNT_W-1:0]   n_core_dies,
  output logic [LAYERCNT_W-1:0]   n_base_dies,
  // §8: height buys capacity, not bandwidth. Both are published so a
  // consumer cannot infer one from the other by accident.
  output logic [CAP_W-1:0]        capacity_gb,
  output logic [CAP_W-1:0]        interface_bits,

  output logic                    err_layer_out_of_range,
  output logic                    any_error
);

  initial begin
    // CURRICULUM-DERIVED height set. A height outside it is refused.
    if (!(CORE_DIES inside {2, 4, 8, 12}))
      $fatal(1, "hbm_stack_layer_map: CORE_DIES must be 2, 4, 8 or 12 (4.8 §2), got %0d",
             CORE_DIES);
    if (LAYERS != CORE_DIES + 1)
      // §7: exactly one base die, and it is not optional. A stack
      // with no base die has no external interface at all.
      $fatal(1, "hbm_stack_layer_map: LAYERS must be CORE_DIES + 1");
    if (LAYERCNT_W <= LAYER_IDX_W && LAYERS > 1)
      // COUNT vs INDEX. Too narrow and n_layers cannot represent the
      // full height, so a consumer sees a shorter stack than exists.
      $fatal(1, "hbm_stack_layer_map: LAYERCNT_W too narrow to count LAYERS");
    // §8's identity: capacity is dies x per-die density, in GB.
    if (((CORE_DIES * GB_PER_DIE2) / 8) > ((1 << CAP_W) - 1))
      $fatal(1, "hbm_stack_layer_map: CAP_W too narrow for the capacity");
    if ((CORE_DIES * GB_PER_DIE2) % 8 != 0)
      // A capacity that is not a whole number of gigabytes means the
      // per-die density and the height do not combine cleanly, which
      // §8 verified they do for the published pair.
      $fatal(1, "hbm_stack_layer_map: %0d dies x %0d Gb is not a whole number of GB",
             CORE_DIES, GB_PER_DIE2);
  end

  logic e_range;

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

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

  // §7 and §9: layer 0 is the base die, at the bottom, because that
  // is where the interposer is. Core dies are 1..CORE_DIES upward.
  assign q_is_base    = in_rng && (q_layer == '0);
  assign q_is_core    = in_rng && (q_layer != '0);
  assign q_in_range   = in_rng;
  assign q_core_index = (q_layer == '0) ? '0 : (q_layer - LAYER_IDX_W'(1));

  assign n_layers    = LAYERCNT_W'(LAYERS);
  assign n_core_dies = LAYERCNT_W'(CORE_DIES);
  assign n_base_dies = LAYERCNT_W'(1);
  assign capacity_gb = CAP_W'((CORE_DIES * GB_PER_DIE2) / 8);
  // §8: the interface width does NOT depend on the height. Published
  // as a constant beside the capacity so the independence is visible.
  assign interface_bits = CAP_W'(1024);

  assign err_layer_out_of_range = e_range;
  assign any_error = e_range;
endmodule

// ---------------------------------------------------------------------
// bump_assignment_guard -- every bump position gets exactly one role,
// and the field is not complete until every signal has one.
//
// CLASSIFICATION: educational, synthesisable.
//
// WHAT IT DOES NOT MODEL:
//   - any physical bump, its electrical behaviour or its placement
//   - whether an assignment is MANUFACTURABLE. Placement rules,
//     keep-outs and assembly tolerance are outside this block and
//     outside this module's sources.
//   - redundancy or repair. 26.3 owns spare connections and the
//     repair map; this block has a SPARE role and no repair logic.
//
// WHY DOUBLE ASSIGNMENT IS THE FORBIDDEN ONE: a position assigned
// twice is not a conflict the hardware resolves -- it is two nets on
// one connection, which is a short. The block refuses the second
// assignment and reports it rather than overwriting the first.
// ---------------------------------------------------------------------
module bump_assignment_guard #(
  parameter int POSITIONS   = 2048,
  parameter int SIGNALS     = 1024,      // CURRICULUM-DERIVED (4.8 §2)
  parameter int POS_IDX_W   = $clog2(POSITIONS),
  // A COUNT up to POSITIONS needs clog2(POSITIONS+1).
  parameter int POSCNT_W    = $clog2(POSITIONS + 1),
  parameter int SIGCNT_W    = $clog2(SIGNALS + 1)
) (
  input  logic                    clk,
  input  logic                    rst_n,

  // ── Assign a role to a position. Roles are exclusive.
  input  logic                    asg_valid,
  input  logic [POS_IDX_W-1:0]    asg_pos,
  input  logic [1:0]              asg_role,   // 0 unassigned, 1 signal,
                                              // 2 power/ground, 3 spare

  output logic [POSCNT_W-1:0]     n_assigned,
  output logic [SIGCNT_W-1:0]     n_signal,
  output logic [POSCNT_W-1:0]     n_power_ground,
  output logic [POSCNT_W-1:0]     n_spare,
  output logic [POSCNT_W-1:0]     n_unassigned,

  // ── Completeness. §6: a field is not usable until every signal
  //    has a position, and the count is the only way to know.
  output logic                    all_signals_assigned,
  output logic                    field_complete,

  output logic                    err_double_assignment,
  output logic                    err_bad_role,
  output logic                    err_pos_out_of_range,
  output logic                    err_too_many_signals,
  output logic                    any_error
);

  localparam logic [1:0] R_NONE = 2'd0;
  localparam logic [1:0] R_SIG  = 2'd1;
  localparam logic [1:0] R_PG   = 2'd2;
  localparam logic [1:0] R_SPR  = 2'd3;

  initial begin
    if (POSITIONS < 2)
      $fatal(1, "bump_assignment_guard: POSITIONS must be at least 2");
    if (SIGNALS < 1 || SIGNALS > POSITIONS)
      // More signals than positions is not a tight design, it is an
      // impossible one.
      $fatal(1, "bump_assignment_guard: SIGNALS (%0d) must be 1..POSITIONS (%0d)",
             SIGNALS, POSITIONS);
    if (POS_IDX_W != $clog2(POSITIONS))
      $fatal(1, "bump_assignment_guard: POS_IDX_W must address POSITIONS");
    if (POSCNT_W <= POS_IDX_W)
      $fatal(1, "bump_assignment_guard: POSCNT_W too narrow to count POSITIONS");
  end

  logic [1:0]          role [POSITIONS];
  logic [SIGCNT_W-1:0] c_sig;
  logic [POSCNT_W-1:0] c_pg, c_spr;
  logic                e_dbl, e_role, e_rng, e_many;

  // Declared above the continuous assigns that read them.
  logic pos_ok;
  assign pos_ok = ({{(32-POS_IDX_W){1'b0}}, asg_pos} < 32'(POSITIONS));

  logic role_ok;
  assign role_ok = (asg_role != R_NONE);

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      for (int i = 0; i < POSITIONS; i++) role[i] <= R_NONE;
      c_sig <= '0; c_pg <= '0; c_spr <= '0;
      e_dbl <= 1'b0; e_role <= 1'b0; e_rng <= 1'b0; e_many <= 1'b0;
    end else begin
      e_dbl <= 1'b0; e_role <= 1'b0; e_rng <= 1'b0; e_many <= 1'b0;

      if (asg_valid) begin
        if (!pos_ok) begin
          e_rng <= 1'b1;
        end else if (!role_ok) begin
          // "Unassigned" is a state, not a role to assign. Accepting
          // it would let a caller silently un-assign a position and
          // make the completeness count drift.
          e_role <= 1'b1;
        end else if (role[asg_pos] != R_NONE) begin
          // Already assigned: refuse and report. Overwriting would
          // hide two nets competing for one connection.
          e_dbl <= 1'b1;
        end else if ((asg_role == R_SIG) && (c_sig == SIGCNT_W'(SIGNALS))) begin
          // More signal assignments than the interface has signals.
          e_many <= 1'b1;
        end else begin
          role[asg_pos] <= asg_role;
          unique case (asg_role)
            R_SIG : c_sig <= c_sig + SIGCNT_W'(1);
            R_PG  : c_pg  <= c_pg  + POSCNT_W'(1);
            R_SPR : c_spr <= c_spr + POSCNT_W'(1);
            default : ;
          endcase
        end
      end
    end
  end

  assign n_signal       = c_sig;
  assign n_power_ground = c_pg;
  assign n_spare        = c_spr;
  assign n_assigned     = POSCNT_W'(c_sig) + c_pg + c_spr;
  assign n_unassigned   = POSCNT_W'(POSITIONS) - n_assigned;
  assign all_signals_assigned = (c_sig == SIGCNT_W'(SIGNALS));
  // Complete means every signal placed. Spare and unassigned
  // positions are fine; a missing signal is not.
  assign field_complete = all_signals_assigned;
  assign err_double_assignment = e_dbl;
  assign err_bad_role          = e_role;
  assign err_pos_out_of_range  = e_rng;
  assign err_too_many_signals  = e_many;
  assign any_error = e_dbl | e_role | e_rng | e_many;
endmodule

// Bind unit note: P1-P5 reference bump_connection_budget's internals,
// P6-P9 hbm_stack_layer_map's, P10-P14 bump_assignment_guard's.

// P1 -- §3's model, as an invariant: the face count is the positions
// per side squared, and never exceeds what the area can hold.
property p_face_count_is_grid_squared;
  @(posedge clk) disable iff (!rst_n)
    (face_positions == CNT_W'((DIE_SIDE_UM / PITCH_UM) * (DIE_SIDE_UM / PITCH_UM)));
endproperty
assert property (p_face_count_is_grid_squared);

// P2 -- §4's closed form, as a published pair: the advantage is the
// die side over four times the pitch, never a divided scalar.
property p_advantage_is_side_over_four_pitch;
  @(posedge clk) disable iff (!rst_n)
    ((advantage_num == CNT_W'(DIE_SIDE_UM)) &&
     (advantage_den == CNT_W'(4 * PITCH_UM)));
endproperty
assert property (p_advantage_is_side_over_four_pitch);

// P3 -- §4: the face always beats the edge for a die larger than four
// pitches. Stated as the count comparison rather than the ratio, so
// it is checkable without dividing.
property p_face_beats_edge;
  @(posedge clk) disable iff (!rst_n)
    ((DIE_SIDE_UM > 4 * PITCH_UM) |-> (face_positions > edge_positions));
endproperty
assert property (p_face_beats_edge);

// P4 -- §6: the total always includes the power and ground overhead,
// so it is never below the signal count.
property p_total_includes_overhead;
  @(posedge clk) disable iff (!rst_n)
    (total_bumps_needed >= CNT_W'(SIGNAL_BUMPS));
endproperty
assert property (p_total_includes_overhead);

// P5 -- FORBIDDEN. A zero pitch never produces a count. It is a
// division by zero, not an infinitely dense surface.
property p_zero_pitch_never_computes;
  @(posedge clk) disable iff (!rst_n)
    (q_valid && (q_pitch_um == '0)) |=> (err_pitch_zero && !q_out_valid);
endproperty
assert property (p_zero_pitch_never_computes);

// P6 -- exactly one base die, always. §7: a stack without one has no
// external interface at all.
property p_exactly_one_base_die;
  @(posedge clk) disable iff (!rst_n)
    ((n_base_dies == LAYERCNT_W'(1)) &&
     (n_layers == n_core_dies + LAYERCNT_W'(1)));
endproperty
assert property (p_exactly_one_base_die);

// P7 -- §8's separation: the interface width does not depend on the
// stack height. The property that makes "height buys capacity, not
// bandwidth" checkable rather than memorable.
property p_interface_width_is_height_independent;
  @(posedge clk) disable iff (!rst_n)
    (interface_bits == CAP_W'(1024));
endproperty
assert property (p_interface_width_is_height_independent);

// P8 -- §8's identity: capacity is core dies times per-die density.
property p_capacity_is_dies_times_density;
  @(posedge clk) disable iff (!rst_n)
    (capacity_gb == CAP_W'((CORE_DIES * GB_PER_DIE2) / 8));
endproperty
assert property (p_capacity_is_dies_times_density);

// P9 -- base and core are mutually exclusive and exhaustive over an
// in-range layer. A layer that is neither would be unaccounted.
property p_layer_roles_partition;
  @(posedge clk) disable iff (!rst_n)
    (q_in_range |-> (q_is_base ^ q_is_core));
endproperty
assert property (p_layer_roles_partition);

// P10 -- FORBIDDEN. A position is never assigned twice. §15: that is
// two nets on one connection, not a resolvable conflict.
property p_no_double_assignment;
  @(posedge clk) disable iff (!rst_n)
    (asg_valid && (asg_role != 2'd0) &&
     ({{(32-POS_IDX_W){1'b0}}, asg_pos} < 32'(POSITIONS)) &&
     (role[asg_pos] != 2'd0))
      |=> (err_double_assignment && (n_assigned == $past(n_assigned, 1)));
endproperty
assert property (p_no_double_assignment);

// P11 -- the role counts partition the assigned positions exactly.
property p_role_counts_partition;
  @(posedge clk) disable iff (!rst_n)
    ((POSCNT_W'(n_signal) + n_power_ground + n_spare) == n_assigned);
endproperty
assert property (p_role_counts_partition);

// P12 -- assigned and unassigned partition every position.
property p_positions_fully_accounted;
  @(posedge clk) disable iff (!rst_n)
    ((n_assigned + n_unassigned) == POSCNT_W'(POSITIONS));
endproperty
assert property (p_positions_fully_accounted);

// P13 -- FORBIDDEN. The signal count never exceeds the interface's
// signal requirement.
property p_signal_count_bounded;
  @(posedge clk) disable iff (!rst_n)
    (n_signal <= SIGCNT_W'(SIGNALS));
endproperty
assert property (p_signal_count_bounded);

// P14 -- FORBIDDEN. The field is never complete while a signal is
// unassigned. §15: spare and unassigned positions are fine; a
// missing signal is an interface that cannot work.
property p_never_complete_with_a_missing_signal;
  @(posedge clk) disable iff (!rst_n)
    (field_complete |-> (n_signal == SIGCNT_W'(SIGNALS)));
endproperty
assert property (p_never_complete_with_a_missing_signal);

// ── Cover.
// A runtime pitch query answered, at a finer and a coarser pitch.
cover property (@(posedge clk) disable iff (!rst_n) q_out_valid && q_fits);
cover property (@(posedge clk) disable iff (!rst_n) q_out_valid && !q_fits);
// Each forbidden condition ATTEMPTED -- vacuous otherwise.
cover property (@(posedge clk) disable iff (!rst_n) err_pitch_zero);
cover property (@(posedge clk) disable iff (!rst_n) err_pitch_exceeds_die);
cover property (@(posedge clk) disable iff (!rst_n) err_double_assignment);
cover property (@(posedge clk) disable iff (!rst_n) err_bad_role);
cover property (@(posedge clk) disable iff (!rst_n) err_too_many_signals);
// Every layer role reached, at the bottom and the top of the stack.
cover property (@(posedge clk) disable iff (!rst_n) q_is_base);
cover property (@(posedge clk) disable iff (!rst_n)
                  q_is_core && (q_core_index == LAYER_IDX_W'(CORE_DIES - 1)));
// Every bump role actually assigned.
cover property (@(posedge clk) disable iff (!rst_n) n_signal != '0);
cover property (@(posedge clk) disable iff (!rst_n) n_power_ground != '0);
cover property (@(posedge clk) disable iff (!rst_n) n_spare != '0);
// THE COMPLETENESS COVER: every signal placed, with spare and
// unassigned positions remaining -- §5's 2% occupancy as a state.
cover property (@(posedge clk) disable iff (!rst_n)
                  field_complete && (n_unassigned != '0));
// And the near-miss: every position assigned except one signal.
cover property (@(posedge clk) disable iff (!rst_n)
                  !field_complete && (n_signal == SIGCNT_W'(SIGNALS) - 1));

// Independent geometry reference. Computes counts by explicitly
// walking a grid rather than by multiplying, so agreement with the
// DUT is evidence rather than a restatement of the same product.
// SIMULATION-ONLY.
class bump_geometry_ref;
  int side_um, pitch_um;

  function void build(int side, int pitch);
    side_um = side; pitch_um = pitch;
  endfunction

  // Walk the grid. Deliberately O(n) rather than a squared product.
  function int face_positions();
    int n = 0;
    for (int x = 0; x + pitch_um <= side_um; x += pitch_um)
      for (int y = 0; y + pitch_um <= side_um; y += pitch_um)
        n++;
    return n;
  endfunction

  // Walk the perimeter as four sides.
  function int edge_positions();
    int n = 0;
    for (int s = 0; s < 4; s++)
      for (int x = 0; x + pitch_um <= side_um; x += pitch_um)
        n++;
    return n;
  endfunction

  // §4's closed form, as a pair -- never a real.
  function void advantage(output int num, output int den);
    num = side_um;
    den = 4 * pitch_um;
  endfunction

  // §6: signals plus overhead expressed as a ratio.
  function int total_bumps(int signals, int pg_num, int pg_den);
    return (signals * (pg_den + pg_num)) / pg_den;
  endfunction
endclass

  THE HEIGHT THAT WAS ASSUMED TO BUY BANDWIDTH
    Parameterise the stack at 2, 4, 8 and 12 core dies and read both
    published outputs.

      CORE_DIES   capacity_gb   interface_bits
           2            4            1024
           4            8            1024
           8           16            1024
          12           24            1024

    P7 interface_width_is_height_independent   PASS at every height
    P8 capacity_is_dies_times_density          PASS at every height

    what a reader expecting otherwise would predict:
      "a 12-high stack has six times the dies of a 2-high stack,
       so it should deliver more bandwidth"

    diagnosis : it delivers exactly the same bandwidth. The
      interface is 1024 bits wide regardless of how many dies sit
      behind it, because the width is a property of the base die and
      the interposer -- not of the stack.

    why the mistake is easy : capacity and bandwidth are both
      "more memory", both scale with money, and both appear in the
      same product brief. Only one of them scales with height.

    the consequence, which 26.4 develops : an accelerator that needs
      more bandwidth must add STACKS, and one that needs more
      capacity can add DIES. Those are different purchases with
      different costs, and confusing them produces a system that is
      expensive in the wrong dimension.

    the fix : publish both outputs from one block (§14) so the
      independence is visible in the interface rather than
      remembered from prose.