Bring-Up Review Checklist

// ROBUST PLAN MODEL: every gate carries an OBSERVABLE, an EXPECTED
// VALUE, and the assumption a pass licenses. A gate with no observable
// cannot be constructed.
package gate_criterion_pkg;

  typedef enum int {
    K_POSITIVE,     // "X was observed to equal V"
    K_NONEVENT      // "no error was reported"  -- the defect
  } kind_e;

  typedef struct {
    int    stage;
    string observable;     // the signal or register READ
    int    expect_lo;      // the value range that constitutes a pass
    int    expect_hi;
    kind_e kind;
    string licenses;       // what a later stage may now assume
  } gate_t;

  // ILLUSTRATIVE, over 28.7 section 2's stages, taken as given.
  gate_t PLAN[] = '{
    '{1, "trcd_reg_readback",   14,   14, K_POSITIVE, "timing counts applied"},
    '{2, "calib_committed_val",  1, 4095, K_POSITIVE, "calibration converged"},
    '{3, "gate_window_width",    4,   64, K_POSITIVE, "read path has margin"},
    '{4, "first_txn_data",       1, 4095, K_POSITIVE, "one address works"},
    '{5, "sweep_mismatches",     0,    0, K_POSITIVE, "map self-consistent"},
    '{6, "lanes_carrying_data", 64,   64, K_POSITIVE, "every lane carried data"},
    '{7, "refresh_deadline_max", 1, 7800, K_POSITIVE, "refresh deadlines met"},
    '{8, "idle_gap_txn_ok",      1,    1, K_POSITIVE, "long gaps survive"},
    '{9, "freq_bin_margin",      2,   64, K_POSITIVE, "this bin has margin"}
  };
endpackage

module gate_criterion (
    input  logic       clk,
    input  logic       rst_n,
    input  logic       eval,
    input  logic [3:0] stage_id,
    input  logic [15:0] observed,
    input  logic        error_reported,
    output logic        gate_pass,
    output logic        gate_licensed,
    output logic [3:0]  nonevent_gates,
    output logic [3:0]  inert_system_passes
);
  import gate_criterion_pkg::*;

  // The inert-system test, computed once over the plan rather than run.
  // A gate whose criterion is a non-event passes on a dead system, and
  // the count of such gates is the review finding.
  always_comb begin
    nonevent_gates = 4'd0;
    foreach (PLAN[i]) if (PLAN[i].kind == K_NONEVENT) nonevent_gates++;
    // A POSITIVE gate whose expected range INCLUDES the reset value is
    // also inert-passable -- the subtler half of the same defect, and
    // the reason `expect_lo` is 1 rather than 0 on five rows above.
    inert_system_passes = nonevent_gates;
    foreach (PLAN[i])
      if ((PLAN[i].kind == K_POSITIVE) && (PLAN[i].expect_lo == 0)
          && (PLAN[i].expect_hi != 0))
        inert_system_passes++;
  end

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      gate_pass <= 1'b0; gate_licensed <= 1'b0;
    end else if (eval) begin
      // A pass requires the OBSERVED VALUE to be in range. The absence
      // of an error is necessary and never sufficient.
      gate_pass <= (observed >= 16'(PLAN[stage_id-1].expect_lo))
                && (observed <= 16'(PLAN[stage_id-1].expect_hi))
                && !error_reported;
      // The licence is granted only by a positive gate. This is the
      // link section 14's ledger consumes.
      gate_licensed <= (PLAN[stage_id-1].kind == K_POSITIVE)
                    && (observed >= 16'(PLAN[stage_id-1].expect_lo))
                    && (observed <= 16'(PLAN[stage_id-1].expect_hi));
    end
  end
endmodule

// INTENTIONALLY DEFECTIVE. WEAK PLAN: criteria written as non-events.
//
//   gate_t PLAN[] = '{
//     '{1, "",  0, 0, K_NONEVENT, "timing counts applied"},
//     '{2, "calib_done", 1, 1, K_POSITIVE, "calibration converged"},
//     '{3, "",  0, 0, K_NONEVENT, "read path has margin"},
//     ... };
//
//   gate_pass <= !error_reported;          // <-- the defect
//   gate_licensed <= gate_pass;
//
// CONTRACT VIOLATED: 28.7 section 3's requirement that a gate be a
// statement with a stated limit. A non-event has no limit because it
// has no statement.
//
// WHY IT SURVIVES: every criterion is TRUE of a working system. "No
// errors during the register write phase" is a real property of a good
// bring-up, and a plan full of them describes a successful bring-up
// accurately. It just cannot distinguish one from an inert system.
//
// Note row 2 in particular: it is K_POSITIVE and still inert-passable,
// because `calib_done` implemented as `!busy` reads 1 from reset --
// 28.7 section 3's most expensive row, reproduced exactly.
//
// TRACE (ILLUSTRATIVE, 9 stages, run twice: once on a working system
// and once on a system held in reset with no clock to the PHY):
//   working system:
//     robust: 9 of 9 pass, 9 of 9 licensed
//     weak:   9 of 9 pass, 9 of 9 licensed        IDENTICAL
//   inert system (PHY in reset):
//     robust: stage 1 observed 0, expect 14..14 -> FAIL at stage 1.
//             gates licensed: 0
//     weak:   no errors are reported by a PHY that is not running, so
//             every K_NONEVENT gate passes and `calib_done` reads 1:
//             9 of 9 PASS. Bring-up "completes" on a dead PHY.
//
//   gap: robust 0 of 9 licensed on an inert system; weak 9 of 9.
//   nonevent_gates: robust 0, weak 5. inert_system_passes: robust 0,
//   weak 6 (the five non-events plus `calib_done`).

// ROBUST PLAN MODEL: the relation is declared and the order is
// VALIDATED against it, so the order becomes a derived artifact.
module stage_order_check #(
    parameter int NST = 9
)(
    input  logic       clk,
    input  logic       rst_n,
    input  logic       validate,
    // the plan's proposed order: order[k] = the stage run k-th
    input  logic [3:0] order [0:NST-1],
    output logic       order_legal,
    output logic [3:0] violations,
    output logic [3:0] first_violating_slot,
    output logic       relation_declared
);
  // DEPENDS[a][b] = 1 means stage a requires stage b to have passed.
  // ILLUSTRATIVE over 28.7 section 2's stages. This matrix IS the artifact
  // the item demands; its absence is the finding.
  localparam bit DEPENDS [1:NST][1:NST] = '{
    //         1  2  3  4  5  6  7  8  9
    '{ 1'b0,1'b0,1'b0,1'b0,1'b0,1'b0,1'b0,1'b0,1'b0 },  // 1 registers
    '{ 1'b1,1'b0,1'b0,1'b0,1'b0,1'b0,1'b0,1'b0,1'b0 },  // 2 calibration
    '{ 1'b1,1'b1,1'b0,1'b0,1'b0,1'b0,1'b0,1'b0,1'b0 },  // 3 training
    '{ 1'b1,1'b1,1'b1,1'b0,1'b0,1'b0,1'b0,1'b0,1'b0 },  // 4 first txn
    '{ 1'b1,1'b1,1'b1,1'b1,1'b0,1'b0,1'b0,1'b0,1'b0 },  // 5 addr sweep
    '{ 1'b1,1'b1,1'b1,1'b1,1'b0,1'b0,1'b0,1'b0,1'b0 },  // 6 all lanes
    '{ 1'b1,1'b1,1'b1,1'b1,1'b0,1'b0,1'b0,1'b0,1'b0 },  // 7 refresh
    '{ 1'b1,1'b1,1'b1,1'b1,1'b0,1'b0,1'b1,1'b0,1'b0 },  // 8 idle/power
    '{ 1'b1,1'b1,1'b1,1'b1,1'b1,1'b1,1'b1,1'b1,1'b0 }   // 9 frequency
  };

  always_comb relation_declared = 1'b1;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      order_legal <= 1'b0; violations <= '0; first_violating_slot <= '0;
    end else if (validate) begin
      automatic bit  done_before [1:NST];
      automatic int  v = 0;
      automatic int  firstv = 0;
      for (int s = 1; s <= NST; s++) done_before[s] = 1'b0;

      for (int k = 0; k < NST; k++) begin
        automatic int st = int'(order[k]);
        // Every dependency of `st` must already be marked done.
        for (int d = 1; d <= NST; d++) begin
          if (DEPENDS[st][d] && !done_before[d]) begin
            v++;
            if (firstv == 0) firstv = k + 1;
          end
        end
        done_before[st] = 1'b1;
      end

      violations           <= 4'(v);
      first_violating_slot <= 4'(firstv);
      order_legal          <= (v == 0);
    end
  end
