DDR Assertions

// ---------------------------------------------------------------------
// ddr_spacing_property_set -- one property of each class from §10,
// written over a bound command interface, with an antecedent-reach
// output for every implication so vacuity is measurable.
//
// CLASSIFICATION: educational, synthesisable, BINDABLE.
//
// WHY EVERY IMPLICATION PUBLISHES ITS ANTECEDENT: §4. A property's
// checking value is bounded by how often its antecedent occurs, and
// nothing in the property's text reveals that. Publishing the
// antecedent as a signal lets §13's monitor count it.
//
// WHAT IT DOES NOT MODEL:
//   - the device, the array, or any real timing parameter. SPACING is
//     ILLUSTRATIVE; Module 14 owns the real values and their names.
//   - electrical behaviour (Module 22), which no property here reaches
//
// WHAT IT WOULD MISS:
//   - any rule whose antecedent this testbench never creates (§2)
//   - any rule not expressible over the bound signals
// ---------------------------------------------------------------------
module ddr_spacing_property_set #(
  parameter int BANKS   = 16,
  parameter int BANK_W  = $clog2(BANKS),
  parameter int SPACING = 3,            // ILLUSTRATIVE (§5)
  // A COUNT of trips up to N needs clog2(N+1), not clog2(N).
  parameter int CNT_W   = 20
) (
  input  logic              clk,
  input  logic              rst_n,

  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,
  input  logic [BANKS-1:0]  bank_open,
  input  logic              init_complete,

  // ── Antecedent-reach outputs, one per implication class. §4: these
  //    exist so a suite can prove the property was evaluated.
  output logic              ant_spacing,     // an ACT was observed
  output logic              ant_forbidden,   // an illegal access attempted
  output logic              ant_monotone,    // the counter advanced

  // ── Observable results.
  output logic              trip_spacing,
  output logic              trip_forbidden,
  output logic [CNT_W-1:0]  n_trips,
  output logic [BANK_W-1:0] last_act_bank,
  output logic [3:0]        cycles_since_act
);

  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, making [BANK_W-1:0] illegal.
      $fatal(1, "ddr_spacing_property_set: BANKS must be a power of two >= 2");
    if (BANK_W != $clog2(BANKS))
      $fatal(1, "ddr_spacing_property_set: BANK_W must address BANKS");
    if (SPACING < 1)
      $fatal(1, "ddr_spacing_property_set: SPACING must be at least 1");
    if ((1 << 4) <= SPACING)
      // cycles_since_act must be able to represent the whole window,
      // or the spacing check saturates and stops firing -- silently.
      $fatal(1, "ddr_spacing_property_set: cycles_since_act too narrow for SPACING");
  end

  logic [BANK_W-1:0] act_bank_q;
  logic [3:0]        since_q;
  logic              have_act;
  logic [CNT_W-1:0]  trips_q;

  // 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 same_bank_acc;
  assign same_bank_acc = is_acc && have_act && (cmd_bank == act_bank_q);

  // §5's rule: an access to the activated bank inside the window.
  logic spacing_violated;
  assign spacing_violated = same_bank_acc && (since_q < 4'(SPACING));

  // §10's forbidden-transition class: an access to a bank that is not
  // open at all.
  logic forbidden_now;
  assign forbidden_now = is_acc && !bank_open[cmd_bank];

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      act_bank_q <= '0; since_q <= '0; have_act <= 1'b0; trips_q <= '0;
    end else begin
      if (cmd_valid && (cmd_code == C_ACT)) begin
        act_bank_q <= cmd_bank;
        since_q    <= '0;
        have_act   <= 1'b1;
      end else if (have_act && (since_q != 4'hF)) begin
        since_q <= since_q + 4'd1;
      end
      // Compare the INCREMENTED trip count combinationally where it
      // is published, not here -- trips_q's write lands on this edge.
      if ((spacing_violated || forbidden_now) && (trips_q != {CNT_W{1'b1}}))
        trips_q <= trips_q + CNT_W'(1);
    end
  end

  assign ant_spacing      = cmd_valid && (cmd_code == C_ACT);
  assign ant_forbidden    = is_acc;
  assign ant_monotone     = spacing_violated || forbidden_now;
  assign trip_spacing     = spacing_violated;
  assign trip_forbidden   = forbidden_now;
  assign n_trips          = trips_q;
  assign last_act_bank    = act_bank_q;
  assign cycles_since_act = since_q;
endmodule

// ---------------------------------------------------------------------
// vacuity_harness -- per-property antecedent and firing counts, and a
// verdict on which properties were never evaluated at all.
//
// CLASSIFICATION: educational, SIMULATION-ONLY.
//
// WHY IT EXISTS: §2 measures that 662 of this curriculum's 843
// properties are implications, and an implication whose antecedent
// never occurs PASSES. The tool reports success; the harness reports
// whether success meant anything.
//
// WHAT IT DOES NOT MODEL:
//   - the properties, the design, or any protocol
//   - whether a property is CORRECT. A wrong property with a reached
//     antecedent is measured as well-exercised.
//
// WHAT IT WOULD MISS:
//   - antecedent VARIETY. §6's callout: 1 and 10,000 are both
//     "covered" and are not the same evidence. This counts
//     occurrences, not distinct situations, so a property reached
//     only by one repeated stimulus scores as well-exercised.
//   - a property nobody registered. The harness can report every
//     registered property as evaluated and be silent about the rule
//     that has no property at all -- 27.1 §7's structural limit.
// ---------------------------------------------------------------------
typedef enum int {
  PROP_INVARIANT   = 0,   // §2: no antecedent, cannot be vacuous
  PROP_IMPLICATION = 1    // §2: exposed
} prop_shape_e;

class prop_record extends uvm_object;
  `uvm_object_utils(prop_record)

  string       prop_name;
  prop_shape_e shape;
  bit          has_reset_guard;   // §7: 74 of 843 lack one
  int unsigned antecedent_hits;
  int unsigned fire_count;

  function new(string name = "prop_record");
    super.new(name);
    shape = PROP_IMPLICATION;
    has_reset_guard = 1;
  endfunction

  // §2: an invariant is never vacuous, whatever its counts. An
  // implication is vacuous exactly when its antecedent never
  // occurred. Conflating the two would report 181 of this
  // curriculum's properties as at-risk when they structurally are not.
  function bit is_vacuous();
    if (shape == PROP_INVARIANT) return 0;
    return (antecedent_hits == 0);
  endfunction

  // A property that fired more often than its antecedent was reached
  // is an accounting error, not a very effective property.
  function bit counts_consistent();
    if (shape == PROP_INVARIANT) return 1;
    return (fire_count <= antecedent_hits);
  endfunction
endclass


class vacuity_harness extends uvm_component;
  `uvm_component_utils(vacuity_harness)

  protected prop_record m_props[string];
  protected int         m_rejected;

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

  function bit register(string prop_name, prop_shape_e shape,
                        bit has_reset_guard);
    prop_record r;
    if (prop_name == "") begin
      `uvm_error("VAC", "property registered with an empty name")
      m_rejected++;
      return 0;
    end
    if (m_props.exists(prop_name)) begin
      // Duplicate names would merge two properties' counts and make
      // both verdicts meaningless.
      `uvm_error("VAC", $sformatf("duplicate property name '%s'", prop_name))
      m_rejected++;
      return 0;
    end
    r = prop_record::type_id::create(prop_name);
    r.prop_name       = prop_name;
    r.shape           = shape;
    r.has_reset_guard = has_reset_guard;
    m_props[prop_name] = r;
    return 1;
  endfunction

  function void note_antecedent(string prop_name);
    if (!m_props.exists(prop_name)) begin
      `uvm_error("VAC", $sformatf("antecedent noted for unregistered '%s'", prop_name))
      return;
    end
    // An invariant has no antecedent to reach. Accepting one would
    // make its is_vacuous() verdict depend on a count that should
    // not exist.
    if (m_props[prop_name].shape == PROP_INVARIANT) begin
      `uvm_error("VAC", $sformatf("antecedent noted for invariant '%s'", prop_name))
      return;
    end
    m_props[prop_name].antecedent_hits++;
  endfunction

  function void note_fire(string prop_name);
    if (!m_props.exists(prop_name)) begin
      `uvm_error("VAC", $sformatf("fire noted for unregistered '%s'", prop_name))
      return;
    end
    m_props[prop_name].fire_count++;
  endfunction

  function int total();      return m_props.size(); endfunction
  function int rejected();   return m_rejected;     endfunction

  function int count_vacuous();
    int n = 0;
    foreach (m_props[k]) if (m_props[k].is_vacuous()) n++;
    return n;
  endfunction

  function int count_implications();
    int n = 0;
    foreach (m_props[k]) if (m_props[k].shape == PROP_IMPLICATION) n++;
    return n;
  endfunction

  function int count_invariants();
    int n = 0;
    foreach (m_props[k]) if (m_props[k].shape == PROP_INVARIANT) n++;
    return n;
  endfunction

  // §7: an unguarded property is a separate risk from a vacuous one,
  // reported separately because the mitigations differ.
  function int count_unguarded();
    int n = 0;
    foreach (m_props[k]) if (!m_props[k].has_reset_guard) n++;
    return n;
  endfunction

  function int count_inconsistent();
    int n = 0;
    foreach (m_props[k]) if (!m_props[k].counts_consistent()) n++;
    return n;
  endfunction

  // A suite's assertion result is SUPPORTABLE when no implication
  // went unevaluated and no counts are inconsistent. Note an
  // unguarded property does NOT make it unsupportable -- §7: some of
  // the 74 are legitimately guard-free, and the harness cannot tell
  // which, so it reports rather than blocks.
  function bit result_supportable();
    return (count_vacuous() == 0) && (count_inconsistent() == 0)
           && (m_rejected == 0);
  endfunction

  function void report_phase(uvm_phase phase);
    `uvm_info("VAC", $sformatf(
      "props=%0d impl=%0d inv=%0d vacuous=%0d unguarded=%0d inconsistent=%0d rejected=%0d supportable=%0b",
      total(), count_implications(), count_invariants(), count_vacuous(),
      count_unguarded(), count_inconsistent(), m_rejected,
      result_supportable()), UVM_LOW)
    foreach (m_props[k])
      if (m_props[k].is_vacuous())
        `uvm_error("VAC", $sformatf(
          "property '%s' PASSED VACUOUSLY -- antecedent never reached", k))
  endfunction
endclass

// ---------------------------------------------------------------------
// antecedent_variety_monitor -- how many DISTINCT situations reached
// each antecedent, rather than how many times.
//
// CLASSIFICATION: educational, SIMULATION-ONLY.
//
// WHY IT EXISTS: §12's harness cannot see variety, and §6's callout
// establishes that 1 and 10,000 are both "covered" while being very
// different evidence. A property reached only by one repeated
// stimulus is exercised in one situation, however many times.
//
// WHAT IT DOES NOT MODEL:
//   - the property, the design, or the protocol
//   - whether a situation MATTERS. All distinct keys count equally,
//     and a dimension that does not affect the rule inflates the
//     variety figure without improving the evidence.
//
// WHAT IT WOULD MISS:
//   - a situation dimension nobody recorded. Variety is measured over
//     the supplied keys, so ten distinct situations along an
//     unrecorded axis read as one.
// ---------------------------------------------------------------------
class antecedent_variety_monitor extends uvm_component;
  `uvm_component_utils(antecedent_variety_monitor)

  // per property: set of distinct situation keys seen
  protected bit m_seen[string][string];
  protected int m_hits[string];
  protected int m_min_variety_required;

  function new(string name, uvm_component parent);
    super.new(name, parent);
    m_min_variety_required = 2;   // ILLUSTRATIVE default
  endfunction

  function void set_min_variety(int n);
    if (n < 1) begin
      `uvm_error("VAR", "minimum variety must be at least 1")
      return;
    end
    m_min_variety_required = n;
  endfunction

  // situation_key encodes the dimensions a reviewer considers
  // relevant -- for example "bank=5,open=1,init=1". The monitor does
  // not interpret it; it only distinguishes.
  function void note(string prop_name, string situation_key);
    if (prop_name == "" || situation_key == "") begin
      `uvm_error("VAR", "note() needs a property name and a situation key")
      return;
    end
    m_hits[prop_name]++;
    m_seen[prop_name][situation_key] = 1;
  endfunction

  function int hits(string prop_name);
    return m_hits.exists(prop_name) ? m_hits[prop_name] : 0;
  endfunction

  function int variety(string prop_name);
    return m_seen.exists(prop_name) ? m_seen[prop_name].num() : 0;
  endfunction

  // The distinction the chapter is about: reached often, in one way.
  function bit reached_but_monotonous(string prop_name);
    return (hits(prop_name) > 0)
        && (variety(prop_name) < m_min_variety_required);
  endfunction

  function int count_monotonous();
    int n = 0;
    foreach (m_hits[k]) if (reached_but_monotonous(k)) n++;
    return n;
  endfunction

  function void report_phase(uvm_phase phase);
    foreach (m_hits[k])
      `uvm_info("VAR", $sformatf(
        "property '%s': hits=%0d variety=%0d monotonous=%0b",
        k, hits(k), variety(k), reached_but_monotonous(k)), UVM_HIGH)
    `uvm_info("VAR", $sformatf("monotonous properties: %0d of %0d",
      count_monotonous(), m_hits.size()), UVM_LOW)
  endfunction
endclass

// Bind unit note: P1-P12 reference ddr_spacing_property_set's
// internals. P13-P20 are immediate assertions over the SIMULATION-ONLY
// harness and monitor, which are classes and carry no clock.

// ── Bindable, over the property set.

// P1 -- FORBIDDEN. An access inside the spacing window always trips.
// §5's rule, as the property the waveform shows firing.
property p_spacing_violation_trips;
  @(posedge clk) disable iff (!rst_n)
    (cmd_valid && ((cmd_code == 3'd2) || (cmd_code == 3'd3))
     && (cmd_bank == last_act_bank) && (cycles_since_act < 4'(SPACING)))
      |-> trip_spacing;
endproperty
assert property (p_spacing_violation_trips);

// P2 -- FORBIDDEN. An access at or beyond the window never trips the
// spacing rule. §5's second sequence -- the legal half of the trace.
property p_legal_spacing_never_trips;
  @(posedge clk) disable iff (!rst_n)
    (cmd_valid && ((cmd_code == 3'd2) || (cmd_code == 3'd3))
     && (cycles_since_act >= 4'(SPACING))) |-> !trip_spacing;
endproperty
assert property (p_legal_spacing_never_trips);

// P3 -- FORBIDDEN. An access to a bank that is not open always trips
// the forbidden rule. §10's highest-value class.
property p_forbidden_access_trips;
  @(posedge clk) disable iff (!rst_n)
    (cmd_valid && ((cmd_code == 3'd2) || (cmd_code == 3'd3))
     && !bank_open[cmd_bank]) |-> trip_forbidden;
endproperty
assert property (p_forbidden_access_trips);

// P4 -- INVARIANT (§10's second class, structurally non-vacuous).
// The trip count never decreases.
property p_trip_count_monotone;
  @(posedge clk) disable iff (!rst_n)
    (n_trips >= $past(n_trips, 1));
endproperty
assert property (p_trip_count_monotone);

// P5 -- the count advances exactly once per tripping cycle, however
// many rules tripped in it. Counting rules would inflate one bad
// command into several.
property p_count_counts_cycles;
  @(posedge clk) disable iff (!rst_n)
    ((trip_spacing || trip_forbidden) && (n_trips != {CNT_W{1'b1}}))
      |=> (n_trips == $past(n_trips, 1) + CNT_W'(1));
endproperty
assert property (p_count_counts_cycles);

// P6 -- INVARIANT. The spacing counter never exceeds its width's
// maximum, so the window comparison cannot wrap and stop firing.
property p_since_never_wraps;
  @(posedge clk) disable iff (!rst_n)
    (cycles_since_act <= 4'hF);
endproperty
assert property (p_since_never_wraps);

// P7 -- an activate resets the spacing counter on the next cycle.
// §5: the antecedent is one cycle and the obligation outlives it, so
// the counter is what carries the obligation forward.
property p_act_restarts_the_window;
  @(posedge clk) disable iff (!rst_n)
    (cmd_valid && (cmd_code == 3'd1)) |=> (cycles_since_act == '0);
endproperty
assert property (p_act_restarts_the_window);

// P8 -- the counter advances on every non-activate cycle once an
// activate has been seen. A counter that stalled would let a late
// access appear to be inside the window forever.
property p_window_advances;
  @(posedge clk) disable iff (!rst_n)
    (!(cmd_valid && (cmd_code == 3'd1)) && ($past(cycles_since_act,1) < 4'hF)
     && $past(ant_spacing,1) == 1'b0 && $past(rst_n,1))
      |-> (cycles_since_act >= $past(cycles_since_act, 1));
endproperty
assert property (p_window_advances);

// P9 -- §4's requirement, as a property: every implication publishes
// an antecedent signal, and it is exactly the trigger condition.
property p_spacing_antecedent_is_the_activate;
  @(posedge clk) disable iff (!rst_n)
    ant_spacing == (cmd_valid && (cmd_code == 3'd1));
endproperty
assert property (p_spacing_antecedent_is_the_activate);

// P10 -- likewise for the forbidden class's antecedent.
property p_forbidden_antecedent_is_the_access;
  @(posedge clk) disable iff (!rst_n)
    ant_forbidden == (cmd_valid && ((cmd_code == 3'd2) || (cmd_code == 3'd3)));
endproperty
assert property (p_forbidden_antecedent_is_the_access);

// P11 -- FORBIDDEN. No trip without a command. A property firing on
// an idle cycle would attribute a violation to no stimulus.
property p_no_trip_without_command;
  @(posedge clk) disable iff (!rst_n)
    !cmd_valid |-> (!trip_spacing && !trip_forbidden);
endproperty
assert property (p_no_trip_without_command);

// P12 -- FORBIDDEN. No spacing trip before any activate has been
// observed. The rule has no meaning until its antecedent has occurred
// at least once, and firing earlier would be a false positive.
property p_no_spacing_trip_before_first_act;
  @(posedge clk) disable iff (!rst_n)
    (!$past(ant_spacing, 1) && (n_trips == '0)) |-> !trip_spacing;
endproperty
assert property (p_no_spacing_trip_before_first_act);

// ── Cover. §6: a property forbidding something is vacuous until the
// testbench attempts it, so every forbidden condition is covered --
// and the ANTECEDENTS are covered separately from the outcomes.

// The two trips, actually reached.
cover property (@(posedge clk) disable iff (!rst_n) trip_spacing);
cover property (@(posedge clk) disable iff (!rst_n) trip_forbidden);
// The two ANTECEDENTS, separately -- §4: a consequent that held and
// an antecedent that was reached are different evidence.
cover property (@(posedge clk) disable iff (!rst_n) ant_spacing);
cover property (@(posedge clk) disable iff (!rst_n) ant_forbidden);
// The LEGAL half of §5's trace: antecedent reached, consequent
// satisfied. Without this a suite could trip on everything and pass.
cover property (@(posedge clk) disable iff (!rst_n)
                  ant_forbidden && !trip_spacing && !trip_forbidden);
// The window at each interesting boundary: just inside, exactly at,
// and beyond. The exactly-at case is the one an off-by-one breaks.
cover property (@(posedge clk) disable iff (!rst_n)
                  ant_forbidden && (cycles_since_act == 4'(SPACING - 1)));
cover property (@(posedge clk) disable iff (!rst_n)
                  ant_forbidden && (cycles_since_act == 4'(SPACING)));
cover property (@(posedge clk) disable iff (!rst_n)
                  ant_forbidden && (cycles_since_act > 4'(SPACING)));
// Both rules tripping in one cycle -- the case P5 distinguishes.
cover property (@(posedge clk) disable iff (!rst_n) trip_spacing && trip_forbidden);
// An activate restarting a window that was already open.
cover property (@(posedge clk) disable iff (!rst_n)
                  ant_spacing && (cycles_since_act < 4'(SPACING)));
// Commands before and after initialisation, and both bank extremes.
cover property (@(posedge clk) disable iff (!rst_n) cmd_valid && !init_complete);
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 harness and the
// variety monitor -- the class equivalents of P1-P12.
task automatic check_assertion_infrastructure(vacuity_harness vh,
                                              antecedent_variety_monitor avm);
  // P13 -- FORBIDDEN. An invariant is never reported vacuous. §2:
  // 181 of this curriculum's 843 properties are structurally immune,
  // and flagging them would produce 181 false alarms.
  assert (vh.count_vacuous() <= vh.count_implications())
    else $error("P13: %0d vacuous exceeds %0d implications -- an invariant was flagged",
                vh.count_vacuous(), vh.count_implications());

  // P14 -- the shape classes partition the registered properties.
  assert (vh.count_implications() + vh.count_invariants() == vh.total())
    else $error("P14: shapes do not partition %0d properties", vh.total());

  // P15 -- FORBIDDEN. A result is never supportable with a vacuous
  // property. §2: a passing implication whose antecedent never
  // occurred is the single most common false success.
  assert (!(vh.result_supportable() && (vh.count_vacuous() > 0)))
    else $error("P15: result supportable with %0d vacuous properties", vh.count_vacuous());

  // P16 -- FORBIDDEN. A result is never supportable with inconsistent
  // counts. Firing more often than the antecedent was reached is an
  // accounting error, not an effective property.
  assert (!(vh.result_supportable() && (vh.count_inconsistent() > 0)))
    else $error("P16: result supportable with %0d inconsistent properties",
                vh.count_inconsistent());

  // P17 -- §7: an unguarded property does NOT block the result. The
  // harness cannot tell a legitimately guard-free property from a
  // latent failure, so it reports rather than adjudicates.
  assert (vh.count_unguarded() >= 0)
    else $error("P17: unguarded count is not reportable");

  // P18 -- a rejected registration never enters the totals.
  assert (!(vh.result_supportable() && (vh.rejected() > 0)))
    else $error("P18: result supportable with %0d rejected registrations", vh.rejected());

  // P19 -- variety never exceeds hits. A distinct-situation count
  // above the occurrence count would be impossible.
  assert (avm.variety("p_forbidden_access_trips")
          <= avm.hits("p_forbidden_access_trips"))
    else $error("P19: variety exceeds hits -- distinct situations cannot outnumber occurrences");

  // P20 -- §13's distinction: a property can be reached and
  // monotonous at once, and that combination must be reportable
  // rather than collapsed into "covered".
  assert (!(avm.reached_but_monotonous("p_forbidden_access_trips")
            && (avm.hits("p_forbidden_access_trips") == 0)))
    else $error("P20: monotonous reported for a property never reached");
endtask

// SIMULATION-ONLY. Independent reference for the harness's verdicts,
// holding records in a QUEUE and deciding vacuity by explicit
// case analysis rather than by the DUT's own method -- so agreement
// is evidence rather than a restatement.
class vacuity_reference;
  typedef struct {
    string       name;
    prop_shape_e shape;
    bit          guarded;
    int unsigned ant;
    int unsigned fires;
  } rec_t;
  rec_t recs[$];

  function bit would_accept(rec_t r);
    if (r.name == "") return 0;
    foreach (recs[i]) if (recs[i].name == r.name) return 0;
    return 1;
  endfunction

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

  // Explicit case analysis, deliberately not the DUT's expression.
  function bit vacuous(rec_t r);
    case (r.shape)
      PROP_INVARIANT   : return 0;
      PROP_IMPLICATION : return (r.ant == 0);
      default          : return 0;
    endcase
  endfunction

  function int n_vacuous();
    int n = 0;
    foreach (recs[i]) if (vacuous(recs[i])) n++;
    return n;
  endfunction

  function int n_inconsistent();
    int n = 0;
    foreach (recs[i])
      if (recs[i].shape == PROP_IMPLICATION && recs[i].fires > recs[i].ant) n++;
    return n;
  endfunction

  function int n_unguarded();
    int n = 0;
    foreach (recs[i]) if (!recs[i].guarded) n++;
    return n;
  endfunction
endclass

  THE LEGAL-ONLY SUITE, WITH AND WITHOUT THE HARNESS

    stimulus : only legal command sequences. No access inside a
               spacing window, no access to a closed bank.

  (A) as Modules 1-13 would have run it -- assertions, no covers
        P1  spacing violation trips        PASS
        P2  legal spacing never trips      PASS
        P3  forbidden access trips         PASS
        P11 no trip without command        PASS
        P12 no spacing trip before act     PASS
        every property                     PASS
        reported result                    CLEAN

        what actually happened : P1, P3 and P12 were never
        evaluated. Their antecedents -- an access inside the window,
        an access to a closed bank -- never occurred. The design
        could flag nothing and this run would look identical.

  (B) the same stimulus, with §12's harness registered
        props=5 impl=5 inv=0
        vacuous=3                      <-- P1, P3, P12
        supportable=FALSE
        VAC ERROR: 'p_spacing_violation_trips' PASSED VACUOUSLY
        VAC ERROR: 'p_forbidden_access_trips'  PASSED VACUOUSLY
        VAC ERROR: 'p_no_spacing_trip_before_first_act' PASSED VACUOUSLY

    diagnosis : the assertions are correct and the suite is empty.
      §2 measures that 662 of this curriculum's 843 properties have
      this shape, and §3 measures that 75 of its chapters shipped
      with no instrument that would say so.

    what makes it dangerous : (A) is not a weak pass, it is a
      CONFIDENT one. Five properties reported success and three
      constrained nothing, and the only difference between the two
      runs is a harness that counts antecedents.

    the fix : the antecedent covers of §14, plus the harness's
      result_supportable() as a gate. A suite cannot be trusted to
      notice its own vacuity, because vacuity looks exactly like
      correctness from the inside.