DDR VIP Usage

// ---------------------------------------------------------------------
// vip_capability_registry -- §4's observability contract, executable.
//
// CLASSIFICATION: educational, SIMULATION-ONLY.
//
// WHY unknown IS A FIRST-CLASS VALUE (§4): you cannot ask a component
// what it fails to report. A register where unknown silently counts
// as provided is an integration report claiming coverage nobody
// established -- and 27.1 §9's residual() refused to compute a
// percentage for exactly this reason.
//
// WHY A LOWER BOUND ONLY (§5): a checker firing proves a rule is
// implemented; a checker staying silent proves nothing. So the
// determinable result is a LOWER bound on capability, never an upper
// one, and this class will not report otherwise.
//
// WHAT IT DOES NOT MODEL:
//   - any product, vendor implementation, or real capability list
//
// WHAT IT WOULD MISS:
//   - every capability nobody enumerated. 27.1 §5's enumeration
//     problem, which is why review is a flag and not a computation.
// ---------------------------------------------------------------------
typedef enum { CAP_PROVIDED,     // an experiment demonstrated it
               CAP_ABSENT,       // an experiment demonstrated its absence
               CAP_UNKNOWN       // not determined -- the default
             } cap_status_e;

// §4's table: how the status was established. A capability asserted
// from documentation is weaker evidence than one demonstrated, and
// the registry keeps them distinct rather than averaging them.
typedef enum { EV_NONE,          // nothing was done
               EV_DOC,           // the supplier's documentation says so
               EV_EXPERIMENT     // stimulus demonstrated it
             } evidence_e;

