Through-Silicon Vias (TSVs)

   spares available in total        48
   failures the stack tolerates     depends entirely on their DISTRIBUTION
   worst case                       2 failures, if both land in one group
   best case                        48 failures, one per group

// ---------------------------------------------------------------------
// tsv_count_budget -- conductors per die under a bussed or a
// dedicated organisation, and the traversal count a height implies.
//
// CLASSIFICATION: educational, synthesisable. COUNTING ONLY.
//
// WHAT IT DOES NOT MODEL -- the most important part of this header:
//   - capacitance, resistance, inductance. A via has all three and
//     NONE is computed here.
//   - thermal resistance, temperature, mechanical stress, aspect
//     ratio, keep-outs, placement rules.
//   - YIELD, and no probability of any kind. §5 and §6's arithmetic
//     is PROSE, computed outside the design, precisely so that no
//     synthesisable block appears to predict a yield.
//   - electrical loading. §2's callout notes every die on a bussed
//     set presents a load, and says plainly that this chapter cannot
//     quantify it.
// A VIA IS AN INTEGER HERE. Converting one into an electrical result
// would be this module's fake-eye failure (22.3).
//
// BOTH MODELS ARE SUPPORTED because §2 could not establish which is
// used. The structural argument favours bussing; the parameter
// exists so the open question is visible rather than assumed away.
// ---------------------------------------------------------------------
module tsv_count_budget #(
  parameter int SIGNALS     = 1024,      // CURRICULUM-DERIVED (4.8 §2)
  // §1: power/ground per signal, as a ratio so no real is needed.
  parameter int PG_NUM      = 2,
  parameter int PG_DEN      = 1,
  parameter int CORE_DIES   = 12,        // CURRICULUM-DERIVED set (4.8 §2)
  parameter bit DEDICATED   = 1'b0,      // 0 = bussed (§2 model A)
  parameter int DIE_IDX_W   = $clog2(CORE_DIES),
  // A COUNT of dies up to CORE_DIES needs clog2(CORE_DIES+1).
  parameter int DIECNT_W    = $clog2(CORE_DIES + 1),
  parameter int CNT_W        = 32
) (
  input  logic                  clk,
  input  logic                  rst_n,

  // ── Query a die level, counted from the bottom (0 = lowest core).
  input  logic                  q_valid,
  input  logic [DIE_IDX_W-1:0]  q_die,

  output logic [CNT_W-1:0]      q_conductors,
  // §3: a path to this die traverses this many die bodies.
  output logic [DIECNT_W-1:0]   q_traversals,
  output logic                  q_in_range,

  // ── The organisation, published.
  output logic [CNT_W-1:0]      conductors_per_interface,
  output logic [CNT_W-1:0]      conductors_bottom_die,
  output logic [CNT_W-1:0]      conductors_top_die,
  output logic [CNT_W-1:0]      total_traversals,
  output logic                  is_bussed,
  // §2: under a dedicated model the bottom die carries N times the
  // top. Published as a PAIR so no division happens here.
  output logic [CNT_W-1:0]      asymmetry_num,
  output logic [CNT_W-1:0]      asymmetry_den,

  output logic                  err_die_out_of_range,
  output logic                  any_error
);

  // §1: signals plus overhead, without a real.
  localparam int IFACE = (SIGNALS * (PG_DEN + PG_NUM)) / PG_DEN;
  // §2: bussed is constant; dedicated grows downward.
  localparam int BOTTOM = DEDICATED ? (IFACE * CORE_DIES) : IFACE;
  localparam int TOP    = IFACE;
  // §3: N(N+1)/2 traversals to reach every die.
  localparam int TRAV_TOTAL = (CORE_DIES * (CORE_DIES + 1)) / 2;

  initial begin
    if (SIGNALS < 1)
      $fatal(1, "tsv_count_budget: SIGNALS must be at least 1");
    if (PG_DEN < 1 || PG_NUM < 0)
      $fatal(1, "tsv_count_budget: overhead must be non-negative over a positive denominator");
    if (!(CORE_DIES inside {2, 4, 8, 12}))
      // CURRICULUM-DERIVED height set (4.8 §2). A height outside it
      // is refused rather than accommodated, because accommodating
      // it would imply a generality the source does not support.
      $fatal(1, "tsv_count_budget: CORE_DIES must be 2, 4, 8 or 12, got %0d", CORE_DIES);
    if (IFACE < SIGNALS)
      // §1: the overhead must actually be counted.
      $fatal(1, "tsv_count_budget: interface count (%0d) below signal count (%0d)",
             IFACE, SIGNALS);
    if (DIECNT_W <= DIE_IDX_W && CORE_DIES > 1)
      // COUNT vs INDEX. Too narrow and the traversal count for the
      // top die cannot be represented, which silently understates
      // the deepest path -- the flattering direction.
      $fatal(1, "tsv_count_budget: DIECNT_W too narrow to count CORE_DIES");
    if (BOTTOM > ((1 << (CNT_W - 1)) - 1))
      $fatal(1, "tsv_count_budget: CNT_W too narrow for the bottom-die count");
    // §2's asymmetry identity: bussed means symmetric, dedicated
    // means the bottom carries exactly CORE_DIES times the top.
    if (!DEDICATED && (BOTTOM != TOP))
      $fatal(1, "tsv_count_budget: a bussed organisation must be symmetric");
    if (DEDICATED && (BOTTOM != TOP * CORE_DIES))
      $fatal(1, "tsv_count_budget: dedicated bottom count must be CORE_DIES x top");
  end

  logic e_range;

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

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

  // Under the dedicated model a die at level d carries its own set
  // plus every set passing through it to the dies above.
  logic [CNT_W-1:0] dedicated_at_d;
  assign dedicated_at_d = CNT_W'(IFACE) *
                          (CNT_W'(CORE_DIES) - {{(32-DIE_IDX_W){1'b0}}, q_die});

  assign q_conductors = DEDICATED ? dedicated_at_d : CNT_W'(IFACE);
  // §3: reaching die d traverses d+1 die bodies, counting from 0.
  assign q_traversals = DIECNT_W'({{(32-DIE_IDX_W){1'b0}}, q_die} + 32'd1);
  assign q_in_range   = in_rng;

  assign conductors_per_interface = CNT_W'(IFACE);
  assign conductors_bottom_die    = CNT_W'(BOTTOM);
  assign conductors_top_die       = CNT_W'(TOP);
  assign total_traversals         = CNT_W'(TRAV_TOTAL);
  assign is_bussed                = !DEDICATED;
  assign asymmetry_num            = CNT_W'(BOTTOM);
  assign asymmetry_den            = CNT_W'(TOP);

  assign err_die_out_of_range = e_range;
  assign any_error = e_range;