endmodule

// INTENTIONALLY DEFECTIVE. WEAK PLAN: an order with no relation.
//
//   // bringup_plan.md
//   //   1. Program registers
//   //   2. Check calibration done
//   //   3. First transaction            <-- before training
//   //   4. Run training
//   //   5. Address sweep
//   //   ...
//   // (no dependency matrix; no validation; the order is prose)
//
// CONTRACT VIOLATED: 21.5 section 2 -- the order is determined by which
// observable each step requires. Here it is determined by what is
// quickest to try.
//
// WHY IT SURVIVES: stage 3 before stage 4 OFTEN WORKS. A first
// transaction at a low frequency with default delays can succeed on a
// short channel before any training has run -- and when it does, the
// team has a passing stage 3 and a reason to believe the read path is
// good. The order is then never questioned, because it worked.
//
// TRACE (ILLUSTRATIVE, the order above):
//   robust validator on that order:
//     slot 3 runs stage 4 (first txn) with stage 3 (training) not done
//     -> violations 3 (first txn requires 1, 2, 3; 3 is missing)
//     first_violating_slot = 3, order_legal = 0. REJECTED before
//     anybody powers a board.
//   weak: no validator exists. The plan runs.
//
//   and what the passing stage 3 establishes:
//     on a SHORT channel: the transaction succeeds untrained, stage 3
//       passes, and the team believes the read path has margin. It has
//       a default delay that happens to land inside a wide eye.
//     on a LONG channel: the transaction fails, and the suspect list
//       is the whole read path -- because training, the thing that
//       would have made it work, has not run and is not suspected.
//
//   gap: 3 order violations, detected in the plan review at zero cost,
//   versus an investigation that starts with a false premise. And the
//   short-channel case is worse than the long-channel case, because it
//   passes.

// ROBUST LOG MODEL: the closure is computed from a declared consequence
// map, so "one variable" becomes a measured quantity.
module one_variable_audit #(
    parameter int NV = 10
)(
    input  logic       clk,
    input  logic       rst_n,
    input  logic       experiment,
    input  logic [NV-1:0] edited,       // what the operator changed
    output logic [NV-1:0] closure,      // what actually changed
    output logic [3:0] edit_count,
    output logic [3:0] closure_count,
    output logic       is_one_variable,
    output logic [7:0] experiments_logged,
    output logic [7:0] experiments_truly_single
);
  // CONSEQUENCE[a][b] = 1 means changing a also changes b.
  // ILLUSTRATIVE, and every row is taken from 28.7 section 4's table.
  //  0 frequency  1 timing counts  2 calib validity  3 channel behaviour
  //  4 rank count 5 loading        6 termination     7 address space
  //  8 address map 9 burst width
  localparam bit CONSEQ [0:NV-1][0:NV-1] = '{
    '{1'b0,1'b1,1'b1,1'b1,1'b0,1'b0,1'b0,1'b0,1'b0,1'b0}, // frequency
    '{1'b0,1'b0,1'b0,1'b0,1'b0,1'b0,1'b0,1'b0,1'b0,1'b0}, // timing counts
    '{1'b0,1'b0,1'b0,1'b0,1'b0,1'b0,1'b0,1'b0,1'b0,1'b0}, // calib validity
    '{1'b0,1'b0,1'b0,1'b0,1'b0,1'b0,1'b0,1'b0,1'b0,1'b0}, // channel
    '{1'b0,1'b0,1'b0,1'b0,1'b0,1'b1,1'b1,1'b1,1'b0,1'b0}, // rank count
    '{1'b0,1'b0,1'b0,1'b1,1'b0,1'b0,1'b0,1'b0,1'b0,1'b0}, // loading
    '{1'b0,1'b0,1'b0,1'b1,1'b0,1'b0,1'b0,1'b0,1'b0,1'b0}, // termination
    '{1'b0,1'b0,1'b0,1'b0,1'b0,1'b0,1'b0,1'b0,1'b0,1'b0}, // address space
    '{1'b0,1'b0,1'b0,1'b0,1'b0,1'b0,1'b0,1'b0,1'b0,1'b0}, // address map
    '{1'b0,1'b0,1'b0,1'b0,1'b0,1'b0,1'b0,1'b0,1'b0,1'b0}  // burst width
  };

  function automatic logic [NV-1:0] close(logic [NV-1:0] seed);
    logic [NV-1:0] cur = seed;
    logic [NV-1:0] nxt;
    // Transitive closure by iteration to a fixed point. NV passes is
    // sufficient and the bound matters: a single pass misses
    // frequency -> channel -> nothing, but rank -> loading -> channel
    // needs two.
    for (int it = 0; it < NV; it++) begin
      nxt = cur;
      for (int a = 0; a < NV; a++)
        if (cur[a])
          for (int b = 0; b < NV; b++)
            if (CONSEQ[a][b]) nxt[b] = 1'b1;
      if (nxt == cur) break;
      cur = nxt;
    end
    return cur;
  endfunction

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      closure <= '0; edit_count <= '0; closure_count <= '0;
      is_one_variable <= 1'b0;
      experiments_logged <= '0; experiments_truly_single <= '0;
    end else if (experiment) begin
      automatic logic [NV-1:0] c = close(edited);
      closure       <= c;
      edit_count    <= 4'($countones(edited));
      closure_count <= 4'($countones(c));
      // The definition the item enforces: one variable means the
      // CLOSURE has one member, not the edit.
      is_one_variable <= ($countones(c) == 1);
      experiments_logged <= experiments_logged + 1'b1;
      if ($countones(c) == 1)
        experiments_truly_single <= experiments_truly_single + 1'b1;
    end
  end
