JEDEC Compliance

   probability the assumption survives verification  =  f^n

// ---------------------------------------------------------------------
// compliance_rule_registry -- the primary artefact of a rule-organised
// suite: one record per obligation, with the five fields §5 requires.
//
// CLASSIFICATION: educational, SIMULATION-ONLY.
//
// WHAT IT DOES NOT MODEL:
//   - the standard, or any rule's actual content
//   - the design, any device, or any vendor model
//   - whether an interpretation is CORRECT. §5: the gap between a
//     standard's sentence and a team's reading is where
//     interoperability failures live, and no data structure closes it.
//
// WHAT IT WOULD MISS:
//   - a rule that was never enumerated. This is the big one. The
//     registry can report 100% discharged over a set that omits the
//     rule that fails qualification (§7), which is why
//     enumeration_reviewed is a field and not a comment.
//   - a rule enumerated wrongly -- invented, or split, or merged.
//   - anything about the QUALITY of a check. "Discharged by an
//     assertion" says an artefact exists, not that it is adequate.
// ---------------------------------------------------------------------
typedef enum int {
  RULE_NOT_ATTEMPTED = 0,   // a schedule item
  RULE_IN_PROGRESS   = 1,
  RULE_DISCHARGED    = 2,   // an artefact verifies it
  RULE_WAIVED        = 3,   // deliberately not verified, with a reason
  RULE_UNVERIFIABLE  = 4    // cannot be checked in this environment
} rule_status_e;

typedef enum int {
  CHK_NONE      = 0,
  CHK_ASSERTION = 1,        // a bindable property -- 27.2
  CHK_TEST      = 2,        // a directed or random test
  CHK_MONITOR   = 3,        // a passive check -- 27.3
  CHK_SCOREBOARD = 4,       // a data comparison -- 27.4
  CHK_REVIEW    = 5         // a human argument, not a simulation
} check_kind_e;

