Data-Centre Servers

   1  WHICH CONSTRAINT
        DDR does not own the placement decision, and the decision
        that does own it CONSUMES DDR's observed behaviour (§2, §4)

   2  WHAT DECISION
        export a DECOMPOSITION rather than a number, because the
        naive export closes an oscillating loop (§6, §8)

   3  WHAT GRADE
        B for the DDR mechanisms, D for every figure, and the
        placement policy itself is outside this chapter (§9)

   the policy's question, for a given page:

     "if this page lived on the near tier instead of the far tier,
      how much would its access cost change?"

   which decomposes into:

     1  the near tier's cost for THIS page's access pattern
     2  the far tier's cost for the same pattern
     3  the cost of MOVING it

   the DDR controller can speak to (1) and to part of (3).
   It can say nothing about (2), which is the CXL track's.

   GRADE D. Two pages, same tier, different access patterns.

     page P  : row-hit dominant  -> irreducible part 20 units
     page Q  : conflict dominant -> irreducible part 48 units
     current queueing term (shared, load-dependent) : 40 units

   what a MEAN export reports:
     P : 20 + 40 = 60
     Q : 48 + 40 = 88
     ratio Q/P = 1.47

   what the PAGE-DEPENDENT part is:
     P : 20,  Q : 48,  ratio = 2.40

   DERIVED: the blended figure UNDERSTATES the difference between
   the two pages by a factor of 1.63, because a large shared term
   is added to both. So the policy's ability to DISCRIMINATE
   between pages is degraded by exactly the term that has nothing
   to do with either page.

   the placement loop, when the advisory includes queueing

     policy sees DDR advisory latency LOW
         |
         | migrates hot pages TO the near tier
         v
     DDR's offered load RISES
         |
         | 23.1 §8: queueing has NO UPPER BOUND
         v
     DDR advisory latency RISES
         |
         | policy sees the near tier as expensive
         v
     migrates pages AWAY
         |
         | DDR's load FALLS
         v
     advisory latency FALLS        <-- closes here, back to the top

   the delay, and where it comes from

     a migration is not instantaneous. It is a bulk data movement
     (§2 row four), so the load change LAGS the decision by the
     migration time T_m.

     and the measurement is windowed: the advisory reflects an
     average over W cycles, so the observation LAGS the load by W.

   total loop delay  T_d  =  T_m + W  (plus the policy's own period)

   a negative-feedback loop with gain G and delay T_d oscillates
   when the delay is long relative to the loop's own response
   time -- the classic result, and here BOTH terms are large:
   a bulk migration and a measurement window.

   GRADE D.  migration time T_m = 10 ms, window W = 1 ms,
             policy period = 5 ms.

     T_d = 10 + 1 + 5 = 16 ms

   so the policy acts on information about a load state that is
   at least 16 ms old, and its action takes 10 ms to take effect.
   By the time the load has moved, the advisory it acted on
   describes a system that no longer exists.

   observable consequence: pages migrate in, the advisory rises,
   pages migrate out, the advisory falls, pages migrate in. The
   PERIOD is set by T_d and the AMPLITUDE by how many pages the
   policy moves per decision.

   what hysteresis fixes and what it does not

   FIXES: small-signal chatter. A page near the decision boundary
          no longer flips on every window's noise.

   DOES NOT FIX: the delayed loop of §6. Hysteresis widens the
          band a signal must cross; it does not shorten T_d. A
          delayed loop whose swing EXCEEDS the band still
          oscillates, at the same period, with the band
          subtracted from the amplitude.

   and here the swing is large by construction:
     the advisory's swing = the queueing term's swing
     the queueing term's swing = a function of how many pages
       the policy just moved
     -> the loop's own action sets the swing that must be
        damped, so a fixed band cannot be sized against it

   the export, as a contract

     per address region, per window:
       irreducible_cost   -- row-state work + device latency +
                             transfer.  DOES NOT move with load.
       queueing_cost      -- labelled separately. MOVES with load.
       samples            -- so the consumer knows the confidence
       region_id          -- the controller's own regioning

     and one flag:
       advisory_stale     -- the window closed with too few samples
                             for this region to be usable

   the stale flag matters: a region with three samples has an
   irreducible cost estimate that is noise, and 30.8 §11's rule
   says an instrument that can report a meaningless value has
   not been checked.

// ---------------------------------------------------------------------
// tier_advisory_export -- the platform-profile block of §11.
//
// CLASSIFICATION: synthesisable telemetry. Drives nothing directly,
// but its output is CONSUMED BY A CONTROL LOOP (§2 row five), which
// is why its contract is stricter than a debug counter's.
//
// WHAT IT IS: §8's three-part contract. It publishes 23.1's
// decomposition per address region, separating the irreducible terms
// from the load-dependent one, and NEVER sums them.
//
// WHY IT EXISTS HERE: §5 proves a blended export degrades the
// policy's ability to discriminate between pages, and worsens under
// load. §6 proves it closes a delayed negative-feedback loop. §7
// proves hysteresis cannot damp a loop whose swing the controller's
// own action sets. So the fix is structural: publish the component
// with zero load-dependence.
//
// HOW TO RUN IT: run a mixed workload and read irr_cost and
// queue_cost per region under two different load levels.
// EXPECTED RESULT: irr_cost is stable across load levels for the
// same access pattern; queue_cost is not.
// EXPECTED TRACE: irr_cost must not change when offered load
// changes and the access pattern does not.
//
// SYNTHESIS: per-region accumulators plus a sample counter. No
// divider: every cost is published as a sum and a count.
//
// LIMITATIONS: it describes THIS TIER only. The far tier's cost is
// /cxl/cxl-latency-anatomy's and the instruction-to-port path is
// /cxl/cxl-memory-access-cost's, so this block publishes a
// MEASUREMENT and never a RECOMMENDATION -- §8's honest limit. It
// also regions by address, not by page: 18.2 owns what the
// controller can see, and the policy maps regions to pages.
// ---------------------------------------------------------------------
module tier_advisory_export #(
  // The platform property. A single-tier platform has no placement
  // policy to advise, so the mechanism is ABSENT rather than unused.
  parameter bit TIERED       = 1'b1,

  parameter int NUM_REGIONS  = 16,
  parameter int WIN          = 1048576,
  // §8's stale threshold: a region with too few samples has an
  // estimate that is noise, and 30.8 §11's rule says an instrument
  // that can report a meaningless value has not been checked.
  parameter int MIN_SAMPLES  = 64,
  parameter int LAT_W        = 20,
  // COUNT, not INDEX: an accumulator must represent MIN_SAMPLES and
  // beyond at full latency, so it needs LAT_W + $clog2(WIN + 1)
  // bits. One short and it wraps on a hot region -- publishing a LOW
  // irreducible cost for exactly the region the policy is about to
  // move, which is the wrong direction.
  parameter int ACC_W        = LAT_W + $clog2(WIN + 1),
  parameter int SMP_W        = $clog2(WIN + 1),
  parameter int RID_W        = $clog2(NUM_REGIONS > 1 ? NUM_REGIONS : 2)
)(
  input  logic                clk,
  input  logic                rst_n,

  // One completed access, with 23.1's components already separated.
  // This block does NOT decompose -- 23.1 §10 owns the decomposer
  // and 27.3's independence discipline says a consumer must not
  // recompute its producer's result.
  input  logic                acc_done,
  input  logic [RID_W-1:0]    acc_region,
  input  logic [LAT_W-1:0]    acc_irreducible,
  input  logic [LAT_W-1:0]    acc_queueing,

  input  logic                win_tick,

  // The export. Published as SUMS and a COUNT, never as a mean --
  // §5's argument, and 27.5's refusal to produce a lone figure.
  output logic [ACC_W-1:0]    irr_sum   [NUM_REGIONS],
  output logic [ACC_W-1:0]    queue_sum [NUM_REGIONS],
  output logic [SMP_W-1:0]    samples   [NUM_REGIONS],
  output logic [NUM_REGIONS-1:0] advisory_stale,
  output logic                result_valid,
  output logic                acc_saturated
);
  initial begin
    if (NUM_REGIONS < 1) $fatal(1, "tier_advisory_export: NUM_REGIONS >= 1");
    if (MIN_SAMPLES < 1) $fatal(1, "tier_advisory_export: MIN_SAMPLES >= 1");
    if (WIN < MIN_SAMPLES)
      $fatal(1, "tier_advisory_export: WIN < MIN_SAMPLES -- no region can ever be non-stale");
  end

  generate
  if (TIERED) begin : g_tiered

    logic [ACC_W-1:0] a_irr [NUM_REGIONS];
    logic [ACC_W-1:0] a_q   [NUM_REGIONS];
    logic [SMP_W-1:0] a_n   [NUM_REGIONS];

    always_ff @(posedge clk) begin
      if (!rst_n) begin
        for (int r = 0; r < NUM_REGIONS; r++) begin
          a_irr[r] <= '0;  a_q[r] <= '0;  a_n[r] <= '0;
          irr_sum[r] <= '0;  queue_sum[r] <= '0;  samples[r] <= '0;
        end
        advisory_stale <= '1;      // nothing measured yet: ALL stale
        result_valid   <= 1'b0;
        acc_saturated  <= 1'b0;
      end else if (win_tick) begin
        for (int r = 0; r < NUM_REGIONS; r++) begin
          irr_sum[r]   <= a_irr[r];
          queue_sum[r] <= a_q[r];
          samples[r]   <= a_n[r];
          // §8's stale flag, per region. A region with too few
          // samples is REPORTED AS UNUSABLE rather than published
          // with a noisy estimate -- because the consumer is a
          // control loop (§2 row five) and it will act on whatever
          // it is given.
          advisory_stale[r] <= (a_n[r] < MIN_SAMPLES[SMP_W-1:0]);
          a_irr[r] <= '0;  a_q[r] <= '0;  a_n[r] <= '0;
        end
        result_valid <= 1'b1;
      end else begin
        result_valid <= 1'b0;
        if (acc_done) begin
          // The two components are accumulated SEPARATELY and are
          // never added. That separation is the whole block: §5
          // shows a blended figure loses discrimination under load,
          // and §6 shows it closes the loop.
          if (a_irr[acc_region] > ({ACC_W{1'b1}} - acc_irreducible))
            acc_saturated <= 1'b1;
          else
            a_irr[acc_region] <= a_irr[acc_region] + acc_irreducible;

          if (a_q[acc_region] > ({ACC_W{1'b1}} - acc_queueing))
            acc_saturated <= 1'b1;
          else
            a_q[acc_region] <= a_q[acc_region] + acc_queueing;

          if (a_n[acc_region] != {SMP_W{1'b1}})
            a_n[acc_region] <= a_n[acc_region] + 1'b1;
          else
            acc_saturated <= 1'b1;
        end
      end
    end

  end else begin : g_single_tier

    // A single-tier platform has no placement policy to advise. The
    // export is ABSENT, and every region is permanently stale --
    // which is the honest encoding of "there is no advisory here"
    // rather than publishing zeros a consumer might act on.
    always_ff @(posedge clk) begin
      if (!rst_n || 1'b1) begin
        for (int r = 0; r < NUM_REGIONS; r++) begin
          irr_sum[r] <= '0;  queue_sum[r] <= '0;  samples[r] <= '0;
        end
        advisory_stale <= '1;
        result_valid   <= 1'b0;
        acc_saturated  <= 1'b0;
      end
    end

  end
  endgenerate
endmodule

// ---------------------------------------------------------------------
// migration_churn_monitor -- verification/telemetry, CORRECT as written.
//
// CLASSIFICATION: synthesisable telemetry. Drives nothing. Grade D.
//
// WHAT IT DOES: counts migrations per window and, crucially, the
// fraction that migrate BACK within a bounded number of windows --
// which is the observable that distinguishes a converging policy
// from a thrashing one.
//
// WHY IT EXISTS HERE: §6 establishes that the cost of the loop is
// the migration traffic, not the oscillation itself, and §7 that
// hysteresis cannot damp it. So the question a platform must answer
// is "is the policy converging?", and a migration COUNT cannot
// answer it -- a converging policy also migrates. Only the
// migrate-back fraction separates them.
//
// HOW TO RUN IT: run the real policy and read back_fraction as a
// pair over several windows.
// EXPECTED RESULT: a converging policy's back_fraction falls toward
// zero; a thrashing one's stays high indefinitely.
//
// SYNTHESIS: one direction bit and one recency counter per region,
// plus two counters. No divider.
//
// LIMITATIONS: it detects a region returning to a tier it recently
// left. It cannot attribute the cause -- a legitimately changing
// working set also migrates back, and distinguishing that from
// §6's loop requires correlating with the advisory's own swing,
// which §18's row six does. Stating that rather than implying
// attribution is 27.3's independence discipline.
// ---------------------------------------------------------------------
module migration_churn_monitor #(
  parameter int NUM_REGIONS = 16,
  parameter int WIN         = 1048576,
  // How many windows count as "recently". §6's loop period is set by
  // the total delay T_d, so this is a PLATFORM property and on a
  // real system it is a configuration input -- 32.1 §14's lesson.
  parameter int RECENT_WINS = 4,
  parameter int CNT_W       = $clog2(WIN + 1),
  parameter int REC_W       = $clog2(RECENT_WINS + 1),
  parameter int RID_W       = $clog2(NUM_REGIONS > 1 ? NUM_REGIONS : 2)
)(
  input  logic               clk,
  input  logic               rst_n,

  input  logic               mig_event,
  input  logic [RID_W-1:0]   mig_region,
  input  logic               mig_to_near,     // 1 = toward DDR
  input  logic               win_tick,

  output logic [CNT_W-1:0]   r_migrations,
  output logic [CNT_W-1:0]   r_back_migrations,
  output logic [CNT_W-1:0]   r_bytes_moved,
  output logic               result_valid
);
  // Per region: the direction of its last migration and how many
  // windows ago. A "back migration" is a migration in the OPPOSITE
  // direction to the last one, within RECENT_WINS.
  logic             last_dir [NUM_REGIONS];
  logic             has_last [NUM_REGIONS];
  logic [REC_W-1:0] age      [NUM_REGIONS];
  logic [CNT_W-1:0] c_mig, c_back, c_bytes;

  initial begin
    if (RECENT_WINS < 1) $fatal(1, "migration_churn_monitor: RECENT_WINS >= 1");
  end

  always_ff @(posedge clk) begin
    if (!rst_n) begin
      for (int r = 0; r < NUM_REGIONS; r++) begin
        last_dir[r] <= 1'b0;  has_last[r] <= 1'b0;  age[r] <= '0;
      end
      c_mig <= '0;  c_back <= '0;  c_bytes <= '0;
      r_migrations <= '0;  r_back_migrations <= '0;  r_bytes_moved <= '0;
      result_valid <= 1'b0;
    end else if (win_tick) begin
      // Published as a PAIR -- migrations and back-migrations -- so
      // the consumer divides and owns the rounding. 27.5 refuses a
      // lone percentage and 30.8 §11 requires the denominator to be
      // visible; a lone "churn score" would hide that a small
      // back-fraction over three migrations means nothing.
      r_migrations      <= c_mig;
      r_back_migrations <= c_back;
      r_bytes_moved     <= c_bytes;
      result_valid      <= 1'b1;
      c_mig <= '0;  c_back <= '0;  c_bytes <= '0;
      // Age every region's memory of its last migration, saturating
      // so a long-settled region does not wrap back into "recent".
      for (int r = 0; r < NUM_REGIONS; r++) begin
        if (has_last[r]) begin
          if (age[r] >= RECENT_WINS[REC_W-1:0]) has_last[r] <= 1'b0;
          else                                  age[r] <= age[r] + 1'b1;
        end
      end
    end else begin
      result_valid <= 1'b0;
      if (mig_event) begin
        if (c_mig != {CNT_W{1'b1}}) c_mig <= c_mig + 1'b1;
        // A migration in the opposite direction to a recent one is a
        // BACK migration -- the observable §6's loop produces and a
        // converging policy does not.
        if (has_last[mig_region] && (last_dir[mig_region] != mig_to_near)) begin
          if (c_back != {CNT_W{1'b1}}) c_back <= c_back + 1'b1;
        end
        last_dir[mig_region] <= mig_to_near;
        has_last[mig_region] <= 1'b1;
        age[mig_region]      <= '0;
        // §2 row four: a migration is traffic the controller did not
        // request. Counting the BYTES is what turns the oscillation
        // into a number a capacity argument can use.
        if (c_bytes != {CNT_W{1'b1}}) c_bytes <= c_bytes + 1'b1;
      end
    end
  end
endmodule

   migration traffic, placed on 32.1 §3's two axes

     deadline    : NO. Nothing stalls waiting for a migration to
                   complete -- the page is readable at its old
                   location until the move commits.
     droppable   : NO. Discarding it loses the policy's decision
                   and may lose data if the move is destructive.

   -> the writeback class exactly, and 32.1 §3's response for that
      class is DEFER FREELY, NEVER DISCARD.

   so the controller CAN rate-limit migration traffic without
   violating anything, and that is §7 remedy one made available.

// ---------------------------------------------------------------------
// migration_rate_limiter -- CORRECT as written. Grade-D bounds.
//
// CLASSIFICATION: synthesisable. It DELAYS and never drops.
//
// WHAT IT IS: §7's first remedy. It bounds the migration bytes
// admitted per window, so §6's loop swing is bounded by the limiter
// rather than by the policy's appetite -- which is what §7 says
// hysteresis cannot achieve.
//
// WHY IT EXISTS HERE: §7 establishes that a hysteresis band cannot
// be sized against a swing the controller's own action determines.
// Bounding the action bounds the swing, and 32.1 §3's droppability
// axis is what makes bounding LEGAL: migration traffic has no
// deadline, so deferring it violates nothing.
//
// HOW TO RUN IT: offer a migration burst far above the budget.
// EXPECTED RESULT: it is admitted at the budgeted rate over several
// windows, and NOTHING is dropped -- mig_deferred rises and
// mig_dropped does not exist as a concept in this block.
// EXPECTED TRACE: admitted bytes per window never exceed BUDGET,
// and the backlog drains monotonically once the offer stops.
//
// SYNTHESIS: one budget counter, one backlog counter. No memory --
// the migration data itself is elsewhere.
//
// LIMITATIONS: it bounds the RATE. It does not bound the TOTAL, so a
// policy that migrates continuously still consumes the budget
// continuously -- §12's churn monitor is what detects that, and this
// block cannot. Nor does it prioritise between migrations: 17.4 owns
// arbitration. Both boundaries are STATED and neither is the bug.
// ---------------------------------------------------------------------
module migration_rate_limiter #(
  // Grade D. The share of a window's bandwidth migrations may use.
  // On a real platform this is a CONFIGURATION input, per 32.1 §14:
  // a budget is a platform policy and a platform policy compiled in
  // is grade D consumed as grade A.
  parameter int WIN            = 65536,
  parameter int BUDGET_PCT     = 5,
  // COUNT, not INDEX: the backlog must represent a full window's
  // offer, so it needs $clog2(WIN + 1) bits. Sized to the BUDGET it
  // would saturate exactly when a burst exceeds the budget -- the
  // counter failing inside the case it exists to handle, and
  // silently losing a deferred migration.
  parameter int CNT_W          = $clog2(WIN + 1),
  parameter int BUDGET         = (WIN * BUDGET_PCT) / 100
)(
  input  logic               clk,
  input  logic               rst_n,

  input  logic               mig_offer,       // a migration beat offered
  input  logic               app_beat,        // an application beat
  input  logic               win_tick,

  output logic               mig_admit,
  output logic               mig_deferred,
  output logic [CNT_W-1:0]   backlog,
  output logic [CNT_W-1:0]   r_admitted,
  output logic [CNT_W-1:0]   r_offered,
  output logic               backlog_overflow,
  output logic               result_valid
);
  logic [CNT_W-1:0] spent, offered, backlog_q;

  initial begin
    if (BUDGET_PCT < 1 || BUDGET_PCT > 100)
      $fatal(1, "migration_rate_limiter: BUDGET_PCT must be 1..100");
    if (BUDGET < 1)
      $fatal(1, "migration_rate_limiter: BUDGET rounds to zero -- migrations could never complete");
    // §7's remedy must be BOUNDED IN BOTH DIRECTIONS. A budget of
    // 100% is indistinguishable from having no limiter, so the
    // mechanism would be present in the source and absent in the
    // silicon -- 31.2 §7's hazard.
    if (BUDGET_PCT == 100)
      $warning("migration_rate_limiter: BUDGET_PCT = 100 disables the limit (§7)");
  end

  // The admission decision. A migration beat is admitted while the
  // window's budget remains; otherwise it is DEFERRED into the
  // backlog. It is never dropped -- 32.1 §3's response for a
  // non-droppable class with no deadline.
  assign mig_admit    = mig_offer && (spent < BUDGET[CNT_W-1:0]);
  assign mig_deferred = mig_offer && !mig_admit;

  always_ff @(posedge clk) begin
    if (!rst_n) begin
      spent <= '0;  offered <= '0;  backlog_q <= '0;
      r_admitted <= '0;  r_offered <= '0;
      backlog_overflow <= 1'b0;  result_valid <= 1'b0;
    end else if (win_tick) begin
      r_admitted   <= spent;
      r_offered    <= offered;
      result_valid <= 1'b1;
      spent        <= '0;
      offered      <= '0;
      // The backlog SURVIVES the window boundary, because a deferred
      // migration is still owed. Clearing it here would be a silent
      // drop of a non-droppable class.
    end else begin
      result_valid <= 1'b0;
      if (mig_offer) begin
        if (offered != {CNT_W{1'b1}}) offered <= offered + 1'b1;
        if (mig_admit) begin
          if (spent != {CNT_W{1'b1}}) spent <= spent + 1'b1;
        end else begin
          // Deferred: it joins the backlog and is owed. Overflow is
          // REPORTED rather than absorbed, because an absorbed
          // backlog entry is a dropped migration and this class must
          // not be dropped.
          if (backlog_q == {CNT_W{1'b1}}) backlog_overflow <= 1'b1;
          else                            backlog_q <= backlog_q + 1'b1;
        end
      end
      // Drain the backlog with any budget the current offer left
      // unused, so a burst is spread across windows rather than lost.
      if (!mig_offer && (backlog_q != '0) && (spent < BUDGET[CNT_W-1:0])) begin
        backlog_q <= backlog_q - 1'b1;
        if (spent != {CNT_W{1'b1}}) spent <= spent + 1'b1;
      end
    end
  end

  assign backlog = backlog_q;
endmodule

  // ---- The limiter's contract.
  // The bound itself. An invariant: there is no window on which
  // exceeding the budget is acceptable.
  property p_budget_respected;
    @(posedge clk) disable iff (!rst_n)
      result_valid |-> (r_admitted <= BUDGET);
  endproperty
  assert property (p_budget_respected)
    else $error("migration admissions exceeded the window budget");

  // NOTHING IS DROPPED. Every offered beat is either admitted or
  // backlogged -- 32.1 §3's non-droppable class, and this is the
  // property that distinguishes deferral from discard.
  property p_nothing_dropped;
    @(posedge clk) disable iff (!rst_n)
      mig_offer |-> (mig_admit ^ mig_deferred);
  endproperty
  assert property (p_nothing_dropped)
    else $error("an offered migration beat was neither admitted nor deferred");

  // The backlog must DRAIN, or deferral becomes indefinite
  // postponement -- which for a class with no deadline is still
  // wrong, because the policy is waiting. A bounded liveness
  // property, and the bound is JUSTIFIED: a backlog of B beats
  // drains in ceil(B / BUDGET) windows once the offer stops.
  property p_backlog_drains;
    @(posedge clk) disable iff (!rst_n)
      (backlog != '0 && !mig_offer) |->
        ##[1:(WIN * 2)] (backlog < $past(backlog));
  endproperty
  assert property (p_backlog_drains)
    else $error("the migration backlog did not drain with the offer removed");

  // ---- Covers: the two regimes and the boundary.
  // A burst ABOVE the budget -- the case the limiter exists for.
  cover property (@(posedge clk) disable iff (!rst_n)
                  result_valid && (r_offered > BUDGET));
  // A window entirely WITHIN the budget, so the pass-through path is
  // known to work rather than assumed.
  cover property (@(posedge clk) disable iff (!rst_n)
                  result_valid && (r_offered > 0) && (r_offered <= BUDGET));
  // The boundary itself -- 30.3 §10: a rule respected but never
  // exercised at its boundary has not been tested.
  cover property (@(posedge clk) disable iff (!rst_n)
                  mig_offer && (spent == BUDGET - 1));

// ---------------------------------------------------------------------
// latency_advisory -- INTENTIONALLY DEFECTIVE, for review (§14).
//
// CLASSIFICATION: synthesisable telemetry, grade-D values, CONTAINS
// A BUG. Its output is consumed by a CONTROL LOOP (§2 row five).
//
// WHAT IT IS MEANT TO DO: the five-clause contract above -- publish
// 23.1's decomposition per region so a placement policy can act on
// the part that is a property of the page.
//
// WHY IT EXISTS HERE: §5 proves a blended export loses
// discrimination under load; §6 proves it closes a delayed
// negative-feedback loop; §7 proves hysteresis cannot damp it. This
// block is the blended export, and it is the natural design --
// "publish the latency" is what anybody would ask for.
//
// HOW TO RUN IT: hold the access pattern fixed and raise the offered
// load.
// EXPECTED RESULT under clause 4: the published cost is UNCHANGED.
// EXPECTED TRACE: irr_sum must not move with load. It does.
//
// SYNTHESIS: per-region accumulators and a sample counter.
//
// LIMITATIONS: this tier only, as §11's block. That is STATED and is
// not the bug.
// ---------------------------------------------------------------------
module latency_advisory #(
  parameter int NUM_REGIONS  = 16,
  parameter int WIN          = 1048576,
  parameter int MIN_SAMPLES  = 64,
  parameter int LAT_W        = 20,
  parameter int ACC_W        = LAT_W + $clog2(WIN + 1),
  parameter int SMP_W        = $clog2(WIN + 1),
  parameter int RID_W        = $clog2(NUM_REGIONS > 1 ? NUM_REGIONS : 2)
)(
  input  logic                clk,
  input  logic                rst_n,

  input  logic                acc_done,
  input  logic [RID_W-1:0]    acc_region,
  // Both components ARE on the interface. 23.1's decomposer already
  // separated them, so clause 2 is available to this block.
  input  logic [LAT_W-1:0]    acc_irreducible,
  input  logic [LAT_W-1:0]    acc_queueing,

  input  logic                win_tick,

  output logic [ACC_W-1:0]    irr_sum   [NUM_REGIONS],
  output logic [SMP_W-1:0]    samples   [NUM_REGIONS],
  output logic [NUM_REGIONS-1:0] advisory_stale,
  output logic                result_valid,
  output logic                acc_saturated
);
  logic [ACC_W-1:0] a_tot [NUM_REGIONS];
  logic [SMP_W-1:0] a_n   [NUM_REGIONS];

  initial begin
    if (NUM_REGIONS < 1) $fatal(1, "latency_advisory: NUM_REGIONS >= 1");
    if (WIN < MIN_SAMPLES)
      $fatal(1, "latency_advisory: WIN < MIN_SAMPLES -- no region can be non-stale");
  end

  always_ff @(posedge clk) begin
    if (!rst_n) begin
      for (int r = 0; r < NUM_REGIONS; r++) begin
        a_tot[r] <= '0;  a_n[r] <= '0;
        irr_sum[r] <= '0;  samples[r] <= '0;
      end
      // Clause 3's initialisation is CORRECT: everything starts
      // stale, so an unmeasured region is never published as
      // zero-cost. A reviewer checking "can an unmeasured region
      // attract pages?" finds that it cannot.
      advisory_stale <= '1;
      result_valid   <= 1'b0;
      acc_saturated  <= 1'b0;
    end else if (win_tick) begin
      for (int r = 0; r < NUM_REGIONS; r++) begin
        irr_sum[r] <= a_tot[r];
        samples[r] <= a_n[r];
        // Clause 3 is HONOURED per region as well.
        advisory_stale[r] <= (a_n[r] < MIN_SAMPLES[SMP_W-1:0]);
        a_tot[r] <= '0;  a_n[r] <= '0;
      end
      result_valid <= 1'b1;
    end else begin
      result_valid <= 1'b0;
      if (acc_done) begin
        // Clause 5 is HONOURED: overflow flags rather than wraps.
        if (a_tot[acc_region] > ({ACC_W{1'b1}} - acc_irreducible - acc_queueing))
          acc_saturated <= 1'b1;
        else
          // <-- THE DEFECT
          a_tot[acc_region] <= a_tot[acc_region] + acc_irreducible + acc_queueing;

        if (a_n[acc_region] != {SMP_W{1'b1}}) a_n[acc_region] <= a_n[acc_region] + 1'b1;
        else acc_saturated <= 1'b1;
      end
    end
  end
endmodule

   GRADE D, using §5's figures.

   region P, row-hit dominant, irreducible cost 20 units.
   The access pattern is HELD FIXED throughout.

     offered load LOW      : queueing =   2  ->  published 22
     offered load MEDIUM   : queueing =  40  ->  published 60
     offered load HIGH     : queueing = 200  ->  published 220

   DERIVED: the published cost varies by 10x while the access
   pattern -- the only thing clause 4 says it may depend on --
   does not change at all.

   so the policy's input is  dL_adv/dload > 0, which is exactly
   §6's loop gain. With the CORRECT export the same quantity is
   ZERO, and §7's third remedy is the only one that makes it so.

   DERIVED from the figures above.

     at low load : published 22 against a true 20 -- a 10% error,
                   and it is CONSTANT, so a test comparing two
                   regions gets the ratio nearly right:
                       P: 22, Q: 50  ->  ratio 2.27
                       true             ->  ratio 2.40
                   a 5% discrimination error. Nobody notices.

     and the LOOP GAIN at low load is nearly zero, because the
     queueing term barely responds to load when the queue is
     empty. So §6's oscillation DOES NOT OCCUR in a low-load test.

   the defect's magnitude and its loop gain BOTH scale with load,
   and a functional test runs at whatever load it needs to
   exercise its cases -- which is usually not saturation.

      // CORRECTED. Clauses 2 and 4: accumulate the two components
      // SEPARATELY and publish both. The irreducible sum then does
      // not move with load, so §6's loop gain is zero and §7's
      // delay stops mattering -- a loop with zero gain does not
      // oscillate at any delay.
      if (a_irr[acc_region] > ({ACC_W{1'b1}} - acc_irreducible))
        acc_saturated <= 1'b1;
      else
        a_irr[acc_region] <= a_irr[acc_region] + acc_irreducible;

      if (a_q[acc_region] > ({ACC_W{1'b1}} - acc_queueing))
        acc_saturated <= 1'b1;
      else
        a_q[acc_region] <= a_q[acc_region] + acc_queueing;

  // Offered as "proves the advisory is sound". All PASS on the
  // defective block.
  property p_unmeasured_region_is_stale;
    @(posedge clk) disable iff (!rst_n)
      (result_valid && samples[R] < MIN_SAMPLES) |-> advisory_stale[R];
  endproperty
  assert property (p_unmeasured_region_is_stale)
    else $error("a thin region was published as usable");

  property p_all_stale_after_reset;
    @(posedge clk) disable iff (!rst_n)
      $past(!rst_n) |-> (advisory_stale == '1);
  endproperty
  assert property (p_all_stale_after_reset)
    else $error("a region was usable before anything was measured");

  property p_overflow_flags_not_wraps;
    @(posedge clk) disable iff (!rst_n)
      (acc_done && (a_tot[acc_region] > LIMIT)) |=> acc_saturated;
  endproperty
  assert property (p_overflow_flags_not_wraps)
    else $error("an accumulator wrapped instead of flagging");

  property p_results_latched_cleanly;
    @(posedge clk) disable iff (!rst_n)
      (!win_tick) |=> $stable(irr_sum[R]);
  endproperty
  assert property (p_results_latched_cleanly)
    else $error("a published result changed outside a window tick");

  // Clause 4, and it names acc_queueing -- the signal the defective
  // block sums in and never publishes. Variety 2's repair, and it is
  // checkable within one run because the load-dependent term is
  // itself an input.
  property p_irreducible_excludes_queueing;
    @(posedge clk) disable iff (!rst_n)
      (acc_done && !win_tick) |=>
        (a_irr[$past(acc_region)] ==
           $past(a_irr[acc_region]) + $past(acc_irreducible));
  endproperty
  assert property (p_irreducible_excludes_queueing)
    else $error("the irreducible accumulator absorbed a queueing term");

  // Clause 2: the queueing term must be PUBLISHED, not discarded.
  // Stated separately because discarding it is a different defect
  // from blending it, and the correction to one can produce the
  // other.
  property p_queueing_is_published;
    @(posedge clk) disable iff (!rst_n)
      (result_valid && !advisory_stale[R]) |-> (queue_sum[R] != 'x);
  endproperty
  assert property (p_queueing_is_published)
    else $error("the queueing component was not published");

  // The SUM must reconstruct the total, which is 23.2 §9's
  // exhaustive-and-disjoint standard: the components sum exactly, so
  // a consumer wanting the total can compute it and a reviewer can
  // check the decomposition.
  property p_components_reconstruct_total;
    @(posedge clk) disable iff (!rst_n)
      result_valid |-> ((irr_sum[R] + queue_sum[R]) == total_observed[R]);
  endproperty
  assert property (p_components_reconstruct_total)
    else $error("the published components do not sum to the observed total");

  // And the property that encodes clause 4's LOAD-INDEPENDENCE
  // directly, as the invariant a control-loop consumer depends on.
  // It requires an environment signal for the offered load, which is
  // the point: the claim is about a relationship to load, so load
  // must appear.
  property p_irreducible_independent_of_load;
    @(posedge clk) disable iff (!rst_n)
      ($changed(offered_load) && $stable(pattern_id)) |=>
        $stable(irr_rate[R]);
  endproperty
  assert property (p_irreducible_independent_of_load)
    else $error("the irreducible rate moved with offered load");

  // ---- Covers. The dimension this defect scales with is OFFERED
  //      LOAD, and 31.3 §15's rule says the cover must be on that
  //      dimension.
  // The HIGH-LOAD regime: the only one in which the defect is
  // material. §15 shows a low-load test sees a 5% discrimination
  // error and no oscillation at all.
  cover property (@(posedge clk) disable iff (!rst_n)
                  result_valid && (queue_sum[R] > irr_sum[R]));
  // The LOW-LOAD regime, so both are known to have run.
  cover property (@(posedge clk) disable iff (!rst_n)
                  result_valid && (queue_sum[R] * 4 < irr_sum[R]));
  // A load CHANGE with the pattern held -- the antecedent of
  // p_irreducible_independent_of_load, and a stimulus most
  // environments do not generate because they vary both together.
  cover property (@(posedge clk) disable iff (!rst_n)
                  $changed(offered_load) && $stable(pattern_id));
  // A stale region and a usable one, so clause 3 is exercised in
  // both directions rather than only at reset.
  cover property (@(posedge clk) disable iff (!rst_n)
                  result_valid && advisory_stale[R]);
  cover property (@(posedge clk) disable iff (!rst_n)
                  result_valid && !advisory_stale[R]);

  // The property §15 says `irr_sum` finally deserves: the name
  // asserts load-independence, so the logic must provide it. A
  // signal whose name claims a property the logic does not give is
  // a documentation defect on top of a functional one.
  property p_irr_sum_earns_its_name;
    @(posedge clk) disable iff (!rst_n)
      (acc_done && !win_tick) |=>
        (a_irr[$past(acc_region)] ==
           $past(a_irr[acc_region]) + $past(acc_irreducible));
  endproperty
  assert property (p_irr_sum_earns_its_name)
    else $error("irr_sum accumulated something other than the irreducible term");

  // The two accumulators must be INDEPENDENT -- the same isolation
  // class 31.3 §15 named for channels, 32.3 §16 for credit pools, and
  // here for decomposition components. Vacuously true in a blended
  // design, so a design grown from one has never had it checked.
  property p_components_are_independent;
    @(posedge clk) disable iff (!rst_n)
      (acc_done && acc_queueing != '0 && acc_irreducible == '0) |=>
        $stable(a_irr[$past(acc_region)]);
  endproperty
  assert property (p_components_are_independent)
    else $error("a pure-queueing sample moved the irreducible accumulator");

  // Clause 3, both directions. A region must be stale when thin AND
  // usable when thick -- a one-sided property is satisfied by a
  // block that reports everything stale forever, which would be
  // safe and useless (30.3 §9's variety 8).
  property p_staleness_is_two_sided;
    @(posedge clk) disable iff (!rst_n)
      result_valid |-> (advisory_stale[R] == (samples[R] < MIN_SAMPLES));
  endproperty
  assert property (p_staleness_is_two_sided)
    else $error("staleness does not match the sample count");

  // A stale region's numbers must not be actionable. The strongest
  // available statement is that the consumer is TOLD -- and §11's
  // reset-to-all-ones is what makes the unmeasured case safe rather
  // than attractive (30.7 §9: unknown is not a default).
  property p_stale_regions_flagged_before_publication;
    @(posedge clk) disable iff (!rst_n)
      (result_valid && samples[R] == '0) |-> advisory_stale[R];
  endproperty
  assert property (p_stale_regions_flagged_before_publication)
    else $error("a region with zero samples was published as usable");

  // The PLATFORM invariant, parameter in the ANTECEDENT and not in
  // the claim -- 31.1 §14's test. It may be shared across both arms.
  property p_single_tier_publishes_nothing_usable;
    @(posedge clk) disable iff (!rst_n)
      (!TIERED) -> (advisory_stale == '1);
  endproperty
  assert property (p_single_tier_publishes_nothing_usable)
    else $error("a single-tier platform published a usable advisory");

  // Saturation must be reported, because an understated cost
  // ATTRACTS pages -- the direction matters, and 30.8 §11's range
  // rule with its consequence named.
  property p_saturation_reported;
    @(posedge clk) disable iff (!rst_n)
      acc_saturated |-> ##[0:1] (advisory_stale != '0);
  endproperty
  assert property (p_saturation_reported)
    else $error("an accumulator saturated and the advisory stayed usable");

  // ---- Covers: the platform arms and both staleness directions.
  cover property (@(posedge clk) disable iff (!rst_n) TIERED && result_valid);
  cover property (@(posedge clk) disable iff (!rst_n) !TIERED && result_valid);
  cover property (@(posedge clk) disable iff (!rst_n)
                  result_valid && (samples[R] >= MIN_SAMPLES));
  cover property (@(posedge clk) disable iff (!rst_n) acc_saturated);