endmodule

// INTENTIONALLY DEFECTIVE. WEAK LOG: the edit count.
//
//   // bringup_log.csv
//   //   exp,changed,result
//   //   14,"freq 1600->1866",fail
//   //   15,"rank 1->2",fail
//   //   16,"addr map RBC->BRC",pass
//   // and the review note: "experiments 14-16 each changed one thing"
//
//   edit_count      <= $countones(edited);
//   is_one_variable <= ($countones(edited) == 1);    // <-- the defect
//
// CONTRACT VIOLATED: 28.7 section 4 -- not one of its six listed actions
// is a single variable.
//
// WHY IT SURVIVES: the log is TRUE. One field was edited. The operator
// did change one thing, in the only sense available at a keyboard. The
// error is that the suspect list is derived from the edit, and nothing
// in the log says otherwise.
//
// TRACE (ILLUSTRATIVE, 20 experiments; three shown):
//   exp 14, edited = {frequency}
//     robust: closure = {frequency, timing counts, calib validity,
//                        channel behaviour} -> closure_count 4,
//             is_one_variable 0
//     weak:   edit_count 1, is_one_variable 1
//   exp 15, edited = {rank count}
//     robust: closure = {rank, loading, termination, address space,
//                        channel behaviour} -> 5, is_one_variable 0
//             (channel arrives via loading AND termination -- two
//              paths, which is why the closure needs iteration)
//     weak:   1
//   exp 16, edited = {address map}
//     robust: closure = {address map} -> 1, is_one_variable 1. This
//             one genuinely IS a single variable.
//     weak:   1                                     AGREE
//
//   over 20 experiments:
//     robust: experiments_truly_single = 12 of 20
//     weak:   claimed 20 of 20
//
//   gap: 8 experiments whose suspect list is 4 or 5 items and whose log
//   says 1. And the investigation that follows exp 14 will compare a
//   1600 run against an 1866 run and attribute the difference to
//   frequency, when three other things moved with it.