class vip_capability extends uvm_object;
  `uvm_object_utils(vip_capability)

  string       id;
  string       requirement;      // which chapter established the need
  cap_status_e status;
  evidence_e   evidence;
  string       how;              // the experiment, or why none exists

  function new(string name = "vip_capability");
    super.new(name);
    status   = CAP_UNKNOWN;
    evidence = EV_NONE;
  endfunction

  // §5: documentation is not a demonstration. A capability believed
  // present on documentation alone is reported separately, because
  // the whole subject of this chapter is the gap between what a
  // component claims and what it reports.
  function bit demonstrated();
    return (status == CAP_PROVIDED) && (evidence == EV_EXPERIMENT);
  endfunction
endclass


class vip_capability_registry extends uvm_object;
  `uvm_object_utils(vip_capability_registry)

  protected vip_capability m_cap[string];
  protected bit            m_enumeration_reviewed;

  function new(string name = "vip_capability_registry");
    super.new(name);
  endfunction

  function void declare(string id, string requirement);
    vip_capability c;
    if (id == "" || requirement == "") begin
      `uvm_error("VIPREG",
        "a capability needs an id and the requirement it answers")
      return;
    end
    if (m_cap.exists(id)) return;            // idempotent
    c = vip_capability::type_id::create(id);
    c.id = id; c.requirement = requirement;
    m_cap[id] = c;                           // status stays CAP_UNKNOWN
  endfunction

  // Recording a determination requires saying HOW. §4: rows two,
  // three and four of its table are experiments, and an experiment
  // nobody can describe was not run.
  function void record(string id, cap_status_e status,
                       evidence_e evidence, string how);
    if (!m_cap.exists(id)) begin
      `uvm_error("VIPREG", $sformatf("unknown capability '%s'", id))
      return;
    end
    if (status != CAP_UNKNOWN && how == "") begin
      `uvm_error("VIPREG", $sformatf(
        "determination of '%s' refused: no method given", id))
      return;
    end
    if (status != CAP_UNKNOWN && evidence == EV_NONE) begin
      `uvm_error("VIPREG", $sformatf(
        "determination of '%s' refused: status without evidence", id))
      return;
    end
    m_cap[id].status   = status;
    m_cap[id].evidence = evidence;
    m_cap[id].how      = how;
  endfunction

  function void mark_enumeration_reviewed();
    m_enumeration_reviewed = 1;
  endfunction

  function int total();      return m_cap.size();  endfunction

  function int count_with(cap_status_e s);
    int n = 0;
    foreach (m_cap[k]) if (m_cap[k].status == s) n++;
    return n;
  endfunction

  function int count_demonstrated();
    int n = 0;
    foreach (m_cap[k]) if (m_cap[k].demonstrated()) n++;
    return n;
  endfunction

  // 27.1 §9's refusal, in this chapter's terms. Four numbers, and NO
  // percentage -- because a percentage of an enumeration nobody has
  // reviewed is a percentage of a number nobody chose.
  function void residual(output int declared, output int provided,
                         output int absent, output int unknown_n);
    declared  = m_cap.size();
    provided  = count_with(CAP_PROVIDED);
    absent    = count_with(CAP_ABSENT);
    unknown_n = count_with(CAP_UNKNOWN);
  endfunction

  // §4: unknown must stay unknown. An integration report is only
  // supportable when nothing is undetermined, the enumeration was
  // reviewed, and every PROVIDED status was demonstrated rather than
  // read in a document.
  function bit integration_report_supportable();
    if (m_cap.size() == 0)                 return 0;   // nothing enumerated
    if (!m_enumeration_reviewed)           return 0;   // 27.1 §5
    if (count_with(CAP_UNKNOWN) != 0)      return 0;   // §4
    if (count_demonstrated() != count_with(CAP_PROVIDED)) return 0;  // §5
    return 1;
  endfunction

  // §5: what is established about a supplied checker is a LOWER
  // bound. This method exists so nothing downstream can mistake it
  // for a completeness figure.
  function int rules_demonstrated_lower_bound();
    return count_demonstrated();
  endfunction

  function void report_phase(uvm_phase phase);
    int d, p, a, u;
    residual(d, p, a, u);
    `uvm_info("VIPREG", $sformatf(
      "declared=%0d provided=%0d (demonstrated=%0d) absent=%0d unknown=%0d reviewed=%0b supportable=%0b",
      d, p, count_demonstrated(), a, u, m_enumeration_reviewed,
      integration_report_supportable()), UVM_LOW)
  endfunction
endclass

// ---------------------------------------------------------------------
// vip_boundary_check -- CLASSIFICATION: synthesisable, BINDABLE.
//
// Bound at the interface between your environment and a VIP, this set
// checks the INTEGRATION's assumptions rather than the protocol's
// rules. 27.2 §11 owns protocol spacing; this owns the boundary.
//
// WHY BINDABLE AND NOT A CLASS: §7's diagram places this outside the
// VIP boundary deliberately. A check that consumed the VIP's own
// analysis port would inherit its author's judgement, which is the
// correlated-failure problem of §9. These properties see pins only.
//
// Every property is guarded by `disable iff (!rst_n)` -- 27.2's
// census measured 769 of 843 named properties with such a guard and
// 74 without, and the 74 are where reset-time noise comes from.
// ---------------------------------------------------------------------
module vip_boundary_check #(
  parameter int BANKS        = 16,
  parameter int VIP_ACTIVE   = 0,   // §6: 1 when the VIP drives
  parameter int ECC_ENABLED  = 0    // §8's last row
)(
  input  logic                        clk,
  input  logic                        rst_n,
  input  logic                        cmd_valid,
  input  logic [3:0]                  cmd_code,
  input  logic [$clog2(BANKS)-1:0]    cmd_bank,
  input  logic                        vip_drives,      // the VIP owns the bus
  input  logic                        env_drives,      // your env owns it
  input  logic                        cfg_valid,       // §8's config applied
  input  logic                        cfg_locked,
  input  logic                        rsp_valid,
  input  logic                        rsp_error,
  input  logic                        mon_txn_valid,   // VIP's monitor output
  input  logic                        mon_resolved     // and its resolution flag
);
  // BANKS < 2 would make $clog2(BANKS) zero and cmd_bank illegal.
  // The sibling guard in 24.3 accepted 0 and 1; this one does not.
  initial begin
    if (BANKS < 2)
      $fatal(1, "vip_boundary_check: BANKS must be at least 2 (got %0d)", BANKS);
  end

  // ---- §6: exactly one side drives. Both is contention; neither
  // during a command is a floating bus.
  property p_single_driver;
    @(posedge clk) disable iff (!rst_n)
      cmd_valid |-> (vip_drives ^ env_drives);
  endproperty
  assert property (p_single_driver)
    else $error("boundary: both or neither side driving during a command");

  // ---- §6: an ACTIVE VIP drives; a passive one must never.
  property p_mode_respected;
    @(posedge clk) disable iff (!rst_n)
      (VIP_ACTIVE == 0) |-> !vip_drives;
  endproperty
  assert property (p_mode_respected)
    else $error("boundary: a passive VIP drove the bus");

  // ---- §8: no command before the configuration is applied. A VIP
  // modelling a default device is the silent-wrong-geometry case.
  property p_config_before_traffic;
    @(posedge clk) disable iff (!rst_n)
      cmd_valid |-> cfg_valid;
  endproperty
  assert property (p_config_before_traffic)
    else $error("boundary: traffic before the configuration was applied");

  // ---- §8: and the configuration must not change under traffic,
  // which would make every derived timing figure stale mid-test.
  property p_config_stable;
    @(posedge clk) disable iff (!rst_n)
      cfg_locked |=> $stable(cfg_valid);
  endproperty
  assert property (p_config_stable)
    else $error("boundary: configuration changed while locked");

  // ---- The bank index must be in range. A VIP modelling a smaller
  // device aliases silently -- §8's first row.
  property p_bank_in_range;
    @(posedge clk) disable iff (!rst_n)
      cmd_valid |-> (cmd_bank < BANKS);
  endproperty
  assert property (p_bank_in_range)
    else $error("boundary: bank index outside the configured geometry");

  // ---- A response requires a command to have been issued. This is
  // an IMPLICATION and must be: rsp_valid is the only thing that makes
  // the claim meaningful, so there is no invariant form. 27.2's census
  // put 78.53% of this curriculum's properties in this category, which
  // is why the cover statements below are not optional.
  property p_no_unsolicited_response;
    @(posedge clk) disable iff (!rst_n)
      rsp_valid |-> $past(cmd_valid, 1) || $past(cmd_valid, 2)
                 || $past(cmd_valid, 3);
  endproperty
  assert property (p_no_unsolicited_response)
    else $error("boundary: a response with no recent command");

  // ---- §4: a monitor transaction must carry a resolution flag. If
  // the VIP has no such concept the input is tied, and this property
  // is the experiment that demonstrates it.
  property p_resolution_flag_present;
    @(posedge clk) disable iff (!rst_n)
      mon_txn_valid |-> !$isunknown(mon_resolved);
  endproperty
  assert property (p_resolution_flag_present)
    else $error("boundary: monitor output with no resolution flag");

  // ---- A monitor output requires traffic to have occurred. A VIP
  // reporting transactions with no commands is modelling, not
  // observing -- 27.3 §9's cannot-fail monitor at the boundary.
  property p_monitor_observes;
    @(posedge clk) disable iff (!rst_n)
      mon_txn_valid |-> $past(cmd_valid, 1) || $past(cmd_valid, 2)
                     || $past(cmd_valid, 3) || $past(cmd_valid, 4);
  endproperty
  assert property (p_monitor_observes)
    else $error("boundary: a monitor transaction with no preceding command");

  // ---- §8's last row: with ECC enabled, a response error is not a
  // data error, and an integration treating it as one is wrong.
  // 25.4 §4 owns why a corrected error is invisible.
  property p_ecc_error_not_data;
    @(posedge clk) disable iff (!rst_n)
      (ECC_ENABLED == 1) && rsp_error |-> rsp_valid;
  endproperty
  assert property (p_ecc_error_not_data)
    else $error("boundary: an error flag outside a valid response");

  // ---- INVARIANT, not an implication -- the ONE property in this set
  // that is. The two drive signals are never both high, at any time,
  // command or not, so this property has no antecedent to fail to arm
  // and is the only one here structurally immune to vacuity.
  property p_never_both_drive;
    @(posedge clk) disable iff (!rst_n)
      !(vip_drives && env_drives);
  endproperty
  assert property (p_never_both_drive)
    else $error("boundary: bus contention");

  // ---- IMPLICATION, and it cannot be an invariant: cmd_code is
  // don't-care while cmd_valid is low, so an ungated form would fire on
  // idle-cycle noise. A command code outside the configured set is a
  // configuration mismatch, not a protocol violation.
  property p_cmd_code_known;
    @(posedge clk) disable iff (!rst_n)
      cmd_valid |-> (cmd_code <= 4'd7);
  endproperty
  assert property (p_cmd_code_known)
    else $error("boundary: command code outside the configured set");

  // ---- IMPLICATION, and it cannot be an invariant: mon_resolved is
  // meaningless when no transaction is being reported. An unresolved
  // output is permitted; a monitor that is NEVER unresolved across a
  // whole run is the §3 row-one case -- a component assuming a default.
  // That cannot be asserted, so it is COVERED below instead.
  property p_resolved_is_boolean;
    @(posedge clk) disable iff (!rst_n)
      mon_txn_valid |-> (mon_resolved inside {1'b0, 1'b1});
  endproperty
  assert property (p_resolved_is_boolean)
    else $error("boundary: resolution flag neither 0 nor 1");

  // ---- 27.2 §7: publish the antecedents so a silent pass is
  // distinguishable from a property that never armed. Without these
  // the twelve asserts above are 78.53%-style vacuity risks.
  cover property (@(posedge clk) disable iff (!rst_n) cmd_valid);
  cover property (@(posedge clk) disable iff (!rst_n) rsp_valid);
  cover property (@(posedge clk) disable iff (!rst_n) mon_txn_valid);
  cover property (@(posedge clk) disable iff (!rst_n) cfg_locked);
  cover property (@(posedge clk) disable iff (!rst_n) vip_drives);
  cover property (@(posedge clk) disable iff (!rst_n) env_drives);

  // ---- §3, row one, as coverage rather than assertion: a monitor
  // that reports UNRESOLVED at least once has the three-valued
  // concept. One that never does may simply never have needed it --
  // which is why this is a cover and not an assert.
  cover property (@(posedge clk) disable iff (!rst_n)
                  mon_txn_valid && !mon_resolved);
  cover property (@(posedge clk) disable iff (!rst_n)
                  mon_txn_valid && mon_resolved);

  // ---- §8: traffic under a locked configuration, which is the only
  // configuration state in which a derived timing figure is sound.
  cover property (@(posedge clk) disable iff (!rst_n)
                  cmd_valid && cfg_locked);

  // ---- §6: the passive mode actually exercised.
  cover property (@(posedge clk) disable iff (!rst_n)
                  (VIP_ACTIVE == 0) && cmd_valid && env_drives);

  // ---- §8's ECC row reached at all.
  cover property (@(posedge clk) disable iff (!rst_n)
                  (ECC_ENABLED == 1) && rsp_valid);

  // ---- And a response arriving with no error, so the error path's
  // silence is distinguishable from an absent error path.
  cover property (@(posedge clk) disable iff (!rst_n)
                  rsp_valid && !rsp_error);
endmodule

// ---------------------------------------------------------------------
// vip_cross_check -- compares your monitor against theirs, and
// reports the SHARED INPUTS beside the agreement rate.
//
// CLASSIFICATION: educational, SIMULATION-ONLY.
//
// WHY THE SHARED INPUTS ARE PART OF THE RESULT (§9): two independent
// models agreeing is evidence; two models with a shared input
// agreeing is not. An agreement rate published alone invites exactly
// the inference §9 exists to refuse.
//
// WHAT IT DOES NOT MODEL:
//   - either monitor's internals
//
// WHAT IT WOULD MISS:
//   - every divergence both monitors make identically. A shared
//     misreading of a spec clause produces perfect agreement, and
//     all this class can do is report that the clause is shared.
// ---------------------------------------------------------------------
class vip_cross_check extends uvm_component;
  `uvm_component_utils(vip_cross_check)

  protected int m_compared;
  protected int m_agreed;
  protected int m_diverged;
  protected int m_ours_only;
  protected int m_theirs_only;
  // §9's table, recorded rather than assumed.
  protected string m_shared_input[$];

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

  function void note_shared_input(string what);
    if (what == "") begin
      `uvm_error("XCHK", "a shared input must be named")
      return;
    end
    foreach (m_shared_input[i]) if (m_shared_input[i] == what) return;
    m_shared_input.push_back(what);
  endfunction

  // Compare one pair of observations. 27.3 §6: a field either
  // monitor could not resolve is NOT a divergence -- it is an
  // absence of evidence, and counting it either way is wrong.
  function void compare(bit ours_valid, bit theirs_valid,
                        bit ours_resolved, bit theirs_resolved,
                        longint ours_addr, longint theirs_addr);
    if (!ours_valid && !theirs_valid) return;
    if (ours_valid && !theirs_valid) begin m_ours_only++;   return; end
    if (!ours_valid && theirs_valid) begin m_theirs_only++; return; end

    // Both saw it. If either could not resolve the address, there is
    // nothing to compare -- and this is NOT agreement.
    if (!ours_resolved || !theirs_resolved) begin
      m_compared++;                 // a comparison was attempted
      return;                       // and neither agreed nor diverged
    end

    m_compared++;
    if (ours_addr == theirs_addr) m_agreed++;
    else begin
      m_diverged++;
      `uvm_error("XCHK", $sformatf(
        "monitors disagree: ours %0h theirs %0h", ours_addr, theirs_addr))
    end
  endfunction

  function int compared();     return m_compared;    endfunction
  function int agreed();       return m_agreed;      endfunction
  function int diverged();     return m_diverged;    endfunction
  function int ours_only();    return m_ours_only;   endfunction
  function int theirs_only();  return m_theirs_only; endfunction
  function int shared_inputs(); return m_shared_input.size(); endfunction

  // Attempted comparisons that resolved to neither outcome. §9: this
  // is the number that stops a high agreement rate from being read
  // as a high confidence.
  function int inconclusive();
    int n = m_compared - m_agreed - m_diverged;
    return (n < 0) ? 0 : n;
  endfunction

  // §9: agreement is only evidence to the extent the inputs are
  // independent. This is deliberately NOT a confidence figure.
  function bit agreement_is_evidence();
    if (m_compared == 0)          return 0;   // nothing compared
    if (m_shared_input.size() != 0) return 0; // §9 -- correlated
    return (m_diverged == 0);
  endfunction

  // One-sided observation is the more informative result: a
  // transaction only one monitor saw is a finding about the other.
  function bit one_sided_findings_present();
    return (m_ours_only + m_theirs_only) > 0;
  endfunction

  function void report_phase(uvm_phase phase);
    `uvm_info("XCHK", $sformatf(
      "compared=%0d agreed=%0d diverged=%0d inconclusive=%0d ours_only=%0d theirs_only=%0d shared_inputs=%0d evidence=%0b",
      m_compared, m_agreed, m_diverged, inconclusive(),
      m_ours_only, m_theirs_only, m_shared_input.size(),
      agreement_is_evidence()), UVM_LOW)
    foreach (m_shared_input[i])
      `uvm_info("XCHK", $sformatf("  shared input: %s", m_shared_input[i]),
                UVM_LOW)
  endfunction
