Mobile SoCs

   1  WHICH CONSTRAINT
        two ceilings -- energy and heat -- and the heat ceiling
        closes a POSITIVE FEEDBACK LOOP through refresh (§3)

   2  WHAT DECISION
        the controller must be THROTTLEABLE, with a bounded
        response time and authority over the LOOP term (§6, §7)

   3  WHAT GRADE
        mostly B and D. The mechanisms are documented -- PASR,
        temperature-compensated self refresh, the state set -- and
        the VALUES are per-device and per-platform (§9)

   the loop, as a signal path

     temperature  T
         |
         | retention falls (2.3 §4)
         v
     required refresh RATE rises (15.4: a specified condition,
         |                        expressed as a temperature band)
         | each refresh costs energy (15.5)
         v
     refresh POWER rises
         |
         | dissipated through the thermal path
         v
     temperature  T        <-- closes here

   DEFINITIONS
     T        temperature rise above ambient           K
     P_ext    all heat EXCEPT memory refresh           W
     P_ref(T) refresh power, rising with T             W
     theta    thermal resistance of the path out       K/W
     k        dP_ref/dT, the loop's slope              W/K

   the steady state, with the loop OPEN (refresh fixed):
       T = theta * (P_ext + P_ref)

   with the loop CLOSED (refresh rises with T):
       T = theta * (P_ext + P_ref0 + k*T)

   solve for T:
       T * (1 - theta*k) = theta * (P_ext + P_ref0)

       T = theta * (P_ext + P_ref0) / (1 - G)   where  G = theta * k

   DERIVED. TWO results, and the second matters more:

     STABILITY :  the loop is stable iff  G < 1.
                  at G >= 1 there is no steady state -- temperature
                  rises until something else limits it.

     AMPLIFICATION : below G = 1, EVERY heat source in the device
                  is amplified by  1 / (1 - G).
                  The memory does not need to be the heat source
                  to be the problem.

   GRADE D, chosen for legibility. The RATIO is CURRICULUM-DERIVED
   from 24.2 §7 -- more than 20x cool-to-hot -- and the span and the
   absolute values are invented.

     refresh power, cool part            P_ref  = 0.05 W
     refresh power, hot part (+40 K)     P_ref  = 1.00 W   (20x)
     DERIVED slope  k = (1.00 - 0.05) / 40    = 0.024 W/K

   three thermal paths, all GRADE D:

     path                  theta      G = theta*k    1/(1-G)
     ------------------    --------   -----------    -------
     on a bench, open      15 K/W        0.356        1.55
     in a pocket           40 K/W        0.950       20.0
     insulated / blocked   45 K/W        1.080        NONE

   DERIVED, all recomputed. And read the third column rather than
   the second: at theta = 15 the loop costs 55% extra temperature
   rise; at theta = 40 it costs TWENTY TIMES.

   the two limits, as controller requirements

   BURST limit   -- an instantaneous power cap
       enforced by: nothing. The device's thermal mass absorbs it.
       controller requirement: NONE. A burst is free.

   SUSTAINED limit -- an average over a thermal time constant
       enforced by: temperature rising until something responds
       controller requirement: the throttle of §6, and its response
       time must be short RELATIVE TO THE THERMAL TIME CONSTANT --
       not relative to anything in the memory's own timing.

   32.1's platform:  the mix is HETEROGENEOUS in obligation.
                     the controller must distinguish WHO is asking.

   this platform:    the mix is homogeneous enough, and the
                     controller must instead respond to something
                     that is not asking at all -- a thermal state
                     with no request, no queue entry and no class.

   STRUCTURAL: the throttle is an input with no requester behind it.
   Every other input to the scheduler in thirty-one chapters came
   from something that wanted memory. This one comes from physics.