// ROBUST PROVENANCE MODEL: the comparand is derived INDEPENDENTLY of
// the write path, from the device figure, in this module.
module config_readback #(
    parameter int NROW = 6
)(
    input  logic       clk,
    input  logic       rst_n,
    input  logic       check,
    // the device figure and its condition, from the datasheet row
    input  logic [15:0] spec_ns_x100,    // ILLUSTRATIVE: ns * 100
    input  logic [15:0] spec_min_nck,    // the max(nCK, ns) form's nCK part
    input  logic [15:0] clk_period_x100, // ns * 100
    // the value the driver actually wrote, and what the register reads
    input  logic [15:0] written_value,
    input  logic [15:0] read_value,
    output logic        row_ok,
    output logic [15:0] derived_value,
    output logic        write_path_ok,
    output logic        value_correct,
    output logic [3:0]  rows_confirmed,
    output logic [3:0]  rows_write_only
);
  // The derivation. 28.7 section 5 requires the rounding DIRECTION to be
  // stated, and 28.2 section 10 establishes it: a minimum time requirement
  // rounds UP. A ceiling is written explicitly so a reviewer can see it.
  function automatic logic [15:0] derive();
    logic [31:0] ns_cycles;
    // ceil(spec_ns / clk_period), in hundredths to avoid a divide by a
    // fraction.
    ns_cycles = (32'(spec_ns_x100) + 32'(clk_period_x100) - 32'd1)
                / 32'(clk_period_x100);
    // max(nCK, ns) form: the larger of the two constraints binds.
    return (ns_cycles > 32'(spec_min_nck)) ? 16'(ns_cycles) : spec_min_nck;
  endfunction

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      row_ok <= 1'b0; derived_value <= '0;
      write_path_ok <= 1'b0; value_correct <= 1'b0;
      rows_confirmed <= '0; rows_write_only <= '0;
    end else if (check) begin
      automatic logic [15:0] d = derive();
      derived_value <= d;
      // TWO separate facts, because they answer different questions and
      // collapsing them is the item.
      write_path_ok <= (read_value == written_value);   // the path works
      value_correct <= (read_value == d);               // the value is right
      row_ok        <= (read_value == d) && (read_value == written_value);

      if ((read_value == d) && (read_value == written_value))
        rows_confirmed <= rows_confirmed + 1'b1;
      else if (read_value == written_value)
        // The path works and the value is wrong: this is the state the
        // weak build reports as a pass.
        rows_write_only <= rows_write_only + 1'b1;
    end
  end
endmodule

// INTENTIONALLY DEFECTIVE. WEAK PROVENANCE: the comparand is the write.
//
//   // config_check.c
//   //   for (each row) {
//   //     write_reg(row.addr, row.value);
//   //     if (read_reg(row.addr) != row.value)   // <-- the defect
//   //       fail("readback mismatch");
//   //   }
//   // and the provenance table's `conversion` and `readback` columns
//   // are both populated from `row.value`.
//
// CONTRACT VIOLATED: 28.7 section 5's stage-1 gate -- the readback must
// match the CONVERSION, not the write.
//
// WHY IT SURVIVES: it catches everything a read-back is usually
// expected to catch -- a wrong address, a locked register, a
// write-only shadow, a bus fault. It is a genuinely useful check. It
// simply cannot see an error in the conversion, and the conversion is
// where 28.2's hardest bugs live.
//
// TRACE (ILLUSTRATIVE, tRCD at two frequencies; spec 13.75 ns,
// min 8 nCK):
//   1600 MT/s, clk_period 1.25 ns:
//     correct: ceil(13.75 / 1.25) = 11; max(11, 8) = 11
//     the driver's code uses a FLOOR: 13.75 / 1.25 = 11.0 exactly,
//     so floor gives 11 too.
//     robust: derived 11, written 11, read 11 -> row_ok 1
//     weak:   read == written -> pass                 IDENTICAL
//     -- 28.2 section 10's point exactly: a floor is invisible wherever the
//        division is exact.
//   1866 MT/s, clk_period 1.071 ns:
//     correct: ceil(13.75 / 1.071) = ceil(12.83) = 13; max(13, 8) = 13
//     the driver's FLOOR gives 12.
//     robust: derived 13, written 12, read 12
//             -> write_path_ok 1, value_correct 0, row_ok 0. FAIL,
//                and it names WHICH of the two facts failed.
//     weak:   read == written -> PASS. Stage 1's gate is satisfied with
//             tRCD programmed one cycle short.
//
//   over 6 provenance rows at the higher bin:
//     robust: rows_confirmed 2, rows_write_only 4  -> 4 conversions wrong
//     weak:   6 of 6 pass
//
//   gap: 4 of 6 timing counts are one cycle short and stage 1 passes.
//   And the failure that follows is a timing violation at stage 4 or
//   later, whose suspect list does not include stage 1 because stage 1
//   passed.

// ROBUST CAPTURE MODEL: each observable carries a survival class, and
// the ledger reports which recorded values are trustworthy.
package recovery_survival_pkg;
  typedef enum int {
    S_STICKY,        // survives reset; latched on first occurrence
    S_VOLATILE,      // changes continuously; a read is a sample
    S_RESET_CLEARED  // destroyed by the reset recovery uses
  } surv_e;

  typedef struct {
    string name;
    surv_e surv;
  } obs_t;

  // ILLUSTRATIVE capture list of twelve observables.
  obs_t LIST[] = '{
    '{"first_err_code",        S_STICKY},
    '{"first_err_addr",        S_STICKY},
    '{"err_count",             S_STICKY},
    '{"training_bitmap",       S_RESET_CLEARED},
    '{"committed_delay",       S_RESET_CLEARED},
    '{"calib_fail_case",       S_RESET_CLEARED},
    '{"queue_occupancy",       S_VOLATILE},
    '{"refresh_debt",          S_VOLATILE},
    '{"bank_open_map",         S_VOLATILE},
    '{"temp_sensor",           S_VOLATILE},
    '{"mode_regs",             S_STICKY},
    '{"phy_lock_status",       S_RESET_CLEARED}
  };
endpackage

module recovery_survival_map (
    input  logic       clk,
    input  logic       rst_n,
    input  logic       capture_done,     // the capture completed
    input  logic       recovery_started,
    input  logic       classify,
    output logic [3:0] trustworthy,
    output logic [3:0] lost_to_recovery,
    output logic [3:0] sampled_only,
    output logic       capture_preceded_recovery
);
  import recovery_survival_pkg::*;
  logic captured_first;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      captured_first <= 1'b0; capture_preceded_recovery <= 1'b0;
      trustworthy <= '0; lost_to_recovery <= '0; sampled_only <= '0;
    end else begin
      // The ordering fact, recorded rather than assumed -- 28.7 section 10's
      // rule turned into a bit.
      if (capture_done && !recovery_started) captured_first <= 1'b1;
      capture_preceded_recovery <= captured_first;

      if (classify) begin
        automatic int t = 0, l = 0, s = 0;
        foreach (LIST[i]) begin
          case (LIST[i].surv)
            // Sticky values are trustworthy whether or not capture won
            // the race: that is what sticky MEANS.
            S_STICKY:        t++;
            // Reset-cleared values are trustworthy ONLY if the capture
            // preceded recovery. Otherwise the recorded value is the
            // post-reset value wearing a pre-failure label.
            S_RESET_CLEARED: if (captured_first) t++; else l++;
            // Volatile values are a SAMPLE even when captured first.
            // They are not lost; they are weaker than they look.
            S_VOLATILE:      s++;
            default: ;
          endcase
        end
        trustworthy      <= 4'(t);
        lost_to_recovery <= 4'(l);
        sampled_only     <= 4'(s);
      end
    end
  end
endmodule

// INTENTIONALLY DEFECTIVE. WEAK CAPTURE: one list, no classes.
//
//   // capture.sh -- run this when it fails
//   //   dump_regs  > capture.txt        # all twelve observables
//   //   reset_phy                       # then recover
//   // and the ledger records all twelve as "captured at 14:22:07"
//
// CONTRACT VIOLATED: nothing in 28.7 section 10 -- the capture DOES precede
// the recovery in this script. The defect is that the ledger reports
// twelve trustworthy values when four are samples and, in the common
// case where the failure itself triggered a reset, four more are gone.
//
// WHY IT SURVIVES: the script is correct and the discipline was
// followed. Somebody wrote the capture, put it before the recovery,
// and ran it. Every value in capture.txt is a real register read.
//
// TRACE (ILLUSTRATIVE, the twelve observables above):
//   case A -- operator-initiated recovery, capture ran first:
//     robust: trustworthy 8 (4 sticky + 4 reset-cleared, captured
//             first), lost 0, sampled_only 4,
//             capture_preceded_recovery 1
//     weak:   "12 captured"
//     gap: 4 volatile values presented as state when they are samples.
//   case B -- the failure triggered an automatic PHY reset, and the
//   capture ran afterwards:
//     robust: captured_first 0 -> trustworthy 4 (sticky only),
//             LOST 4, sampled_only 4
//     weak:   "12 captured" -- and `training_bitmap` reads all zeros,
//             which 28.1 section 2 says is consistent with five different
//             causes. The investigation now has a bitmap signature
//             that is an artefact of the reset.
//
//   gap: in case B, 4 of 12 recorded values are post-recovery values
//   read as pre-failure state, and one of them is the single most
//   misleading signature in the track.

// ROBUST REDUCTION LOG: each step records the signature, and a step
// that changes the signature is REJECTED and backed out.
module reduction_confirmation #(
    parameter int MAXSTEP = 12
)(
    input  logic       clk,
    input  logic       rst_n,
    input  logic       step,
    input  logic [7:0] sig_observed,     // the failure's signature
    input  logic       reproduced,
    input  logic [7:0] baseline_sig,     // the ORIGINAL signature
    output logic [3:0] steps_accepted,
    output logic [3:0] steps_rejected,
    output logic [3:0] steps_signature_drift,
    output logic       chain_intact,
    output logic [7:0] current_sig
);
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      steps_accepted <= '0; steps_rejected <= '0;
      steps_signature_drift <= '0; chain_intact <= 1'b1;
      current_sig <= '0;
    end else if (step) begin
      current_sig <= sig_observed;
      if (!reproduced) begin
        // Stopped reproducing: back the step out. This is the case
        // everybody handles.
        steps_rejected <= steps_rejected + 1'b1;
      end else if (sig_observed != baseline_sig) begin
        // Still fails, DIFFERENT signature. This is the case nobody
        // handles, and it is the item.
        steps_rejected        <= steps_rejected + 1'b1;
        steps_signature_drift <= steps_signature_drift + 1'b1;
        chain_intact          <= 1'b0;
      end else begin
        steps_accepted <= steps_accepted + 1'b1;
      end
    end
  end