class compliance_rule extends uvm_object;
  `uvm_object_utils(compliance_rule)

  // ── §5's five required fields. All five, or the record is rejected.
  string        rule_id;          // which obligation
  string        source_citation;  // where in the standard
  string        interpretation;   // what WE took it to mean -- §5
  check_kind_e  check_kind;
  string        check_artefact;   // the name of the thing that checks it
  rule_status_e status;

  // Non-empty only for WAIVED and UNVERIFIABLE. §5: those are
  // different residuals and each needs its own reason.
  string        residual_reason;

  function new(string name = "compliance_rule");
    super.new(name);
    status     = RULE_NOT_ATTEMPTED;
    check_kind = CHK_NONE;
  endfunction

  // A record is well formed when its fields are mutually consistent.
  // Returns "" when valid, else the first problem found.
  function string validate();
    if (rule_id         == "") return "rule_id is empty";
    if (source_citation == "") return "source_citation is empty";
    // §5: a citation without an interpretation cannot be reviewed --
    // a reader can confirm the citation exists but not whether the
    // team understood it. So interpretation is REQUIRED, always.
    if (interpretation  == "") return "interpretation is empty";
    if (status == RULE_DISCHARGED) begin
      if (check_kind == CHK_NONE) return "discharged with no check kind";
      if (check_artefact == "")   return "discharged with no artefact named";
    end
    if (status inside {RULE_WAIVED, RULE_UNVERIFIABLE}) begin
      if (residual_reason == "")
        return "waived or unverifiable with no reason";
      // A residual must NOT claim a check. Doing so would let a rule
      // appear both unverified and covered.
      if (check_kind != CHK_NONE)
        return "residual rule must not name a check";
    end
    if (status == RULE_NOT_ATTEMPTED && check_artefact != "")
      return "not-attempted rule names an artefact";
    return "";
  endfunction
endclass


class compliance_registry extends uvm_component;
  `uvm_component_utils(compliance_registry)

  protected compliance_rule m_rules[string];   // by rule_id
  // §7: the enumeration is itself a deliverable with its own status,
  // and it BOUNDS every other claim this registry can make.
  protected bit    m_enumeration_reviewed;
  protected string m_enumeration_reviewer;
  protected int    m_rejected_records;

  function new(string name, uvm_component parent);
    super.new(name, parent);
    m_enumeration_reviewed = 0;
  endfunction

  // Returns 1 on acceptance. A malformed record is REJECTED, not
  // stored with a warning -- a registry holding invalid records
  // cannot support any completeness claim at all.
  function bit add_rule(compliance_rule r);
    string why;
    if (r == null) begin
      `uvm_error("REG", "null rule record")
      m_rejected_records++;
      return 0;
    end
    why = r.validate();
    if (why != "") begin
      `uvm_error("REG", $sformatf("rule '%s' rejected: %s", r.rule_id, why))
      m_rejected_records++;
      return 0;
    end
    if (m_rules.exists(r.rule_id)) begin
      // Duplicate ids would make the counts meaningless: the same
      // obligation could be discharged and not-attempted at once.
      `uvm_error("REG", $sformatf("duplicate rule_id '%s'", r.rule_id))
      m_rejected_records++;
      return 0;
    end
    m_rules[r.rule_id] = r;
    return 1;
  endfunction

  function void mark_enumeration_reviewed(string reviewer);
    if (reviewer == "") begin
      `uvm_error("REG", "enumeration review needs a named reviewer")
      return;
    end
    m_enumeration_reviewed = 1;
    m_enumeration_reviewer = reviewer;
  endfunction

  function int count_with_status(rule_status_e s);
    int n = 0;
    foreach (m_rules[id]) if (m_rules[id].status == s) n++;
    return n;
  endfunction

  function int total_rules();  return m_rules.size();       endfunction
  function int rejected();     return m_rejected_records;   endfunction
  function bit enumeration_reviewed(); return m_enumeration_reviewed; endfunction

  // §7: the honest statement is a residual, not a percentage. This
  // returns the FOUR numbers a counterparty actually needs, and it
  // deliberately does not compute a single score.
  function void residual(output int discharged, output int waived,
                         output int unverifiable, output int outstanding);
    discharged   = count_with_status(RULE_DISCHARGED);
    waived       = count_with_status(RULE_WAIVED);
    unverifiable = count_with_status(RULE_UNVERIFIABLE);
    outstanding  = count_with_status(RULE_NOT_ATTEMPTED)
                 + count_with_status(RULE_IN_PROGRESS);
  endfunction

  // A claim is only SUPPORTABLE when nothing is outstanding AND the
  // enumeration was reviewed. Note it can be supportable with a large
  // residual -- §7: waived and unverifiable rules are disclosed, not
  // disqualifying.
  function bit claim_supportable();
    int d, w, u, o;
    residual(d, w, u, o);
    return (o == 0) && m_enumeration_reviewed && (m_rejected_records == 0);
  endfunction

  function void report_phase(uvm_phase phase);
    int d, w, u, o;
    residual(d, w, u, o);
    `uvm_info("REG", $sformatf(
      "rules=%0d discharged=%0d waived=%0d unverifiable=%0d outstanding=%0d rejected=%0d enum_reviewed=%0b(%s) supportable=%0b",
      total_rules(), d, w, u, o, m_rejected_records,
      m_enumeration_reviewed, m_enumeration_reviewer, claim_supportable()), UVM_LOW)
  endfunction
endclass

// ---------------------------------------------------------------------
// compliance_rule_checker -- a bindable checker whose every property
// carries a rule identity, so a firing names the obligation it broke.
//
// CLASSIFICATION: educational, synthesisable, BINDABLE.
//
// WHY BINDABLE MATTERS: §2. The counterparty is external and arrives
// after a failure. A checker that reports "assertion 7 failed" needs
// a human to translate; one that reports a RULE ID answers the
// external question directly.
//
// WHAT IT DOES NOT MODEL:
//   - any real rule from any standard. The document was not
//     obtainable, so the rules below are ILLUSTRATIVE structural
//     ones and are NOT presented as JEDEC's.
//   - the array, any timing parameter, or any electrical behaviour
//
// WHAT IT WOULD MISS:
//   - every rule not expressible over the bound signals, which
//     includes all of Module 22's electrical subject matter
//   - a rule nobody enumerated (§7)
// ---------------------------------------------------------------------
module compliance_rule_checker #(
  parameter int BANKS    = 16,
  parameter int BANK_W   = $clog2(BANKS),
  // A COUNT of violations up to N needs clog2(N+1), not clog2(N).
  parameter int CNT_W    = 20
) (
  input  logic              clk,
  input  logic              rst_n,

  // ── Bound command interface. ILLUSTRATIVE encoding.
  input  logic              cmd_valid,
  input  logic [2:0]        cmd_code,      // 0 NOP 1 ACT 2 RD 3 WR 4 PRE 5 REF
  input  logic [BANK_W-1:0] cmd_bank,

  // ── Bound state, observed rather than reconstructed here. 27.3
  //    owns reconstruction; a bindable checker sees the DUT's own.
  input  logic [BANKS-1:0]  bank_open,
  input  logic              init_complete,

  // ── One violation flag per rule, so a firing names its obligation.
  output logic              v_r001_act_on_open_bank,
  output logic              v_r002_access_closed_bank,
  output logic              v_r003_refresh_with_bank_open,
  output logic              v_r004_command_before_init,
  output logic              v_r005_precharge_nothing_open,

  output logic [CNT_W-1:0]  cnt_violations,
  output logic              any_violation,
  // Which rule fired, as a mask, so a consumer can map a cycle onto
  // registry records without re-deriving the conditions.
  output logic [4:0]        rule_mask
);

  localparam logic [2:0] C_NOP = 3'd0, C_ACT = 3'd1, C_RD = 3'd2,
                         C_WR  = 3'd3, C_PRE = 3'd4, C_REF = 3'd5;

  initial begin
    if (BANKS < 2 || (BANKS & (BANKS - 1)) != 0)
      // The >= 2 bound matters: a power-of-two test ALONE accepts 0
      // and 1, and $clog2(1) is 0, which makes [BANK_W-1:0] illegal.
      // Module 24 and Module 26 each shipped this hole once.
      $fatal(1, "compliance_rule_checker: BANKS must be a power of two >= 2");
    if (BANK_W != $clog2(BANKS))
      $fatal(1, "compliance_rule_checker: BANK_W must address BANKS");
  end

  // Declared above the continuous assigns that read them.
  logic is_acc;
  assign is_acc = cmd_valid && ((cmd_code == C_RD) || (cmd_code == C_WR));

  logic bank_is_open;
  assign bank_is_open = bank_open[cmd_bank];

  logic any_open;
  assign any_open = (bank_open != '0);

  // ILLUSTRATIVE rules, each tagged with the identity a registry
  // record would carry. These are structural, not quoted.
  assign v_r001_act_on_open_bank      = cmd_valid && (cmd_code == C_ACT) && bank_is_open;
  assign v_r002_access_closed_bank    = is_acc && !bank_is_open;
  assign v_r003_refresh_with_bank_open = cmd_valid && (cmd_code == C_REF) && any_open;
  assign v_r004_command_before_init   = cmd_valid && (cmd_code != C_NOP) && !init_complete;
  // R005 -- a precharge issued when nothing is open. Harmless
  // electrically and still a rule: it indicates the controller's
  // model of bank state disagrees with the device's, which is the
  // condition that produces a real violation one command later.
  assign v_r005_precharge_nothing_open = cmd_valid && (cmd_code == C_PRE) && !any_open;

  logic [CNT_W-1:0] n_v;
  logic             viol_now;
  assign viol_now = v_r001_act_on_open_bank | v_r002_access_closed_bank
                  | v_r003_refresh_with_bank_open | v_r004_command_before_init
                  | v_r005_precharge_nothing_open;

  assign rule_mask = {v_r005_precharge_nothing_open, v_r004_command_before_init,
                      v_r003_refresh_with_bank_open, v_r002_access_closed_bank,
                      v_r001_act_on_open_bank};

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) n_v <= '0;
    else if (viol_now && (n_v != {CNT_W{1'b1}})) n_v <= n_v + CNT_W'(1);
  end

  assign cnt_violations = n_v;
  assign any_violation  = viol_now;
endmodule

// ---------------------------------------------------------------------
// vendor_agreement_check -- runs one stimulus against N vendor models
// and reports where they disagree.
//
// CLASSIFICATION: educational, SIMULATION-ONLY.
//
// WHY IT EXISTS: 1.4 prescribes verifying "against multiple vendor
// models", and §3 shows why -- a single model is one legal sample from
// a space of legal devices.
//
// WHAT IT DOES NOT MODEL:
//   - any vendor's model, or any device
//   - WHICH model is right when two disagree. A disagreement is a
//     finding requiring human adjudication against the standard, and
//     this block escalates rather than resolving.
//
// WHAT IT WOULD MISS:
//   - a CORRELATED error. §3's callout: models implement the same
//     standard, often from the same reference behaviour, and may
//     share an ambiguity reading. Two models agreeing and both being
//     wrong is invisible here, and it is the failure mode that
//     matters most.
//   - any behaviour the stimulus never creates.
// ---------------------------------------------------------------------
class vendor_response extends uvm_object;
  `uvm_object_utils(vendor_response)
  string        model_name;
  logic [63:0]  data;
  bit           has_data;      // some responses carry no data
  bit           flagged_error; // the model reported the stimulus illegal
  function new(string name = "vendor_response"); super.new(name); endfunction

  // Two responses agree when they agree on ALL THREE observable
  // facts. Comparing only data would call "error" and "no error"
  // agreement whenever the data field happened to match.
  function bit agrees_with(vendor_response other);
    if (other == null) return 0;
    if (flagged_error != other.flagged_error) return 0;
    if (has_data      != other.has_data)      return 0;
    if (has_data && (data != other.data))     return 0;
    return 1;
  endfunction