endclass

// ---------------------------------------------------------------------
// vip_overlap_plan -- records the seven duplication decisions of this
// section and refuses the ones that leave no independent instrument.
//
// CLASSIFICATION: educational, SIMULATION-ONLY.
//
// WHY A COMPONENT AND NOT A CHECKLIST: the two refusals below are
// structural, not stylistic. Deleting your monitor removes §12's
// cross-check entirely, and deleting your reference model under a
// memory-model VIP leaves the VIP predicting itself. Both present as
// simplifications, which is the form every mistake in this chapter
// takes -- so they are refused rather than documented.
//
// WHAT IT DOES NOT MODEL:
//   - any VIP, any implementation, or the cost of keeping a component
//
// WHAT IT WOULD MISS:
//   - a decision recorded correctly and never implemented. This
//     checks the PLAN; §15's report (A) is what an unimplemented
//     plan looks like at the boundary.
// ---------------------------------------------------------------------
typedef enum { OWN_KEPT,        // yours stays, as an instrument
               OWN_DELETED,     // yours goes, the VIP's is sole
               OWN_SHARED       // one object, used by both -- §9
             } overlap_e;

typedef enum { VIP_PASSIVE,     // §6: the device is your device
               VIP_MEMORY,      // §6: the device IS the VIP
               VIP_CONTROLLER   // §6: the host is the VIP
             } vip_mode_e;