endmodule

// INTENTIONALLY DEFECTIVE. WEAK REDUCTION LOG: confirm at the end.
//
//   // reduce.sh
//   //   remove_requester 3; remove_requester 2; disable_refresh;
//   //   narrow_addr_range; single_bank; single_lane
//   //   run_test    # and if it still fails, we have a minimal case
//   //
//   steps_accepted <= steps_accepted + 1;      // every step accepted
//   chain_intact   <= reproduced;              // checked once, at the end
//
// CONTRACT VIOLATED: 28.7 section 11 -- reduction during bring-up requires
// confirmation during reduction. The script's logic is sound if
// "fails" identifies the phenomenon, and it does not.
//
// WHY IT SURVIVES: it produces a small failing case, quickly, and a
// small failing case is genuinely valuable. Nobody notices the swap
// because both the original and the final case fail.
//
// TRACE (ILLUSTRATIVE, 8 reduction steps; baseline_sig = 0x41, a
// read-data mismatch on lane 17 under refresh):
//   step 1  remove requester 3    repro 1  sig 0x41   -> accept
//   step 2  remove requester 2    repro 1  sig 0x41   -> accept
//   step 3  disable refresh       repro 1  sig 0x08   -> the failure
//           still happens, and it is now a TIMING violation with no
//           refresh in the picture. Different phenomenon.
//     robust: signature drift -> REJECT, back out, chain_intact 0.
//             The reduction continues from step 2 with refresh on.
//     weak:   accept. Refresh is now out of the reproducer, and the
//             original failure -- which required refresh -- is gone.
//   steps 4-8 reduce the NEW failure: narrow the range, one bank, one
//           lane. All reproduce 0x08.
//   final: a six-line reproducer that fails 0x08 every time.
//
//   robust: steps_accepted 2, steps_rejected 6, signature_drift 1,
//           chain_intact 0 -- and it says WHICH step broke the chain
//   weak:   steps_accepted 8, chain_intact 1, "minimal reproducer found"
//
//   gap: the weak build delivers a clean, small, reliably-failing
//   reproducer of a failure that is not the one being investigated.
//   The original -- a lane-17 mismatch under refresh -- has no
//   reproducer at all, and the team believes it has one.

