Calibration Failures

   validity is not a flag you set. It is a comparison you can run.

     valid  ==  (committed_tag == current_conditions)

   a design that stores `valid` as a latched bit is asserting that
   nothing has changed since the commit -- which is exactly the
   assumption that fails. A design that stores the TAG can answer
   the question at any moment, including after a change nobody
   thought to hook up an invalidation for.

   the practical difference: an invalidation you forgot to wire
   leaves a latched bit set and a tag comparison FALSE.

   committed code over eight recalibration passes, ILLUSTRATIVE

   tracking (healthy)        drifting (a finding)
   ------------------        --------------------
   41 42 41 42 43 42 41 42   41 42 44 46 49 51 54 56
   ^ oscillates about 42      ^ monotone, +15 over 8 passes

   both are "calibration succeeded" on every pass. Both commit a
   value, read back clean, and keep a matching tag. The first is a
   loop doing its job; the second is a loop whose feedback is wrong,
   or which is tracking something genuinely moving.

   §12's code_min/code_max bound the spread but do NOT separate these
   two: both have a spread of 15 if you only keep extremes. What
   separates them is MONOTONICITY, which needs the direction of the
   last few steps.

// ---------------------------------------------------------------------
// unverifiable_cal_obligations -- CLASSIFICATION: synthesisable, BINDABLE.
//
// WHAT IT DOES: §10's three checkable statements for a calibration
// whose RESULT cannot be read -- precondition at issue, occupancy
// respected, cadence maintained.
//
// WHY IT CHECKS OBLIGATIONS AND NOT THE RESULT: 7.7 owns the
// unverifiability of ZQ's result. Treating the absence of an error as
// evidence of success would be 27.2 §2's vacuity argument in its
// purest form -- a check that cannot fail. So this block asserts
// nothing about the outcome and everything about the contract.
//
// WHAT IT CANNOT TELL YOU: whether the calibration did anything. Every
// check here passes on a device that silently ignored the command.
//
// SYNTHESIS: three counters and a down-counter. No DUT handle.
// ---------------------------------------------------------------------
module unverifiable_cal_obligations #(
  parameter int OCCUPANCY = 64,     // cycles the command occupies, ILLUSTRATIVE
  parameter int CADENCE   = 4096,   // required maximum interval between issues
  parameter int CAD_W     = 24
)(
  input  logic              clk,
  input  logic              rst_n,
  input  logic              cmd_issue,      // the unverifiable command
  input  logic              precond_met,    // 7.7's precondition
  input  logic              traffic_valid,  // any other bus activity
  input  logic              clear,

  output logic              busy,
  output logic [15:0]       issues,
  output logic [15:0]       precond_violations,
  output logic [15:0]       occupancy_violations,
  output logic [15:0]       cadence_misses,
  output logic [CAD_W-1:0]  since_issue,
  output logic              ever_issued
);
  initial begin
    if (OCCUPANCY < 1) $fatal(1, "unverifiable_cal_obligations: OCCUPANCY must be >= 1");
    if (CADENCE   < 2) $fatal(1, "unverifiable_cal_obligations: CADENCE must be >= 2");
    // The interval counter must represent CADENCE, so it needs
    // $clog2(CADENCE+1) bits -- COUNT versus INDEX. Checking it here
    // rather than silently saturating below the deadline.
    if (CAD_W < $clog2(CADENCE + 1))
      $fatal(1, "unverifiable_cal_obligations: CAD_W too narrow for CADENCE");
  end

  localparam int OCC_W = (OCCUPANCY + 1 < 2) ? 1 : $clog2(OCCUPANCY + 1);
  logic [OCC_W-1:0] occ_left;

  always_ff @(posedge clk) begin
    if (!rst_n || clear) begin
      occ_left             <= '0;
      issues               <= '0;
      precond_violations   <= '0;
      occupancy_violations <= '0;
      cadence_misses       <= '0;
      since_issue          <= '0;
      ever_issued          <= 1'b0;
    end else begin
      if (cmd_issue) begin
        if (issues != 16'hFFFF) issues <= issues + 1'b1;
        ever_issued <= 1'b1;
        occ_left    <= OCCUPANCY[OCC_W-1:0];
        since_issue <= '0;
        // Obligation 1: the precondition must hold AT ISSUE. A command
        // issued without it is a definite defect even though its
        // result is unobservable.
        if (!precond_met && precond_violations != 16'hFFFF)
          precond_violations <= precond_violations + 1'b1;
      end else begin
        if (occ_left != '0) occ_left <= occ_left - 1'b1;
        // Saturate rather than wrap: a wrapped interval would compute a
        // small gap from a long silence and hide a cadence miss.
        if (since_issue != {CAD_W{1'b1}}) since_issue <= since_issue + 1'b1;
      end

      // Obligation 2: no other activity during the occupancy window.
      if (occ_left != '0 && traffic_valid && occupancy_violations != 16'hFFFF)
        occupancy_violations <= occupancy_violations + 1'b1;

      // Obligation 3: the cadence. Counted once per crossing, not once
      // per cycle beyond it, so one long silence is one miss.
      if (ever_issued && since_issue == CADENCE[CAD_W-1:0]
          && cadence_misses != 16'hFFFF)
        cadence_misses <= cadence_misses + 1'b1;
    end
  end

  assign busy = (occ_left != '0);
endmodule

// ---------------------------------------------------------------------
// calib_lifecycle_monitor -- CLASSIFICATION: synthesisable, BINDABLE.
//
// WHAT IT DOES: publishes §1's four facts separately -- started,
// converged, committed, valid -- because one `done` flag makes five
// different failures indistinguishable.
//
// WHY VALID IS A COMPARISON, NOT A LATCH (§5): a latched valid bit
// asserts that nothing has changed since the commit, which is exactly
// the assumption staleness violates. Comparing a stored PROVENANCE TAG
// against the live conditions answers the question at any moment --
// including after a change nobody wired an invalidation for. A missed
// invalidation leaves a latched bit set; a tag comparison still
// returns false.
//
// WHY started IS A COUNT (§2, §7): "did it run" and "how many times"
// are different questions, and the retry investigation needs the
// second. A routine whose `done` is implemented as !busy reads done
// from the first cycle after reset, and start_count == 0 is the only
// evidence that distinguishes that from a real success.
//
// WHY THE READBACK (§3): a computed value and an applied value are
// different things, and five plumbing failures live between them.
//
// WHAT IT CANNOT TELL YOU: whether the value has margin (§11).
//
// SYNTHESIS: counters, a tag register, one comparator. No DUT handle.
// ---------------------------------------------------------------------
module calib_lifecycle_monitor #(
  parameter int CODE_W = 8,
  parameter int TAG_W  = 16,   // packed conditions the result depends on
  parameter int LANES  = 8
)(
  input  logic                     clk,
  input  logic                     rst_n,

  // ---- routine interface (observed only)
  input  logic                     precond_met,
  input  logic                     start,
  input  logic                     probing,
  input  logic                     converged,
  input  logic                     commit,
  input  logic [CODE_W-1:0]        computed_code,
  input  logic [CODE_W-1:0]        applied_code,   // read back from the datapath
  input  logic [$clog2(LANES)-1:0] lane,
  input  logic                     timeout,

  // ---- §5: the conditions the result depends on, packed by the caller
  input  logic [TAG_W-1:0]         conditions_now,

  input  logic                     clear,

  // ---- published evidence: four SEPARATE facts
  output logic [15:0]              start_count,
  output logic [15:0]              converge_count,
  output logic [15:0]              commit_count,
  output logic [15:0]              timeout_count,
  output logic                     ever_started,
  output logic                     have_result,
  output logic [CODE_W-1:0]        committed_code,
  output logic [TAG_W-1:0]         committed_tag,
  output logic                     valid,
  output logic                     readback_mismatch,
  output logic [CODE_W-1:0]        mismatch_computed,
  output logic [CODE_W-1:0]        mismatch_applied,
  output logic [$clog2(LANES)-1:0] mismatch_lane,
  output logic [15:0]              stale_events,
  output logic [CODE_W-1:0]        code_min,
  output logic [CODE_W-1:0]        code_max
);
  // $clog2(1) is 0, making the lane vector illegal as [-1:0].
  initial begin
    if (LANES  < 2) $fatal(1, "calib_lifecycle_monitor: LANES must be >= 2 (got %0d)", LANES);
    if (CODE_W < 1) $fatal(1, "calib_lifecycle_monitor: CODE_W must be >= 1");
    if (TAG_W  < 1) $fatal(1, "calib_lifecycle_monitor: TAG_W must be >= 1");
  end

  logic valid_q;

  always_ff @(posedge clk) begin
    if (!rst_n || clear) begin
      start_count       <= '0;
      converge_count    <= '0;
      commit_count      <= '0;
      timeout_count     <= '0;
      ever_started      <= 1'b0;
      have_result       <= 1'b0;
      committed_code    <= '0;
      committed_tag     <= '0;
      readback_mismatch <= 1'b0;
      mismatch_computed <= '0;
      mismatch_applied  <= '0;
      mismatch_lane     <= '0;
      stale_events      <= '0;
      code_min          <= {CODE_W{1'b1}};
      code_max          <= '0;
      valid_q           <= 1'b0;
    end else begin
      // §2: a count, not a flag. Saturating -- a wrapped start count
      // reading 0 would reproduce the exact failure it detects.
      if (start) begin
        ever_started <= 1'b1;
        if (start_count != 16'hFFFF) start_count <= start_count + 1'b1;
      end
      if (converged && converge_count != 16'hFFFF) converge_count <= converge_count + 1'b1;
      if (timeout   && timeout_count  != 16'hFFFF) timeout_count  <= timeout_count  + 1'b1;

      if (commit) begin
        if (commit_count != 16'hFFFF) commit_count <= commit_count + 1'b1;
        committed_code <= computed_code;
        // §5: capture the conditions the value was calibrated AGAINST.
        // This is what makes validity computable later.
        committed_tag  <= conditions_now;
        have_result    <= 1'b1;

        // §7 row three: the spread of committed values across boots is
        // the honest proxy for how close the decision is -- in CODE
        // STEPS, which 21.4 is explicit are not volts.
        if (computed_code < code_min) code_min <= computed_code;
        if (computed_code > code_max) code_max <= computed_code;

        // §3: the readback test. Latched first-wins: a later matching
        // commit must not erase the evidence of an earlier mismatch.
        if (!readback_mismatch && (applied_code !== computed_code)) begin
          readback_mismatch <= 1'b1;
          mismatch_computed <= computed_code;
          mismatch_applied  <= applied_code;
          mismatch_lane     <= lane;
        end
      end

      // §5: count the transitions of validity from true to false, so a
      // staleness event is a recorded fact rather than a momentary
      // level nobody sampled.
      valid_q <= valid;
      if (valid_q && !valid && stale_events != 16'hFFFF)
        stale_events <= stale_events + 1'b1;
    end
  end

  // §5's central decision: validity is a COMPARISON, evaluated now.
  // A result is valid when one exists, its commit was clean, and the
  // conditions it was calibrated against still hold.
  always_comb begin
    valid = have_result && !readback_mismatch
         && (committed_tag == conditions_now);
  end
endmodule

// Bound to §12's monitor. Every property carries `disable iff`, and
// every antecedent is covered below -- 27.2 measured this curriculum
// at 78.53% implications, so a silent pass is otherwise
// indistinguishable from an unbound block.
module calib_lifecycle_sva #(
  parameter int CODE_W = 8, parameter int TAG_W = 16
)(
  input logic clk, rst_n, clear,
  input logic precond_met, start, probing, converged, commit, timeout,
  input logic [CODE_W-1:0] computed_code, applied_code, committed_code,
  input logic [TAG_W-1:0]  conditions_now, committed_tag,
  input logic valid, have_result, ever_started, readback_mismatch,
  input logic [15:0] start_count, converge_count, commit_count, stale_events
);
  // ---- P1. FORBIDDEN. Validity is never asserted without a result.
  // §2: a routine that never ran must not read as usable.
  property p_no_valid_without_result;
    @(posedge clk) disable iff (!rst_n)
      valid |-> have_result;
  endproperty
  assert property (p_no_valid_without_result)
    else $error("calib: valid asserted with no committed result");

  // ---- P2. FORBIDDEN. Validity is never asserted when the conditions
  // differ from the ones the value was calibrated against. §5 -- this
  // is the staleness contract, and it holds WITHOUT any invalidation
  // signal having been wired.
  property p_valid_implies_tag_match;
    @(posedge clk) disable iff (!rst_n)
      valid |-> (committed_tag == conditions_now);
  endproperty
  assert property (p_valid_implies_tag_match)
    else $error("calib: valid with a stale provenance tag");

  // ---- P3. FORBIDDEN. A readback mismatch permanently denies
  // validity. §3: the computed value never reached the hardware.
  property p_mismatch_denies_valid;
    @(posedge clk) disable iff (!rst_n)
      readback_mismatch |-> !valid;
  endproperty
  assert property (p_mismatch_denies_valid)
    else $error("calib: valid asserted despite a readback mismatch");

  // ---- P4. A condition change drops validity in the SAME cycle.
  // §6's defect is a bit that did not fall; this is the property that
  // would have caught it.
  property p_condition_change_drops_valid;
    @(posedge clk) disable iff (!rst_n)
      (have_result && (conditions_now != committed_tag)) |-> !valid;
  endproperty
  assert property (p_condition_change_drops_valid)
    else $error("calib: conditions changed and valid stayed asserted");

  // ---- P5. FORBIDDEN. The readback mismatch flag is sticky. §12: an
  // intermittent commit race must not be erased by the next good one.
  property p_mismatch_sticky;
    @(posedge clk) disable iff (!rst_n)
      (readback_mismatch && !clear) |=> readback_mismatch;
  endproperty
  assert property (p_mismatch_sticky)
    else $error("calib: a readback mismatch was cleared by a later commit");

  // ---- P6. ever_started is sticky and set by a start. §2: it is the
  // one bit separating "never ran" from "ran and succeeded".
  property p_ever_started_faithful;
    @(posedge clk) disable iff (!rst_n)
      start |=> ever_started;
  endproperty
  assert property (p_ever_started_faithful)
    else $error("calib: a start did not set ever_started");

  property p_ever_started_sticky;
    @(posedge clk) disable iff (!rst_n)
      (ever_started && !clear) |=> ever_started;
  endproperty
  assert property (p_ever_started_sticky)
    else $error("calib: ever_started dropped");

  // ---- P7. FORBIDDEN. A commit never occurs while the search is
  // still probing. Committing mid-search applies a value the search
  // has not finished evaluating.
  property p_no_commit_while_probing;
    @(posedge clk) disable iff (!rst_n)
      commit |-> !probing;
  endproperty
  assert property (p_no_commit_while_probing)
    else $error("calib: commit while the search was still probing");

  // ---- P8. FORBIDDEN. A start requires its precondition. §2: a
  // routine started without its lifecycle precondition produces a
  // result computed under undefined conditions.
  property p_start_requires_precondition;
    @(posedge clk) disable iff (!rst_n)
      start |-> precond_met;
  endproperty
  assert property (p_start_requires_precondition)
    else $error("calib: started without its precondition");

  // ---- P9. INVARIANT. Commits never exceed starts. More commits than
  // starts means something is committing outside the routine.
  property p_commits_le_starts;
    @(posedge clk) disable iff (!rst_n)
      (commit_count <= start_count);
  endproperty
  assert property (p_commits_le_starts)
    else $error("calib: %0d commits against %0d starts", commit_count, start_count);

  // ---- P10. INVARIANT. Convergences never exceed starts.
  property p_converges_le_starts;
    @(posedge clk) disable iff (!rst_n)
      (converge_count <= start_count);
  endproperty
  assert property (p_converges_le_starts)
    else $error("calib: more convergences than starts");

  // ---- P11. FORBIDDEN. A timeout and a convergence never coincide.
  // §1: they are different exits and a routine reporting both has
  // collapsed the distinction the whole chapter depends on.
  property p_timeout_xor_converge;
    @(posedge clk) disable iff (!rst_n)
      !(timeout && converged);
  endproperty
  assert property (p_timeout_xor_converge)
    else $error("calib: timeout and converged asserted together");

  // ---- P12. The committed code is the computed code at commit. §3's
  // transform failures are between COMPUTED and APPLIED, not here --
  // this property pins the monitor's own capture so a mismatch cannot
  // be blamed on the recorder.
  property p_capture_is_faithful;
    @(posedge clk) disable iff (!rst_n)
      commit |=> (committed_code == $past(computed_code));
  endproperty
  assert property (p_capture_is_faithful)
    else $error("calib: the monitor did not capture the computed code");

  // ---- 27.2 §7: publish every antecedent.
  cover property (@(posedge clk) disable iff (!rst_n) start);
  cover property (@(posedge clk) disable iff (!rst_n) probing);
  cover property (@(posedge clk) disable iff (!rst_n) converged);
  cover property (@(posedge clk) disable iff (!rst_n) commit);
  cover property (@(posedge clk) disable iff (!rst_n) timeout);
  cover property (@(posedge clk) disable iff (!rst_n) clear);
  cover property (@(posedge clk) disable iff (!rst_n) valid);
  cover property (@(posedge clk) disable iff (!rst_n) have_result && !valid);
  cover property (@(posedge clk) disable iff (!rst_n) readback_mismatch);
  cover property (@(posedge clk) disable iff (!rst_n) !ever_started);
  cover property (@(posedge clk) disable iff (!rst_n) stale_events != 16'd0);
  cover property (@(posedge clk) disable iff (!rst_n)
                  have_result && (conditions_now != committed_tag));
  cover property (@(posedge clk) disable iff (!rst_n) commit && !precond_met);
endmodule

// SIMULATION-ONLY. Independent reference. It models validity by
// REPLAYING the event history and asking whether a condition change
// has occurred since the last commit, rather than by comparing a
// stored tag. A different formulation, so agreement is evidence --
// 27.4 §15's argument.
class calib_reference;
  typedef struct { int code; int tag; bit clean; } result_t;
  result_t history[$];
  int current_conditions;

  function void commit(int code, int tag, bit readback_ok);
    result_t r; r.code = code; r.tag = tag; r.clean = readback_ok;
    history.push_back(r);
  endfunction

  function void set_conditions(int c); current_conditions = c; endfunction

  // Validity by replay: the last commit must exist, have been clean,
  // and have been taken under the conditions in force now.
  function bit valid();
    if (history.size() == 0) return 1'b0;
    if (!history[$].clean)   return 1'b0;
    return history[$].tag == current_conditions;
  endfunction

  // §7 row three: the spread of committed codes across repeats, in
  // CODE STEPS -- which 21.4 establishes are not volts.
  function int code_spread();
    int lo, hi;
    if (history.size() == 0) return -1;      // not zero: no data
    lo = history[0].code; hi = history[0].code;
    foreach (history[i]) begin
      if (history[i].code < lo) lo = history[i].code;
      if (history[i].code > hi) hi = history[i].code;
    end
    return hi - lo;
  endfunction

  function int commits();  return history.size(); endfunction

  // §3: the count of commits whose readback did not match.
  function int dirty_commits();
    int n = 0;
    foreach (history[i]) if (!history[i].clean) n++;
    return n;
  endfunction
endclass

  TWO PASSING CALIBRATION REPORTS

  (A) calibration never ran
        stimulus : the precondition is never satisfied; the platform's
                   `done` is wired to !busy
        done (platform view)        1      from the first cycle
        start_count                 0
        ever_started                0      <-- the only honest field
        converge_count              0
        commit_count                0
        have_result                 0
        valid                       0
        ------------------------------------------------
        all 12 properties           PASS
        all 13 covers               0 hits

        every property passes because nothing happened. The platform
        reports calibration complete. 28.1's hypothesis C reads this
        prerequisite's flag as TRUE and proceeds -- and the training
        failure that follows is investigated as a training problem for
        the rest of the afternoon.

        ONE field distinguishes it: ever_started.

  (B) calibration succeeded and the system corrupts data
        stimulus : full lifecycle, conditions held, traffic running
        start_count                 1
        converge_count              1
        commit_count                1
        readback_mismatch           0
        valid                       1
        stale_events                0
        code_min / code_max         42 / 42    (spread 0 over 50 boots)
        ------------------------------------------------
        all 12 properties           PASS
        all 13 covers               HIT
        data errors                 present

        the routine started, converged, committed, read back clean and
        remains valid. The committed code is perfectly repeatable
        across fifty boots. And data is corrupt.

        this is §11: the digital evidence is EXHAUSTED at valid. Four
        of five failures are excluded and the fifth has no digital
        signature at all.

    diagnosis : (A) is the vacuity case with a calibration face -- and
      it is the one that costs the most debugging time, because it
      sends the investigation to the WRONG CHAPTER. (B) is honest
      exhaustion: calibration is no longer the cheapest hypothesis,
      which is a result, not a failure of the instrument.

    the fix : (A) publish ever_started and never implement done as
      !busy. (B) hand off to 28.5 with the lifecycle evidence
      attached, so the corruption investigation starts knowing the
      four digital calibration failures are excluded.