endclass


class vendor_agreement_check extends uvm_component;
  `uvm_component_utils(vendor_agreement_check)

  protected int m_stimuli;
  protected int m_unanimous;
  protected int m_disagreements;
  protected int m_single_model_runs;   // §3: runs that prove nothing
  protected int m_min_models_seen;

  function new(string name, uvm_component parent);
    super.new(name, parent);
    m_min_models_seen = -1;
  endfunction

  // Returns 1 when every model agreed. A run with FEWER THAN TWO
  // models is counted separately and never reported as agreement --
  // §3: one model cannot agree with anything.
  function bit check_stimulus(string stim_id, vendor_response resp[$]);
    bit unanimous = 1;
    m_stimuli++;
    if (resp.size() < 2) begin
      m_single_model_runs++;
      `uvm_warning("VENDOR", $sformatf(
        "stimulus '%s' ran against %0d model(s): agreement is undefined below two",
        stim_id, resp.size()))
      if (m_min_models_seen < 0 || resp.size() < m_min_models_seen)
        m_min_models_seen = resp.size();
      return 0;
    end
    if (m_min_models_seen < 0 || resp.size() < m_min_models_seen)
      m_min_models_seen = resp.size();

    for (int i = 1; i < resp.size(); i++) begin
      if (!resp[0].agrees_with(resp[i])) begin
        unanimous = 0;
        // Escalated, not resolved. Which model is right is a question
        // about the standard, and this block does not have it.
        `uvm_error("VENDOR", $sformatf(
          "stimulus '%s': model '%s' disagrees with '%s' -- adjudicate against the standard",
          stim_id, resp[i].model_name, resp[0].model_name))
      end
    end
    if (unanimous) m_unanimous++;
    else           m_disagreements++;
    return unanimous;
  endfunction

  function int stimuli();          return m_stimuli;           endfunction
  function int unanimous();        return m_unanimous;         endfunction
  function int disagreements();    return m_disagreements;     endfunction
  function int single_model_runs(); return m_single_model_runs; endfunction
  function int min_models();       return m_min_models_seen;   endfunction

  // §3: the strength of an agreement claim is bounded by the SMALLEST
  // number of models any stimulus ran against, not the largest.
  function bit multi_model_claim_supportable();
    return (m_single_model_runs == 0) && (m_min_models_seen >= 2);
  endfunction

  function void report_phase(uvm_phase phase);
    `uvm_info("VENDOR", $sformatf(
      "stimuli=%0d unanimous=%0d disagreements=%0d single_model_runs=%0d min_models=%0d supportable=%0b",
      m_stimuli, m_unanimous, m_disagreements, m_single_model_runs,
      m_min_models_seen, multi_model_claim_supportable()), UVM_LOW)
  endfunction