class vip_overlap_plan extends uvm_object;
  `uvm_object_utils(vip_overlap_plan)

  protected overlap_e  m_decision[string];
  protected string     m_reason[string];
  protected vip_mode_e m_mode;
  protected bit        m_mode_set;

  function new(string name = "vip_overlap_plan");
    super.new(name);
  endfunction

  function void set_mode(vip_mode_e mode);
    m_mode     = mode;
    m_mode_set = 1;
  endfunction

  // Every decision carries its reason, for the same cause §10's
  // record() demands a method: a decision nobody can justify is
  // indistinguishable from one nobody made.
  function bit decide(string component, overlap_e d, string reason);
    if (!m_mode_set) begin
      `uvm_error("OVERLAP", "the VIP mode must be set first -- §6")
      return 0;
    end
    if (component == "" || reason == "") begin
      `uvm_error("OVERLAP", "a decision needs a component and a reason")
      return 0;
    end

    // REFUSAL 1 -- deleting your monitor removes §12's cross-check,
    // and with it the only instrument that can detect a supplied
    // component diverging from an independent observation.
    if (component == "monitor" && d == OWN_DELETED) begin
      `uvm_error("OVERLAP", $sformatf(
        "refused: deleting your monitor removes the cross-check (§12)"))
      return 0;
    end

    // REFUSAL 2 -- under a memory-model VIP, keeping BOTH reference
    // models compares two predictions of each other. The device is
    // the VIP, so there is no third party for either to be right
    // about.
    if (component == "ref_model" && d == OWN_KEPT
        && m_mode == VIP_MEMORY) begin
      `uvm_error("OVERLAP", $sformatf(
        "refused: two reference models with a memory-model VIP have no subject (§6)"))
      return 0;
    end

    m_decision[component] = d;
    m_reason[component]   = reason;
    return 1;
  endfunction

  function bit decided(string component);
    return m_decision.exists(component);
  endfunction

  function int count_with(overlap_e d);
    int n = 0;
    foreach (m_decision[k]) if (m_decision[k] == d) n++;
    return n;
  endfunction

  // §9 row two: a shared object is right AND correlating, so the
  // plan reports how many shares exist rather than hiding them.
  function int shared_count(); return count_with(OWN_SHARED); endfunction

  // At least one instrument must remain yours, or §12 has nothing
  // independent to compare against and the whole environment's
  // findings come from components you did not write.
  function bit independent_instrument_remains();
    return count_with(OWN_KEPT) > 0;
  endfunction

  // The plan is complete only when all seven rows of this section's
  // table have an answer. A missing row is an undecided duplication,
  // which resolves itself by accident at integration time.
  function bit complete(ref string missing[$]);
    string rows[$] = '{"bfm", "monitor", "ref_model", "scoreboard",
                       "checker", "coverage", "config"};
    missing.delete();
    foreach (rows[i])
      if (!m_decision.exists(rows[i])) missing.push_back(rows[i]);
    return missing.size() == 0;
  endfunction

  function void report_phase(uvm_phase phase);
    string missing[$];
    void'(complete(missing));
    `uvm_info("OVERLAP", $sformatf(
      "mode_set=%0b kept=%0d deleted=%0d shared=%0d undecided=%0d independent=%0b",
      m_mode_set, count_with(OWN_KEPT), count_with(OWN_DELETED),
      shared_count(), missing.size(),
      independent_instrument_remains()), UVM_LOW)
    foreach (missing[i])
      `uvm_warning("OVERLAP", $sformatf("undecided duplication: %s", missing[i]))
  endfunction
endclass

// SIMULATION-ONLY. Independent reference for §10's registry: a
// QUEUE of records scanned linearly rather than an associative array,
// so agreement between the two is evidence rather than a restatement.
class capability_reference;
  typedef struct { string id; int status; int evidence; } rec_t;
  rec_t recs[$];

  function void declare(string id);
    rec_t r; r.id = id; r.status = 2; r.evidence = 0;   // 2 = UNKNOWN
    recs.push_back(r);
  endfunction

  function bit record(string id, int status, int evidence, string how);
    if (status != 2 && (how == "" || evidence == 0)) return 0;
    foreach (recs[i])
      if (recs[i].id == id) begin
        recs[i].status = status; recs[i].evidence = evidence;
        return 1;
      end
    return 0;
  endfunction

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

  function int demonstrated();
    int n = 0;
    foreach (recs[i]) if (recs[i].status == 0 && recs[i].evidence == 2) n++;
    return n;
  endfunction
endclass

  TWO PASSING BOUNDARY REPORTS

  (A) the VIP was never connected
        stimulus : the environment runs; the VIP's interface is
                   present but nothing drives it
        p_single_driver           PASS
        p_mode_respected          PASS
        p_config_before_traffic   PASS
        p_bank_in_range           PASS
        p_no_unsolicited_response PASS
        p_resolution_flag_present PASS
        p_monitor_observes        PASS
        ... all 12 properties     PASS
        --------------------------------------------
        cover cmd_valid           0 hits
        cover rsp_valid           0 hits
        cover mon_txn_valid       0 hits
        cover cfg_locked          0 hits

        eleven of the twelve properties are implications, so with no
        command they never arm. 27.2's census put 78.53% of this
        curriculum's properties in that category, and this is what
        that number looks like when the antecedent is absent
        entirely. The single INVARIANT also passes, correctly -- there
        was no contention because there was no traffic.

  (B) the VIP was connected and the integration is still blind
        stimulus : full random traffic, VIP passive, all 12 covers hit
        all 12 properties         PASS
        all 12 covers             HIT
        --------------------------------------------
        cover mon_txn_valid && !mon_resolved    0 hits
        cover mon_txn_valid &&  mon_resolved    2,041,883 hits

        every boundary check passes and every antecedent armed. And
        the VIP's monitor reported RESOLVED on every one of two
        million transactions -- which is either a monitor that never
        needed the third value, or §3 row one: a component that
        assumes a default and reports a confident wrong answer.
        27.3 §6 says those are not equivalent, and the boundary
        cannot tell them apart.

    diagnosis : (A) is the vacuity case -- the covers are the only
      thing separating a passing boundary from an unconnected one.
      (B) is §3: the covers all hit, and the ONE cover that would
      have distinguished a three-valued monitor from a defaulting
      one is empty.

    the fix : (A) needs the covers read, not just the asserts. (B)
      needs §4's row-two experiment -- attach the VIP mid-traffic and
      see what it reports for the first access. That is a stimulus
      question, and no property at the boundary can answer it.