endmodule

// ---------------------------------------------------------------------
// tsv_repair_map -- which conductor in each group has been replaced
// by that group's spare, and what happens when a group runs out.
//
// CLASSIFICATION: educational, synthesisable.
//
// WHAT IT DOES NOT MODEL:
//   - any physical via, defect mechanism, probability or yield.
//     §5 and §6's arithmetic is prose for exactly this reason.
//   - any real device's repair mechanism. §8's callout: 4.8 deferred
//     "the initialisation and test infrastructure" to this module and
//     this module could not obtain it. This is the SHAPE §6 requires,
//     not a specification.
//   - non-volatile storage, or when a map is loaded. §8 argues both
//     are necessary and neither is modelled.
//
// WHY EXHAUSTION IS AN OUTPUT AND NOT AN ERROR: §6. Two failures in
// one group with one spare is unrepairable, and that is a property of
// where the defects landed rather than a fault in this logic. The
// block reports it; it cannot fix it.
// ---------------------------------------------------------------------
module tsv_repair_map #(
  parameter int GROUPS        = 48,
  parameter int PER_GROUP     = 64,      // ILLUSTRATIVE (§6)
  parameter int SPARES_PER_GRP = 1,      // ILLUSTRATIVE (§5)
  // Ternary-guarded, matching 26.1's hbm_channel_organisation. A bare
  // $clog2(GROUPS) gives 0 at GROUPS=1, and [0-1:0] is an illegal
  // width -- the same sibling-block guard inconsistency Module 24
  // shipped once between two blocks doing the same job.
  parameter int GRP_IDX_W     = (GROUPS <= 1) ? 1 : $clog2(GROUPS),
  parameter int MEM_IDX_W     = (PER_GROUP <= 1) ? 1 : $clog2(PER_GROUP),
  // COUNTS need one more bit than the matching index.
  parameter int GRPCNT_W      = $clog2(GROUPS + 1),
  parameter int SPRCNT_W      = $clog2(SPARES_PER_GRP + 1),
  parameter int TOTCNT_W      = $clog2(GROUPS * SPARES_PER_GRP + 1)
) (
  input  logic                   clk,
  input  logic                   rst_n,

  // ── Report a failed conductor. Repair is attempted immediately.
  input  logic                   fail_valid,
  input  logic [GRP_IDX_W-1:0]   fail_group,
  input  logic [MEM_IDX_W-1:0]   fail_member,

  // ── Verdict for this report.
  output logic                   repaired,
  output logic                   unrepairable,

  // ── Map state.
  output logic [SPRCNT_W-1:0]    spares_used   [GROUPS],
  output logic [TOTCNT_W-1:0]    total_spares_used,
  output logic [TOTCNT_W-1:0]    total_spares,
  output logic [GRPCNT_W-1:0]    groups_exhausted,
  output logic                   stack_repairable,

  // §6: the same spare count tolerates a different number of
  // failures depending on their distribution. Both bounds published,
  // because the count alone does not say which applies.
  output logic [TOTCNT_W-1:0]    tolerable_best_case,
  output logic [SPRCNT_W-1:0]    tolerable_worst_case,

  output logic                   err_group_out_of_range,
  output logic                   err_member_out_of_range,
  output logic                   err_double_repair,
  output logic                   any_error
);

  initial begin
    if (GROUPS < 1 || PER_GROUP < 2)
      $fatal(1, "tsv_repair_map: need at least one group of at least two members");
    if (SPARES_PER_GRP < 1)
      // A group with no spare is a group with no repair, which makes
      // the whole block a counter. §5 establishes the first spare is
      // worth more than all the rest, so zero is the one value that
      // defeats the mechanism entirely.
      $fatal(1, "tsv_repair_map: SPARES_PER_GRP must be at least 1");
    if (SPARES_PER_GRP >= PER_GROUP)
      $fatal(1, "tsv_repair_map: spares must be fewer than the group's members");
    if (GRPCNT_W <= GRP_IDX_W && GROUPS > 1)
      $fatal(1, "tsv_repair_map: GRPCNT_W too narrow to count GROUPS");
    if (TOTCNT_W < $clog2(GROUPS * SPARES_PER_GRP + 1))
      $fatal(1, "tsv_repair_map: TOTCNT_W too narrow for the total spare count");
  end

  logic [SPRCNT_W-1:0] used [GROUPS];
  // One repair record per group per spare: which member it replaced.
  logic [MEM_IDX_W-1:0] repl [GROUPS][SPARES_PER_GRP];
  logic [SPARES_PER_GRP-1:0] slot_taken [GROUPS];
  logic                e_grp, e_mem, e_dbl, rep_q, unrep_q;

  // Declared above the continuous assigns that read them.
  logic grp_ok, mem_ok;
  assign grp_ok = ({{(32-GRP_IDX_W){1'b0}}, fail_group}  < 32'(GROUPS));
  assign mem_ok = ({{(32-MEM_IDX_W){1'b0}}, fail_member} < 32'(PER_GROUP));

  logic [TOTCNT_W-1:0] tot_used;
  logic [GRPCNT_W-1:0] n_exh;
  always_comb begin
    tot_used = '0;
    n_exh    = '0;
    for (int g = 0; g < GROUPS; g++) begin
      tot_used = tot_used + TOTCNT_W'(used[g]);
      if (used[g] == SPRCNT_W'(SPARES_PER_GRP)) n_exh = n_exh + GRPCNT_W'(1);
    end
  end

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      for (int g = 0; g < GROUPS; g++) begin
        used[g] <= '0;
        slot_taken[g] <= '0;
        for (int s = 0; s < SPARES_PER_GRP; s++) repl[g][s] <= '0;
      end
      e_grp <= 1'b0; e_mem <= 1'b0; e_dbl <= 1'b0;
      rep_q <= 1'b0; unrep_q <= 1'b0;
    end else begin
      e_grp <= 1'b0; e_mem <= 1'b0; e_dbl <= 1'b0;
      rep_q <= 1'b0; unrep_q <= 1'b0;

      if (fail_valid) begin
        if (!grp_ok) begin
          e_grp <= 1'b1;
        end else if (!mem_ok) begin
          e_mem <= 1'b1;
        end else begin
          begin : attempt
            logic already;
            logic [SPRCNT_W-1:0] u;
            already = 1'b0;
            u = used[fail_group];
            // Already repaired: reported, and NOT re-assigned. A
            // second spare for the same member would consume a spare
            // that another member may need.
            for (int s = 0; s < SPARES_PER_GRP; s++)
              if (slot_taken[fail_group][s] && (repl[fail_group][s] == fail_member))
                already = 1'b1;

            if (already) begin
              e_dbl <= 1'b1;
            end else if (u == SPRCNT_W'(SPARES_PER_GRP)) begin
              // §6: the group is out of spares. Not an error in this
              // logic -- a property of where the defects landed.
              unrep_q <= 1'b1;
            end else begin
              // Take the lowest free slot. Which slot is irrelevant;
              // that one is taken is what matters.
              for (int s = 0; s < SPARES_PER_GRP; s++)
                if (!slot_taken[fail_group][s] && (SPRCNT_W'(s) == u)) begin
                  slot_taken[fail_group][s] <= 1'b1;
                  repl[fail_group][s] <= fail_member;
                end
              used[fail_group] <= u + SPRCNT_W'(1);
              rep_q <= 1'b1;
            end
          end
        end
      end
    end
  end

  assign repaired     = rep_q;
  assign unrepairable = unrep_q;
  assign spares_used  = used;
  assign total_spares_used = tot_used;
  assign total_spares = TOTCNT_W'(GROUPS * SPARES_PER_GRP);
  assign groups_exhausted = n_exh;
  // The stack is repairable while no group has been asked for more
  // than it has. Exhaustion is permanent for that group.
  assign stack_repairable = (n_exh == '0);
  // §6: the same total tolerates a range depending on distribution.
  assign tolerable_best_case  = TOTCNT_W'(GROUPS * SPARES_PER_GRP);
  assign tolerable_worst_case = SPRCNT_W'(SPARES_PER_GRP);
  assign err_group_out_of_range  = e_grp;
  assign err_member_out_of_range = e_mem;
  assign err_double_repair       = e_dbl;
  assign any_error = e_grp | e_mem | e_dbl;
endmodule

// ---------------------------------------------------------------------
// stack_assembly_guard -- dies join the stack bottom-up, only after
// passing test, and never again once placed.
//
// CLASSIFICATION: educational, synthesisable.
//
// WHAT IT DOES NOT MODEL:
//   - any physical assembly step, bonding, alignment or thermal
//     processing
//   - what a test DOES. known_good is an input. §9's tension --
//     that the vertical connections needing test do not exist until
//     placement -- is real and this block cannot resolve it.
//   - yield or cost. 4.8 §3 owns the argument that a late defect
//     scraps an expensive assembly; no block computes it.
//
// THE FORBIDDEN TRANSITIONS ARE THE POINT (§9): a die may not join
// out of order, may not join untested, and a placed die may not be
// replaced. Asserting the legal sequence alone would also hold for a
// machine that permitted all three.
// ---------------------------------------------------------------------
module stack_assembly_guard #(
  parameter int CORE_DIES = 12,          // CURRICULUM-DERIVED (4.8 §2)
  parameter int LEVELS    = CORE_DIES + 1,   // plus the base die (26.2 §7)
  parameter int LVL_IDX_W = $clog2(LEVELS),
  parameter int LVLCNT_W  = $clog2(LEVELS + 1),
  parameter int CNT_W     = 16
) (
  input  logic                  clk,
  input  logic                  rst_n,

  // ── Attempt to place a die at a level.
  input  logic                  place_valid,
  input  logic [LVL_IDX_W-1:0]  place_level,
  input  logic                  known_good,

  // ── State.
  output logic [LVLCNT_W-1:0]   levels_placed,
  output logic [LVL_IDX_W-1:0]  next_level,
  output logic                  stack_complete,
  output logic                  place_accepted,

  // ── Accounting.
  output logic [CNT_W-1:0]      cnt_accepted,
  output logic [CNT_W-1:0]      cnt_rejected,

  // ── FORBIDDEN, each by kind so a debug session learns which rule
  //    was broken rather than that one was.
  output logic                  err_out_of_order,
  output logic                  err_not_known_good,
  output logic                  err_already_placed,
  output logic                  err_place_after_complete,
  output logic                  any_violation
);

  initial begin
    if (!(CORE_DIES inside {2, 4, 8, 12}))
      $fatal(1, "stack_assembly_guard: CORE_DIES must be 2, 4, 8 or 12");
    if (LEVELS != CORE_DIES + 1)
      // 26.2 §7: exactly one base die, and it is level 0.
      $fatal(1, "stack_assembly_guard: LEVELS must be CORE_DIES + 1");
    if (LVLCNT_W <= LVL_IDX_W && LEVELS > 1)
      // COUNT vs INDEX: too narrow and stack_complete is unreachable.
      $fatal(1, "stack_assembly_guard: LVLCNT_W too narrow to count LEVELS");
  end

  logic [LVLCNT_W-1:0] placed;
  logic [CNT_W-1:0]    n_ok, n_no;
  logic                e_ord, e_kgd, e_dup, e_aft, acc;

  // Declared above the continuous assigns that read them.
  logic complete_now;
  assign complete_now = (placed == LVLCNT_W'(LEVELS));

  logic is_next;
  assign is_next = ({{(32-LVL_IDX_W){1'b0}}, place_level} == 32'(placed));

  logic below_placed;
  assign below_placed = ({{(32-LVL_IDX_W){1'b0}}, place_level} < 32'(placed));

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      placed <= '0; n_ok <= '0; n_no <= '0; acc <= 1'b0;
      e_ord <= 1'b0; e_kgd <= 1'b0; e_dup <= 1'b0; e_aft <= 1'b0;
    end else begin
      acc <= 1'b0;
      e_ord <= 1'b0; e_kgd <= 1'b0; e_dup <= 1'b0; e_aft <= 1'b0;

      if (place_valid) begin
        if (complete_now) begin
          // §9: a placed stack is not revisited. Placing onto a
          // complete stack is refused rather than growing it beyond
          // its verified height.
          e_aft <= 1'b1;
          if (n_no != {CNT_W{1'b1}}) n_no <= n_no + CNT_W'(1);
        end else if (below_placed) begin
          // A level below the frontier already holds a die, and the
          // dies above it are committed. Replacement is impossible.
          e_dup <= 1'b1;
          if (n_no != {CNT_W{1'b1}}) n_no <= n_no + CNT_W'(1);
        end else if (!is_next) begin
          // Out of order: a die cannot rest on a level that is empty.
          e_ord <= 1'b1;
          if (n_no != {CNT_W{1'b1}}) n_no <= n_no + CNT_W'(1);
        end else if (!known_good) begin
          // §9: test precedes placement, because placement cannot be
          // undone. An untested die is refused.
          e_kgd <= 1'b1;
          if (n_no != {CNT_W{1'b1}}) n_no <= n_no + CNT_W'(1);
        end else begin
          placed <= placed + LVLCNT_W'(1);
          acc    <= 1'b1;
          if (n_ok != {CNT_W{1'b1}}) n_ok <= n_ok + CNT_W'(1);
        end
      end
    end
  end

  assign levels_placed  = placed;
  // The frontier: the only level a die may join at.
  assign next_level     = complete_now ? LVL_IDX_W'(LEVELS - 1)
                                       : LVL_IDX_W'(placed);
  assign stack_complete = complete_now;
  assign place_accepted = acc;
  assign cnt_accepted   = n_ok;
  assign cnt_rejected   = n_no;
  assign err_out_of_order         = e_ord;
  assign err_not_known_good       = e_kgd;
  assign err_already_placed       = e_dup;
  assign err_place_after_complete = e_aft;
  assign any_violation = e_ord | e_kgd | e_dup | e_aft;
endmodule

// Bind unit note: P1-P5 reference tsv_count_budget's internals,
// P6-P10 tsv_repair_map's, P11-P15 stack_assembly_guard's.

// P1 -- §1: the interface count always includes the overhead.
property p_interface_includes_overhead;
  @(posedge clk) disable iff (!rst_n)
    (conductors_per_interface >= CNT_W'(SIGNALS));
endproperty
assert property (p_interface_includes_overhead);

// P2 -- §2's identity: bussed is symmetric, dedicated is N to 1.
property p_asymmetry_matches_the_model;
  @(posedge clk) disable iff (!rst_n)
    (is_bussed ? (asymmetry_num == asymmetry_den)
               : (asymmetry_num == asymmetry_den * CNT_W'(CORE_DIES)));
endproperty
assert property (p_asymmetry_matches_the_model);

// P3 -- §2: a bussed organisation's per-die count does not depend on
// which die is queried. The property that makes "every core die is
// identical" checkable rather than asserted.
property p_bussed_count_is_uniform;
  @(posedge clk) disable iff (!rst_n)
    ((is_bussed && q_in_range) |-> (q_conductors == conductors_per_interface));
endproperty
assert property (p_bussed_count_is_uniform);

// P4 -- §3: reaching die d traverses d+1 bodies, so the traversal
// count is strictly increasing with height and never zero.
property p_traversals_increase_with_level;
  @(posedge clk) disable iff (!rst_n)
    (q_in_range |-> ((q_traversals != '0) &&
                     (q_traversals == DIECNT_W'({{(32-DIE_IDX_W){1'b0}}, q_die} + 32'd1))));
endproperty
assert property (p_traversals_increase_with_level);

// P5 -- §3: the total is N(N+1)/2.
property p_total_traversals_is_triangular;
  @(posedge clk) disable iff (!rst_n)
    (total_traversals == CNT_W'((CORE_DIES * (CORE_DIES + 1)) / 2));
endproperty
assert property (p_total_traversals_is_triangular);

// P6 -- FORBIDDEN. A group never uses more spares than it has. §6:
// exhaustion is the boundary the whole grouping argument rests on.
property p_never_exceed_group_spares;
  @(posedge clk) disable iff (!rst_n)
    (spares_used[fail_group] <= SPRCNT_W'(SPARES_PER_GRP));
endproperty
assert property (p_never_exceed_group_spares);

// P7 -- FORBIDDEN. A member is never repaired twice. A second spare
// for one member consumes a spare another member may need.
property p_no_double_repair;
  @(posedge clk) disable iff (!rst_n)
    (err_double_repair |-> (total_spares_used == $past(total_spares_used, 1)));
endproperty
assert property (p_no_double_repair);

// P8 -- repaired and unrepairable are mutually exclusive, and
// neither holds without a report.
property p_verdict_is_exclusive;
  @(posedge clk) disable iff (!rst_n)
    (!(repaired && unrepairable) &&
     ((repaired || unrepairable) |-> $past(fail_valid, 1)));
endproperty
assert property (p_verdict_is_exclusive);

// P9 -- §6: unrepairable is NOT an error. The logic did nothing
// wrong; the defects landed badly. Conflating them would make a
// distribution problem look like a design fault.
property p_unrepairable_is_not_an_error;
  @(posedge clk) disable iff (!rst_n)
    (unrepairable |-> !any_error);
endproperty
assert property (p_unrepairable_is_not_an_error);

// P10 -- §6: the two tolerance bounds bracket the total, and the
// worst case is the per-group spare count. Published together
// because the count alone does not say which applies.
property p_tolerance_bounds_bracket;
  @(posedge clk) disable iff (!rst_n)
    ((tolerable_best_case == total_spares) &&
     (tolerable_worst_case == SPRCNT_W'(SPARES_PER_GRP)));
endproperty
assert property (p_tolerance_bounds_bracket);

// P11 -- FORBIDDEN. A die never joins out of order. §9: a die cannot
// rest on a level that is empty.
property p_no_out_of_order_placement;
  @(posedge clk) disable iff (!rst_n)
    (place_valid && !stack_complete &&
     ({{(32-LVL_IDX_W){1'b0}}, place_level} > {{(32-LVLCNT_W){1'b0}}, levels_placed}))
      |=> (err_out_of_order && (levels_placed == $past(levels_placed, 1)));
endproperty
assert property (p_no_out_of_order_placement);

// P12 -- FORBIDDEN. An untested die never joins. §9: test precedes
// placement because placement cannot be undone.
property p_no_untested_placement;
  @(posedge clk) disable iff (!rst_n)
    (place_valid && !known_good) |=> !place_accepted;
endproperty
assert property (p_no_untested_placement);

// P13 -- FORBIDDEN. A placed level is never re-placed.
property p_no_replacement;
  @(posedge clk) disable iff (!rst_n)
    (place_valid &&
     ({{(32-LVL_IDX_W){1'b0}}, place_level} < {{(32-LVLCNT_W){1'b0}}, levels_placed}))
      |=> (err_already_placed && (levels_placed == $past(levels_placed, 1)));
endproperty
assert property (p_no_replacement);

// P14 -- the frontier advances by exactly one per acceptance, and
// never otherwise. Rules out a machine that skips or repeats a level.
property p_frontier_advances_by_one;
  @(posedge clk) disable iff (!rst_n)
    (place_accepted ? (levels_placed == $past(levels_placed, 1) + LVLCNT_W'(1))
                    : (levels_placed == $past(levels_placed, 1)));
endproperty
assert property (p_frontier_advances_by_one);

// P15 -- every placement attempt is accounted exactly once.
property p_attempts_are_accounted;
  @(posedge clk) disable iff (!rst_n)
    (place_valid |=> ((cnt_accepted + cnt_rejected) ==
                      ($past(cnt_accepted,1) + $past(cnt_rejected,1) + CNT_W'(1))));
endproperty
assert property (p_attempts_are_accounted);

// ── Cover.
// Both organisation models exercised, and both extremes of the stack.
cover property (@(posedge clk) disable iff (!rst_n) is_bussed && q_in_range);
cover property (@(posedge clk) disable iff (!rst_n) !is_bussed && q_in_range);
cover property (@(posedge clk) disable iff (!rst_n)
                  q_in_range && (q_die == '0));
cover property (@(posedge clk) disable iff (!rst_n)
                  q_in_range && (q_die == DIE_IDX_W'(CORE_DIES - 1)));
cover property (@(posedge clk) disable iff (!rst_n) err_die_out_of_range);
// Repair: a success, an exhaustion, and a double attempt.
cover property (@(posedge clk) disable iff (!rst_n) repaired);
cover property (@(posedge clk) disable iff (!rst_n) unrepairable);
cover property (@(posedge clk) disable iff (!rst_n) err_double_repair);
// §6's two distributions: spares spread one per group, versus two
// failures in one group. The same count, opposite outcomes.
cover property (@(posedge clk) disable iff (!rst_n)
                  (total_spares_used > TOTCNT_W'(1)) && (groups_exhausted == '0));
cover property (@(posedge clk) disable iff (!rst_n) groups_exhausted != '0);
cover property (@(posedge clk) disable iff (!rst_n) !stack_repairable);
// Assembly: EACH forbidden placement ATTEMPTED, plus a complete stack.
cover property (@(posedge clk) disable iff (!rst_n) err_out_of_order);
cover property (@(posedge clk) disable iff (!rst_n) err_not_known_good);
cover property (@(posedge clk) disable iff (!rst_n) err_already_placed);
cover property (@(posedge clk) disable iff (!rst_n) err_place_after_complete);
cover property (@(posedge clk) disable iff (!rst_n) stack_complete);

// Independent references. The geometry reference counts by walking
// rather than multiplying; the repair reference models groups as
// explicit queues rather than as counters. SIMULATION-ONLY.
//
// NOTE: the probability arithmetic of §5 and §6 is deliberately NOT
// here. It is prose, computed outside the design, because no part of
// this module -- synthesisable or not -- should appear to predict a
// yield. The checks below verify COUNTING and BOOKKEEPING only.
class tsv_reference;
  int signals, pg_num, pg_den, dies;
  bit dedicated;

  function void build(int s, int pn, int pd, int n, bit ded);
    signals = s; pg_num = pn; pg_den = pd; dies = n; dedicated = ded;
  endfunction

  function int iface();
    return (signals * (pg_den + pg_num)) / pg_den;
  endfunction

  // Walk the levels rather than multiplying.
  function int conductors_at(int level);
    int n = 0;
    if (!dedicated) return iface();
    for (int d = level; d < dies; d++) n += iface();
    return n;
  endfunction

  // Walk the traversals rather than using the triangular formula.
  function int total_traversals();
    int n = 0;
    for (int d = 1; d <= dies; d++) n += d;
    return n;
  endfunction
endclass

class repair_reference;
  int per_group_spares;
  int used[$];                 // used[g] = spares consumed in group g
  int claimed[$][$];           // claimed[g] = members already repaired

  function void build(int groups, int spares);
    per_group_spares = spares;
    used.delete(); claimed.delete();
    for (int g = 0; g < groups; g++) begin
      used.push_back(0);
      claimed.push_back({});
    end
  endfunction

  // Returns 1 repaired, 0 unrepairable, -1 double-report.
  function int report_fail(int g, int member);
    foreach (claimed[g][i]) if (claimed[g][i] == member) return -1;
    if (used[g] >= per_group_spares) return 0;
    used[g]++;
    claimed[g].push_back(member);
    return 1;
  endfunction

  function int groups_exhausted();
    int n = 0;
    foreach (used[g]) if (used[g] >= per_group_spares) n++;
    return n;
  endfunction
endclass

  THE SAME SPARES, TWO OPPOSITE OUTCOMES
    48 groups of 64, one spare each. 48 spares in total.

  (A) 48 failures, one per group
        total_spares_used     48
        groups_exhausted       0
        stack_repairable       1     <-- every failure repaired
        any_error              0
        unrepairable           never asserted

  (B) 2 failures, both in group 17
        total_spares_used      1
        groups_exhausted       1
        stack_repairable       0     <-- stack is scrap
        any_error              0     <-- NOTHING IS WRONG with the logic
        unrepairable           asserted once

    every property PASSES in both runs.

    diagnosis : 48 failures are fine and 2 are fatal, with identical
      redundancy. The repairable count is not a property of the
      spares -- it is a property of where the defects landed, which
      §6 establishes and which no amount of spare counting reveals.

    what makes it dangerous : "we have 48 spares" is the number a
      design review hears, and it is true in both runs. The useful
      number is the WORST CASE -- tolerable_worst_case, which is 1
      per group regardless of the total -- and a review that hears
      only the total will conclude the stack tolerates 48 failures
      when it may tolerate 2.

    and note any_error is LOW in run (B). The logic is correct; the
      stack is unusable. A monitor that treated unrepairable as an
      error would blame the wrong thing, which is why P9 forbids it.

    the fix : publish both bounds (§12) and treat the worst case as
      the design figure. §6's clustering caveat then matters
      directly: clustered defects push the outcome toward run (B),
      and real defects cluster.