// ---------------------------------------------------------------------
// thermal_response -- the platform-profile block of §11.
//
// CLASSIFICATION: synthesisable, grade-D parameter values, CORRECT as
// written. The intentionally defective block is §12.
//
// WHAT IT IS: §7's three requirements as hardware -- a bounded
// response, an AUTHORITY SET that includes the refresh term, and
// mandatory hysteresis. It is a MODIFIER on policy and on the refresh
// manager, not a requester: §8 establishes that a thermal state has
// no queue entry and no class.
//
// WHY IT EXISTS HERE: §4 derives that the loop amplifies every heat
// source by 1/(1-G) and that G is set by a thermal path the memory
// does not own. So the response cannot be designed open-loop; it must
// be a mechanism with stated authority, and §7 is its specification.
//
// HOW TO RUN IT: drive filt_temp above the level-1 threshold and hold
// it there.
// EXPECTED RESULT: policy_limit AND refresh_mode_req both change
// within RESP_DEADLINE cycles, and neither clears until filt_temp
// falls below the engage threshold by HYST_K.
// EXPECTED TRACE: refresh_mode_req must move. A response that
// changes only policy_limit has no authority over the loop (§13).
//
// SYNTHESIS: one level comparator chain, one deadline counter, one
// hysteresis register. No memory.
//
// LIMITATIONS: this block DECIDES the response. It does not filter --
// WIN_LEN is a platform property and filt_temp is an INPUT, per §5's
// requirement that the window be configured rather than compiled
// (32.1 §13's defect class). Nor does it implement PASR's mask: 24.2
// §9 owns that as a mask with a RETENTION consequence, so selecting
// a region is a data-placement decision this block must not make
// unilaterally -- it requests a mode and the placement owner
// consents. That boundary is STATED and is not the bug.
// ---------------------------------------------------------------------
module thermal_response #(
  // The platform property. A fanned platform has no runtime heat
  // ceiling in this sense, so the mechanism is ABSENT rather than
  // disabled -- §2's row five.
  parameter bit THERMAL_LIMITED = 1'b1,

  parameter int LEVELS        = 3,
  // Grade D. Engage thresholds, in filtered-temperature units. They
  // are PARAMETERS here and should be configuration inputs on a real
  // platform, for 32.1 §13's reason: a threshold is a platform
  // property and a platform property in a parameter is grade D
  // consumed as grade A.
  parameter int T_L1          = 70,
  parameter int T_L2          = 80,
  parameter int T_L3          = 88,
  // §7 requirement 3. Mandatory, not an optimisation: without it the
  // loop of §3 becomes an oscillator (23.5's hysteresis argument
  // with a physical mechanism underneath).
  parameter int HYST_K        = 4,
  // §7 requirement 1. Derived from the THERMAL time constant, which
  // is not a memory quantity -- §5. It must be short enough at the
  // WORST permitted G, not the nominal one (§4's third conclusion).
  parameter int RESP_DEADLINE = 2000,

  // COUNT, not INDEX: the deadline counter must REPRESENT
  // RESP_DEADLINE, so it needs $clog2(RESP_DEADLINE + 1) bits. Sized
  // $clog2(RESP_DEADLINE) it saturates one short of the deadline it
  // enforces, and the deadline check becomes unreachable -- a
  // response requirement present in the source and absent in the
  // silicon (31.2 §7).
  parameter int DL_W          = $clog2(RESP_DEADLINE + 1),
  parameter int TMP_W         = 8,
  parameter int LVL_W         = $clog2(LEVELS + 1)
)(
  input  logic               clk,
  input  logic               rst_n,

  // §5: FILTERED, never instantaneous. A burst is free and must not
  // engage the throttle.
  input  logic [TMP_W-1:0]   filt_temp,
  input  logic               filt_valid,

  // Authority set -- BOTH outputs are required (§7 requirement 2).
  output logic [LVL_W-1:0]   level,
  output logic [LVL_W-1:0]   policy_limit,
  output logic [1:0]         refresh_mode_req,
  output logic               response_late,
  output logic [LVL_W-1:0]   authority_reported
);
  // Refresh mode requests. The MECHANISMS are grade B -- 24.1 §8
  // cites a device feature summary listing partial-array self refresh
  // and temperature-compensated self refresh as supported functions.
  // The ENCODING here is local to this block.
  localparam logic [1:0] RM_NORMAL = 2'd0;
  localparam logic [1:0] RM_TCSR   = 2'd1;  // temperature-compensated
  localparam logic [1:0] RM_PASR   = 2'd2;  // masked, WITH consent

  initial begin
    if (LEVELS < 1) $fatal(1, "thermal_response: LEVELS >= 1");
    if (!(T_L1 < T_L2 && T_L2 < T_L3))
      $fatal(1, "thermal_response: thresholds must be strictly increasing");
    // §7 requirement 3, enforced: a hysteresis band wider than the
    // gap between two levels would make the upper level
    // unreachable once entered from below.
    if (HYST_K >= (T_L2 - T_L1))
      $fatal(1, "thermal_response: HYST_K (%0d) >= level gap (%0d): a level becomes unreachable",
             HYST_K, T_L2 - T_L1);
    if (RESP_DEADLINE < 1) $fatal(1, "thermal_response: RESP_DEADLINE >= 1");
  end

  generate
  if (THERMAL_LIMITED) begin : g_thermal

    logic [LVL_W-1:0] lvl_q, lvl_target;
    logic [DL_W-1:0]  dl_cnt;
    logic             pending;

    // The level decision, WITH hysteresis. Engage on crossing up;
    // disengage only after falling HYST_K below the engage point.
    // Written as an explicit comparison against (threshold - HYST_K)
    // on the way down rather than as a single band, because the two
    // directions genuinely differ -- and a single band is the bug
    // 23.5 warns about.
    always_comb begin
      lvl_target = lvl_q;
      if (filt_valid) begin
        // Upward: plain thresholds.
        if      (filt_temp >= T_L3[TMP_W-1:0]) lvl_target = LVL_W'(3);
        else if (filt_temp >= T_L2[TMP_W-1:0]) lvl_target = (lvl_q > 2) ? lvl_q : LVL_W'(2);
        else if (filt_temp >= T_L1[TMP_W-1:0]) lvl_target = (lvl_q > 1) ? lvl_q : LVL_W'(1);
        // Downward: only below (threshold - HYST_K).
        if (lvl_q == 3 && filt_temp <  (T_L3 - HYST_K)) lvl_target = LVL_W'(2);
        if (lvl_q == 2 && filt_temp <  (T_L2 - HYST_K)) lvl_target = LVL_W'(1);
        if (lvl_q == 1 && filt_temp <  (T_L1 - HYST_K)) lvl_target = LVL_W'(0);
      end
    end

    // The response, with its deadline. `pending` is set when the
    // target changes and cleared when the outputs have followed;
    // `response_late` is the observable §7 requirement 1 needs, and
    // it exists because a deadline nobody measures is a wish.
    always_ff @(posedge clk) begin
      if (!rst_n) begin
        lvl_q         <= '0;
        dl_cnt        <= '0;
        pending       <= 1'b0;
        response_late <= 1'b0;
      end else begin
        if (lvl_target != lvl_q) begin
          pending <= 1'b1;
          dl_cnt  <= '0;
          lvl_q   <= lvl_target;      // the response IS the level move
        end else if (pending) begin
          // The outputs are combinational from lvl_q, so the response
          // completes the cycle after the level moves. The counter
          // exists to catch a design where it does NOT -- which is
          // why the check is kept even though it is currently
          // unreachable. 30.5 §11: a guard another guard always
          // shadows is untested, so §16's cover watches it.
          pending <= 1'b0;
        end
        if (pending && dl_cnt != {DL_W{1'b1}}) dl_cnt <= dl_cnt + 1'b1;
        if (pending && dl_cnt >= RESP_DEADLINE[DL_W-1:0]) response_late <= 1'b1;
      end
    end

    assign level = lvl_q;

    // AUTHORITY -- §7 requirement 2, and BOTH terms. policy_limit
    // reduces the term the controller chooses; refresh_mode_req
    // reduces the term that CLOSES THE LOOP (§3) and which 17.3 §2
    // establishes cannot be declined.
    assign policy_limit = lvl_q;

    always_comb begin
      unique case (lvl_q)
        LVL_W'(0) : refresh_mode_req = RM_NORMAL;
        // Level 1 asks for temperature-compensated self refresh: the
        // device adjusts its own rate to the condition rather than
        // running the worst-case rate always. 24.1 §8 lists it as a
        // supported function; the VALUE of the saving is per-device.
        LVL_W'(1) : refresh_mode_req = RM_TCSR;
        LVL_W'(2) : refresh_mode_req = RM_TCSR;
        // Level 3 REQUESTS a masked mode. It is a request and not a
        // command because 24.2 §9 owns PASR as a mask with a
        // RETENTION consequence -- an excluded region is not
        // preserved -- so the placement owner must consent.
        default   : refresh_mode_req = RM_PASR;
      endcase
    end

    // §9's finding, as an output: theta is not a memory property, so
    // the loop gain cannot be computed here and must be MEASURED.
    // This reports what authority was actually applied, which is the
    // input §14's monitor needs to recompute G.
    assign authority_reported = lvl_q;

  end else begin : g_fanned

    // A platform with a fan has no runtime heat ceiling in this
    // sense. The mechanism is absent, and every output is inert --
    // not "disabled", which would imply it could be enabled.
    assign level              = '0;
    assign policy_limit       = '0;
    assign refresh_mode_req   = RM_NORMAL;
    assign response_late      = 1'b0;
    assign authority_reported = '0;

  end
  endgenerate
endmodule

// ---------------------------------------------------------------------
// traffic_throttle -- INTENTIONALLY DEFECTIVE, for review (§12).
//
// CLASSIFICATION: synthesisable, grade-D values, and CONTAINS A BUG.
//
// WHAT IT IS MEANT TO DO: the five-clause contract above -- reduce the
// controller's contribution to dissipation on request, within a
// deadline, with hysteresis, including the loop term.
//
// WHY IT EXISTS HERE: §7 requirement 2 is AUTHORITY, and §3 names the
// term that closes the loop. This block is what happens when a
// throttle is given authority over the power it can SEE -- traffic --
// and none over the power that closes the loop. It is the obvious
// design, which is why it is the dangerous one.
//
// HOW TO RUN IT: hold filt_temp above T_L3 on a platform where the
// refresh term dominates dissipation.
// EXPECTED RESULT under clause 2: refresh_mode_req moves away from
// RM_NORMAL.
// EXPECTED TRACE: at maximum level, BOTH outputs must have changed.
// Only one does.
//
// SYNTHESIS: a comparator chain and a hysteresis register.
//
// LIMITATIONS: decides the response only; filtering is upstream, per
// §5. That is STATED and is not the bug.
// ---------------------------------------------------------------------
module traffic_throttle #(
  parameter int T_L1          = 70,    // grade D
  parameter int T_L2          = 80,
  parameter int T_L3          = 88,
  parameter int HYST_K        = 4,
  parameter int RESP_DEADLINE = 2000,
  parameter int TMP_W         = 8,
  parameter int LVL_W         = 2,
  parameter int DL_W          = $clog2(RESP_DEADLINE + 1)
)(
  input  logic               clk,
  input  logic               rst_n,

  input  logic [TMP_W-1:0]   filt_temp,
  input  logic               filt_valid,

  output logic [LVL_W-1:0]   level,
  output logic [LVL_W-1:0]   policy_limit,
  output logic [1:0]         refresh_mode_req,
  output logic               response_late
);
  localparam logic [1:0] RM_NORMAL = 2'd0;

  logic [LVL_W-1:0] lvl_q;
  logic [DL_W-1:0]  dl_cnt;
  logic             pending;

  initial begin
    if (HYST_K >= (T_L2 - T_L1))
      $fatal(1, "traffic_throttle: HYST_K >= level gap");
  end

  // Clauses 1, 3 and 4 are ALL HONOURED. The level moves only on a
  // filtered temperature; hysteresis is applied in the downward
  // direction only; the deadline is counted and reported. A reviewer
  // checking "does this throttle respond correctly?" finds that it
  // does, and that is what conceals the defect.
  always_ff @(posedge clk) begin
    if (!rst_n) begin
      lvl_q <= '0;  dl_cnt <= '0;  pending <= 1'b0;  response_late <= 1'b0;
    end else if (filt_valid) begin
      logic [LVL_W-1:0] tgt;
      tgt = lvl_q;
      if      (filt_temp >= T_L3[TMP_W-1:0]) tgt = LVL_W'(3);
      else if (filt_temp >= T_L2[TMP_W-1:0]) tgt = (lvl_q > 2) ? lvl_q : LVL_W'(2);
      else if (filt_temp >= T_L1[TMP_W-1:0]) tgt = (lvl_q > 1) ? lvl_q : LVL_W'(1);
      if (lvl_q == 3 && filt_temp < (T_L3 - HYST_K)) tgt = LVL_W'(2);
      if (lvl_q == 2 && filt_temp < (T_L2 - HYST_K)) tgt = LVL_W'(1);
      if (lvl_q == 1 && filt_temp < (T_L1 - HYST_K)) tgt = LVL_W'(0);

      if (tgt != lvl_q) begin pending <= 1'b1; dl_cnt <= '0; lvl_q <= tgt; end
      else if (pending)  pending <= 1'b0;

      if (pending && dl_cnt != {DL_W{1'b1}}) dl_cnt <= dl_cnt + 1'b1;
      if (pending && dl_cnt >= RESP_DEADLINE[DL_W-1:0]) response_late <= 1'b1;
    end
  end

  assign level        = lvl_q;
  assign policy_limit = lvl_q;
  assign refresh_mode_req = RM_NORMAL;   // <-- THE DEFECT
endmodule

   GRADE D. Suppose at the hot operating point the memory's
   dissipation splits as:

       traffic-dependent term   P_traf  = 0.60 W
       refresh term             P_ref   = 1.00 W   (the 20x figure,
                                          CURRICULUM-DERIVED ratio)

   THIS BLOCK at maximum level: P_traf -> ~0, P_ref unchanged.

       power removed            0.60 W
       loop slope k             UNCHANGED at 0.024 W/K
       loop gain G = theta*k    UNCHANGED

   DERIVED, at theta = 40 K/W (a pocket, §4):
       G = 0.950,  amplification 1/(1-G) = 20.0

       so the 0.60 W that was removed reduces the steady-state rise
       by  0.60 * 40 = 24 K  open-loop -- but the loop is still
       amplifying everything that remains by TWENTY.

   and the failure mode: as temperature keeps rising, P_ref rises
   further, which the throttle cannot touch. The throttle escalates
   to maximum, reports "engaged, level 3, responded on time", and
   the temperature continues to climb.

  // CORRECTED. Clause 2: the response must include the LOOP term.
  // The policy limit acts on the OFFSET; the refresh mode acts on
  // the SLOPE, and only the slope changes G (§4).
  //
  // The deepest level REQUESTS a masked mode rather than commanding
  // it, because 24.2 §9 owns PASR as a mask with a retention
  // consequence -- so this block gains a handshake it did not have.
  always_comb begin
    unique case (lvl_q)
      LVL_W'(0) : refresh_mode_req = RM_NORMAL;
      LVL_W'(1),
      LVL_W'(2) : refresh_mode_req = RM_TCSR;
      default   : refresh_mode_req = RM_PASR;
    endcase
  end

// ---------------------------------------------------------------------
// loop_gain_monitor -- verification/telemetry, CORRECT as written.
//
// CLASSIFICATION: synthesisable telemetry. Drives nothing. Grade-D
// parameter values, and it computes NO physical constant.
//
// WHAT IT DOES: samples the filtered temperature and the refresh rate
// over a window and reports the OBSERVED slope between them, plus the
// applied authority. The slope is k of §4; theta must come from the
// platform, and the two together give G.
//
// WHY IT EXISTS HERE: §9's honest finding is that theta has no grade
// from any memory source. So the memory team can supply exactly one
// half of the loop gain -- k -- and this block supplies it as a
// measurement rather than a claim. 18.4 §1's discipline: the number
// this reports is grade C about THIS machine, and it must be carried
// with that qualification.
//
// HOW TO RUN IT: let temperature drift across a band under steady
// traffic, and read the slope.
// EXPECTED RESULT: a non-zero slope whose sign is positive --
// refresh rate rises with temperature (2.3 §4, 15.4).
//
// SYNTHESIS: two accumulators, one min/max tracker, one subtract.
// NO divider: the slope is reported as a numerator and a denominator
// so the consumer owns the rounding -- 27.5 refuses a lone
// percentage and 30.8 §11 requires a derived statistic's range to be
// visible.
//
// LIMITATIONS: reports k, not G. It cannot measure theta, it cannot
// detect a throttle whose authority is wrong -- §12's defect
// produces a PERFECTLY VALID k -- and it says so rather than
// implying coverage it does not give (27.3's independence
// discipline). What it CAN show is that k did not fall when the
// throttle engaged, which is §12's signature.
// ---------------------------------------------------------------------
module loop_gain_monitor #(
  parameter int WIN     = 1048576,
  parameter int TMP_W   = 8,
  // COUNT, not INDEX: the refresh accumulator must represent a window
  // in which every cycle carried a refresh, so it needs
  // $clog2(WIN + 1) bits. Sized for an expected rate it would
  // saturate at exactly the hot operating point the loop analysis is
  // about, and report a FALLING rate as temperature rose.
  parameter int CNT_W   = $clog2(WIN + 1),
  parameter int LVL_W   = 2
)(
  input  logic               clk,
  input  logic               rst_n,

  input  logic [TMP_W-1:0]   filt_temp,
  input  logic               filt_valid,
  input  logic               ref_issued,
  input  logic [LVL_W-1:0]   authority_applied,
  input  logic               win_tick,

  // The slope, as a PAIR. num / den is k in refreshes per degree.
  output logic signed [CNT_W:0] slope_num,
  output logic signed [TMP_W:0] slope_den,
  output logic [CNT_W-1:0]      r_refresh,
  output logic [TMP_W-1:0]      r_t_min,
  output logic [TMP_W-1:0]      r_t_max,
  output logic [LVL_W-1:0]      r_authority,
  output logic                  span_too_small,
  output logic                  result_valid
);
  initial begin
    if (WIN < 2) $fatal(1, "loop_gain_monitor: WIN >= 2");
  end

  logic [CNT_W-1:0] c_ref, c_ref_cold, c_ref_hot;
  logic [TMP_W-1:0] t_min, t_max;
  logic [TMP_W-1:0] t_mid;
  logic [LVL_W-1:0] auth_max;

  always_ff @(posedge clk) begin
    if (!rst_n) begin
      c_ref <= '0;  c_ref_cold <= '0;  c_ref_hot <= '0;
      // AND-accumulator discipline: a minimum tracker starts at
      // all-ones or the first sample never wins and the reported
      // minimum stays zero, which would make every span look
      // enormous and every slope look flat.
      t_min <= '1;  t_max <= '0;  t_mid <= '0;
      auth_max <= '0;
      slope_num <= '0;  slope_den <= '0;
      r_refresh <= '0;  r_t_min <= '0;  r_t_max <= '0;  r_authority <= '0;
      span_too_small <= 1'b0;  result_valid <= 1'b0;
    end else if (win_tick) begin
      r_refresh   <= c_ref;
      r_t_min     <= t_min;
      r_t_max     <= t_max;
      r_authority <= auth_max;

      // The slope, as a difference of refresh counts across the
      // temperature span, over the span. Reported as a pair.
      slope_num <= $signed({1'b0, c_ref_hot}) - $signed({1'b0, c_ref_cold});
      slope_den <= $signed({1'b0, t_max})     - $signed({1'b0, t_min});

      // A slope over a tiny span is noise, not a measurement. Flagged
      // rather than reported as a number -- 30.8 §11's rule that an
      // instrument which can report an impossible value has never
      // been checked, applied to a meaningless one.
      span_too_small <= (t_max <= t_min) || ((t_max - t_min) < 4);

      result_valid <= 1'b1;
      c_ref <= '0;  c_ref_cold <= '0;  c_ref_hot <= '0;
      t_min <= '1;  t_max <= '0;  auth_max <= '0;
    end else begin
      result_valid <= 1'b0;
      if (ref_issued && c_ref != {CNT_W{1'b1}}) c_ref <= c_ref + 1'b1;

      if (filt_valid) begin
        if (filt_temp < t_min) t_min <= filt_temp;
        if (filt_temp > t_max) t_max <= filt_temp;
        // The midpoint is recomputed from the running extremes, so
        // the cold/hot split follows the observed span rather than a
        // compiled threshold -- 32.1 §13's defect class avoided.
        t_mid <= (t_min >> 1) + (t_max >> 1);
        // Bucket each refresh by which half of the observed span its
        // temperature fell in.
        if (ref_issued) begin
          if (filt_temp >= t_mid) begin
            if (c_ref_hot  != {CNT_W{1'b1}}) c_ref_hot  <= c_ref_hot  + 1'b1;
          end else begin
            if (c_ref_cold != {CNT_W{1'b1}}) c_ref_cold <= c_ref_cold + 1'b1;
          end
        end
      end

      if (authority_applied > auth_max) auth_max <= authority_applied;
    end
  end
endmodule

// ---------------------------------------------------------------------
// thermal_filter -- CORRECT as written. Grade-D bounds only.
//
// CLASSIFICATION: synthesisable. No physical constant appears.
//
// WHAT IT IS: §5's requirement as hardware. A burst is free, so the
// throttle must see a WINDOWED quantity; and the window length is a
// property of the platform's thermal mass, so it is an INPUT.
//
// WHY IT EXISTS HERE: §5 derives that the throttle's deadline and its
// input window both come from a thermal mass rather than from any
// memory parameter. 32.1 §13 showed what happens when a platform
// property is compiled in; this block is the same discipline applied
// correctly, and the contrast is the point.
//
// HOW TO RUN IT: apply a short high-temperature burst shorter than
// cfg_win_len, then a sustained rise.
// EXPECTED RESULT: the burst does NOT raise filt_temp enough to
// engage a level; the sustained rise does.
// EXPECTED TRACE: filt_valid must stay LOW until a full window has
// been accumulated -- a partial-window average of a burst looks
// exactly like a sustained load, which is the subtle failure this
// block's clause 3 forbids.
//
// SYNTHESIS: one accumulator, one shift-divide, one sample counter.
// The divide is by a power of two only -- cfg_win_log2 is the
// configuration field, so no divider is instantiated.
//
// LIMITATIONS: a boxcar average over a power-of-two window. A real
// platform may need a different response shape, and if so the SHAPE
// is a platform property too and belongs in configuration by the
// same argument. Stated rather than implied.
// ---------------------------------------------------------------------
module thermal_filter #(
  parameter int TMP_W       = 8,
  // Bounds on the CONFIGURABLE window, not the window itself. A
  // bound is a design property; the value is a platform property.
  parameter int MAX_WIN_LOG2 = 16,
  // COUNT, not INDEX: the accumulator must represent
  // (2**MAX_WIN_LOG2) samples each up to 2**TMP_W - 1, so it needs
  // MAX_WIN_LOG2 + TMP_W bits. One bit short and it wraps at the
  // hottest sustained load -- reporting a LOW filtered temperature
  // exactly when the throttle is most needed.
  parameter int ACC_W        = MAX_WIN_LOG2 + TMP_W,
  parameter int SMP_W        = MAX_WIN_LOG2 + 1
)(
  input  logic                  clk,
  input  logic                  rst_n,

  input  logic [TMP_W-1:0]      raw_temp,
  input  logic                  raw_valid,

  // The window length, as a CONFIGURATION input. Expressed as a
  // log2 so the division is a shift: a divider here would be
  // hardware paid for a platform constant.
  input  logic [4:0]            cfg_win_log2,
  input  logic                  cfg_valid,

  output logic [TMP_W-1:0]      filt_temp,
  output logic                  filt_valid,
  output logic [TMP_W-1:0]      raw_peak,
  output logic                  cfg_out_of_range
);
  logic [ACC_W-1:0] acc;
  logic [SMP_W-1:0] smp;

  // Clause 4's range check, at RUNTIME rather than elaboration --
  // because the value is a configuration input and a register can
  // hold something that does not fit. 32.1 §13's correction needed
  // exactly this transition, and here it is designed in.
  assign cfg_out_of_range = cfg_valid && (cfg_win_log2 > MAX_WIN_LOG2[4:0]);

  always_ff @(posedge clk) begin
    if (!rst_n) begin
      acc        <= '0;
      smp        <= '0;
      filt_temp  <= '0;
      filt_valid <= 1'b0;
      raw_peak   <= '0;
    end else if (!cfg_valid || cfg_out_of_range) begin
      // No configuration, no output. 30.7 §9: an unconfigured value
      // is unknown, and unknown is not a default. A filter that
      // guessed a window would hand the throttle a number whose
      // meaning nobody knows.
      filt_valid <= 1'b0;
      acc        <= '0;
      smp        <= '0;
    end else if (raw_valid) begin
      // The raw peak is kept separately and is NOT filtered, because
      // §5 needs both quantities: the filtered one decides the
      // throttle and the peak shows what the thermal mass absorbed.
      // Reporting only the filtered value would hide the burst
      // entirely, and 24.1 §4's sustained-versus-burst distinction
      // would be unobservable.
      if (raw_temp > raw_peak) raw_peak <= raw_temp;

      acc <= acc + {{(ACC_W-TMP_W){1'b0}}, raw_temp};

      if (smp >= ((1 << cfg_win_log2) - 1)) begin
        // A full window: publish and restart.
        filt_temp  <= (acc + {{(ACC_W-TMP_W){1'b0}}, raw_temp}) >> cfg_win_log2;
        filt_valid <= 1'b1;
        acc        <= '0;
        smp        <= '0;
      end else begin
        // Clause 3: NOT a full window, so NOTHING is published. A
        // partial-window average of a burst is numerically identical
        // to a sustained load at a lower temperature, so publishing
        // early would make a free burst engage the throttle -- the
        // exact behaviour §5 says costs performance the thermal mass
        // had already paid for.
        filt_valid <= 1'b0;
        smp        <= smp + 1'b1;
      end
    end else begin
      filt_valid <= 1'b0;
    end
  end
endmodule

  // ---- The filter's own contract, asserted.
  // Clause 3: no output before a full window. This is the property
  // that forbids the numerically-plausible early publish.
  property p_no_output_before_full_window;
    @(posedge clk) disable iff (!rst_n)
      filt_valid |-> ($past(smp) >= ((1 << $past(cfg_win_log2)) - 1));
  endproperty
  assert property (p_no_output_before_full_window)
    else $error("a filtered value was published before a full window");

  // The configuration discipline, positively: an out-of-range or
  // absent configuration produces no output rather than a default.
  property p_unconfigured_produces_nothing;
    @(posedge clk) disable iff (!rst_n)
      (!cfg_valid || cfg_out_of_range) |-> !filt_valid;
  endproperty
  assert property (p_unconfigured_produces_nothing)
    else $error("the filter published a value with no valid configuration");

  // The accumulator must never wrap, because a wrapped accumulator
  // reports a LOW filtered temperature at the hottest sustained
  // load -- 30.8 §11's range rule, and the direction of the error
  // is what makes it dangerous rather than merely wrong.
  property p_accumulator_never_wraps;
    @(posedge clk) disable iff (!rst_n)
      (raw_valid && cfg_valid) |-> (acc <= ({ACC_W{1'b1}} - raw_temp));
  endproperty
  assert property (p_accumulator_never_wraps)
    else $error("the filter accumulator wrapped: the filtered value is understated");

  // ---- Covers: the window length must VARY, or the configuration
  //      mechanism was never tested even though it was honoured --
  //      32.1 §15's lesson, applied to a different platform value.
  cover property (@(posedge clk) disable iff (!rst_n)
                  filt_valid && (cfg_win_log2 == 4));
  cover property (@(posedge clk) disable iff (!rst_n)
                  filt_valid && (cfg_win_log2 == MAX_WIN_LOG2));
  // A BURST that did not engage: the case clause 3 exists for.
  cover property (@(posedge clk) disable iff (!rst_n)
                  (raw_peak > T_L1) && !filt_valid);
  // And the out-of-range configuration, so the refusal path is known
  // to have been exercised rather than merely present.
  cover property (@(posedge clk) disable iff (!rst_n) cfg_out_of_range);

  // Offered as "proves the throttle works". All three PASS on the
  // defective block.
  property p_engages_within_deadline;
    @(posedge clk) disable iff (!rst_n)
      (filt_valid && filt_temp >= T_L1 && level == 0) |->
        ##[1:RESP_DEADLINE] (level != 0);
  endproperty
  assert property (p_engages_within_deadline)
    else $error("the throttle did not engage within its deadline");

  property p_hysteresis_holds;
    @(posedge clk) disable iff (!rst_n)
      (level == 1 && filt_valid && filt_temp >= (T_L1 - HYST_K)) |=> (level >= 1);
  endproperty
  assert property (p_hysteresis_holds)
    else $error("the throttle disengaged inside the hysteresis band");

  property p_limit_tracks_level;
    @(posedge clk) disable iff (!rst_n) policy_limit == level;
  endproperty
  assert property (p_limit_tracks_level)
    else $error("the policy limit did not track the level");

  // Clause 2. It names refresh_mode_req, so it cannot pass while
  // that output is tied off. Variety 2's repair.
  property p_authority_includes_refresh;
    @(posedge clk) disable iff (!rst_n)
      (level >= 1) |-> (refresh_mode_req != RM_NORMAL);
  endproperty
  assert property (p_authority_includes_refresh)
    else $error("the throttle engaged without authority over the refresh term");

  // And the monotonicity of the authority set: a deeper level must
  // never REDUCE authority. This catches a related bug -- a level
  // table with a transcription error -- that the property above
  // would miss, because it only requires "not normal".
  property p_authority_is_monotone;
    @(posedge clk) disable iff (!rst_n)
      (level > $past(level)) |-> (refresh_mode_req >= $past(refresh_mode_req));
  endproperty
  assert property (p_authority_is_monotone)
    else $error("a deeper throttle level reduced the refresh authority");

  // Clause 5. The reported authority must be the applied authority,
  // or §14's measurement is being fed a number the block does not
  // mean -- 32.1 §13's "the block reports a configuration it is not
  // using", in a different domain.
  property p_reported_authority_is_applied;
    @(posedge clk) disable iff (!rst_n) authority_reported == level;
  endproperty
  assert property (p_reported_authority_is_applied)
    else $error("the block reports an authority it did not apply");

  // The masked mode must never be applied WITHOUT consent, because
  // 24.2 §9's retention consequence means it discards data. This is
  // the one property in the chapter whose violation is a
  // CORRECTNESS failure rather than a thermal one.
  property p_masked_mode_requires_consent;
    @(posedge clk) disable iff (!rst_n)
      (refresh_mode_req == RM_PASR) |-> placement_consent;
  endproperty
  assert property (p_masked_mode_requires_consent)
    else $error("a masked refresh mode was applied without placement consent");

  // TEMPTING, and it is NOT a proof. The consequent depends on the
  // TESTBENCH'S THERMAL MODEL -- on theta, on the mass, on the
  // ambient. §9 established that none of those is a memory property.
  //
  // So this property's outcome is a statement about the model, and a
  // model that under-states the loop will let it pass on the
  // defective block: at a bench-like theta, throttling traffic DOES
  // reduce temperature (§13).
  property p_temperature_falls_after_throttle;
    @(posedge clk) disable iff (!rst_n)
      (level >= 2) |-> ##[1:SETTLE] (filt_temp < $past(filt_temp, SETTLE));
  endproperty

  // ---- Covers. The dimension this defect scales with is the
  //      THERMAL PATH -- a property of the environment's model, and
  //      31.4 §14's rule says running longer never reaches it.
  // The loop-dominated regime: the only one in which the defect is
  // observable. If this cover is zero, thermal validation ran
  // exclusively in the regime where §13 says the bug cannot appear.
  cover property (@(posedge clk) disable iff (!rst_n)
                  (level >= 2) && (refresh_power_est > traffic_power_est));
  // The traffic-dominated regime, so both are known to have run.
  cover property (@(posedge clk) disable iff (!rst_n)
                  (level >= 2) && (traffic_power_est >= refresh_power_est));
  // Each level reached, per 31.3 §15's per-index rule applied to a
  // level space.
  cover property (@(posedge clk) disable iff (!rst_n) level == 1);
  cover property (@(posedge clk) disable iff (!rst_n) level == 2);
  cover property (@(posedge clk) disable iff (!rst_n) level == 3);
  // The hysteresis band actually occupied -- a fall that did NOT
  // disengage. Without this, p_hysteresis_holds is vacuous.
  cover property (@(posedge clk) disable iff (!rst_n)
                  (level == 1) && filt_valid &&
                  (filt_temp < T_L1) && (filt_temp >= (T_L1 - HYST_K)));
  // The deadline path, which should be unreachable in the correct
  // block -- 30.10 §12's dead-or-live distinction: this cover must
  // go DEAD after the fix and be LIVE while debugging one.
  cover property (@(posedge clk) disable iff (!rst_n) response_late);

  // §6's tension, resolved as a table rather than a single bound. A
  // throttle extends every progress bound, so one bound justified at
  // full rate is VIOLATED by a correct throttle and one justified at
  // the deepest throttle is uselessly loose at full rate. 30.9 §5 Q2
  // owns that a bound must be justified rather than chosen.
  property p_progress_bound_per_level;
    @(posedge clk) disable iff (!rst_n)
      req_accepted |-> ##[1:MAX_LAT_FOR_LEVEL(level)] resp_valid;
  endproperty
  assert property (p_progress_bound_per_level)
    else $error("a request exceeded the progress bound for the active throttle level");

  // The response deadline itself, as a bounded liveness property --
  // never as unbounded eventuality (30.9 §5 Q2). RESP_DEADLINE is
  // justified from the THERMAL time constant (§5), not from any
  // memory parameter, and that derivation is the property's warrant.
  property p_response_meets_deadline;
    @(posedge clk) disable iff (!rst_n)
      $rose(pending) |-> ##[1:RESP_DEADLINE] !pending;
  endproperty
  assert property (p_response_meets_deadline)
    else $error("the response did not complete within its deadline");

  // A burst must NOT engage the throttle -- §5's requirement that the
  // input be filtered. This is the two-sided bound: the safety
  // property alone is satisfied by a throttle that engages always.
  property p_no_engage_without_filtered_input;
    @(posedge clk) disable iff (!rst_n)
      (!filt_valid) |-> $stable(level);
  endproperty
  assert property (p_no_engage_without_filtered_input)
    else $error("the level moved on an unfiltered sample");

  // The PLATFORM invariant, parameter in the antecedent and not in
  // the claim -- 31.1 §14's test for sharing a property across
  // configurations. It may be shared.
  property p_fanned_platform_never_throttles;
    @(posedge clk) disable iff (!rst_n)
      (!THERMAL_LIMITED) -> (level == 0 && refresh_mode_req == RM_NORMAL);
  endproperty
  assert property (p_fanned_platform_never_throttles)
    else $error("a platform with no heat ceiling engaged a throttle");

  // And the invariant that makes the hysteresis specification
  // MEANINGFUL rather than merely present: the level must never
  // oscillate on consecutive filtered samples. §7 requirement 3, and
  // 24.2 §14's oscillation corner case is what it forbids.
  property p_no_single_sample_oscillation;
    @(posedge clk) disable iff (!rst_n)
      (filt_valid && level != $past(level)) |=>
        (!filt_valid || level == $past(level));
  endproperty
  assert property (p_no_single_sample_oscillation)
    else $error("the level changed on two consecutive samples: hysteresis is ineffective");