On-DIMM PMIC

   PWR_GOOD  =  VIN_Bulk in tolerance
             AND every ENABLED buck in tolerance
             AND every LDO in tolerance

// ---------------------------------------------------------------------
// pwr_good_aggregator -- PWR_GOOD as the DEVICE-VERIFIED conjunction:
// the bulk input AND every ENABLED buck AND every LDO, each against a
// threshold held in a register.
//
// CLASSIFICATION: educational, synthesisable.
//
// WHAT IT DOES NOT MODEL:
//   - any regulator, voltage, slew rate or settling time
//   - the conversion loss §2's callout names, which is real and not
//     quantified anywhere in the consulted specification
//   - SEQUENCING. 24.5 §10 owns rail order and the reverse-shutdown
//     hazard, for a different standard. §5's callout: ordering is in
//     time, aggregation is over a set, and this block does the latter
//     only. There is deliberately no order state here.
//
// WHY "ENABLED" MATTERS (§4): a DISABLED buck is not a term in the
// conjunction. So the expression's arity is a runtime value, which is
// the same shape as 24.4's runtime modulus and has the same hazard --
// a fixed-arity implementation is wrong whenever a rail is off.
// ---------------------------------------------------------------------
module pwr_good_aggregator #(
  parameter int N_BUCK   = 3,          // VDD, VDDQ, VPP (§1)
  parameter int N_LDO    = 2,          // 1.8 V to hub, 1.0 V (§1)
  parameter int N_RAILS  = N_BUCK + N_LDO,
  // Terms in the conjunction: the rails plus VIN_Bulk (§4).
  parameter int N_TERMS  = N_RAILS + 1,
  parameter int MARG_W   = 12,
  // A COUNT of terms up to N_TERMS needs clog2(N_TERMS+1).
  parameter int TERMCNT_W = $clog2(N_TERMS + 1),
  parameter int CNT_W    = 24
) (
  input  logic                 clk,
  input  logic                 rst_n,

  // ── Bulk input status. Not a rail the PMIC makes; a precondition.
  input  logic                 vin_in_tolerance,

  // ── Per-rail: enabled, in tolerance, and an abstract margin.
  input  logic [N_RAILS-1:0]   rail_enabled,
  input  logic [N_RAILS-1:0]   rail_in_tolerance,
  input  logic [MARG_W-1:0]    rail_margin [N_RAILS],

  // ── Thresholds are REGISTER values (§5), so configuration is a
  //    state this block must know about rather than assume.
  input  logic                 thresholds_programmed,

  // ── The signal. Open-drain in the real part; modelled as an active
  //    HIGH "good" plus the drive-low condition it implies.
  output logic                 pwr_good,
  output logic                 driving_low,

  // ── Which term broke it. The whole diagnostic value of the block.
  output logic                 fail_vin,
  output logic [N_RAILS-1:0]   fail_rail,
  output logic [TERMCNT_W-1:0] n_terms_active,
  output logic [TERMCNT_W-1:0] n_terms_failing,

  // ── Worst margin across ENABLED rails only. A disabled rail has no
  //    margin to report and must not drag the minimum down.
  output logic [MARG_W-1:0]    worst_margin,
  output logic                 worst_margin_valid,

  // ── History, because an open-drain pulse can be missed.
  output logic                 ever_deasserted,
  output logic [CNT_W-1:0]     cnt_deassertions,
  output logic [CNT_W-1:0]     cy_deasserted,

  output logic                 err_good_before_programmed,
  output logic                 err_tolerance_without_enable,
  output logic                 any_error
);

  initial begin
    if (N_BUCK < 1 || N_LDO < 1)
      $fatal(1, "pwr_good_aggregator: need at least one buck and one LDO");
    if (N_TERMS != N_RAILS + 1)
      // §4: VIN_Bulk is a term. Omitting it would make the signal
      // report rail health while the input was already gone.
      $fatal(1, "pwr_good_aggregator: N_TERMS must include VIN_Bulk");
    if (TERMCNT_W <= $clog2(N_TERMS) && N_TERMS > 1)
      // A COUNT up to N_TERMS needs one more bit than an INDEX into
      // it when N_TERMS is a power of two. Getting this wrong makes
      // n_terms_active unable to represent "all of them".
      $fatal(1, "pwr_good_aggregator: TERMCNT_W too narrow to count N_TERMS");
    if (MARG_W < 2)
      $fatal(1, "pwr_good_aggregator: MARG_W must be at least 2");
  end

  logic             good_q, ever_bad, e_early, e_tol;
  logic [CNT_W-1:0] n_deassert, cy_bad;

  // ── The conjunction. Declared above the continuous assigns that
  //    read them. A disabled rail contributes NOTHING -- neither a
  //    pass nor a fail (§4).
  logic [N_RAILS-1:0] rail_bad;
  assign rail_bad = rail_enabled & ~rail_in_tolerance;

  logic all_rails_ok;
  assign all_rails_ok = (rail_bad == '0);

  logic good_now;
  assign good_now = vin_in_tolerance && all_rails_ok;

  logic [TERMCNT_W-1:0] n_active, n_failing;
  always_comb begin
    n_active  = TERMCNT_W'(1);          // VIN_Bulk always counts
    n_failing = vin_in_tolerance ? TERMCNT_W'(0) : TERMCNT_W'(1);
    for (int i = 0; i < N_RAILS; i++) begin
      if (rail_enabled[i]) begin
        n_active = n_active + TERMCNT_W'(1);
        if (!rail_in_tolerance[i]) n_failing = n_failing + TERMCNT_W'(1);
      end
    end
  end

  // Worst margin over ENABLED rails only.
  logic [MARG_W-1:0] wm;
  logic              wm_v;
  always_comb begin
    wm   = {MARG_W{1'b1}};
    wm_v = 1'b0;
    for (int i = 0; i < N_RAILS; i++)
      if (rail_enabled[i]) begin
        wm_v = 1'b1;
        if (rail_margin[i] < wm) wm = rail_margin[i];
      end
    if (!wm_v) wm = '0;
  end

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      good_q <= 1'b0;            // safe state: NOT good until proven
      ever_bad <= 1'b0; n_deassert <= '0; cy_bad <= '0;
      e_early <= 1'b0; e_tol <= 1'b0;
    end else begin
      e_early <= 1'b0; e_tol <= 1'b0;

      // §5: until the thresholds are programmed, "in tolerance"
      // means "inside a default window", not "inside the system's
      // intent". Asserting good then is reported.
      if (good_now && !thresholds_programmed) e_early <= 1'b1;

      // A rail reporting in-tolerance while disabled is a status
      // inconsistency: a rail that is off has no tolerance to be in.
      if ((rail_in_tolerance & ~rail_enabled) != '0) e_tol <= 1'b1;

      if (good_q && !good_now) begin
        ever_bad <= 1'b1;
        if (n_deassert != {CNT_W{1'b1}}) n_deassert <= n_deassert + CNT_W'(1);
      end
      if (!good_now && (cy_bad != {CNT_W{1'b1}})) cy_bad <= cy_bad + CNT_W'(1);

      good_q <= good_now;
    end
  end

  assign pwr_good    = good_q && good_now;
  // Open-drain: the part DRIVES low and releases high, so the drive
  // condition is the one with electrical meaning.
  assign driving_low = !good_now;
  assign fail_vin    = !vin_in_tolerance;
  assign fail_rail   = rail_bad;
  assign n_terms_active  = n_active;
  assign n_terms_failing = n_failing;
  assign worst_margin       = wm;
  assign worst_margin_valid = wm_v;
  assign ever_deasserted  = ever_bad;
  assign cnt_deassertions = n_deassert;
  assign cy_deasserted    = cy_bad;
  assign err_good_before_programmed   = e_early;
  assign err_tolerance_without_enable = e_tol;
  assign any_error = e_early | e_tol;
endmodule

// ---------------------------------------------------------------------
// module_transport_budget -- compares resistive transport loss for
// delivering a given power at the bulk input voltage versus at a
// rail voltage. §2's arithmetic, in abstract units.
//
// CLASSIFICATION: educational, synthesisable.
//
// ALL UNITS ARE ABSTRACT. No volts, amps, watts or ohms. Voltages are
// integer LEVELS and the result is a ratio of squares, which is the
// SHAPE of the I^2 R argument rather than a measurement.
//
// WHAT IT DOES NOT MODEL:
//   - the regulator's own efficiency. §2's callout: converting on the
//     module dissipates real power ON the module, and no efficiency
//     figure appears in the consulted specification. This block
//     compares TRANSPORT only and the omission is deliberate.
//   - noise, which 4.6 §3 names alongside loss and which does not
//     reduce to an I^2 R ratio at all
//   - any thermal consequence (§8), which is where the conversion
//     loss actually lands
//
// NO DIVISION: the comparison is published as a numerator and
// denominator pair, so the caller states its own denominator -- the
// discipline every accountant in Modules 24 and 25 follows.
// ---------------------------------------------------------------------
module module_transport_budget #(
  // Abstract voltage levels, scaled by the caller. The SODIMM's
  // verified 5 V / 1.1 V is 50 / 11 at a scale of 10 (§1, §3).
  parameter int V_SCALE   = 10,
  parameter int VIN_LEVEL = 50,
  parameter int N_RAILS   = 5,
  parameter int LVL_W     = 10,
  parameter int RATIO_W   = 2 * LVL_W + 2,
  parameter int IDX_W     = (N_RAILS <= 1) ? 1 : $clog2(N_RAILS)
) (
  input  logic                 clk,
  input  logic                 rst_n,

  input  logic                 q_valid,
  input  logic [IDX_W-1:0]     q_rail,
  input  logic [LVL_W-1:0]     rail_level [N_RAILS],

  // ── The comparison, as a PAIR. loss(at rail V) / loss(at VIN) =
  //    (VIN/Vrail)^2, published as numerator over denominator.
  output logic [RATIO_W-1:0]   loss_num,       // VIN^2
  output logic [RATIO_W-1:0]   loss_den,       // Vrail^2
  output logic                 q_out_valid,

  // Which rail benefits most: the LOWEST voltage, since the ratio
  // grows as the rail falls (§2).
  output logic [IDX_W-1:0]     best_rail,
  output logic [LVL_W-1:0]     lowest_level,

  // §2: the connector carries this many regulated supplies if the
  // board regulates, and exactly one if the module does.
  output logic [7:0]           supplies_if_board,
  output logic [7:0]           supplies_if_module,

  output logic                 err_rail_above_vin,
  output logic                 err_zero_level,
  output logic                 any_error
);

  initial begin
    if (VIN_LEVEL < 2)
      $fatal(1, "module_transport_budget: VIN_LEVEL must be at least 2");
    if (V_SCALE < 1)
      $fatal(1, "module_transport_budget: V_SCALE must be positive");
    if (N_RAILS < 1)
      $fatal(1, "module_transport_budget: need at least one rail");
    if (RATIO_W < 2 * LVL_W + 2)
      // VIN^2 needs twice the level width plus headroom; too narrow
      // and the ratio silently wraps, which reads as a SMALL benefit
      // -- the flattering direction, and therefore the dangerous one.
      $fatal(1, "module_transport_budget: RATIO_W too narrow for a square");
    if (VIN_LEVEL > ((1 << LVL_W) - 1))
      $fatal(1, "module_transport_budget: VIN_LEVEL exceeds LVL_W");
  end

  logic [RATIO_W-1:0] num_q, den_q;
  logic               v_q, e_above, e_zero;
  logic [IDX_W-1:0]   best_q;
  logic [LVL_W-1:0]   low_q;

  // Declared above the continuous assigns that read them.
  logic [LVL_W-1:0] sel_level;
  assign sel_level = rail_level[q_rail];

  logic [IDX_W-1:0] best_c;
  logic [LVL_W-1:0] low_c;
  always_comb begin
    best_c = '0;
    low_c  = {LVL_W{1'b1}};
    for (int i = 0; i < N_RAILS; i++)
      if ((rail_level[i] != '0) && (rail_level[i] < low_c)) begin
        low_c  = rail_level[i];
        best_c = IDX_W'(i);
      end
  end

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      num_q <= '0; den_q <= '0; v_q <= 1'b0;
      best_q <= '0; low_q <= '0;
      e_above <= 1'b0; e_zero <= 1'b0;
    end else begin
      v_q <= 1'b0; e_above <= 1'b0; e_zero <= 1'b0;
      best_q <= best_c;
      low_q  <= low_c;

      if (q_valid) begin
        if (sel_level == '0) begin
          e_zero <= 1'b1;
        end else if ({{(LVL_W){1'b0}}, sel_level} > {{(LVL_W){1'b0}}, LVL_W'(VIN_LEVEL)}) begin
          // A rail above the bulk input is not a step-down at all --
          // reported rather than producing a ratio below one, which
          // would read as local regulation being WORSE.
          e_above <= 1'b1;
        end else begin
          num_q <= RATIO_W'(VIN_LEVEL) * RATIO_W'(VIN_LEVEL);
          den_q <= RATIO_W'(sel_level) * RATIO_W'(sel_level);
          v_q   <= 1'b1;
        end
      end
    end
  end

  assign loss_num    = num_q;
  assign loss_den    = den_q;
  assign q_out_valid = v_q;
  assign best_rail    = best_q;
  assign lowest_level = low_q;
  assign supplies_if_board  = 8'(N_RAILS);
  assign supplies_if_module = 8'd1;
  assign err_rail_above_vin = e_above;
  assign err_zero_level     = e_zero;
  assign any_error = e_above | e_zero;
endmodule

// ---------------------------------------------------------------------
// spd_hub_reporter -- the module's own telemetry: a presence-detect
// store and a thermal threshold report, readable independently of
// whether the memory is usable.
//
// CLASSIFICATION: educational, synthesisable.
//
// WHY INDEPENDENCE IS THE POINT (§6): the hub has its own LDO supply,
// DEVICE-VERIFIED as "1.8 V LDO output: from PMIC to HUB". So it can
// answer questions before the DRAM is configured and while the DRAM
// is unusable -- which is when the questions matter most.
//
// WHAT IT DOES NOT MODEL:
//   - temperature, the sensor's physics or its accuracy
//   - the real SPD data layout or ANY of its semantics. 1024 bytes is
//     DEVICE-VERIFIED as the size; the contents are not modelled.
//   - what a host should DO about a thermal event, which is a system
//     policy and not a module behaviour
// ---------------------------------------------------------------------
module spd_hub_reporter #(
  parameter int SPD_BYTES = 1024,        // DEVICE-VERIFIED size
  parameter int ADDR_W    = $clog2(SPD_BYTES),
  parameter int TEMP_W    = 10,          // abstract temperature units
  parameter int CNT_W     = 20
) (
  input  logic                clk,
  input  logic                rst_n,

  // ── The hub's own supply. §6: separate from the DRAM's rails, so
  //    hub_powered can be true while dram_usable is false.
  input  logic                hub_powered,
  input  logic                dram_usable,

  // ── Presence-detect reads.
  input  logic                rd_valid,
  input  logic [ADDR_W-1:0]   rd_addr,
  output logic                rd_ack,
  output logic                rd_in_range,

  // ── Thermal.
  input  logic [TEMP_W-1:0]   temp_now,
  input  logic [TEMP_W-1:0]   thr_warn,
  input  logic [TEMP_W-1:0]   thr_crit,
  input  logic                thr_programmed,

  output logic                warn_now,
  output logic                crit_now,
  // Sticky, because a thermal excursion a host polled past still
  // happened -- the same reasoning as §11's deassertion record.
  output logic                ever_warned,
  output logic                ever_critical,
  output logic [TEMP_W-1:0]   peak_temp,
  output logic [CNT_W-1:0]    cy_above_warn,
  output logic [CNT_W-1:0]    cnt_warn_events,

  // ── The property §6 exists to establish, published so a consumer
  //    can rely on it rather than infer it.
  output logic                readable_without_dram,

  output logic                err_read_while_unpowered,
  output logic                err_addr_out_of_range,
  output logic                err_thresholds_inverted,
  output logic                err_report_before_programmed,
  output logic                any_error
);

  initial begin
    if (SPD_BYTES != 1024)
      $fatal(1, "spd_hub_reporter: SPD_BYTES is 1024 (device-verified), got %0d",
             SPD_BYTES);
    if (ADDR_W != $clog2(SPD_BYTES))
      $fatal(1, "spd_hub_reporter: ADDR_W must address exactly SPD_BYTES");
    if (TEMP_W < 2)
      $fatal(1, "spd_hub_reporter: TEMP_W must be at least 2");
  end

  logic             ack, in_rng, w_ever, c_ever;
  logic [TEMP_W-1:0] pk;
  logic [CNT_W-1:0]  cy_warn, n_warn;
  logic              e_unpow, e_addr, e_inv, e_early;
  logic              warn_q;

  // Declared above the continuous assigns that read them.
  logic addr_ok;
  assign addr_ok = ({{(32-ADDR_W){1'b0}}, rd_addr} < 32'(SPD_BYTES));

  logic w_now, c_now;
  assign w_now = thr_programmed && hub_powered && (temp_now >= thr_warn);
  assign c_now = thr_programmed && hub_powered && (temp_now >= thr_crit);

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      ack <= 1'b0; in_rng <= 1'b0;
      w_ever <= 1'b0; c_ever <= 1'b0; pk <= '0;
      cy_warn <= '0; n_warn <= '0; warn_q <= 1'b0;
      e_unpow <= 1'b0; e_addr <= 1'b0; e_inv <= 1'b0; e_early <= 1'b0;
    end else begin
      ack <= 1'b0; in_rng <= 1'b0;
      e_unpow <= 1'b0; e_addr <= 1'b0; e_inv <= 1'b0; e_early <= 1'b0;

      // A critical threshold below the warning one inverts the
      // escalation: every warning would also be critical.
      if (thr_programmed && (thr_crit < thr_warn)) e_inv <= 1'b1;

      if (rd_valid) begin
        if (!hub_powered)      e_unpow <= 1'b1;
        else if (!addr_ok)     e_addr  <= 1'b1;
        else begin ack <= 1'b1; in_rng <= 1'b1; end
      end

      if (hub_powered) begin
        // A temperature report before thresholds are programmed is
        // a reading against defaults, not against system intent.
        if (!thr_programmed && (temp_now != '0)) e_early <= 1'b1;
        if (temp_now > pk) pk <= temp_now;
        if (w_now) begin
          w_ever <= 1'b1;
          if (cy_warn != {CNT_W{1'b1}}) cy_warn <= cy_warn + CNT_W'(1);
          if (!warn_q && (n_warn != {CNT_W{1'b1}})) n_warn <= n_warn + CNT_W'(1);
        end
        if (c_now) c_ever <= 1'b1;
        warn_q <= w_now;
      end
    end
  end

  assign rd_ack      = ack;
  assign rd_in_range = in_rng;
  assign warn_now    = w_now;
  assign crit_now    = c_now;
  assign ever_warned    = w_ever;
  assign ever_critical  = c_ever;
  assign peak_temp      = pk;
  assign cy_above_warn  = cy_warn;
  assign cnt_warn_events = n_warn;
  // §6's property, as an output: the hub answers whenever it has its
  // own supply, regardless of the DRAM's state.
  assign readable_without_dram = hub_powered && !dram_usable;
  assign err_read_while_unpowered     = e_unpow;
  assign err_addr_out_of_range        = e_addr;
  assign err_thresholds_inverted      = e_inv;
  assign err_report_before_programmed = e_early;
  assign any_error = e_unpow | e_addr | e_inv | e_early;
endmodule

// Bind unit note: P1-P6 reference pwr_good_aggregator's internals,
// P7-P10 module_transport_budget's, P11-P15 spd_hub_reporter's.

// P1 -- FORBIDDEN. PWR_GOOD is never asserted while any term fails.
// §4's conjunction, as the property the signal exists to guarantee.
property p_never_good_with_a_failing_term;
  @(posedge clk) disable iff (!rst_n)
    pwr_good |-> ((n_terms_failing == '0) && !fail_vin && (fail_rail == '0));
endproperty
assert property (p_never_good_with_a_failing_term);

// P2 -- FORBIDDEN. A DISABLED rail never contributes a failure. §4:
// "all ENABLED output buck regulators" -- a fixed-arity AND over all
// rails would hold the signal low forever with any rail off.
property p_disabled_rail_never_fails;
  @(posedge clk) disable iff (!rst_n)
    ((fail_rail & ~rail_enabled) == '0);
endproperty
assert property (p_disabled_rail_never_fails);

// P3 -- the active term count is VIN plus the enabled rails, so the
// conjunction's arity tracks configuration rather than a constant.
property p_arity_tracks_enables;
  @(posedge clk) disable iff (!rst_n)
    (n_terms_active == (TERMCNT_W'(1) + TERMCNT_W'($countones(rail_enabled))));
endproperty
assert property (p_arity_tracks_enables);

// P4 -- the bulk input is always a term. Omitting it would report
// rail health while the input was already gone (§4).
property p_vin_is_always_a_term;
  @(posedge clk) disable iff (!rst_n)
    (!vin_in_tolerance |-> !pwr_good);
endproperty
assert property (p_vin_is_always_a_term);

// P5 -- the open-drain drive condition is the complement of the
// instantaneous conjunction, so a consumer can model the net.
property p_drive_low_is_not_good_now;
  @(posedge clk) disable iff (!rst_n)
    (driving_low == !(vin_in_tolerance && ((rail_enabled & ~rail_in_tolerance) == '0)));
endproperty
assert property (p_drive_low_is_not_good_now);

// P6 -- a deassertion is never forgotten. §11's callout: an
// open-drain pulse a host polled past still happened.
property p_deassertion_record_is_sticky;
  @(posedge clk) disable iff (!rst_n)
    ($past(ever_deasserted, 1) |-> ever_deasserted);
endproperty
assert property (p_deassertion_record_is_sticky);

// P7 -- the published ratio is exactly VIN squared over the rail
// squared. §2's model, as an invariant rather than a comment.
property p_ratio_is_squares;
  @(posedge clk) disable iff (!rst_n)
    q_out_valid |-> (loss_num == (RATIO_W'(VIN_LEVEL) * RATIO_W'(VIN_LEVEL)));
endproperty
assert property (p_ratio_is_squares);

// P8 -- FORBIDDEN. A ratio is never published for a rail above the
// bulk input. It would read as local regulation being WORSE.
property p_no_ratio_above_vin;
  @(posedge clk) disable iff (!rst_n)
    (q_valid && (rail_level[q_rail] > LVL_W'(VIN_LEVEL))) |=> !q_out_valid;
endproperty
assert property (p_no_ratio_above_vin);

// P9 -- the numerator is never below the denominator for a published
// result, so the reported benefit is never inverted.
property p_benefit_never_inverted;
  @(posedge clk) disable iff (!rst_n)
    q_out_valid |-> (loss_num >= loss_den);
endproperty
assert property (p_benefit_never_inverted);

// P10 -- §2: the lowest rail benefits most, so best_rail names a
// rail whose level is the minimum non-zero level.
property p_best_rail_is_lowest;
  @(posedge clk) disable iff (!rst_n)
    ((lowest_level != '0) |-> (rail_level[best_rail] == lowest_level));
endproperty
assert property (p_best_rail_is_lowest);

// P11 -- FORBIDDEN. The hub never acknowledges a read while
// unpowered. Answering without a supply would be a fiction.
property p_no_ack_unpowered;
  @(posedge clk) disable iff (!rst_n)
    (!hub_powered |-> !rd_ack);
endproperty
assert property (p_no_ack_unpowered);

// P12 -- §6's property: the hub answers with its own supply
// regardless of the DRAM's state. This is what the separate LDO buys.
property p_hub_answers_without_dram;
  @(posedge clk) disable iff (!rst_n)
    (rd_valid && hub_powered && !dram_usable &&
     ({{(32-ADDR_W){1'b0}}, rd_addr} < 32'(SPD_BYTES))) |=> rd_ack;
endproperty
assert property (p_hub_answers_without_dram);

// P13 -- FORBIDDEN. An out-of-range address is never acknowledged.
property p_no_ack_out_of_range;
  @(posedge clk) disable iff (!rst_n)
    (rd_valid && ({{(32-ADDR_W){1'b0}}, rd_addr} >= 32'(SPD_BYTES))) |=> !rd_ack;
endproperty
assert property (p_no_ack_out_of_range);

// P14 -- critical implies warning, so the escalation is ordered. An
// inverted threshold pair is reported rather than silently making
// every warning critical.
property p_critical_implies_warning;
  @(posedge clk) disable iff (!rst_n)
    ((thr_crit >= thr_warn) && crit_now) |-> warn_now;
endproperty
assert property (p_critical_implies_warning);

// P15 -- the peak is monotone and the sticky flags never clear. A
// thermal excursion that evaporated from the record would let a host
// conclude nothing happened.
property p_thermal_record_is_monotone;
  @(posedge clk) disable iff (!rst_n)
    ((peak_temp >= $past(peak_temp, 1)) &&
     ($past(ever_warned,1)   |-> ever_warned) &&
     ($past(ever_critical,1) |-> ever_critical));
endproperty
assert property (p_thermal_record_is_monotone);

// ── Cover.
// The conjunction good, and failing by EACH term separately -- a
// property forbidding something is vacuous until it is attempted.
cover property (@(posedge clk) disable iff (!rst_n) pwr_good);
cover property (@(posedge clk) disable iff (!rst_n) fail_vin);
cover property (@(posedge clk) disable iff (!rst_n) $countones(fail_rail) == 1);
cover property (@(posedge clk) disable iff (!rst_n) $countones(fail_rail) > 1);
// A rail DISABLED while out of tolerance -- P2 is vacuous without it,
// and it is the case a fixed-arity AND gets wrong.
cover property (@(posedge clk) disable iff (!rst_n)
                  ((rail_enabled & ~rail_in_tolerance) == '0) &&
                  ((~rail_enabled & ~rail_in_tolerance) != '0) && pwr_good);
// Good asserted before thresholds were programmed — §5's window.
cover property (@(posedge clk) disable iff (!rst_n) err_good_before_programmed);
// Both extremes of the transport comparison.
cover property (@(posedge clk) disable iff (!rst_n)
                  q_out_valid && (lowest_level == rail_level[best_rail]));
cover property (@(posedge clk) disable iff (!rst_n) err_rail_above_vin);
// THE PROPERTY §6 EXISTS FOR: the hub read while the DRAM is unusable.
cover property (@(posedge clk) disable iff (!rst_n) readable_without_dram && rd_ack);
cover property (@(posedge clk) disable iff (!rst_n) err_read_while_unpowered);
cover property (@(posedge clk) disable iff (!rst_n) err_addr_out_of_range);
// Thermal: warning, critical, and an inverted threshold pair.
cover property (@(posedge clk) disable iff (!rst_n) warn_now && !crit_now);
cover property (@(posedge clk) disable iff (!rst_n) crit_now);
cover property (@(posedge clk) disable iff (!rst_n) err_thresholds_inverted);
// Oscillation across the warning threshold — the case a single
// counter cannot distinguish from a steady excursion (§13).
cover property (@(posedge clk) disable iff (!rst_n)
                  warn_now ##1 !warn_now ##1 warn_now);

// Independent conjunction reference. Evaluates PWR_GOOD by walking an
// explicit term LIST rather than by bitwise masking, so agreement
// with the DUT is evidence and not a restatement of the same
// expression. SIMULATION-ONLY.
class pwr_good_ref;
  typedef struct { bit enabled; bit in_tol; int margin; } term_t;
  term_t rails[$];
  bit    vin_ok;

  function void build(int n);
    rails.delete();
    for (int i = 0; i < n; i++) begin
      term_t t; t.enabled = 0; t.in_tol = 0; t.margin = 0;
      rails.push_back(t);
    end
  endfunction

  function bit good();
    if (!vin_ok) return 0;
    foreach (rails[i])
      if (rails[i].enabled && !rails[i].in_tol) return 0;   // enabled only
    return 1;
  endfunction

  function int active_terms();
    int n = 1;                                  // VIN always counts
    foreach (rails[i]) if (rails[i].enabled) n++;
    return n;
  endfunction

  function int worst_margin();
    int w = -1;
    foreach (rails[i])
      if (rails[i].enabled && (w < 0 || rails[i].margin < w)) w = rails[i].margin;
    return w;                                   // -1 when none enabled
  endfunction

  // §11's model, for comparing an observed deassertion rate against
  // what a six-term conjunction predicts.
  function real predicted_failure(real p, int terms);
    return 1.0 - (p ** terms);
  endfunction
endclass

  THE CONJUNCTION THAT LOOKED MORE CAREFUL
    PWR_GOOD implemented as the obvious safe thing:
        good = vin_ok && (rail_in_tolerance == 5'b11111);
    i.e. ALL five rails must be in tolerance, enabled or not.

    module configuration: the 1.0 V LDO is unused on this design
    and is DISABLED. Its status bit reads 0.

    result:  PWR_GOOD never asserts. Not once. The host never
             releases memory, and the module appears dead on
             arrival.

    assertions : P1 never good with a failing term    PASS
                 P3 arity tracks enables              PASS
                 P4 vin is always a term              PASS
                 P2 disabled rail never fails         FAIL

    diagnosis : the implementation is STRICTER than the
      specification, and strictness is the wrong direction here.
      §4's verified wording is "all ENABLED output buck regulators",
      and a disabled regulator has no tolerance to be in -- its
      status bit is not a fault, it is meaningless.

    what makes it instructive : this is not a careless bug. It is
      what you write if you reason "a power-good signal should be
      conservative", which is usually correct and is wrong here.
      The specification's one word -- "enabled" -- is the whole
      difference, and only P2 encodes it.

    and it fails LOUDLY, unlike most bugs in these two modules: the
      module simply never comes up. That makes it the easiest
      failure in Module 25 to find and the easiest to introduce.