// ROBUST REPAIR LOG: three facts per repair, and a verdict that
// requires all three.
module repair_proof #(
    parameter int NREP = 8
)(
    input  logic       clk,
    input  logic       rst_n,
    input  logic       submit,
    input  logic       repro_passes_with_fix,
    input  logic       repro_fails_without_fix,   // the REVERT test
    input  logic       regression_still_passes,
    input  logic [7:0] mechanism_len,             // 0 = no mechanism stated
    output logic       repair_proved,
    output logic [3:0] proved_count,
    output logic [3:0] unproved_count,
    output logic [3:0] no_revert_count,
    output logic [3:0] coincidence_count
);
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      repair_proved <= 1'b0; proved_count <= '0; unproved_count <= '0;
      no_revert_count <= '0; coincidence_count <= '0;
    end else if (submit) begin
      // All four, and the revert is not optional.
      automatic bit ok = repro_passes_with_fix
                      && repro_fails_without_fix
                      && regression_still_passes
                      && (mechanism_len != 8'd0);
      repair_proved <= ok;
      if (ok) proved_count <= proved_count + 1'b1;
      else    unproved_count <= unproved_count + 1'b1;

      // The two diagnostic sub-counts, because "unproved" is not
      // actionable and these are.
      if (!repro_fails_without_fix && repro_passes_with_fix) begin
        // Passes with the fix AND passes without it: the fix is not
        // the cause. Something else changed.
        coincidence_count <= coincidence_count + 1'b1;
      end
      if (mechanism_len == 8'd0)
        no_revert_count <= no_revert_count + 1'b1;
    end
  end
endmodule

// INTENTIONALLY DEFECTIVE. WEAK REPAIR LOG: one fact.
//
//   // bringup_log.csv
//   //   repair,result
//   //   "increase tRP by 1",   "reproducer passes"
//   //   "re-run training",     "reproducer passes"
//   //   "disable write CRC",   "reproducer passes"
//   //
//   repair_proved <= repro_passes_with_fix;      // <-- the defect
//
// CONTRACT VIOLATED: 28.7 section 15's proof of a repair, weakened to its
// necessary condition.
//
// WHY IT SURVIVES: the reproducer really does pass. Under schedule
// pressure a passing reproducer is the definition of done, and asking
// to break it again on purpose reads as obstruction.
//
// TRACE (ILLUSTRATIVE, 8 repairs submitted during one bring-up):
//   repair A  "increase tRP by 1"
//     with fix: pass.  without fix: FAIL.  regression: pass.
//     mechanism: "tRP was floored; 28.2 section 10 requires ceiling" -> PROVED
//   repair B  "re-run training"
//     with fix: pass.  without fix: PASS.  -> the failure had already
//     stopped reproducing before the repair. A board had been reseated
//     that morning.
//     robust: coincidence_count++, repair_proved 0
//     weak:   PROVED. And the real defect -- an intermittent connector
//             -- is now closed as "fixed by retraining".
//   repair C  "disable write CRC"
//     with fix: pass.  without fix: FAIL.  regression: FAIL (CRC
//     coverage lost).  mechanism: none stated.
//     robust: repair_proved 0 -- it is a WORKAROUND, correctly
//             classified, and the regression failure is recorded
//     weak:   PROVED
//   repairs D-H: 3 proved, 2 coincidences
//
//   robust: proved 5 of 8, coincidences 2, no mechanism 1
//   weak:   8 of 8 proved
//
//   gap: 3 of 8 repairs are not repairs -- two coincidences and one
//   undocumented workaround that costs a regression. And repair B is
//   the expensive one: an intermittent connector is now a closed
//   ticket, and it will come back.

// ROBUST PLAN MODEL: a failure is classified, the facts still available
// are gathered, and the branch is declared per stage.
package failure_as_result_pkg;
  // 28.1 section 4's six failure domains, taken as given.
  typedef enum int { D_SEARCH, D_OBSERVE, D_CONFIG, D_STALE,
                     D_ORDER, D_MARGIN } domain_e;

  typedef enum int { B_STOP,          // downstream evidence would be void
                     B_CONTINUE,      // downstream stages remain valid
                     B_SKIP_DEPS      // skip dependents, run independents
                   } branch_e;

  typedef struct {
    int      stage;
    branch_e on_fail;
    int      facts_still_collectable;
  } stage_policy_t;

  // ILLUSTRATIVE, and the branch on each row is a JUDGEMENT the plan
  // must record rather than a rule this chapter supplies.
  stage_policy_t POLICY[] = '{
    '{1, B_STOP,      2},   // wrong timing counts void everything
    '{2, B_STOP,      3},   // an uncalibrated PHY voids everything
    '{3, B_SKIP_DEPS, 4},   // training failed: 28.1's bitmap is still data
    '{4, B_SKIP_DEPS, 3},
    '{5, B_CONTINUE,  4},   // map inconsistent: lanes and refresh still valid
    '{6, B_CONTINUE,  3},
    '{7, B_CONTINUE,  4},
    '{8, B_CONTINUE,  2},
    '{9, B_CONTINUE,  3}
  };
endpackage

module failure_as_result (
    input  logic       clk,
    input  logic       rst_n,
    input  logic       stage_failed,
    input  logic [3:0] failed_stage,
    input  logic [2:0] observed_domain,
    output logic [2:0] branch_taken,
    output logic [3:0] facts_gathered,
    output logic       classified,
    output logic [3:0] stages_still_run
);
  import failure_as_result_pkg::*;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      branch_taken <= '0; facts_gathered <= '0;
      classified <= 1'b0; stages_still_run <= '0;
    end else if (stage_failed) begin
      automatic stage_policy_t p = POLICY[failed_stage-1];
      // The classification is mandatory. An unclassified failure is
      // 28.1's five-causes-one-signature problem by construction.
      classified   <= (observed_domain <= 3'(D_MARGIN));
      branch_taken <= 3'(p.on_fail);
      // The facts the failing stage can still yield -- 28.1's bitmap,
      // a partial sweep result, a per-lane map -- are gathered whether
      // or not the plan continues.
      facts_gathered <= 4'(p.facts_still_collectable);

      case (p.on_fail)
        B_STOP:      stages_still_run <= 4'd0;
        B_SKIP_DEPS: stages_still_run <= 4'd9 - failed_stage - 4'd1;
        default:     stages_still_run <= 4'd9 - failed_stage;
      endcase
    end
  end
endmodule

// INTENTIONALLY DEFECTIVE. WEAK PLAN: halt, unclassified.
//
//   // run_bringup.sh
//   //   for stage in 1..9; do
//   //     run_stage $stage || { echo "BLOCKED at stage $stage"; exit 1; }
//   //   done
//
// CONTRACT VIOLATED: nothing 28.7 states as a rule. The script is
// careful, conventional, and the safest-looking thing to write.
//
// WHY IT SURVIVES: stopping on failure is correct for stages 1 and 2,
// and those are the stages that fail most often early in a bring-up.
// By the time a stage-5 failure happens, the script's behaviour is
// established practice.
//
// TRACE (ILLUSTRATIVE, stage 5 fails -- an address-map inconsistency):
//   robust: classified into D_CONFIG; branch B_CONTINUE;
//           facts_gathered 4 (the sweep's mismatch pattern, the first
//           mismatching address, the bit position, the stride);
//           stages_still_run 4 -> lanes, refresh, idle and frequency
//           all execute and all pass.
//           Result: the team knows the failure is config-domain, has
//           a mismatch pattern, and knows four later stages are clean.
//           The suspect list is the address map alone.
//   weak:   "BLOCKED at stage 5". One fact.
//           Result: the suspect list is stages 5 through 9.
//
//   gap: 9 facts versus 1, from the same run on the same hardware.
//   And the expensive part is not the facts -- it is that the weak
//   run's suspect list includes four subsystems that the robust run
//   proved clean in the same afternoon.

// ROBUST PLAN MODEL: establishes-sets and assumes-sets, and the
// difference computed. The difference is the review's output.
module assumption_ledger #(
    parameter int NST  = 9,
    parameter int NFACT = 12
)(
    input  logic       clk,
    input  logic       rst_n,
    input  logic       audit,
    input  logic [NST-1:0] gate_passed,
    output logic [NFACT-1:0] established,
    output logic [NFACT-1:0] unlicensed,
    output logic [3:0] unlicensed_count,
    output logic [3:0] first_unlicensed_stage,
    output logic       plan_sound
);
  // The twelve facts a DDR bring-up's stages reason about. ILLUSTRATIVE
  // set, chosen to cover 28.7 section 3's eight rows plus four the table's
  // "does not establish" column implies.
  //  0 access path  1 timing counts correct  2 calib started
  //  3 calib converged  4 setting committed  5 window is wide
  //  6 one address works  7 map self-consistent  8 map matches geometry
  //  9 every lane carried data  10 every lane has margin
  // 11 refresh deadlines met
  localparam bit ESTABLISHES [1:NST][0:NFACT-1] = '{
    '{1'b1,1'b1,0,0,0,0,0,0,0,0,0,0},   // 1 registers + provenance
    '{0,0,1'b1,1'b1,0,0,0,0,0,0,0,0},   // 2 calibration
    '{0,0,0,0,1'b1,0,0,0,0,0,0,0},      // 3 training: COMMITTED, not wide
    '{0,0,0,0,0,0,1'b1,0,0,0,0,0},      // 4 first transaction
    '{0,0,0,0,0,0,0,1'b1,0,0,0,0},      // 5 sweep: self-consistent only
    '{0,0,0,0,0,0,0,0,0,1'b1,0,0},      // 6 lanes: carried data only
    '{0,0,0,0,0,0,0,0,0,0,0,1'b1},      // 7 refresh
    '{0,0,0,0,0,0,0,0,0,0,0,0},         // 8 idle/power: establishes none
    '{0,0,0,0,0,0,0,0,0,0,0,0}          // 9 frequency: none beyond itself
  };
  // What each stage ASSUMES. This is the column a normal plan lacks.
  localparam bit ASSUMES [1:NST][0:NFACT-1] = '{
    '{0,0,0,0,0,0,0,0,0,0,0,0},                    // 1
    '{1'b1,1'b1,0,0,0,0,0,0,0,0,0,0},              // 2
    '{1'b1,1'b1,1'b1,1'b1,0,0,0,0,0,0,0,0},        // 3
    '{1'b1,1'b1,0,1'b1,1'b1,0,0,0,0,0,0,0},        // 4
    '{1'b1,1'b1,0,0,1'b1,0,1'b1,0,0,0,0,0},        // 5
    '{1'b1,1'b1,0,0,1'b1,0,1'b1,0,0,0,0,0},        // 6
    '{1'b1,1'b1,0,0,1'b1,0,1'b1,0,0,0,0,0},        // 7
    '{1'b1,1'b1,0,0,1'b1,0,1'b1,0,0,0,0,1'b1},     // 8
    // Stage 9 is the interesting row: a frequency sweep assumes MARGIN,
    // and no gate establishes margin. That is the finding.
    '{1'b1,1'b1,0,0,1'b1,1'b1,1'b1,0,1'b1,1'b1,1'b1,1'b1}
  };

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      established <= '0; unlicensed <= '0; unlicensed_count <= '0;
      first_unlicensed_stage <= '0; plan_sound <= 1'b0;
    end else if (audit) begin
      automatic bit [NFACT-1:0] est = '0;
      automatic bit [NFACT-1:0] unl = '0;
      automatic int             cnt = 0;
      automatic int             firsts = 0;

      for (int s = 1; s <= NST; s++) begin
        // Before running stage s, check its assumptions against what
        // the gates BEFORE it established.
        for (int f = 0; f < NFACT; f++) begin
          if (ASSUMES[s][f] && !est[f]) begin
            unl[f] = 1'b1;
            cnt++;
            if (firsts == 0) firsts = s;
          end
        end
        // Then add what stage s establishes, but only if its gate passed.
        if (gate_passed[s-1])
          for (int f = 0; f < NFACT; f++)
            if (ESTABLISHES[s][f]) est[f] = 1'b1;
      end

      established            <= est;
      unlicensed             <= unl;
      unlicensed_count       <= 4'(cnt);
      first_unlicensed_stage <= 4'(firsts);
      plan_sound             <= (cnt == 0);
    end
  end
