“Training Happens Only Once”

   "TRAINING HAPPENS ONLY ONCE" HOLDS WHEN ALL FIVE HOLD:

     1  temperature CONSTANT          -> no drift in the eye
     2  supply voltage CONSTANT       -> no drift in the reference
     3  frequency CONSTANT            -> the trained set stays applicable
     4  no power-state transitions    -> nothing is powered down and back
     5  no warm reset                 -> nothing clears a trained register

   and then:  the boot-time values remain correct indefinitely, and
              the belief is exactly right

// ROBUST MODEL: every trained value carries a LIFETIME class, so
// "training" stops being one thing. 19.5 section 4's one-time versus
// continuous split, made a per-value property.
package value_lifetime_pkg;
  typedef enum int {
    L_ONE_TIME,      // valid until a reset clears it
    L_PERIODIC,      // re-established on an interval
    L_EVENT_DRIVEN,  // re-established on a named condition
    L_PER_FREQUENCY  // one set per operating point
  } lifetime_e;

  typedef struct {
    string     name;
    lifetime_e lifetime;
    bit        drifts_with_temp;
    bit        drifts_with_voltage;
    bit        period_dependent;
  } tv_t;

  // ILLUSTRATIVE assignment over the searches Module 21 builds plus the
  // calibrations 19.5 and 7.7 own.
  tv_t VALUES[] = '{
    '{"write_level_delay",  L_ONE_TIME,      1'b0, 1'b0, 1'b1},
    '{"gate_offset",        L_ONE_TIME,      1'b0, 1'b0, 1'b1},
    '{"read_level_delay",   L_PER_FREQUENCY, 1'b1, 1'b0, 1'b1},
    '{"vref_host",          L_PERIODIC,      1'b1, 1'b1, 1'b0},
    '{"vref_device",        L_PERIODIC,      1'b1, 1'b1, 1'b0},
    '{"zq_drive_strength",  L_PERIODIC,      1'b1, 1'b1, 1'b0},
    '{"dll_lock",           L_EVENT_DRIVEN,  1'b0, 1'b0, 1'b1},
    '{"flight_offset",      L_PER_FREQUENCY, 1'b1, 1'b0, 1'b1}
  };
endpackage

module value_lifetime_census #(
    parameter int NV = 8
)(
    input  logic       clk,
    input  logic       rst_n,
    input  logic       audit,
    output logic [3:0] one_time_count,
    output logic [3:0] revisited_count,
    output logic [3:0] temp_sensitive,
    output logic [3:0] period_dependent_count,
    output logic       all_one_time,
    output logic [7:0] revisited_share_pct
);
  import value_lifetime_pkg::*;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      one_time_count <= '0; revisited_count <= '0; temp_sensitive <= '0;
      period_dependent_count <= '0; all_one_time <= 1'b0;
      revisited_share_pct <= '0;
    end else if (audit) begin
      automatic int ot = 0, rv = 0, ts = 0, pd = 0;
      foreach (VALUES[i]) begin
        if (VALUES[i].lifetime == L_ONE_TIME) ot++; else rv++;
        if (VALUES[i].drifts_with_temp)       ts++;
        if (VALUES[i].period_dependent)       pd++;
      end
      one_time_count         <= 4'(ot);
      revisited_count        <= 4'(rv);
      temp_sensitive         <= 4'(ts);
      period_dependent_count <= 4'(pd);
      // The belief, as a predicate.
      all_one_time           <= (rv == 0);
      revisited_share_pct    <= 8'((rv * 100) / NV);
    end
  end
endmodule

// INTENTIONALLY DEFECTIVE. WEAK MODEL: one lifetime for all of them.
//
//   // "training" is a phase, so its outputs share its lifetime
//   localparam lifetime_e TRAINING_LIFETIME = L_ONE_TIME;
//   all_one_time    <= 1'b1;            // <-- the defect
//   revisited_count <= '0;
//
// CONTRACT VIOLATED: 19.5 section 4's split. And the weak model is right
// about two of the eight values -- write levelling and gate training
// really are one-time.
//
// TRACE (ILLUSTRATIVE, the eight values above):
//   robust: one_time 2, REVISITED 6, temp_sensitive 5,
//           period_dependent 5, all_one_time 0,
//           revisited_share 75%
//   weak:   one_time 8, revisited 0, all_one_time 1
//
//   gap: six of eight values need re-establishing and the belief plans
//   for none. And the split is not 50/50 in the belief's favour -- it
//   is 75% against, which is why a census dislodges the belief where a
//   sentence does not.
//
//   The five period-dependent values are the sharpest sub-finding:
//   they are not DRIFTING, they are ENCODED against a clock period, and
//   a DVFS transition invalidates all five at once with no physical
//   change whatsoever.

