HBM for AI Accelerators

   required bandwidth  =  C / I        bytes per second

   stacks required  =  (C / I)  /  307.2 GB/s

   one requester, Q outstanding, 64 B each, latency T
      bandwidth  =  Q x 64 B / T

   streams usefully occupied  =  min(Q, total streams)

// ---------------------------------------------------------------------
// hbm_system_budget -- what K stacks of a given height offer, and the
// independence between the two purchases.
//
// CLASSIFICATION: educational, synthesisable.
//
// UNITS: bandwidth in GB/s scaled by 10 (so 307.2 -> 3072) to stay in
// integers. Capacity in GB. No reals, no division where a comparison
// will do.
//
// WHAT IT DOES NOT MODEL:
//   - the interposer, the stacks, TSVs, or any physical property
//     (26.2 and 26.3 own all of it)
//   - any latency. §7's model needs one and it is ILLUSTRATIVE there;
//     this block has none.
//   - any real accelerator, product or workload
//   - single-stack bandwidth arithmetic (4.8 §5's bandwidth_account
//     owns it; this aggregates rather than recomputes)
//
// THE INDEPENDENCE IS ENFORCED, NOT ASSUMED (§1, 26.2 §8): bandwidth
// and stream count depend on STACKS only, capacity on stacks AND
// height. P2 and P3 assert it because a budget that let height leak
// into bandwidth would reproduce the exact error §3's callout warns
// about.
// ---------------------------------------------------------------------
module hbm_system_budget #(
  parameter int STACKS        = 12,
  parameter int HEIGHT        = 4,       // CURRICULUM-DERIVED set (4.8 §2)
  parameter int GB_PER_DIE    = 2,       // 26.2 §8's inference
  parameter int BW_PER_STACK_X10 = 3072, // 307.2 GB/s, x10 (4.8 §2)
  parameter int STREAMS_PER_STACK = 16,  // 26.1 §4
  parameter int MAX_STACKS    = 16,
  parameter int STK_IDX_W     = $clog2(MAX_STACKS),
  // COUNTS need one more bit than the matching index.
  parameter int STKCNT_W      = $clog2(MAX_STACKS + 1),
  parameter int ACC_W         = 32
) (
  input  logic                  clk,
  input  logic                  rst_n,

  // ── Query a hypothetical configuration at runtime.
  input  logic                  q_valid,
  input  logic [STK_IDX_W:0]    q_stacks,
  input  logic [4:0]            q_height,

  output logic [ACC_W-1:0]      q_capacity_gb,
  output logic [ACC_W-1:0]      q_bandwidth_x10,
  output logic [ACC_W-1:0]      q_streams,
  output logic                  q_out_valid,

  // ── The elaborated configuration.
  output logic [ACC_W-1:0]      capacity_gb,
  output logic [ACC_W-1:0]      bandwidth_x10,
  output logic [ACC_W-1:0]      streams,
  output logic [STKCNT_W-1:0]   n_stacks,

  // §2's ratio, as a PAIR. bandwidth/capacity is rarely an integer,
  // so it is never divided here.
  output logic [ACC_W-1:0]      bw_per_cap_num,
  output logic [ACC_W-1:0]      bw_per_cap_den,
  // §6: constant at 19.2 GB/s, also as a pair.
  output logic [ACC_W-1:0]      bw_per_stream_num,
  output logic [ACC_W-1:0]      bw_per_stream_den,

  output logic                  err_height_unsupported,
  output logic                  err_stacks_out_of_range,
  output logic                  any_error
);

  localparam int CAP   = STACKS * HEIGHT * GB_PER_DIE;
  localparam int BW10  = STACKS * BW_PER_STACK_X10;
  localparam int STRM  = STACKS * STREAMS_PER_STACK;

  initial begin
    if (MAX_STACKS < 2)
      // A single-stack maximum makes the whole budget degenerate, and
      // $clog2(1) is 0 -- legal here only because the port is
      // [STK_IDX_W:0] rather than [STK_IDX_W-1:0]. Guarded anyway, for
      // consistency with 26.1 and 26.3, which require >= 2 for
      // anything they index.
      $fatal(1, "hbm_system_budget: MAX_STACKS must be at least 2");
    if (STACKS < 1 || STACKS > MAX_STACKS)
      $fatal(1, "hbm_system_budget: STACKS must be 1..%0d, got %0d", MAX_STACKS, STACKS);
    if (!(HEIGHT inside {2, 4, 8, 12}))
      // CURRICULUM-DERIVED height set (4.8 §2). Refused rather than
      // accommodated, because accommodating it would imply a
      // generality the source does not support.
      $fatal(1, "hbm_system_budget: HEIGHT must be 2, 4, 8 or 12, got %0d", HEIGHT);
    if (GB_PER_DIE < 1 || BW_PER_STACK_X10 < 1 || STREAMS_PER_STACK < 1)
      $fatal(1, "hbm_system_budget: per-stack figures must be positive");
    if (STKCNT_W <= STK_IDX_W && MAX_STACKS > 1)
      // COUNT vs INDEX: too narrow and n_stacks cannot represent a
      // fully populated system.
      $fatal(1, "hbm_system_budget: STKCNT_W too narrow to count MAX_STACKS");
    // §1's independence, checked at elaboration for every legal
    // height: bandwidth and streams must not depend on HEIGHT.
    if (BW10 != STACKS * BW_PER_STACK_X10)
      $fatal(1, "hbm_system_budget: bandwidth must depend on STACKS alone");
    if (STRM != STACKS * STREAMS_PER_STACK)
      $fatal(1, "hbm_system_budget: stream count must depend on STACKS alone");
    if (CAP > ((1 << (ACC_W - 1)) - 1) || BW10 > ((1 << (ACC_W - 1)) - 1))
      $fatal(1, "hbm_system_budget: ACC_W too narrow for this configuration");
  end

  logic             qv, e_hgt, e_stk;
  logic [ACC_W-1:0] qc, qb, qs;

  // Declared above the continuous assigns that read them.
  logic hgt_ok, stk_ok;
  assign hgt_ok = (q_height inside {5'd2, 5'd4, 5'd8, 5'd12});
  assign stk_ok = (q_stacks != '0) &&
                  ({{(32-(STK_IDX_W+1)){1'b0}}, q_stacks} <= ACC_W'(MAX_STACKS));

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      qv <= 1'b0; qc <= '0; qb <= '0; qs <= '0;
      e_hgt <= 1'b0; e_stk <= 1'b0;
    end else begin
      qv <= 1'b0; e_hgt <= 1'b0; e_stk <= 1'b0;
      if (q_valid) begin
        if (!stk_ok)      e_stk <= 1'b1;
        else if (!hgt_ok) e_hgt <= 1'b1;
        else begin
          qc <= ACC_W'(q_stacks) * ACC_W'(q_height) * ACC_W'(GB_PER_DIE);
          qb <= ACC_W'(q_stacks) * ACC_W'(BW_PER_STACK_X10);
          qs <= ACC_W'(q_stacks) * ACC_W'(STREAMS_PER_STACK);
          qv <= 1'b1;
        end
      end
    end
  end

  assign capacity_gb   = ACC_W'(CAP);
  assign bandwidth_x10 = ACC_W'(BW10);
  assign streams       = ACC_W'(STRM);
  assign n_stacks      = STKCNT_W'(STACKS);
  assign bw_per_cap_num    = ACC_W'(BW10);
  assign bw_per_cap_den    = ACC_W'(CAP);
  assign bw_per_stream_num = ACC_W'(BW10);
  assign bw_per_stream_den = ACC_W'(STRM);
  assign q_capacity_gb   = qc;
  assign q_bandwidth_x10 = qb;
  assign q_streams       = qs;
  assign q_out_valid     = qv;
  assign err_height_unsupported  = e_hgt;
  assign err_stacks_out_of_range = e_stk;
  assign any_error = e_hgt | e_stk;
endmodule

// ---------------------------------------------------------------------
// stream_supply_monitor -- can the requester side actually fill the
// streams the configuration offers?
//
// CLASSIFICATION: educational, synthesisable.
//
// COLLISION NOTE: 26.1 §12's pc_stream_monitor observes which
// pseudo-channels within ONE stack are active. This block observes
// the REQUESTER side across a whole system: how many accesses are
// outstanding, and how many distinct streams they reach. Different
// side of the same interface, different question.
//
// WHAT IT DOES NOT MODEL:
//   - latency, or bandwidth in bytes per second. 1.8 owns the
//     latency model and 4.8 §5 the bandwidth arithmetic; neither is
//     rebuilt.
//   - the memory, the stacks, or any physical property
//   - WHY a stream is unreached. §9: concentration and insufficient
//     parallelism produce the same symptom, and this block separates
//     the two measurements so a diagnosis is possible. It does not
//     make the diagnosis.
// ---------------------------------------------------------------------
module stream_supply_monitor #(
  parameter int STREAMS   = 192,         // §6: K x 16
  parameter int STRM_IDX_W = $clog2(STREAMS),
  // A COUNT up to STREAMS needs clog2(STREAMS+1).
  parameter int STRMCNT_W = $clog2(STREAMS + 1),
  parameter int OUTS_W    = 12,
  parameter int CNT_W     = 28
) (
  input  logic                    clk,
  input  logic                    rst_n,

  // ── Requester side: an access issued to a stream, and a completion.
  input  logic                    issue_valid,
  input  logic [STRM_IDX_W-1:0]   issue_stream,
  input  logic                    complete_valid,

  // ── MEASUREMENT ONE: are there enough accesses in flight?
  output logic [OUTS_W-1:0]       outstanding,
  output logic [OUTS_W-1:0]       peak_outstanding,
  output logic                    enough_outstanding,

  // ── MEASUREMENT TWO: do they reach the streams? §9 -- reported
  //    separately because the two causes share a symptom.
  output logic [STRMCNT_W-1:0]    streams_reached,
  output logic                    full_coverage,
  output logic [STRMCNT_W-1:0]    streams_never_reached,

  // The two diagnoses §9 says must be distinguishable.
  output logic                    starved_not_enough_requests,
  output logic                    starved_concentrated,

  output logic [CNT_W-1:0]        cnt_issued,
  output logic [CNT_W-1:0]        cnt_completed,

  output logic                    err_stream_out_of_range,
  output logic                    err_complete_without_outstanding,
  output logic                    any_error
);

  initial begin
    if (STREAMS < 2)
      $fatal(1, "stream_supply_monitor: need at least 2 streams");
    if (STRM_IDX_W != $clog2(STREAMS))
      $fatal(1, "stream_supply_monitor: STRM_IDX_W must address STREAMS");
    if (STRMCNT_W <= STRM_IDX_W)
      // COUNT vs INDEX: too narrow and full_coverage is unreachable,
      // which reads as permanent under-coverage -- the pessimistic
      // direction, and still wrong.
      $fatal(1, "stream_supply_monitor: STRMCNT_W too narrow to count STREAMS");
    if ((1 << OUTS_W) <= STREAMS)
      // §8: filling every stream needs at least STREAMS accesses in
      // flight, so the counter must be able to represent that.
      $fatal(1, "stream_supply_monitor: OUTS_W cannot represent STREAMS outstanding");
  end

  logic [STREAMS-1:0]  touched;
  logic [OUTS_W-1:0]   outs, pk;
  logic [CNT_W-1:0]    n_iss, n_cmp;
  logic                e_rng, e_cmp;

  // Declared above the continuous assigns that read them.
  logic strm_ok;
  assign strm_ok = ({{(32-STRM_IDX_W){1'b0}}, issue_stream} < 32'(STREAMS));

  logic [STRMCNT_W-1:0] n_touch;
  always_comb begin
    n_touch = '0;
    for (int s = 0; s < STREAMS; s++)
      if (touched[s]) n_touch = n_touch + STRMCNT_W'(1);
  end

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      touched <= '0; outs <= '0; pk <= '0;
      n_iss <= '0; n_cmp <= '0; e_rng <= 1'b0; e_cmp <= 1'b0;
    end else begin
      e_rng <= 1'b0; e_cmp <= 1'b0;

      if (issue_valid) begin
        if (!strm_ok) begin
          // Out of range: reported, and NOT counted. A bad stream
          // index folded into coverage would inflate it.
          e_rng <= 1'b1;
        end else begin
          touched[issue_stream] <= 1'b1;
          if (outs != {OUTS_W{1'b1}}) begin
            // Compare the INCREMENTED value: outs's write lands on
            // this edge, so testing outs here would under-report the
            // peak by one. The stale-register hazard Module 21 §10,
            // 24.3 §12, 25.2 §15 and 26.1 §11 all name.
            if ((outs + OUTS_W'(1)) > pk) pk <= outs + OUTS_W'(1);
            outs <= outs + OUTS_W'(1);
          end
          if (n_iss != {CNT_W{1'b1}}) n_iss <= n_iss + CNT_W'(1);
        end
      end

      if (complete_valid) begin
        if (outs == '0) begin
          // A completion with nothing outstanding is a bookkeeping
          // error somewhere, not a negative occupancy.
          e_cmp <= 1'b1;
        end else begin
          outs <= outs - OUTS_W'(1);
          if (n_cmp != {CNT_W{1'b1}}) n_cmp <= n_cmp + CNT_W'(1);
        end
      end
    end
  end

  assign outstanding      = outs;
  assign peak_outstanding = pk;
  // §8: at least one access per stream is needed to touch them all.
  assign enough_outstanding = (pk >= OUTS_W'(STREAMS));
  assign streams_reached  = n_touch;
  assign full_coverage    = (n_touch == STRMCNT_W'(STREAMS));
  assign streams_never_reached = STRMCNT_W'(STREAMS) - n_touch;
  // §9's two diagnoses, separated. Not enough requests: the peak
  // never reached the stream count. Concentrated: it did, and
  // coverage is still short.
  assign starved_not_enough_requests = !full_coverage && !enough_outstanding;
  assign starved_concentrated        = !full_coverage &&  enough_outstanding;
  assign cnt_issued    = n_iss;
  assign cnt_completed = n_cmp;
  assign err_stream_out_of_range          = e_rng;
  assign err_complete_without_outstanding = e_cmp;
  assign any_error = e_rng | e_cmp;
endmodule

// ---------------------------------------------------------------------
// intensity_balance_checker -- given a compute rate, an arithmetic
// intensity and an available bandwidth, which side limits?
//
// CLASSIFICATION: educational, synthesisable.
//
// UNITS ARE SCALED INTEGERS. Compute in Gops/s; intensity in ops per
// byte; bandwidth in GB/s x10 (matching hbm_system_budget). No reals
// and NO DIVISION -- the comparison is done by cross-multiplication.
//
// WHAT IT DOES NOT MODEL:
//   - any real compute rate, workload intensity or utilisation. §5's
//     callout: the model assumes peak compute is achievable,
//     intensity is a single number, and bandwidth is fully
//     deliverable. All three are optimistic, so every requirement it
//     reports is a LOWER BOUND.
//   - latency (1.8 owns it), or the memory itself
//   - what to DO about an imbalance. Raising intensity is a compute
//     architecture decision and adding stacks is a purchasing one;
//     this block says which side is short.
// ---------------------------------------------------------------------
module intensity_balance_checker #(
  parameter int BW_SCALE = 10,           // bandwidth is GB/s x10
  parameter int W        = 40
) (
  input  logic              clk,
  input  logic              rst_n,

  input  logic              eval,
  input  logic [W-1:0]      compute_gops,        // ILLUSTRATIVE
  input  logic [W-1:0]      intensity_ops_byte,  // ILLUSTRATIVE
  input  logic [W-1:0]      bandwidth_x10,       // from the budget

  // ── Verdict. Three outcomes, because "balanced" is a real answer.
  output logic              memory_limited,
  output logic              compute_limited,
  output logic              balanced,

  // Required bandwidth as a PAIR: compute over intensity, never
  // divided. A caller states its own denominator.
  output logic [W-1:0]      required_num,
  output logic [W-1:0]      required_den,

  // How many stacks' worth short or spare, as a comparison rather
  // than a quotient.
  output logic [W-1:0]      have_scaled,
  output logic [W-1:0]      need_scaled,

  output logic              err_zero_intensity,
  output logic              err_zero_bandwidth,
  output logic              any_error
);

  initial begin
    if (BW_SCALE < 1)
      $fatal(1, "intensity_balance_checker: BW_SCALE must be positive");
    if (W < 32)
      // The cross-multiplication multiplies two supplied values;
      // too narrow and it wraps, which silently inverts the verdict.
      $fatal(1, "intensity_balance_checker: W must be at least 32 for the cross product");
  end

  logic v_mem, v_cmp, v_bal, e_int, e_bw;
  logic [W-1:0] have_q, need_q;

  // ── No division. required = compute/intensity GB/s; available =
  //    bandwidth_x10 / BW_SCALE GB/s. Compare by cross-multiplying:
  //      compute * BW_SCALE   vs   bandwidth_x10 * intensity
  //    Declared above the continuous assigns that read them.
  logic [W-1:0] lhs, rhs;
  assign lhs = compute_gops  * W'(BW_SCALE);
  assign rhs = bandwidth_x10 * intensity_ops_byte;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      v_mem <= 1'b0; v_cmp <= 1'b0; v_bal <= 1'b0;
      e_int <= 1'b0; e_bw <= 1'b0; have_q <= '0; need_q <= '0;
    end else begin
      e_int <= 1'b0; e_bw <= 1'b0;
      if (eval) begin
        if (intensity_ops_byte == '0) begin
          // Zero intensity means every operation touches memory
          // without reuse, so the requirement is unbounded. Reported
          // rather than computed as a very large number.
          e_int <= 1'b1;
          v_mem <= 1'b0; v_cmp <= 1'b0; v_bal <= 1'b0;
        end else if (bandwidth_x10 == '0) begin
          e_bw <= 1'b1;
          v_mem <= 1'b0; v_cmp <= 1'b0; v_bal <= 1'b0;
        end else begin
          have_q <= rhs;
          need_q <= lhs;
          // lhs > rhs : the compute rate needs more bandwidth than
          // exists -> memory limited.
          v_mem <= (lhs >  rhs);
          v_cmp <= (lhs <  rhs);
          v_bal <= (lhs == rhs);
        end
      end
    end
  end

  assign memory_limited  = v_mem;
  assign compute_limited = v_cmp;
  assign balanced        = v_bal;
  assign required_num    = compute_gops;
  assign required_den    = intensity_ops_byte;
  assign have_scaled     = have_q;
  assign need_scaled     = need_q;
  assign err_zero_intensity = e_int;
  assign err_zero_bandwidth = e_bw;
  assign any_error = e_int | e_bw;
endmodule

// Bind unit note: P1-P5 reference hbm_system_budget's internals,
// P6-P10 stream_supply_monitor's, P11-P14
// intensity_balance_checker's.

// P1 -- §1's identity: capacity is stacks x height x per-die.
property p_capacity_is_the_product;
  @(posedge clk) disable iff (!rst_n)
    (capacity_gb == ACC_W'(STACKS * HEIGHT * GB_PER_DIE));
endproperty
assert property (p_capacity_is_the_product);

// P2 -- FORBIDDEN. Bandwidth depends on the stack count ALONE. §3's
// callout: a budget in which height leaked into bandwidth would
// reproduce the exact error the chapter exists to prevent, silently.
property p_bandwidth_ignores_height;
  @(posedge clk) disable iff (!rst_n)
    (bandwidth_x10 == ACC_W'(STACKS * BW_PER_STACK_X10));
endproperty
assert property (p_bandwidth_ignores_height);

// P3 -- FORBIDDEN. The stream count likewise depends on stacks alone.
property p_streams_ignore_height;
  @(posedge clk) disable iff (!rst_n)
    (streams == ACC_W'(STACKS * STREAMS_PER_STACK));
endproperty
assert property (p_streams_ignore_height);

// P4 -- §6: bandwidth per stream is constant, because both scale
// with the stack count. Asserted as the cross product so no division
// is needed.
property p_bandwidth_per_stream_is_constant;
  @(posedge clk) disable iff (!rst_n)
    ((bw_per_stream_num * ACC_W'(STREAMS_PER_STACK)) ==
     (bw_per_stream_den * ACC_W'(BW_PER_STACK_X10)));
endproperty
assert property (p_bandwidth_per_stream_is_constant);

// P5 -- FORBIDDEN. An unsupported height never produces a result.
property p_bad_height_never_computes;
  @(posedge clk) disable iff (!rst_n)
    (q_valid && !(q_height inside {5'd2, 5'd4, 5'd8, 5'd12}) && (q_stacks != '0))
      |=> (err_height_unsupported && !q_out_valid);
endproperty
assert property (p_bad_height_never_computes);

// P6 -- outstanding never goes negative, and a completion with
// nothing in flight is reported rather than wrapping.
property p_outstanding_never_underflows;
  @(posedge clk) disable iff (!rst_n)
    (complete_valid && (outstanding == '0)) |=> err_complete_without_outstanding;
endproperty
assert property (p_outstanding_never_underflows);

// P7 -- the peak is monotone and never below the current occupancy.
// §12's hazard: a peak compared pre-increment is one short, which
// flips the §9 diagnosis at exactly the boundary.
property p_peak_is_monotone_and_covering;
  @(posedge clk) disable iff (!rst_n)
    ((peak_outstanding >= outstanding) &&
     (peak_outstanding >= $past(peak_outstanding, 1)));
endproperty
assert property (p_peak_is_monotone_and_covering);

// P8 -- FORBIDDEN. An out-of-range stream index never counts toward
// coverage. A bad index folded in would inflate it.
property p_bad_stream_never_counted;
  @(posedge clk) disable iff (!rst_n)
    (err_stream_out_of_range |-> (streams_reached == $past(streams_reached, 1)));
endproperty
assert property (p_bad_stream_never_counted);

// P9 -- coverage and never-reached partition the streams exactly.
property p_coverage_partitions_streams;
  @(posedge clk) disable iff (!rst_n)
    ((streams_reached + streams_never_reached) == STRMCNT_W'(STREAMS));
endproperty
assert property (p_coverage_partitions_streams);

// P10 -- §9's two diagnoses are mutually exclusive, and neither holds
// under full coverage. The property that makes them distinguishable.
property p_starvation_causes_are_exclusive;
  @(posedge clk) disable iff (!rst_n)
    (!(starved_not_enough_requests && starved_concentrated) &&
     (full_coverage |-> (!starved_not_enough_requests && !starved_concentrated)));
endproperty
assert property (p_starvation_causes_are_exclusive);

// P11 -- the three balance verdicts are mutually exclusive.
property p_balance_verdict_exclusive;
  @(posedge clk) disable iff (!rst_n)
    $onehot0({memory_limited, compute_limited, balanced});
endproperty
assert property (p_balance_verdict_exclusive);

// P12 -- FORBIDDEN. Zero intensity never produces a verdict. §5: the
// requirement is unbounded, and a finite number would invite a
// caller to treat it as a target.
property p_zero_intensity_no_verdict;
  @(posedge clk) disable iff (!rst_n)
    (eval && (intensity_ops_byte == '0))
      |=> (err_zero_intensity && !memory_limited && !compute_limited && !balanced);
endproperty
assert property (p_zero_intensity_no_verdict);

// P13 -- the verdict matches the cross product, so no division was
// smuggled in anywhere.
property p_verdict_matches_cross_product;
  @(posedge clk) disable iff (!rst_n)
    (memory_limited |-> (need_scaled > have_scaled));
endproperty
assert property (p_verdict_matches_cross_product);

// P14 -- the required-bandwidth pair is the inputs verbatim, never a
// quotient. §5: the caller states its own denominator.
property p_required_is_published_as_a_pair;
  @(posedge clk) disable iff (!rst_n)
    ((required_num == compute_gops) && (required_den == intensity_ops_byte));
endproperty
assert property (p_required_is_published_as_a_pair);

// ── Cover.
// Both of §3's configurations, which is the chapter's central result:
// the same capacity at different bandwidths.
cover property (@(posedge clk) disable iff (!rst_n)
                  q_out_valid && (q_capacity_gb == ACC_W'(96)) &&
                  (q_bandwidth_x10 == ACC_W'(12288)));
cover property (@(posedge clk) disable iff (!rst_n)
                  q_out_valid && (q_capacity_gb == ACC_W'(96)) &&
                  (q_bandwidth_x10 == ACC_W'(36864)));
// Every verified height queried, and each error attempted.
cover property (@(posedge clk) disable iff (!rst_n)
                  q_out_valid && (q_height == 5'd2));
cover property (@(posedge clk) disable iff (!rst_n)
                  q_out_valid && (q_height == 5'd12));
cover property (@(posedge clk) disable iff (!rst_n) err_height_unsupported);
cover property (@(posedge clk) disable iff (!rst_n) err_stacks_out_of_range);
// Full stream coverage reached, and BOTH starvation causes -- §9's
// whole point is that these are different, so a suite must reach each.
cover property (@(posedge clk) disable iff (!rst_n) full_coverage);
cover property (@(posedge clk) disable iff (!rst_n) starved_not_enough_requests);
cover property (@(posedge clk) disable iff (!rst_n) starved_concentrated);
cover property (@(posedge clk) disable iff (!rst_n) err_complete_without_outstanding);
cover property (@(posedge clk) disable iff (!rst_n) err_stream_out_of_range);
// Outstanding reaching exactly the stream count -- the boundary at
// which §12's hazard flips the diagnosis.
cover property (@(posedge clk) disable iff (!rst_n)
                  peak_outstanding == OUTS_W'(STREAMS));
// All three balance verdicts, and the unbounded case.
cover property (@(posedge clk) disable iff (!rst_n) memory_limited);
cover property (@(posedge clk) disable iff (!rst_n) compute_limited);
cover property (@(posedge clk) disable iff (!rst_n) balanced);
cover property (@(posedge clk) disable iff (!rst_n) err_zero_intensity);

// Independent configuration reference. Builds the stack list
// explicitly and sums, rather than multiplying, so agreement with
// the DUT is evidence rather than a restatement of the same product.
// SIMULATION-ONLY.
class hbm_config_ref;
  int stacks, height, gb_per_die, bw_per_stack_x10, streams_per_stack;

  function void build(int k, int h);
    stacks = k; height = h;
    gb_per_die = 2; bw_per_stack_x10 = 3072; streams_per_stack = 16;
  endfunction

  // Sum per stack rather than multiply.
  function int capacity_gb();
    int c = 0;
    for (int s = 0; s < stacks; s++) c += height * gb_per_die;
    return c;
  endfunction

  function int bandwidth_x10();
    int b = 0;
    for (int s = 0; s < stacks; s++) b += bw_per_stack_x10;
    return b;   // deliberately does NOT reference height
  endfunction

  function int streams();
    int n = 0;
    for (int s = 0; s < stacks; s++) n += streams_per_stack;
    return n;   // likewise
  endfunction

  // §4's requirement, as a pair.
  function void required(int compute_gops, int intensity,
                         output int num, output int den);
    num = compute_gops; den = intensity;
  endfunction

  // The cross-multiplied comparison, computed independently.
  function int limited(int compute_gops, int intensity, int bw_x10);
    if (intensity == 0) return -1;                    // unbounded
    if (compute_gops * 10 >  bw_x10 * intensity) return 1;   // memory
    if (compute_gops * 10 <  bw_x10 * intensity) return 2;   // compute
    return 0;                                         // balanced
  endfunction
endclass

  THREE WAYS TO SEE THE SAME SYMPTOM
    A 12-stack system: 192 streams, 3686.4 GB/s rated.

  (A) 4 accesses outstanding, spread across 4 streams
        peak_outstanding              4
        streams_reached               4
        enough_outstanding            0
        starved_not_enough_requests   1   <-- too little parallelism
        starved_concentrated          0
        fix: more outstanding requests. An address remap changes
             nothing, because there is nothing to spread.

  (B) 192 accesses outstanding, all within one stack
        peak_outstanding            192
        streams_reached              16
        enough_outstanding            1
        starved_not_enough_requests   0
        starved_concentrated          1   <-- distribution, not count
        fix: address mapping. Adding requests changes nothing,
             because 176 streams are unreachable by construction.

  (C) the same as (B), but with the peak compared PRE-INCREMENT
        peak_outstanding            191   <-- one short
        enough_outstanding            0   <-- flips FALSE at 192
        starved_not_enough_requests   1   <-- WRONG DIAGNOSIS
        starved_concentrated          0
        P7 peak_is_monotone_and_covering   FAIL

    (A) and (B) both present externally as "we are getting a
    fraction of the rated bandwidth and the memory looks idle" --
    1.8 §15's symptom exactly. They need OPPOSITE fixes.

    and (C) is the one that matters for this chapter: a peak
    under-reported by exactly one turns (B) into (A). The flip
    happens precisely at peak == STREAMS, which is the boundary the
    whole diagnosis hinges on -- so the off-by-one is not a small
    error, it is a reliable misdiagnosis at the only interesting
    operating point.

    the fix : both measurements published separately (§12), the
    peak folded combinationally, and both starvation covers
    required. A single "underutilised" flag cannot distinguish any
    of the three.