endmodule

// INTENTIONALLY DEFECTIVE. WEAK PLAN: no assumes column.
//
//   // bringup_plan.md has an "establishes" note per stage, copied
//   // from 28.7 section 3's table, and no "assumes" column at all. The
//   // review consists of reading each stage's note and agreeing.
//
// CONTRACT VIOLATED: none stated anywhere. 28.7 section 3 requires the
// establishes column and does not require the other one, because its
// subject is a gate and this item's subject is the relation.
//
// WHY IT SURVIVES: every stage's own reasoning is sound, every gate
// passes, and the establishes notes are correct and cited. There is no
// row to object to. The defect is in a column that does not exist.
//
// TRACE (ILLUSTRATIVE, all nine gates passing):
//   robust audit: established after stage 8 =
//     {access path, timing counts, calib started, calib converged,
//      setting committed, one address works, map self-consistent,
//      lanes carried data, refresh deadlines met}   -- 9 of 12
//   unlicensed, found at stage 9:
//     fact 5   window is wide            -- 28.1 section 5: a committed
//                                           setting at the centre of a
//                                           one-tap window passes every
//                                           digital check
//     fact 8   map matches geometry      -- 28.7 section 3: a clean sweep
//                                           establishes self-consistency,
//                                           not agreement with the device
//     fact 10  every lane has margin     -- 28.7 section 3: lanes carried
//                                           data; margin is not shown
//   plus three more that stage 9 assumes and that stages 1-8 establish
//   only for the PREVIOUS frequency bin -- 28.4 section 5's staleness.
//     unlicensed_count = 6, first_unlicensed_stage = 9, plan_sound = 0
//   weak: nine gates, nine passes, plan complete.
//
//   gap: six assumptions that no gate established, and three of the six
//   are margin -- the quantity 28.1 and 28.7 both say a digital gate
//   cannot see. A frequency sweep is exactly the activity that consumes
//   margin, so stage 9 is where the plan's unlicensed premises are
//   spent.

  // ---- Section 6: gate criteria. The obligation is on the PLAN, so the
  // property is over the plan's data rather than over a design's signals.
  property p_no_inert_passable_gate;
    @(posedge clk) disable iff (!rst_n) inert_system_passes == '0;
  endproperty
  assert property (p_no_inert_passable_gate)
    else $error("a gate can be satisfied by a system that is not running");

  property p_licence_requires_a_positive_observation;
    @(posedge clk) disable iff (!rst_n)
      gate_licensed |-> gate_pass;
  endproperty
  assert property (p_licence_requires_a_positive_observation)
    else $error("a gate granted a licence without passing");

  // And the two-sided companion -- 30.3 section 9's variety 8: a plan of
  // nothing but refusals satisfies the property above.
  property p_working_system_passes;
    @(posedge clk) disable iff (!rst_n)
      (eval && all_observables_nominal) |=> gate_pass;
  endproperty
  assert property (p_working_system_passes)
    else $error("a gate rejected a nominal system: the criterion is too strict");

  // ---- Section 7: stage order.
  property p_order_is_topological;
    @(posedge clk) disable iff (!rst_n)
      (validate && order_legal) |-> (violations == '0);
  endproperty
  assert property (p_order_is_topological)
    else $error("an order was declared legal with dependency violations");

  property p_relation_exists;
    @(posedge clk) disable iff (!rst_n) relation_declared;
  endproperty
  assert property (p_relation_exists)
    else $error("the plan has an order and no dependency relation");

  // ---- Section 8: the closure. The property that a single EDIT does not
  // license a single-variable claim.
  property p_single_variable_means_closure;
    @(posedge clk) disable iff (!rst_n)
      is_one_variable |-> (closure_count == 4'd1);
  endproperty
  assert property (p_single_variable_means_closure)
    else $error("an experiment was logged as one variable with a larger closure");

  property p_closure_contains_the_edit;
    @(posedge clk) disable iff (!rst_n)
      experiment |=> ((closure & $past(edited)) == $past(edited));
  endproperty
  assert property (p_closure_contains_the_edit)
    else $error("the closure omits a variable that was edited");

  property p_closure_is_a_fixed_point;
    @(posedge clk) disable iff (!rst_n)
      experiment |=> (closure_count >= edit_count);
  endproperty
  assert property (p_closure_is_a_fixed_point)
    else $error("the closure is smaller than the edit set");

  // ---- Section 9: the read-back's comparand. TWO properties, because the
  // whole item is that these are different facts.
  property p_value_checked_against_derivation;
    @(posedge clk) disable iff (!rst_n)
      row_ok |-> (read_value == derived_value);
  endproperty
  assert property (p_value_checked_against_derivation)
    else $error("a provenance row passed without matching its conversion");

  property p_write_path_and_value_are_separate;
    @(posedge clk) disable iff (!rst_n)
      (check && (read_value == written_value) && (read_value != derived_value))
        |=> (write_path_ok && !value_correct);
  endproperty
  assert property (p_write_path_and_value_are_separate)
    else $error("a wrong value with a working write path was not distinguished");

  // ---- Section 10: recovery survival.
  property p_reset_cleared_needs_capture_first;
    @(posedge clk) disable iff (!rst_n)
      (classify && !capture_preceded_recovery) |=> (lost_to_recovery != '0);
  endproperty
  assert property (p_reset_cleared_needs_capture_first)
    else $error("reset-cleared observables were reported trustworthy after recovery");

  property p_volatile_is_never_trustworthy_state;
    @(posedge clk) disable iff (!rst_n)
      classify |=> (trustworthy + lost_to_recovery + sampled_only == 4'd12);
  endproperty
  assert property (p_volatile_is_never_trustworthy_state)
    else $error("the survival classification does not account for every observable");

  // ---- Section 11: reduction. The signature, not the failure.
  property p_step_accepted_only_on_same_signature;
    @(posedge clk) disable iff (!rst_n)
      (step && reproduced && (sig_observed == baseline_sig))
        |=> (steps_accepted == $past(steps_accepted) + 1'b1);
  endproperty
  assert property (p_step_accepted_only_on_same_signature)
    else $error("a reduction step was accepted with a drifted signature");

  property p_signature_drift_breaks_the_chain;
    @(posedge clk) disable iff (!rst_n)
      (step && reproduced && (sig_observed != baseline_sig)) |=> !chain_intact;
  endproperty
  assert property (p_signature_drift_breaks_the_chain)
    else $error("signature drift did not break the reduction chain");

  // ---- Section 12: the repair. The revert is a CONJUNCT, which is the item.
  property p_repair_requires_a_revert;
    @(posedge clk) disable iff (!rst_n)
      repair_proved |-> (repro_fails_without_fix && repro_passes_with_fix
                         && regression_still_passes && (mechanism_len != '0));
  endproperty
  assert property (p_repair_requires_a_revert)
    else $error("a repair was proved without all four facts");

  property p_coincidence_is_classified;
    @(posedge clk) disable iff (!rst_n)
      (submit && repro_passes_with_fix && !repro_fails_without_fix)
        |=> (coincidence_count == $past(coincidence_count) + 1'b1);
  endproperty
  assert property (p_coincidence_is_classified)
    else $error("a coincidence was not distinguished from a repair");

  // ---- Section 13: failure as a result.
  property p_failure_is_classified;
    @(posedge clk) disable iff (!rst_n)
      stage_failed |=> classified;
  endproperty
  assert property (p_failure_is_classified)
    else $error("a stage failed and was not classified into a failure domain");

  property p_facts_gathered_on_failure;
    @(posedge clk) disable iff (!rst_n)
      stage_failed |=> (facts_gathered != '0);
  endproperty
  assert property (p_facts_gathered_on_failure)
    else $error("a failing stage gathered no facts");

  property p_stop_only_where_policy_says;
    @(posedge clk) disable iff (!rst_n)
      (stage_failed && (branch_taken == 3'd0)) |=> (stages_still_run == '0);
  endproperty
  assert property (p_stop_only_where_policy_says)
    else $error("the branch taken does not match the stage's declared policy");

  // ---- Section 14: the assumption ledger. The whole-plan property, and the
  // only one here whose antecedent is an audit rather than an event.
  property p_no_unlicensed_assumption;
    @(posedge clk) disable iff (!rst_n)
      audit |=> (unlicensed_count == '0);
  endproperty
  assert property (p_no_unlicensed_assumption)
    else $error("a stage assumes a fact no earlier gate established");

  property p_established_requires_a_passing_gate;
    @(posedge clk) disable iff (!rst_n)
      (audit && (gate_passed == '0)) |=> (established == '0);
  endproperty
  assert property (p_established_requires_a_passing_gate)
    else $error("facts were marked established with no gate passing");

  // ---- COVERS. Each on the dimension its defect scales with.
  // Section 6: the INERT SYSTEM run. The dimension is the system's state,
  // and running the plan on working hardware a thousand times never
  // reaches it -- 31.2 section 14's coverage-dimension rule.
  cover property (@(posedge clk) disable iff (!rst_n)
                  eval && !all_observables_nominal && gate_pass);
  // Section 7: an ILLEGAL permutation offered to the validator. Without
  // it, p_order_is_topological is satisfied by never validating.
  cover property (@(posedge clk) disable iff (!rst_n)
                  validate && (violations != '0));
  // Section 8: an experiment whose closure EXCEEDS its edit set. A log
  // of only atomic changes never reaches it.
  cover property (@(posedge clk) disable iff (!rst_n)
                  experiment && (closure_count > edit_count));
  // Section 9: a frequency bin where the division is INEXACT -- 28.2
  // section 10's point. At an exact bin floor and ceiling agree and the
  // cover is uninformative.
  cover property (@(posedge clk) disable iff (!rst_n)
                  check && (derived_value != written_value));
  // Section 10: capture AFTER recovery. The dimension is the recovery's
  // trigger -- operator or automatic -- and it belongs to the failure.
  cover property (@(posedge clk) disable iff (!rst_n)
                  classify && !capture_preceded_recovery);
  // Section 11: signature DRIFT with continued failure. A reduction that
  // either holds or stops never reaches it.
  cover property (@(posedge clk) disable iff (!rst_n)
                  step && reproduced && (sig_observed != baseline_sig));
  // Section 12: a repair whose revert PASSES -- the coincidence. A log
  // that never reverts cannot produce it.
  cover property (@(posedge clk) disable iff (!rst_n)
                  submit && repro_passes_with_fix && !repro_fails_without_fix);
  // Section 13: a failure at a stage whose policy is CONTINUE. A bring-up
  // that only ever fails at stages 1 and 2 never reaches it.
  cover property (@(posedge clk) disable iff (!rst_n)
                  stage_failed && (branch_taken == 3'd1));
  // Section 14: an audit with EVERY gate passing and unlicensed
  // assumptions remaining -- the state the weak plan is in.
  cover property (@(posedge clk) disable iff (!rst_n)
                  audit && (gate_passed == '1) && (unlicensed_count != '0));
  // And the positive companion: an audit that finds NONE, so
  // p_no_unlicensed_assumption is not satisfied by never auditing.
  cover property (@(posedge clk) disable iff (!rst_n)
                  audit && (unlicensed_count == '0));