// ROBUST MODEL: validity is a function of the CONDITIONS the value was
// measured under, so it can fall without anything failing. 19.5
// section 2's "stop being correct while the system is running".
module validity_tracking #(
    parameter int TAP_W       = 6,
    parameter int TEMP_DELTA  = 10,   // ILLUSTRATIVE degrees before stale
    parameter int STALE_TICKS = 512   // ILLUSTRATIVE
)(
    input  logic             clk,
    input  logic             rst_n,
    input  logic             commit,
    input  logic [TAP_W-1:0] committed_tap,
    input  logic [7:0]       temp_now,
    input  logic             tick,
    input  logic             freq_changed,
    output logic [TAP_W-1:0] tap_in_use,
    output logic             valid,
    output logic             stale,
    output logic             inapplicable,
    output logic [7:0]       temp_at_commit,
    output logic [15:0]      age,
    output logic [15:0]      validity_falls,
    output logic [15:0]      used_while_invalid
);
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      tap_in_use <= '0; valid <= 1'b0; stale <= 1'b0;
      inapplicable <= 1'b0; temp_at_commit <= '0; age <= '0;
      validity_falls <= '0; used_while_invalid <= '0;
    end else begin
      if (commit) begin
        tap_in_use     <= committed_tap;
        valid          <= 1'b1;
        stale          <= 1'b0;
        inapplicable   <= 1'b0;
        // The provenance that makes validity computable later --
        // 28.4's "what a committed value was calibrated AGAINST".
        temp_at_commit <= temp_now;
        age            <= '0;
      end

      if (valid) begin
        // Drift: the condition moved away from the one measured at.
        automatic logic [7:0] d = (temp_now > temp_at_commit)
                                ? (temp_now - temp_at_commit)
                                : (temp_at_commit - temp_now);
        if (d >= 8'(TEMP_DELTA)) begin
          valid <= 1'b0; stale <= 1'b1;
          validity_falls <= validity_falls + 1'b1;
        end else if (tick && (age == 16'(STALE_TICKS))) begin
          valid <= 1'b0; stale <= 1'b1;
          validity_falls <= validity_falls + 1'b1;
        end else if (tick) begin
          age <= age + 1'b1;
        end

        // A frequency change makes it INAPPLICABLE, not stale: the
        // physical measurement is still right and its encoding is not.
        if (freq_changed) begin
          valid <= 1'b0; inapplicable <= 1'b1;
          validity_falls <= validity_falls + 1'b1;
        end
      end

      // The escape counter: a consumer using the value while it is
      // neither valid nor re-established.
      if (!valid && (tap_in_use != '0) && !stale && !inapplicable)
        used_while_invalid <= used_while_invalid + 1'b1;
    end
  end
endmodule

// INTENTIONALLY DEFECTIVE. WEAK MODEL: validity is monotonic.
//
//   if (commit) begin
//     tap_in_use <= committed_tap;
//     valid      <= 1'b1;          // and it never falls
//   end
//   // no temp_at_commit, no age, no freq_changed handling
//
// CONTRACT VIOLATED: 19.5 section 2 -- "some of those values stop being
// correct while the system is running" -- and 28.4 section 2's fifth case.
//
// WHY IT SURVIVES: it is correct for the whole of a bench session, and
// it is correct FOREVER for the two genuinely one-time values. A
// monotonic valid bit is also what a boot flow wants, because a boot
// flow asks "is it trained yet" and never asks "is it still".
//
// TRACE (ILLUSTRATIVE, a 90-minute run: 25C at boot, rising to 70C,
// one DVFS transition at minute 40):
//   robust: commit at boot, temp_at_commit 25
//           minute 18, temp 35: d = 10 -> valid 0, stale 1
//                               validity_falls 1, retrain
//           minute 40, freq change: valid 0, inapplicable 1
//                               validity_falls 2, retrain for the bin
//           minute 61, temp 60: d = 10 from the last commit -> stale
//                               validity_falls 3
//           total: 3 falls, 3 retrains, used_while_invalid 0
//   weak:   valid 1 from boot to the end. 0 falls, 0 retrains.
//           and the tap in use at minute 90 was measured at 25C
//           against a period that changed at minute 40.
//
//   gap: three invalidations in ninety minutes, none of them detected,
//   and the final operating point is a value measured under two
//   conditions that no longer hold.

// ROBUST MODEL: the trigger set is declared and audited against the
// exits, so a missing trigger is a finding rather than an absence.
module retrain_trigger_coverage #(
    parameter int NTRIG = 6
)(
    input  logic       clk,
    input  logic       rst_n,
    input  logic       audit,
    input  logic [5:0] triggers_implemented,  // one bit per exit
    // live events, to show which fire in practice
    input  logic [5:0] event_now,
    output logic [3:0] implemented_count,
    output logic [3:0] missing_count,
    output logic [5:0] missing_mask,
    output logic       coverage_complete,
    output logic [5:0] unhandled_events,
    output logic [15:0] unhandled_event_count
);
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      implemented_count <= '0; missing_count <= '0; missing_mask <= '0;
      coverage_complete <= 1'b0; unhandled_events <= '0;
      unhandled_event_count <= '0;
    end else begin
      if (audit) begin
        implemented_count <= 4'($countones(triggers_implemented));
        missing_count     <= 4'(NTRIG - $countones(triggers_implemented));
        missing_mask      <= ~triggers_implemented & 6'h3F;
        coverage_complete <= ($countones(triggers_implemented) == NTRIG);
      end
      // An event with no trigger is silently absorbed -- which is the
      // whole mechanism by which the belief survives in a running
      // system.
      unhandled_events <= event_now & ~triggers_implemented;
      if ((event_now & ~triggers_implemented) != '0)
        unhandled_event_count <= unhandled_event_count
                               + 16'($countones(event_now & ~triggers_implemented));
    end
  end
endmodule

   TRIGGER COVERAGE IN A TYPICAL DESIGN   (ILLUSTRATIVE)

     exit                       implemented?   events in 90 min
     1 temperature threshold        no                2
     2 voltage movement             no                0
     3 frequency change             no                1
     4 power-down exit             YES                7
     5 warm reset                  YES                1
     6 periodic interval            no               10

   robust: implemented 2 of 6, missing 4,
           missing_mask names temp, voltage, frequency, periodic
           unhandled_event_count 13
   weak:   coverage_complete reported on a 2-trigger set, because the
           set the design has is the set it declared

   DERIVED: 13 events in 90 minutes were absorbed with no retraining.
   And the two triggers that ARE implemented are the two that are
   impossible to miss -- a power-down exit and a reset both have an
   obvious hook, while a temperature threshold needs somebody to
   decide to watch a sensor.

// ROBUST MODEL: one trained set PER operating point, because a count in
// cycles is meaningless at another period -- 19.3 section 2's decomposition.
module per_frequency_set #(
    parameter int NBIN  = 3,
    parameter int TAP_W = 6
)(
    input  logic             clk,
    input  logic             rst_n,
    input  logic [1:0]       bin_now,
    input  logic             commit,
    input  logic [TAP_W-1:0] committed_tap,
    input  logic [15:0]      period_x100,     // ILLUSTRATIVE ps x100
    output logic [TAP_W-1:0] tap_in_use,
    output logic             set_valid,
    output logic [2:0]       bins_trained,
    output logic             needs_training,
    output logic [15:0]      wrong_bin_uses,
    output logic [TAP_W-1:0] would_be_tap     // the correct tap here
);
  logic [TAP_W-1:0] tap_of  [0:NBIN-1];
  logic             val_of  [0:NBIN-1];
  logic [15:0]      per_of  [0:NBIN-1];

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      tap_in_use <= '0; set_valid <= 1'b0; bins_trained <= '0;
      needs_training <= 1'b1; wrong_bin_uses <= '0; would_be_tap <= '0;
      for (int b = 0; b < NBIN; b++) begin
        tap_of[b] <= '0; val_of[b] <= 1'b0; per_of[b] <= '0;
      end
    end else begin
      if (commit) begin
        tap_of[bin_now] <= committed_tap;
        val_of[bin_now] <= 1'b1;
        per_of[bin_now] <= period_x100;
      end

      // Selection is indexed by the CURRENT bin. A design with one set
      // has no index, which is the defect.
      tap_in_use     <= tap_of[bin_now];
      set_valid      <= val_of[bin_now];
      needs_training <= !val_of[bin_now];
      bins_trained   <= 3'($countones({val_of[2], val_of[1], val_of[0]}));

      // The physical time is invariant; the COUNT is not. If a tap
      // trained at another period were used here, this is what it
      // would have to be -- and the difference is the error.
      if (val_of[bin_now] && (per_of[bin_now] != '0))
        would_be_tap <= TAP_W'((32'(tap_of[bin_now])
                                * 32'(per_of[bin_now])) / 32'(period_x100));
    end
  end
endmodule

// INTENTIONALLY DEFECTIVE. WEAK MODEL: one set, no index.
//
//   logic [TAP_W-1:0] the_tap;        // <-- one value for all bins
//   if (commit) the_tap <= committed_tap;
//   tap_in_use <= the_tap;
//   set_valid  <= trained_once;
//
// CONTRACT VIOLATED: 19.3 section 2 -- the measured term is a physical time
// and the applied value is a count, so the conversion is
// period-dependent.
//
// WHY IT SURVIVES: on a system that never changes frequency it is
// identical to the robust build, and that includes every bench setup
// and most first bring-ups. DVFS is usually enabled late.
//
// TRACE (ILLUSTRATIVE, flight time 2.8 ns; three bins):
//   bin 0  1.25 ns/cycle  ->  correct tap 2   (2.24 rounded)
//   bin 1  0.833 ns/cycle ->  correct tap 3   (3.36 rounded)
//   bin 2  0.625 ns/cycle ->  correct tap 4   (4.48 rounded)
//
//   robust: trained in bin 0 -> bins_trained 1; entering bin 2 sets
//           needs_training 1 and the search runs. bins_trained 2.
//           wrong_bin_uses 0.
//   weak:   trained in bin 0 -> the_tap 2. Entering bin 2, tap_in_use
//           is still 2 where 4 is correct: an error of 2 taps, which
//           at 0.625 ns/cycle is 1.25 ns of misalignment.
//           set_valid stays 1 and nothing reports anything.
//
//   gap: a 2-tap error at the highest bin, silent, and it appears only
//   after DVFS is enabled -- typically weeks after the PHY was
//   declared working.

// ROBUST MODEL: the measured physical quantity is stored, and the
// applied count is derived from it at the current period. A frequency
// change costs a division; only drift costs a search.
module reconversion_vs_research #(
    parameter int TAP_W   = 6,
    parameter int PS_W    = 16,
    parameter int SEARCH_CYCLES = 4096   // ILLUSTRATIVE cost of a search
)(
    input  logic             clk,
    input  logic             rst_n,
    input  logic             search_done,
    input  logic [PS_W-1:0]  measured_ps,      // the PHYSICAL quantity
    input  logic [PS_W-1:0]  period_ps,        // current, changes on DVFS
    input  logic             freq_changed,
    input  logic             drift_detected,
    output logic [TAP_W-1:0] tap_in_use,
    output logic             have_measurement,
    output logic             search_requested,
    output logic [15:0]      searches_run,
    output logic [15:0]      reconversions,
    output logic [31:0]      cycles_spent_searching
);
  logic [PS_W-1:0] held_ps;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      held_ps <= '0; tap_in_use <= '0; have_measurement <= 1'b0;
      search_requested <= 1'b1; searches_run <= '0;
      reconversions <= '0; cycles_spent_searching <= '0;
    end else begin
      search_requested <= 1'b0;

      if (search_done) begin
        // Store the PHYSICAL quantity, not the count. This one choice
        // is the difference between the two builds.
        held_ps          <= measured_ps;
        have_measurement <= 1'b1;
        searches_run     <= searches_run + 1'b1;
        cycles_spent_searching <= cycles_spent_searching
                                + 32'(SEARCH_CYCLES);
      end

      // A frequency change: re-derive the count. No search, no traffic
      // interruption, a handful of cycles.
      if (freq_changed && have_measurement) begin
        reconversions <= reconversions + 1'b1;
      end

      // Drift: the MEASUREMENT is wrong, so a search is unavoidable.
      if (drift_detected) begin
        have_measurement <= 1'b0;
        search_requested <= 1'b1;
      end

      // The applied count, always derived at the current period.
      if (have_measurement && (period_ps != '0))
        tap_in_use <= TAP_W'((32'(held_ps) + 32'(period_ps) - 32'd1)
                             / 32'(period_ps));
    end
  end
endmodule

// INTENTIONALLY DEFECTIVE, TWO WAYS. The correction invites an
// over-reaction, so both errors are shown.
//
// WEAK BUILD A -- store the COUNT, ignore the period:
//   if (search_done) held_tap <= measured_tap;   // a count, not a time
//   tap_in_use <= held_tap;                      // applied at any period
//   -> section 11's defect: the wrong count at the new bin, silently.
//
// WEAK BUILD B -- re-search on every frequency change:
//   if (freq_changed) search_requested <= 1'b1;  // <-- over-reaction
//   -> correct values, and a full search at every DVFS transition.
//
// CONTRACT VIOLATED: 19.3 section 2's decomposition, in both directions --
// A treats the measured term as period-independent, B treats the
// configuration term as unmeasurable.
//
// WHY B SURVIVES REVIEW: it is CORRECT. Every applied value is right,
// every property about validity passes, and the only cost is time --
// 30.3 section 9's variety 8 again, in a PHY flow rather than a timing
// comparison.
//
// TRACE (ILLUSTRATIVE, 40 DVFS transitions and 3 drift events in an
// hour; SEARCH_CYCLES 4096):
//   robust:   searches_run 4 (1 boot + 3 drift), reconversions 40,
//             cycles_spent_searching 16,384
//   weak A:   searches_run 4, reconversions 0,
//             and 40 transitions applied a count from another period
//   weak B:   searches_run 44, reconversions 0,
//             cycles_spent_searching 180,224 -- 11x the robust build
//
//   gap: A is wrong 40 times; B is right and spends 164,000 extra
//   cycles of interrupted traffic. DERIVED: the belief's correction
//   has two failure modes and only one of them is a correctness bug.

// ROBUST MODEL: recalibration as a schedulable obligation with the
// three requirements enforced -- the same shape 17.3 uses for refresh,
// as 19.5 section 4 says.
module recal_scheduling #(
    parameter int MAX_PASS_CYCLES = 64,    // ILLUSTRATIVE "brief"
    parameter int INTERVAL        = 4096,  // ILLUSTRATIVE
    parameter int MAX_DEFER       = 4      // ILLUSTRATIVE headroom
)(
    input  logic             clk,
    input  logic             rst_n,
    input  logic             tick,
    input  logic             inflight_txn,
    input  logic             bus_idle,
    input  logic             pass_done,
    output logic             pass_start,
    output logic             pass_active,
    output logic signed [7:0] recal_debt,
    output logic [15:0]      pass_cycles,
    output logic             brief_ok,
    output logic             noncorrupting_ok,
    output logic             schedulable_ok,
    output logic [15:0]      deferrals,
    output logic [15:0]      corrupted_txns
);
  logic [15:0] ivl;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      ivl <= '0; recal_debt <= '0; pass_start <= 1'b0;
      pass_active <= 1'b0; pass_cycles <= '0;
      brief_ok <= 1'b1; noncorrupting_ok <= 1'b1; schedulable_ok <= 1'b1;
      deferrals <= '0; corrupted_txns <= '0;
    end else begin
      pass_start <= 1'b0;

      if (tick) begin
        if (ivl == INTERVAL[15:0]) begin
          ivl        <= '0;
          recal_debt <= recal_debt + 8'sd1;
        end else begin
          ivl <= ivl + 1'b1;
        end
      end

      // REQUIREMENT 3, schedulable: the pass waits for a window, and
      // the wait is bounded so it cannot be deferred forever.
      if ((recal_debt > 8'sd0) && !pass_active) begin
        if (bus_idle && !inflight_txn) begin
          pass_start  <= 1'b1;
          pass_active <= 1'b1;
          pass_cycles <= '0;
        end else if (recal_debt >= 8'sd(MAX_DEFER)) begin
          // At the bound it goes regardless -- 17.3's
          // illegal-versus-deprioritised line, reused.
          pass_start  <= 1'b1;
          pass_active <= 1'b1;
          pass_cycles <= '0;
          // REQUIREMENT 2: starting with a transaction in flight is
          // the corruption case, counted rather than assumed away.
          if (inflight_txn) corrupted_txns <= corrupted_txns + 1'b1;
        end else if (tick) begin
          deferrals <= deferrals + 1'b1;
        end
      end

      if (pass_active) begin
        pass_cycles <= pass_cycles + 1'b1;
        // REQUIREMENT 1, brief: a pass that overruns is a finding.
        if (pass_cycles > 16'(MAX_PASS_CYCLES)) brief_ok <= 1'b0;
        if (pass_done) begin
          pass_active <= 1'b0;
          recal_debt  <= recal_debt - 8'sd1;
        end
      end

      noncorrupting_ok <= (corrupted_txns == '0);
      schedulable_ok   <= (recal_debt <= 8'sd(MAX_DEFER));
    end
  end
endmodule

   THE THREE REQUIREMENTS, MEASURED   (ILLUSTRATIVE, one hour,
                                       INTERVAL 4096, 14 passes due)

     design                  brief  non-corrupting  schedulable
     ------------------------------------------------------------
     no recalibration          --         --             --
       (the belief: nothing to schedule; 0 of 3 met)
     recalibrate immediately   yes        NO             yes
       (corrupted_txns 9 of 14 -- it starts mid-transaction)
     recalibrate when idle     yes        yes            NO
       (deferrals unbounded; on a busy hour, 0 of 14 passes ran)
     robust: idle, with a bound yes       yes            yes
       (11 passes at idle, 3 forced at the bound, 1 corrupted)

   DERIVED: the middle two designs each satisfy two requirements and
   fail one, and they are the two an engineer writes first. Only the
   bounded-deferral form satisfies all three, and it is exactly
   17.3's refresh structure.

  // ---- Section 8: the census. The belief is a predicate, and it is false.
  property p_not_all_values_are_one_time;
    @(posedge clk) disable iff (!rst_n)
      audit |=> !all_one_time;
  endproperty
  assert property (p_not_all_values_are_one_time)
    else $error("the census reports every trained value as one-time");

  property p_census_partitions_the_values;
    @(posedge clk) disable iff (!rst_n)
      audit |=> ((one_time_count + revisited_count) == 4'(NV));
  endproperty
  assert property (p_census_partitions_the_values)
    else $error("the lifetime classes do not partition the trained values");

  // ---- Section 9: validity must be able to FALL -- 19.5 section 2.
  property p_validity_falls_on_drift;
    @(posedge clk) disable iff (!rst_n)
      (valid && (temp_now > (temp_at_commit + 8'(TEMP_DELTA)))) |=> !valid;
  endproperty
  assert property (p_validity_falls_on_drift)
    else $error("a trained value stayed valid past its drift threshold");

  property p_frequency_change_makes_inapplicable;
    @(posedge clk) disable iff (!rst_n)
      (valid && freq_changed) |=> (inapplicable && !valid);
  endproperty
  assert property (p_frequency_change_makes_inapplicable)
    else $error("a frequency change left the value valid");

  // Stale and inapplicable are DIFFERENT states -- section 7's distinction.
  property p_stale_and_inapplicable_are_exclusive;
    @(posedge clk) disable iff (!rst_n) !(stale && inapplicable);
  endproperty
  assert property (p_stale_and_inapplicable_are_exclusive)
    else $error("a value was reported both stale and inapplicable");

  property p_never_used_while_invalid;
    @(posedge clk) disable iff (!rst_n) used_while_invalid == '0;
  endproperty
  assert property (p_never_used_while_invalid)
    else $error("a consumer used a value that was neither valid nor re-established");

  // Two-sided -- 30.3 section 9's variety 8: a design that invalidates
  // every cycle satisfies every property above and never operates.
  property p_validity_survives_within_threshold;
    @(posedge clk) disable iff (!rst_n)
      (commit && (temp_now == temp_at_commit)) |=> valid;
  endproperty
  assert property (p_validity_survives_within_threshold)
    else $error("a freshly committed value was invalidated at its own temperature");

  // ---- Section 10: the trigger set, against section 6's six exits.
  property p_trigger_coverage_is_complete;
    @(posedge clk) disable iff (!rst_n)
      (audit && coverage_complete) |=> (implemented_count == 4'(NTRIG));
  endproperty
  assert property (p_trigger_coverage_is_complete)
    else $error("trigger coverage was called complete with an exit unhandled");

  property p_no_event_is_absorbed;
    @(posedge clk) disable iff (!rst_n) unhandled_events == '0;
  endproperty
  assert property (p_no_event_is_absorbed)
    else $error("an invalidating event occurred with no retraining trigger");

  property p_missing_mask_matches_the_count;
    @(posedge clk) disable iff (!rst_n)
      audit |=> (missing_count == 4'($countones(missing_mask)));
  endproperty
  assert property (p_missing_mask_matches_the_count)
    else $error("the missing trigger count disagrees with the mask");

  // ---- Section 11: per-frequency sets.
  property p_set_is_indexed_by_bin;
    @(posedge clk) disable iff (!rst_n)
      set_valid |-> (tap_in_use == tap_of[bin_now]);
  endproperty
  assert property (p_set_is_indexed_by_bin)
    else $error("the applied tap did not come from the current bin's set");

  property p_untrained_bin_requests_training;
    @(posedge clk) disable iff (!rst_n)
      (!val_of[bin_now]) |=> needs_training;
  endproperty
  assert property (p_untrained_bin_requests_training)
    else $error("an untrained operating point did not request training");

  property p_no_wrong_bin_use;
    @(posedge clk) disable iff (!rst_n) wrong_bin_uses == '0;
  endproperty
  assert property (p_no_wrong_bin_use)
    else $error("a tap trained at another period was applied");

  // ---- Section 12: re-conversion. The measured term is stored in
  // physical units, so the count follows the period -- 19.3 section 2.
  property p_tap_tracks_the_period;
    @(posedge clk) disable iff (!rst_n)
      (have_measurement && (period_ps != '0))
        |=> (tap_in_use == TAP_W'((32'($past(held_ps))
                                   + 32'($past(period_ps)) - 32'd1)
                                  / 32'($past(period_ps))));
  endproperty
  assert property (p_tap_tracks_the_period)
    else $error("the applied tap did not follow the current period");

  property p_frequency_change_needs_no_search;
    @(posedge clk) disable iff (!rst_n)
      (freq_changed && have_measurement) |=> !search_requested;
  endproperty
  assert property (p_frequency_change_needs_no_search)
    else $error("a frequency change triggered a full search");

  property p_drift_does_need_a_search;
    @(posedge clk) disable iff (!rst_n)
      drift_detected |=> search_requested;
  endproperty
  assert property (p_drift_does_need_a_search)
    else $error("drift did not request a new search");

  // ---- Section 13: the three requirements -- 19.5 section 4.
  property p_pass_is_brief;
    @(posedge clk) disable iff (!rst_n) brief_ok;
  endproperty
  assert property (p_pass_is_brief)
    else $error("a recalibration pass exceeded its brevity budget");

  property p_pass_does_not_corrupt;
    @(posedge clk) disable iff (!rst_n)
      pass_start |-> (!inflight_txn || (recal_debt >= 8'sd(MAX_DEFER)));
  endproperty
  assert property (p_pass_does_not_corrupt)
    else $error("a pass started mid-transaction with headroom remaining");

  property p_pass_is_schedulable;
    @(posedge clk) disable iff (!rst_n) schedulable_ok;
  endproperty
  assert property (p_pass_is_schedulable)
    else $error("recalibration debt exceeded its deferral bound");

  // And the two-sided partner: it must actually RUN, not merely defer.
  property p_pass_runs_at_idle;
    @(posedge clk) disable iff (!rst_n)
      ((recal_debt > 8'sd0) && bus_idle && !inflight_txn && !pass_active)
        |=> pass_start;
  endproperty
  assert property (p_pass_runs_at_idle)
    else $error("a due pass did not start in an idle window");

  // ---- The CLAIM, as a conditional pair -- 34.1 section 1's required form.
  property p_claim_holds_in_its_region;
    @(posedge clk) disable iff (!rst_n)
      (valid && (temp_now == temp_at_commit) && !freq_changed && !tick)
        |=> valid;
  endproperty
  assert property (p_claim_holds_in_its_region)
    else $error("with every condition constant the value still went invalid");

  property p_claim_fails_outside_its_region;
    @(posedge clk) disable iff (!rst_n)
      (valid && freq_changed) |=> (validity_falls > $past(validity_falls));
  endproperty
  assert property (p_claim_fails_outside_its_region)
    else $error("a frequency change did not invalidate anything");

  // ---- COVERS. Each on the dimension the belief's failure scales with.
  // The REGION: conditions constant, so the claim pair is not vacuous.
  cover property (@(posedge clk) disable iff (!rst_n)
                  valid && (temp_now == temp_at_commit) && !freq_changed);
  // A TEMPERATURE excursion past the threshold. The dimension is the
  // ENVIRONMENT, and a bench at 25C never reaches it.
  cover property (@(posedge clk) disable iff (!rst_n)
                  valid && (temp_now > (temp_at_commit + 8'(TEMP_DELTA))));
  // A FREQUENCY change -- the dimension is the operating point, and a
  // single-bin system never reaches it however long it runs.
  cover property (@(posedge clk) disable iff (!rst_n) valid && freq_changed);
  // Validity actually FALLING, so the properties about falling are not
  // vacuous in a design where it never does.
  cover property (@(posedge clk) disable iff (!rst_n) validity_falls > 16'd0);
  // Both post-valid states, separately.
  cover property (@(posedge clk) disable iff (!rst_n) stale);
  cover property (@(posedge clk) disable iff (!rst_n) inapplicable);
  // Section 10: an event with NO trigger -- the absorption mechanism.
  cover property (@(posedge clk) disable iff (!rst_n) unhandled_events != '0);
  // And complete coverage, so p_trigger_coverage_is_complete has a
  // witness rather than being satisfied by never completing.
  cover property (@(posedge clk) disable iff (!rst_n)
                  audit && coverage_complete);
  // Section 11: a SECOND bin trained -- which requires a DVFS transition
  // to occur at all.
  cover property (@(posedge clk) disable iff (!rst_n) bins_trained >= 3'd2);
  // And an untrained bin entered, so the request path is exercised.
  cover property (@(posedge clk) disable iff (!rst_n)
                  needs_training && !set_valid);
  // A census reporting a REVISITED majority -- section 8's 75%.
  cover property (@(posedge clk) disable iff (!rst_n)
                  audit && (revisited_share_pct > 8'd50));
  // Section 12: a RE-CONVERSION without a search -- the cheap path, which
  // a design storing a tap index can never take.
  cover property (@(posedge clk) disable iff (!rst_n)
                  freq_changed && have_measurement && !search_requested);
  // And a search caused by DRIFT, so the two causes are separated.
  cover property (@(posedge clk) disable iff (!rst_n)
                  drift_detected && search_requested);
  // Section 13: a pass FORCED at the deferral bound -- the case the
  // idle-only design never reaches and the belief has no pass for.
  cover property (@(posedge clk) disable iff (!rst_n)
                  pass_start && (recal_debt >= 8'sd(MAX_DEFER)));
  // And a pass starting in a genuine idle window.
  cover property (@(posedge clk) disable iff (!rst_n)
                  pass_start && bus_idle && !inflight_txn);