endclass

// Bind unit note: P1-P12 reference compliance_rule_checker's internals.
// P13-P18 are written as immediate assertions over the SIMULATION-ONLY
// registry and cross-check, since those are classes rather than
// modules and carry no clock.

// ── Bindable, over compliance_rule_checker.

// P1 -- FORBIDDEN. An activate to an already-open bank is always
// flagged. ILLUSTRATIVE rule R001, structural not quoted.
property p_r001_always_flagged;
  @(posedge clk) disable iff (!rst_n)
    (cmd_valid && (cmd_code == 3'd1) && bank_open[cmd_bank])
      |-> v_r001_act_on_open_bank;
endproperty
assert property (p_r001_always_flagged);

// P2 -- FORBIDDEN. An access to a closed bank is always flagged.
property p_r002_always_flagged;
  @(posedge clk) disable iff (!rst_n)
    (cmd_valid && ((cmd_code == 3'd2) || (cmd_code == 3'd3))
     && !bank_open[cmd_bank]) |-> v_r002_access_closed_bank;
endproperty
assert property (p_r002_always_flagged);

// P3 -- FORBIDDEN. A refresh with any bank open is always flagged.
property p_r003_always_flagged;
  @(posedge clk) disable iff (!rst_n)
    (cmd_valid && (cmd_code == 3'd5) && (bank_open != '0))
      |-> v_r003_refresh_with_bank_open;
endproperty
assert property (p_r003_always_flagged);

// P4 -- FORBIDDEN. Any non-NOP command before initialisation is
// flagged. The one rule here that does not depend on bank state.
property p_r004_always_flagged;
  @(posedge clk) disable iff (!rst_n)
    (cmd_valid && (cmd_code != 3'd0) && !init_complete)
      |-> v_r004_command_before_init;
endproperty
assert property (p_r004_always_flagged);

// P5 -- no rule flag asserts without a command. A checker that
// flagged on an idle cycle would attribute a violation to a
// command that was never issued.
property p_no_flag_without_command;
  @(posedge clk) disable iff (!rst_n)
    !cmd_valid |-> !any_violation;
endproperty
assert property (p_no_flag_without_command);

// P6 -- INVARIANT. any_violation is exactly the disjunction of the
// five rule flags. An aggregate that could assert alone would be a
// violation with no obligation attached, which §12's design forbids.
property p_aggregate_is_the_disjunction;
  @(posedge clk) disable iff (!rst_n)
    any_violation == (|rule_mask);
endproperty
assert property (p_aggregate_is_the_disjunction);

// P7 -- INVARIANT. The mask's bits are exactly the individual flags,
// in a fixed order. A consumer maps a mask bit onto a registry
// record, so a reordering would silently misattribute violations.
property p_mask_matches_the_flags;
  @(posedge clk) disable iff (!rst_n)
    rule_mask == {v_r005_precharge_nothing_open, v_r004_command_before_init,
                  v_r003_refresh_with_bank_open, v_r002_access_closed_bank,
                  v_r001_act_on_open_bank};
endproperty
assert property (p_mask_matches_the_flags);

// P8 -- FORBIDDEN. R001 and R002 are mutually exclusive, because they
// require different command codes. Both firing at once would mean the
// command decode is ambiguous.
property p_r001_r002_exclusive;
  @(posedge clk) disable iff (!rst_n)
    !(v_r001_act_on_open_bank && v_r002_access_closed_bank);
endproperty
assert property (p_r001_r002_exclusive);

// P9 -- R004 dominates: before initialisation, EVERY non-NOP command
// is flagged regardless of bank state. A checker that let bank state
// suppress R004 would pass traffic issued before the device was ready.
property p_r004_dominates_before_init;
  @(posedge clk) disable iff (!rst_n)
    (cmd_valid && (cmd_code != 3'd0) && !init_complete) |-> any_violation;
endproperty
assert property (p_r004_dominates_before_init);

// P10 -- FORBIDDEN. A precharge with nothing open is always flagged.
// §12: harmless electrically, and evidence the controller's model of
// bank state has diverged from the device's.
property p_r005_always_flagged;
  @(posedge clk) disable iff (!rst_n)
    (cmd_valid && (cmd_code == 3'd4) && (bank_open == '0))
      |-> v_r005_precharge_nothing_open;
endproperty
assert property (p_r005_always_flagged);

// P11 -- the counter advances exactly once per violating cycle,
// however many rules fired in it. Counting rules rather than cycles
// would make one bad command look like several.
property p_counter_counts_cycles_not_rules;
  @(posedge clk) disable iff (!rst_n)
    (any_violation && (cnt_violations != {CNT_W{1'b1}}))
      |=> (cnt_violations == $past(cnt_violations, 1) + CNT_W'(1));
endproperty
assert property (p_counter_counts_cycles_not_rules);

// P12 -- INVARIANT. The counter never decreases. A violation record
// that could unwind would let a passing final state hide a failure.
property p_counter_is_monotone;
  @(posedge clk) disable iff (!rst_n)
    (cnt_violations >= $past(cnt_violations, 1));
endproperty
assert property (p_counter_is_monotone);

// ── Cover, over the bindable checker. Each ILLUSTRATIVE rule must be
// ATTEMPTED or its property is vacuous -- 27.2 §5 measures how much
// of this curriculum's corpus is exposed to exactly that.
cover property (@(posedge clk) disable iff (!rst_n) v_r001_act_on_open_bank);
cover property (@(posedge clk) disable iff (!rst_n) v_r002_access_closed_bank);
cover property (@(posedge clk) disable iff (!rst_n) v_r003_refresh_with_bank_open);
cover property (@(posedge clk) disable iff (!rst_n) v_r004_command_before_init);
cover property (@(posedge clk) disable iff (!rst_n) v_r005_precharge_nothing_open);
// The mask carrying exactly one bit, and more than one -- P11
// distinguishes those cases and a suite must reach both.
cover property (@(posedge clk) disable iff (!rst_n) $onehot(rule_mask));
// A clean run: commands issued, no rule broken. Without this cover a
// suite could be flagging everything and still pass P1-P8.
cover property (@(posedge clk) disable iff (!rst_n) cmd_valid && !any_violation);
// Two rules broken in one cycle -- the case P7 distinguishes.
cover property (@(posedge clk) disable iff (!rst_n)
                  $countones(rule_mask) > 1);
// Commands before and after initialisation, so R004's antecedent is
// reached in both directions.
cover property (@(posedge clk) disable iff (!rst_n) cmd_valid && init_complete);
cover property (@(posedge clk) disable iff (!rst_n) cmd_valid && !init_complete);
// Every bank exercised at the extremes of the index.
cover property (@(posedge clk) disable iff (!rst_n) cmd_valid && (cmd_bank == '0));
cover property (@(posedge clk) disable iff (!rst_n)
                  cmd_valid && (cmd_bank == BANK_W'(BANKS - 1)));

// SIMULATION-ONLY. Immediate assertions over the registry's and the
// cross-check's invariants -- the class equivalents of P1-P12.
task automatic check_registry_invariants(compliance_registry reg_h,
                                         vendor_agreement_check va_h);
  int d, w, u, o;
  reg_h.residual(d, w, u, o);

  // P13 -- the four residual categories partition the rule set exactly.
  // A rule in no category, or in two, would make every count wrong.
  assert (d + w + u + o == reg_h.total_rules())
    else $error("P13: residual categories do not partition %0d rules", reg_h.total_rules());

  // P14 -- FORBIDDEN. A claim is never supportable while anything is
  // outstanding. §7: waived and unverifiable are disclosed; an
  // outstanding rule is simply unfinished.
  assert (!(reg_h.claim_supportable() && (o > 0)))
    else $error("P14: claim reported supportable with %0d outstanding rules", o);

  // P15 -- FORBIDDEN. A claim is never supportable without a reviewed
  // enumeration. §7: the extraction bounds every other claim.
  assert (!(reg_h.claim_supportable() && !reg_h.enumeration_reviewed()))
    else $error("P15: claim reported supportable with an unreviewed enumeration");

  // P16 -- a rejected record never enters the counts. A registry
  // holding invalid records cannot support any completeness claim.
  assert (!(reg_h.claim_supportable() && (reg_h.rejected() > 0)))
    else $error("P16: claim supportable with %0d rejected records", reg_h.rejected());

  // P17 -- FORBIDDEN. Agreement is never claimed below two models.
  // §3: one model cannot agree with anything.
  assert (!(va_h.multi_model_claim_supportable() && (va_h.min_models() < 2)))
    else $error("P17: multi-model claim supportable with min_models=%0d", va_h.min_models());

  // P18 -- unanimous and disagreeing runs partition the multi-model
  // stimuli, with single-model runs excluded from both.
  assert (va_h.unanimous() + va_h.disagreements() + va_h.single_model_runs()
          == va_h.stimuli())
    else $error("P18: agreement outcomes do not partition %0d stimuli", va_h.stimuli());
endtask

// SIMULATION-ONLY. Independent reference for the registry's
// accounting, holding records in a QUEUE and counting by iteration
// rather than by the DUT's own status tallies -- so agreement is
// evidence rather than a restatement.
class registry_reference;
  typedef struct {
    string        id;
    rule_status_e st;
    bit           has_artefact;
    bit           has_reason;
    bit           has_interp;
  } rec_t;
  rec_t recs[$];

  function bit would_accept(rec_t r);
    if (r.id == "" || !r.has_interp) return 0;
    if (r.st == RULE_DISCHARGED && !r.has_artefact) return 0;
    if (r.st inside {RULE_WAIVED, RULE_UNVERIFIABLE} && !r.has_reason) return 0;
    if (r.st == RULE_NOT_ATTEMPTED && r.has_artefact) return 0;
    foreach (recs[i]) if (recs[i].id == r.id) return 0;   // duplicate
    return 1;
  endfunction

  function void add(rec_t r);
    if (would_accept(r)) recs.push_back(r);
  endfunction

  function int count(rule_status_e s);
    int n = 0;
    foreach (recs[i]) if (recs[i].st == s) n++;
    return n;
  endfunction

  function int total(); return recs.size(); endfunction
endclass

  THE SUITE THAT DISCHARGED EVERY RULE AND PROVES NOTHING

    rules enumerated         412
    discharged               412
    waived                     0
    unverifiable               0
    outstanding                0
    rejected records           0
    enumeration_reviewed       0     <-- nobody checked the extraction

    the percentage a report would quote :  412/412 = 100%
    claim_supportable()                 :  FALSE

    assertions : P13 residual partitions          PASS
                 P14 not supportable if outstanding PASS
                 P15 not supportable if unreviewed  PASS  <-- this one
                 P16 no rejected records            PASS
                 every property                     PASS

    diagnosis : the suite is internally perfect and externally
      unsupported. Every rule the team extracted is discharged, and
      nothing establishes that the extraction resembles the standard.
      §7: five layers of self-selection, and this run has verified
      the inner four while leaving the outermost untouched.

    what makes it dangerous : 100% is the number that gets reported,
      and it is true. The missing field is a boolean nobody asked
      for, and 1.4's qualification failure lives exactly there --
      "found at qualification with a second supplier, which is late
      and expensive."

    the fix : enumeration_reviewed is a REQUIRED input to
      claim_supportable(), not an advisory field. A suite cannot
      review its own extraction, so the check must be a gate rather
      than a metric.