Verification Review Checklist

The first three gates reviewed a design. This one reviews the thing that was supposed to prove the design wrong.

33.1 asked what mechanism enforces each invariant. 33.2 asked whether the code is that mechanism. 33.3 asked whether the design's beliefs about measured values are warranted. Every one of those gates ended by handing something to this one, and 33.3 §19 handed over a measurement rather than a question: of nine PHY defects, five require the testbench to model a different system rather than different traffic — and a project can pass all nine items with an environment that cannot produce one.

Could this environment ever have found this design wrong — and if it did, would the report say so in a form a reviewer can check?

Two clauses, and the second is the one nobody reviews. A property can be correct, reachable, non-vacuous and independent, and the evidence that it was any of those things can be absent from the report the project signed off on. §7 is that item, and it is the reason this chapter's central question has two halves.

And this chapter has an obligation the first three did not. The track has built an eleven-variety taxonomy of ways a green assertion proves nothing, consolidated in 30.9 §6 and extended twice since. 33.3 §18 produced three surviving mutations that none of the eleven explains — correct properties, reachable antecedents, independent checkers, and silent about the thing that mattered. §15 opens the twelfth.

1. How To Use This Chapter

Each of the nine review items answers the same eight questions.

The sixth facet is different here, and the difference is the whole chapter. At the three preceding gates, how DV proves it named a stimulus. Here the design under test is the testbench, so the stimulus is a deliberately broken design — and an environment that does not fail on one is not an environment.

And the misleading evidence at this gate is the most convincing in the whole module: a coverage number. CURRICULUM-DERIVED from 27.5 §2's cited warning that “coverage is the map of where verification has been, and a map is” not the territory — and from its own arithmetic: a naive DDR cross is 11,520 bins, of which 288 are legal and 96 test anything. A report claiming 96% of 11,520 bins has said almost nothing, and it is the most reassuring artifact a project produces.

2. The One-Sentence Model

A verification review is sound when the environment can vary every dimension the design's correctness depends on, when every property's antecedent count is published in the report that was signed off, when every cover sits on the dimension its defect scales with, when the reference model computes the truth by a different route than the design, when every checker has a recorded run in which it failed, when every expected value's cardinality is stated, when every coverage exclusion carries a reachability argument that is recomputed rather than stored, when what a supplied component does not check has been established by experiment, and when every quantity a property's mechanism operates on is bounded by some artifact — and “the regression is green” is bit 0.

3. What This Chapter Owns

The boundary with 30.9 is the one that needs care, because the two chapters look similar and are not.

30.9 §7 owns a procedure applied to a property: three questions, under a minute each, that find every variety in its table. This chapter's unit is not a property — it is an environment, and six of its nine items are about artifacts no property contains: a configuration space, a coverage manifest, an exclusion list, an injection matrix, a recorded failing run, a documented bound. DERIVED: 30.9's procedure run over every property in a project can pass while eight of this chapter's nine items fail, because a set of individually excellent properties is not an environment.

And the boundary with 27.2 is a division of labour rather than of subject. 27.2 owns the measurement — 843 named properties, 78.5% implications, 74 with no reset guard, 89 chapters with no cover at all. This chapter owns the review question that measurement implies: for this project, which number is it, who published it, and was it in the report?

4. Teaching-Model Boundary And Source Discipline

Every SystemVerilog block below is an educational model of a verification component, and that makes the modelling problem unusual: the thing under test is itself a checker.

So each paired build here has three parts rather than two — a small design with an injectable fault, a robust environment that detects it, and a weak environment that does not. DERIVED: the gap figure for every item in this chapter is a detection rate, not a behaviour difference, because both environments are correct about the design they were pointed at and differ in what they could have noticed.

The corpus statistics in this chapter are STRUCTURAL and were measured on this repository. Re-measured for this chapter, across the live track excluding Module 33: 187 DDR chapters, 574 systemverilog fence blocks, 1,209 assert property, 738 cover property, and 18 chapters carrying an INTENTIONALLY DEFECTIVE block. Module 33 itself is excluded deliberately: its eight chapters are the review of those eighteen defects, so counting them would put the reviewer inside the corpus being reviewed. (With Module 33 included the track reads 195 chapters, 705 blocks, 1,365 assertions and 826 covers.) Where a number describes the corpus it is a count; where it describes a design it is ILLUSTRATIVE.

No external source was consulted, and no network tool was used. Every structural claim about DDR traces to a chapter of this track, cited inline by section.

5. The Eleven Varieties, As a Review Procedure — And the Gap in Them

The track has eleven named ways a green assertion proves nothing. 30.9 §6 consolidated eight; three were added later. This section does not re-derive them. It states what each costs a reviewer to check, because that is what decides whether a review actually runs.

Four of the eleven are cheap, and a reviewer who checks only those four has done most of what the taxonomy can do — varieties 2, 4, 6 and 9. DERIVED: two are greps, one is a two-file trace, and one is a report lookup.

And variety 6's entry carries a conditional that is the seed of this chapter's §7 and §15. “A coverage report — if one exists.” CURRICULUM-DERIVED from 27.2's corpus measurement: 89 chapters contain no cover at all, 84 of them in Modules 1 to 13, which wrote 343 assertions and zero covers — so for every implication in that range, variety 6 is not merely present, it is unmeasurable. The variety is a property defect. Its undetectability is a report defect, and the taxonomy has no entry for that.

Here is the gap, stated precisely, because §15 will need it. Every one of the eleven varieties describes a property that is wrong, unreachable, or dependent on something it should not be. None describes a property that is right, reachable, non-vacuous, independent, and silent about the thing that matters. DERIVED from 33.3 §18: three mutations there changed a sweep width, a staleness threshold and a drift fraction; every mechanism stayed correct, every property passed, every cover stayed non-zero, and all three made the design worse. Run 30.9 §7's three questions against the properties that let those mutations through and all three questions answer cleanly.

6. Review Item 1 — Can This Environment Vary the System, or Only the Traffic?

The pass criterion is a set comparison, and the finding is always a set difference. CURRICULUM-DERIVED from 31.2 §14's coverage-dimension rule and this track's standing refinement: when the dimension a defect scales with belongs to the environment's model rather than its stimulus, running longer never reaches it.

// ROBUST ENVIRONMENT: the SYSTEM is randomised, not just the traffic.
// ILLUSTRATIVE dimension set, chosen to match 33.3's five.
class ddr_system_cfg;
  // ---- traffic dimensions: what almost every environment randomises
  rand int unsigned  burst_count;
  rand int unsigned  read_fraction_pct;
  rand int unsigned  address_stride;

  // ---- SYSTEM dimensions: what 33.3 section 19 says five of nine PHY
  // defects live on. Each is `rand`, and each has a constraint that
  // makes the non-nominal value REACHABLE rather than merely legal.
  rand int unsigned  window_taps;        // narrow-part dimension
  rand bit           sides_asymmetric;   // device-vs-host Vref split
  rand bit           warm_reset_in_run;  // reset TYPE, not count
  rand bit           region_one_sided;   // pass-region shape
  rand int unsigned  sweep_taps;         // range adequacy
  rand int unsigned  hw_taps;

  // The census the reviewer asked for, as a declaration the environment
  // can print. A dimension absent from this list is the finding.
  static string DIMENSIONS[] = '{
    "burst_count", "read_fraction_pct", "address_stride",
    "window_taps", "sides_asymmetric", "warm_reset_in_run",
    "region_one_sided", "sweep_taps", "hw_taps"
  };

  constraint c_traffic {
    burst_count       inside {[64:4096]};
    read_fraction_pct inside {[0:100]};
    address_stride    inside {1, 2, 4, 8, 64};
  }

  // The constraints that matter. A 1-in-16 weight is not "reachable" in
  // a 200-run regression; these are deliberately shaped so every value
  // appears -- 27.5 section 6's legal / reachable / interesting split.
  constraint c_system {
    window_taps inside {[4:32]};
    // ILLUSTRATIVE: a third of runs use a narrow part.
    window_taps dist { [4:8] := 1, [9:16] := 1, [17:32] := 1 };
    sweep_taps  inside {[8:64]};
    hw_taps     inside {32, 64};
    sweep_taps  <= hw_taps;
    // The inadequate-range case, made a first-class outcome.
    (sweep_taps < hw_taps) dist { 1 := 1, 0 := 2 };
    sides_asymmetric  dist { 1 := 1, 0 := 1 };
    warm_reset_in_run dist { 1 := 1, 0 := 1 };
    region_one_sided  dist { 1 := 1, 0 := 1 };
  }

  // Traceability: which dimensions took a non-nominal value this run.
  function int unsigned nonnominal_count();
    int unsigned n = 0;
    if (window_taps <= 8)          n++;
    if (sides_asymmetric)          n++;
    if (warm_reset_in_run)         n++;
    if (region_one_sided)          n++;
    if (sweep_taps < hw_taps)      n++;
    return n;
  endfunction
endclass

// INTENTIONALLY DEFECTIVE. WEAK ENVIRONMENT: the system is a constant.
//
//   class ddr_system_cfg;
//     rand int unsigned burst_count;
//     rand int unsigned read_fraction_pct;
//     rand int unsigned address_stride;
//     // the system, fixed at the values the bring-up board had
//     localparam int unsigned WINDOW_TAPS       = 24;   // a good part
//     localparam bit          SIDES_ASYMMETRIC  = 1'b0;
//     localparam bit          WARM_RESET_IN_RUN = 1'b0;
//     localparam bit          REGION_ONE_SIDED  = 1'b0;
//     localparam int unsigned SWEEP_TAPS        = 64;   // == hw_taps
//   endclass
//
// CONTRACT VIOLATED: none. This environment is CORRECT. It constrains
// nothing falsely and checks everything it claims to check.
//
// WHY IT SURVIVES: it is not a bug, it is a scope. And its scope is
// invisible in every artifact a project publishes -- the transaction
// count is enormous, the functional coverage of TRAFFIC bins is
// complete, and no report has a row for a dimension nobody declared.
//
// TRACE (ILLUSTRATIVE, 200 runs, the five PHY defects of 33.3 injected):
//   robust:  dimensions randomised 9 of 9
//            runs reaching >= 1 non-nominal dimension: 193 of 200
//            injected defects detected: 5 of 5
//   weak:    dimensions randomised 3 of 9
//            runs reaching >= 1 non-nominal dimension: 0 of 200
//            injected defects detected: 0 of 5
//
//   gap: 5 of 5 versus 0 of 5, at IDENTICAL transaction counts.

The measured gap is 5 of 5 against 0 of 5, and the two environments run the same number of transactions. DERIVED: that is the cleanest demonstration in this module that verification effort and verification reach are different quantities, and a report that publishes the first says nothing about the second.

The misleading evidence deserves its own sentence because it is the industry default. A weak environment of this shape produces a better-looking coverage report than the robust one — its traffic bins fill faster, because every run uses the same system and the same bins. DERIVED: adding a system dimension divides the runs across more configurations and slows every traffic bin's fill rate, so the correct change makes the headline metric worse for the same compute.

And the pass criterion has a subtlety worth stating: rand is not enough. A dimension declared rand with a 1-in-64 weight is legal, reachable in principle, and absent from a 200-run regression. CURRICULUM-DERIVED from 27.5 §6's three-way split — legal, reachable, interesting — so this item's evidence is a per-dimension value histogram from the actual sign-off runs, not the constraint block.

7. Review Item 2 — Is This Property's Antecedent Count in the Report That Was Signed Off?

This item is about a report, not a property, and that distinction is load-bearing enough that §15 returns to it.

CURRICULUM-DERIVED from 27.2, which both owns the mechanism and measured the corpus: of 843 named properties in this curriculum, 78.5% are implications and therefore vacuity-exposed; 89 chapters contain no cover at all. And it records a documented instance: a legal-only testbench in which three forbidden-transition properties passed while their antecedents never became true — and “the only evidence was a coverage report nobody was reading.”

The escape in that instance was not the property. It was the reading. DERIVED: this item's pass criterion is therefore not does a cover exist but is its count in the artifact the project signed off on — because a cover that exists and is not exported is, from a reviewer's chair, identical to no cover.

// ROBUST ENVIRONMENT: every implication ships with a named antecedent
// cover, and the manifest that pairs them is generated from one source
// so it cannot drift.
package antecedent_publication_pkg;

  // ILLUSTRATIVE: the obligation set for a small scheduler.
  typedef enum int {
    OB_TRCD, OB_TRAS, OB_TRP, OB_TURN, OB_REF, OB_LEGAL
  } obligation_e;

  // One record per property. The ANTECEDENT is named, not described,
  // and `ante_cover` is the cover whose count the report must carry.
  typedef struct {
    string       prop_name;
    string       ante_cover;
    obligation_e obligation;
    bit          is_implication;
  } prop_record_t;

  prop_record_t MANIFEST[] = '{
    '{"p_trcd_respected",  "c_act_then_col",   OB_TRCD,  1'b1},
    '{"p_tras_respected",  "c_act_then_pre",   OB_TRAS,  1'b1},
    '{"p_trp_respected",   "c_pre_then_act",   OB_TRP,   1'b1},
    '{"p_turn_respected",  "c_rd_then_wr",     OB_TURN,  1'b1},
    '{"p_refresh_issued",  "c_refresh_due",    OB_REF,   1'b1},
    '{"p_grant_is_legal",  "c_grant_asserted", OB_LEGAL, 1'b1}
  };
endpackage

class antecedent_publication;
  int unsigned ante_hits[string];
  int unsigned prop_pass[string];

  // The check that makes this item mechanical. A property that passed
  // with a zero antecedent count is reported as UNPROVEN, not as passed.
  function void classify(output int unsigned proven,
                         output int unsigned unproven,
                         output int unsigned failed);
    proven = 0; unproven = 0; failed = 0;
    foreach (antecedent_publication_pkg::MANIFEST[i]) begin
      automatic string pn = antecedent_publication_pkg::MANIFEST[i].prop_name;
      automatic string an = antecedent_publication_pkg::MANIFEST[i].ante_cover;
      automatic int unsigned ah = ante_hits.exists(an) ? ante_hits[an] : 0;
      if (prop_pass.exists(pn) && (prop_pass[pn] == 0)) failed++;
      else if (ah == 0)                                  unproven++;
      else                                               proven++;
    end
  endfunction

  // The export. A manifest entry with no exported count is itself a
  // finding, so the writer refuses to omit a row.
  function void write_report(string path);
    int fd = $fopen(path, "w");
    $fdisplay(fd, "property,antecedent,antecedent_hits,verdict");
    foreach (antecedent_publication_pkg::MANIFEST[i]) begin
      automatic string pn = antecedent_publication_pkg::MANIFEST[i].prop_name;
      automatic string an = antecedent_publication_pkg::MANIFEST[i].ante_cover;
      automatic int unsigned ah = ante_hits.exists(an) ? ante_hits[an] : 0;
      $fdisplay(fd, "%s,%s,%0d,%s", pn, an, ah,
                (ah == 0) ? "UNPROVEN" : "PROVEN");
    end
    $fclose(fd);
  endfunction
endclass

// INTENTIONALLY DEFECTIVE. WEAK ENVIRONMENT: the covers exist and the
// report does not carry them.
//
//   // assertions.sv  -- correct, complete, well-written
//   assert property (p_trcd_respected);
//   cover  property (c_act_then_col);        // it IS there
//   ...
//   // signoff.tcl
//   report_assertions -status all            // pass/fail only
//   // no `report_coverage`, because the coverage database is used by
//   // a different team on a different cadence.
//
// CONTRACT VIOLATED: none, in the RTL or the properties. The violation
// is in the ARTIFACT, which is why no tool reports it.
//
// WHY IT SURVIVES: it is not even wrong. Six properties, six covers,
// all present in source, 100% pass. The vacuity is discoverable by
// anyone who opens the coverage database. Nobody does, because the
// sign-off report is the thing that is reviewed.
//
// TRACE (ILLUSTRATIVE, legal-only stimulus, 6 properties):
//   actual state: 3 antecedents never true (OB_TURN, OB_REF, OB_LEGAL)
//   robust report: proven 3, UNPROVEN 3, failed 0
//   weak report:   "6 of 6 properties passed"
//
//   gap: 3 properties are indistinguishable from proven, and the
//   distinguishing data EXISTS in the run. Reviewer-verifiable
//   properties: robust 6 of 6, weak 0 of 6.

The gap is 6 of 6 against 0 of 6 verifiable, and neither number is a count of correct properties. DERIVED: all six properties are correct in both builds; three are vacuous in both builds; and the difference is entirely in whether a reviewer can tell.

This is the item that forced a decision about the taxonomy, and it is worth being explicit about the decision. The eleven varieties classify properties. This defect is in a report. DERIVED: it is therefore not a twelfth variety, and §15 does not make it one — a taxonomy that admits report defects stops being a property taxonomy and becomes a list of everything that can go wrong. What it is instead is the reason variety 6 is under-detected in practice, and the fix is a manifest rather than a better property.

The misleading evidence is a number every project publishes. CURRICULUM-DERIVED from 27.2's 78.5%: a 100% pass rate over a set that is 78.5% implications is consistent with 78.5% of the set proving nothing, and the pass rate cannot distinguish the cases. A reviewer who is handed a pass rate and no antecedent counts has been handed one number where two were needed.

8. Review Item 3 — Is This Cover on the Dimension Its Defect Scales With?

CURRICULUM-DERIVED from 31.2 §14's scale-vacuity refinement, stated there as a correction to a natural reading of coverage: an antecedent cover proves a condition occurred, not that it occurred at a scale where the defect is observable.

The canonical instance is in this module. 33.2 §10's refresh-debt defect needs 256 ticks of held ownership before the counter saturates. A cover on dev_owns fires in the first microsecond of every run. A cover on dev_owns [*256] fires only in runs that hold it that long. Both are 100% covered in the report; one of them means something.

// ROBUST ENVIRONMENT: each cover carries its dimension and threshold,
// and the threshold is DERIVED from the failure mechanism rather than
// chosen.
package cover_dimension_pkg;

  typedef enum int { D_DURATION, D_OCCUPANCY, D_INDEX, D_CONFIG,
                     D_LOAD_SHAPE, D_RESET_TYPE, D_ORDER } dim_e;

  typedef struct {
    string name;
    dim_e  dim;
    int unsigned threshold;   // 0 = the dimension is categorical
    string mechanism;         // why THIS threshold, in one clause
  } cover_record_t;

  // ILLUSTRATIVE thresholds, each traced to the defect it guards.
  cover_record_t COVERS[] = '{
    '{"c_debt_held",     D_DURATION,   256, "counter is DEBT_W=8 wide"},
    '{"c_queue_full",    D_OCCUPANCY,   16, "queue DEPTH=16"},
    '{"c_top_index",     D_INDEX,       15, "highest legal index"},
    '{"c_narrow_part",   D_CONFIG,       8, "margin constant is 6 taps"},
    '{"c_skewed_load",   D_LOAD_SHAPE,   4, "denominator ratio 4:1"},
    '{"c_warm_reset",    D_RESET_TYPE,   0, "reset TYPE is categorical"},
    '{"c_out_of_order",  D_ORDER,        2, "two outstanding minimum"}
  };
endpackage

class cover_dimension_audit;
  int unsigned hits[string];       // times the condition occurred
  int unsigned max_seen[string];   // the largest value reached

  // The audit. A cover whose condition fires but whose dimension never
  // reaches the threshold is SCALE-VACUOUS: a term this track needed a
  // name for, and 31.2 section 14 supplied.
  function void classify(output int unsigned effective,
                         output int unsigned scale_vacuous,
                         output int unsigned unhit);
    effective = 0; scale_vacuous = 0; unhit = 0;
    foreach (cover_dimension_pkg::COVERS[i]) begin
      automatic string nm = cover_dimension_pkg::COVERS[i].name;
      automatic int unsigned th = cover_dimension_pkg::COVERS[i].threshold;
      automatic int unsigned h  = hits.exists(nm) ? hits[nm] : 0;
      automatic int unsigned mx = max_seen.exists(nm) ? max_seen[nm] : 0;
      if (h == 0)                      unhit++;
      else if (th == 0)                effective++;      // categorical
      else if (mx >= th)               effective++;
      else                             scale_vacuous++;
    end
  endfunction
endclass

// INTENTIONALLY DEFECTIVE. WEAK ENVIRONMENT: covers without thresholds.
//
//   cover property (@(posedge clk) dev_owns);          // not [*256]
//   cover property (@(posedge clk) queue_occ != 0);    // not == DEPTH
//   cover property (@(posedge clk) burst_index != 0);  // not == 15
//   ...
// and no `max_seen` instrumentation, so the report has hit counts and
// no magnitudes.
//
// CONTRACT VIOLATED: 31.2 section 14's scale-vacuity refinement.
//
// WHY IT SURVIVES: the covers are CORRECT and they are HIT. Every one
// reads 100%. The coverage report is the most reassuring artifact the
// project produces, and it is reassuring about the wrong quantity.
//
// TRACE (ILLUSTRATIVE, 200 runs of 4096 cycles, 7 covers):
//   robust: effective 3, SCALE-VACUOUS 4, unhit 0
//           (c_debt_held max 41 of 256; c_queue_full max 9 of 16;
//            c_narrow_part max window 24, threshold 8; c_out_of_order
//            max 1 of 2)  -> the report NAMES four gaps
//   weak:   "7 of 7 covers hit, 100%"
//
//   gap: four scale-vacuous covers reported as complete, and the four
//   correspond exactly to four defects of this module's eighteen.

The gap is four covers, and the diagnostic value is that the robust report names which four. DERIVED: a max-value column converts a coverage report from a binary into a distance — c_debt_held reaching 41 of 256 tells a reviewer both that the cover is inadequate and how much longer the runs would need to be.

And there is a second finding here that is not about duration, and it is the one that makes the item hard. Two of the four scale-vacuous covers cannot be fixed by running longer at all. c_narrow_part's dimension is a configuration — the part's window width — and c_warm_reset's is a reset type. CURRICULUM-DERIVED from this track's coverage-dimension rule: when the dimension belongs to the environment's model rather than its stimulus, running longer never reaches it — so item 3's findings partition into two kinds, and only one of them has a compute-time fix. DERIVED: of the four, two need longer runs and two need item 1.

9. Review Item 4 — Does the Reference Model Reach the Truth by a Different Route?

CURRICULUM-DERIVED from 27.3, which owns the independence requirement and names its failure mode: the cannot-fail checker. This item is that requirement turned into a procedure, and the procedure is a mutation run — because independence is not visible by reading either file.

33.2 §17 already applied the rule once, to its own property set: the truth loop for widest eligible is written differently on purpose, even though it looks redundant. This item is the general form, and its pass criterion is mechanical: mutate the design's algorithm and require the model to disagree.

// ROBUST MODEL: computes the widest run by EXHAUSTIVE SCAN, which is a
// different algorithm from any incremental tracker a design would use.
// Deliberately O(N^2) and deliberately not shared.
class widest_run_model #(parameter int N = 32);
  // Returns the width of the widest run of 1s in `map`, and its start.
  function automatic void widest(input bit [N-1:0] map,
                                 output int unsigned width,
                                 output int unsigned start);
    width = 0; start = 0;
    // Exhaustive: for every start, extend as far as possible. A design
    // would never do this -- which is the point.
    for (int s = 0; s < N; s++) begin
      if (map[s]) begin
        int unsigned w = 0;
        for (int e = s; e < N; e++) begin
          if (!map[e]) break;
          w++;
        end
        if (w > width) begin width = w; start = s; end
      end
    end
  endfunction

  // The independence audit: mutate the DESIGN and require disagreement.
  int unsigned mutations_run, mutations_caught;

  function automatic void audit(input bit [N-1:0] map,
                                input int unsigned dut_width,
                                input int unsigned dut_start);
    int unsigned mw, ms;
    widest(map, mw, ms);
    mutations_run++;
    if ((mw != dut_width) || (ms != dut_start)) mutations_caught++;
  endfunction
endclass

// INTENTIONALLY DEFECTIVE. WEAK MODEL: the model reuses the design's
// incremental tracker, because "it is already written and tested".
//
//   // in the model:
//   import dut_pkg::run_tracker;          // <-- the defect
//   function void widest(bit [N-1:0] map, output int w, output int s);
//     run_tracker rt = new();             // the SAME class the RTL's
//     rt.scan(map);                       // testbench-visible model uses
//     w = rt.best_width; s = rt.best_start;
//   endfunction
//
// CONTRACT VIOLATED: 27.3's independence requirement. And the failure
// mode is the one 27.3 names: the checker CANNOT FAIL.
//
// WHY IT SURVIVES: reuse is good engineering everywhere else. The
// tracker is well-tested, the model is shorter, and the scoreboard has
// never reported a spurious mismatch -- which reads as quality.
//
// TRACE (ILLUSTRATIVE, 6 mutations of the design's tracker):
//   M-a  ">" becomes ">="   (ties pick the later run)
//   M-b  scan starts at 1 instead of 0
//   M-c  run length off by one at the top index
//   M-d  best_start not updated when best_width is
//   M-e  the tracker stops at the first run of length >= 4
//   M-f  the map is read one cycle stale
//
//   robust model: caught 6 of 6 (it recomputes from `map`)
//   weak model:   caught 1 of 6 -- only M-f, and only because the
//                 STALENESS is outside the shared code, not inside it.
//
//   gap: 6 of 6 versus 1 of 6. And the one it caught is the one that
//   was not actually in the shared algorithm.

The gap is 6 of 6 against 1 of 6, and the single catch is the tell. DERIVED: the weak model caught exactly the mutation that lived outside the shared code. A shared algorithm makes a checker blind to precisely the class of defect the sharing covers, and blind to nothing else — which means the checker's apparent effectiveness against unrelated bugs stays intact and hides the hole.

And the misleading evidence is a metric projects treat as good news: zero mismatches. CURRICULUM-DERIVED from 27.3's cannot-fail failure mode. DERIVED: a scoreboard with zero lifetime mismatches is consistent with a correct design, and equally consistent with a scoreboard that cannot produce one — and item 5 is the item that distinguishes them.

Note the boundary with 33.2 §11. That item reviews a design that picks the first eligible candidate where the specification says widest. This item reviews the model that was supposed to catch it — and a project can hold 33.2's finding, fix the design, and still have a model that would not have found the next one.

10. Review Item 5 — Has This Checker Ever Failed?

This item and item 2 are both about evidence, and the distinction matters. Item 2 asks whether a property's antecedent was reached. This item asks whether the property, having been reached, is capable of reporting a failure. DERIVED: a property can have a fully hit antecedent and still be unable to fail — variety 7, non-independence — so the two items are independent and a project needs both.

CURRICULUM-DERIVED from 27.3's cannot-fail failure mode, and from this track's standing rule on mutation harnesses: a mutation run needs a passing baseline or every mutation false-kills — and its mirror, which this item is: a checker needs a demonstrated failure or every pass is uninformative.

// ROBUST ENVIRONMENT: a positive-control matrix, maintained as a
// first-class deliverable and re-run every release.
package checker_liveness_pkg;

  typedef struct {
    string checker;        // the checker under control
    string fault;          // the injection that must trip it
    string obligation;     // what it protects, for traceability
  } control_t;

  // ILLUSTRATIVE, one row per checker. The rule is one row per checker,
  // with no exceptions -- an unfalsifiable checker is the finding.
  control_t MATRIX[] = '{
    '{"p_trcd_respected",  "force tRCD counter -1",      "tRCD"},
    '{"p_tras_respected",  "precharge one cycle early",  "tRAS"},
    '{"p_grant_is_legal",  "drop the legal-set mask",    "legality"},
    '{"sb_read_data",      "corrupt one returned beat",  "data integrity"},
    '{"mon_txn_compose",   "drop one command of a burst","composition"},
    '{"p_refresh_issued",  "suppress one refresh",       "retention"},
    '{"cov_bank_state",    "freeze the state model",     "coverage validity"}
  };
endpackage

class checker_liveness;
  bit caught[string];      // did the checker fire under its injection?
  string last_run[string]; // the dated run that caught it

  function void record(string checker, bit fired, string run_id);
    caught[checker] = fired;
    if (fired) last_run[checker] = run_id;
  endfunction

  function void classify(output int unsigned live,
                         output int unsigned inert,
                         output int unsigned uncontrolled);
    live = 0; inert = 0; uncontrolled = 0;
    foreach (checker_liveness_pkg::MATRIX[i]) begin
      automatic string ck = checker_liveness_pkg::MATRIX[i].checker;
      if (!caught.exists(ck))    uncontrolled++;   // no injection exists
      else if (caught[ck])       live++;
      else                       inert++;          // injected, did not fire
    end
  endfunction

  // The distinction that makes this item usable: an INERT checker is a
  // bug in the environment. An UNCONTROLLED checker is a gap in this
  // matrix, and the two need different owners.
endclass

// INTENTIONALLY DEFECTIVE. WEAK ENVIRONMENT: no positive controls.
//
//   // there is no injection suite. The regression is green, and the
//   // team's confidence comes from the green.
//
// CONTRACT VIOLATED: 27.3's independence requirement is UNTESTED here
// rather than violated -- which this track has flagged before as a
// distinct state: a guard shadowed by another rule is untested, not
// working.
//
// WHY IT SURVIVES: an injection suite is a test suite that is SUPPOSED
// to fail, and every piece of CI infrastructure a project owns is built
// to treat failure as bad. Adding one means adding a regression whose
// green light means red.
//
// TRACE (ILLUSTRATIVE, the 7 checkers above, 7 injections applied by
// hand for this chapter's measurement):
//   robust: live 7, inert 0, uncontrolled 0
//   weak:   the same 7 checkers exist and pass every run.
//           Applying the injections for the first time:
//             live 5, INERT 2, uncontrolled 0
//           -- `sb_read_data` compares against a model that reads the
//              design's own return buffer (variety 7), so corrupting a
//              beat corrupts both sides.
//           -- `cov_bank_state` samples a state model that is the
//              design's, so freezing it freezes the sampler too.
//
//   gap: 2 of 7 checkers were inert for the project's whole life, and
//   the ONLY way to discover it was to try to make them fail.

The gap is 2 of 7, and the number is the point: it is not zero and it is not most. DERIVED: a project with no positive controls has an unknown number of inert checkers, and the expected value is not small — two of seven here, and both are variety 7, which is the variety 30.9 §6 costs at read the checker's inputs and which therefore should have been cheap to find.

That is worth dwelling on, because it is a finding about review practice rather than about environments. Variety 7 is one of the eleven, it is cheap to check, and it survived here anyway. DERIVED: the taxonomy's cost column (§5) says what a check costs, not whether anyone runs it — and an injection matrix is the artifact that makes a cheap check unskippable, because it fails loudly instead of requiring someone to look.

And the misleading evidence is structural rather than incidental. A clean regression is indistinguishable from an inert regression by construction, and every tool a project owns is built to reward the first reading. The pass criterion here is therefore a regression that is expected to fail — an artifact whose green light means something is broken, which is why it is the item most often absent.

11. Review Item 6 — Is the Expected Value a Value or a Set, and Does the Checker Know Which?

CURRICULUM-DERIVED from 27.4, which owns the mechanism: ordering makes the expected value a set rather than a value. 27.4 establishes that. This item reviews what a project did about it — and the interesting failure is not the obvious one.

The obvious failure is a checker that compares against one legal order and reports false failures. That failure is loud, it is found in a week, and it gets fixed. The dangerous failure is how it gets fixed: the set is widened until the false failures stop. DERIVED: a set widened until nothing complains is 33.2 §14's tolerance parameter in a different costume — “a checker adjusted until it stopped complaining has been calibrated against the design rather than against the specification.”

// ROBUST SCOREBOARD: the legal set is COMPUTED from the ordering rules,
// and its cardinality is published.
class expected_set_model #(parameter int MAXQ = 8);
  typedef struct {
    int unsigned tag;
    int unsigned bank;
    bit          is_read;
    int unsigned arrival;
  } req_t;

  req_t outstanding[$];

  // The legal set of NEXT returns, derived from two rules and no others:
  //  R1: same-bank, same-direction returns keep arrival order
  //  R2: anything else may return in any order
  // 27.4 section 5's set, computed rather than assumed.
  function automatic void legal_next(output int unsigned legal_tags[$],
                                     output int unsigned cardinality);
    legal_tags.delete();
    foreach (outstanding[i]) begin
      automatic bit blocked = 1'b0;
      foreach (outstanding[j]) begin
        if (j == i) continue;
        // Blocked iff an older request shares bank AND direction.
        if ((outstanding[j].bank    == outstanding[i].bank) &&
            (outstanding[j].is_read == outstanding[i].is_read) &&
            (outstanding[j].arrival <  outstanding[i].arrival))
          blocked = 1'b1;
      end
      if (!blocked) legal_tags.push_back(outstanding[i].tag);
    end
    cardinality = legal_tags.size();
  endfunction

  int unsigned accepted, rejected;
  int unsigned card_hist[int unsigned];   // the published distribution

  function automatic bit check_return(int unsigned tag);
    int unsigned legal[$], card;
    legal_next(legal, card);
    card_hist[card]++;
    // Membership in a COMPUTED set. Not "is it outstanding" -- that is
    // a superset, and the superset is the defect.
    foreach (legal[k]) begin
      if (legal[k] == tag) begin
        accepted++;
        foreach (outstanding[m]) if (outstanding[m].tag == tag) begin
          outstanding.delete(m); break;
        end
        return 1'b1;
      end
    end
    rejected++;
    return 1'b0;
  endfunction
endclass

// INTENTIONALLY DEFECTIVE. WEAK SCOREBOARD: the legal set is
// "everything outstanding".
//
//   function bit check_return(int unsigned tag);
//     foreach (outstanding[m])
//       if (outstanding[m].tag == tag) begin      // <-- the defect
//         outstanding.delete(m); return 1'b1;     // any outstanding tag
//       end                                       // is accepted
//     return 1'b0;
//   endfunction
//
// CONTRACT VIOLATED: 27.4 section 5 -- the expected value is a SET, and
// this checker used a SUPERSET of it.
//
// WHY IT SURVIVES: this is the shape the checker takes AFTER the false
// failures were fixed. The original compared against one order, reported
// mismatches on every legal reorder, and was "corrected" by accepting
// any outstanding tag. The correction removed the false failures and
// every true one with them. The commit message says "fix scoreboard
// ordering false-fails" and it is telling the truth.
//
// TRACE (ILLUSTRATIVE, 64 returns, mixed banks and directions):
//   legal-set cardinality distribution (robust): 1 -> 11, 2 -> 26,
//     3 -> 19, 4 -> 8   (mean 2.4 of up to 8 outstanding)
//   robust: accepted 55, REJECTED 9
//   weak:   accepted 64, rejected 0
//
//   gap: 9 of 64 returns (14%) violate same-bank same-direction order
//   and are accepted. And the weak build cannot publish a cardinality
//   distribution, because it never computes one.

The gap is 9 of 64, and the cardinality distribution is the artifact that makes the item reviewable. DERIVED: the robust build's mean legal-set size is 2.4 out of up to 8 outstanding — so the weak build's set is on average 3.3× too large, and the multiple is a direct measure of how much checking was given up.

This is the one item in this chapter whose defect has a commit message that is honest. DERIVED: “fix scoreboard ordering false-fails” describes exactly what was done. The false failures were real, the fix removed them, and the review question is one nobody asked: what did the fix stop rejecting? CURRICULUM-DERIVED from 30.5 §11's variety 2 and its own defect — the aged set not intersected with the legal set: the same error, once in a design and once in the checker built to catch it.

And the pass criterion is a number, which makes this item unusually cheap for a scoreboard item. Demand the legal-set cardinality distribution. A checker that cannot produce one is comparing against a set it never computed — and whether that set is right or a superset is then unknowable from the source.

12. Review Item 7 — Does Every Coverage Exclusion Carry a Reachability Argument, Recomputed?

CURRICULUM-DERIVED from 27.5 §4, which owns the arithmetic and supplies this item's scale: a naive DDR cross is 11,520 bins, of which 288 are legal and 96 test anything. An exclusion list for that cross removes 11,232 bins — 97.5% of the denominator — and every one of those removals is an argument.

And 27.6 is the reason this is a review item rather than a maintenance task: it records that a VIP's configuration surface makes 27.5 §8's exclusion list “now someone else's.” DERIVED: an exclusion list you did not write, for a coverage model you did not write, at a configuration the author did not have, is three degrees removed from any argument.

This item is also variety 10 in a place the taxonomy has not been applied. CURRICULUM-DERIVED from 31.1 §14's parameter-conditional soundness: a property whose soundness depends on a parameter value is sound at one elaboration and unsound at another. DERIVED: an exclusion is exactly such a claim — it asserts unreachability, which is a claim about the parameterised state space — so variety 10 applies to exclusions as directly as it applies to properties, and no chapter had said so.

// ROBUST ENVIRONMENT: exclusions are DERIVED from the configuration at
// elaboration, with a reason attached to each.
package exclusion_provenance_pkg;

  // ILLUSTRATIVE configuration.
  typedef struct {
    int unsigned banks;
    int unsigned bank_groups;
    int unsigned burst_len;
    bit          two_cycle_cmd;   // DDR5-style command timing
    bit          bg_present;      // bank groups exist at all
  } cfg_t;

  typedef enum int { R_ILLEGAL_BY_SPEC, R_UNREACHABLE_BY_CFG,
                     R_UNREACHABLE_BY_TIMING, R_NOT_INTERESTING } reason_e;
endpackage

class exclusion_provenance;
  import exclusion_provenance_pkg::*;

  cfg_t cfg;
  reason_e reason_of[int unsigned];   // bin id -> reason
  int unsigned total_bins;

  // The generator. Every exclusion is computed FROM `cfg`, so changing
  // `cfg` changes the set -- the whole item in one function.
  function automatic void derive(cfg_t c, int unsigned bins);
    cfg = c; total_bins = bins;
    reason_of.delete();
    for (int unsigned b = 0; b < bins; b++) begin
      automatic int unsigned bank = b % 32;
      automatic int unsigned bg   = (b / 32) % 8;
      automatic int unsigned bl   = (b / 256) % 4;
      // Spec-illegal: independent of configuration.
      if (bl == 3)                        reason_of[b] = R_ILLEGAL_BY_SPEC;
      // Configuration-unreachable: DEPENDS ON cfg, and this is the
      // class that silently becomes reachable.
      else if (bank >= cfg.banks)         reason_of[b] = R_UNREACHABLE_BY_CFG;
      else if (!cfg.bg_present && bg > 0) reason_of[b] = R_UNREACHABLE_BY_CFG;
      else if (bg >= cfg.bank_groups)     reason_of[b] = R_UNREACHABLE_BY_CFG;
      // Timing-unreachable: depends on a timing parameter.
      else if (cfg.two_cycle_cmd && (bank % 2 == 1) && (bl == 0))
                                          reason_of[b] = R_UNREACHABLE_BY_TIMING;
    end
  endfunction

  function automatic int unsigned excluded_count();
    return reason_of.size();
  endfunction

  // The audit a reviewer runs: re-derive at a second configuration and
  // report bins that moved from excluded to reachable. 31.1 section 14's
  // variety 10, mechanised.
  function automatic int unsigned newly_reachable(cfg_t c2);
    int unsigned before[int unsigned];
    int unsigned n = 0;
    before = reason_of;
    derive(c2, total_bins);
    foreach (before[b])
      if (!reason_of.exists(b)) n++;
    return n;
  endfunction
endclass

// INTENTIONALLY DEFECTIVE. WEAK ENVIRONMENT: a static exclusion file.
//
//   // excludes.el -- generated once, on 2024-03-11, for the 16-bank
//   // 2-bank-group bring-up configuration. Checked in. Never regenerated.
//   exclude_bin  bank_state_cross  bin_id  1024:11519
//   exclude_bin  bank_state_cross  bin_id  768:1023
//   ...
//
// CONTRACT VIOLATED: 27.5 section 8's requirement that an exclusion carry an
// argument, and 31.1 section 14's variety 10 -- the argument was sound at
// one elaboration.
//
// WHY IT SURVIVES: the file was CORRECT when written, it is reviewed at
// the time it is written, and the coverage number it produces is high
// and stable. Nothing in any tool flags a stale exclusion, because an
// exclusion is an instruction rather than a claim.
//
// TRACE (ILLUSTRATIVE, total_bins = 11520):
//   cfg A (bring-up): banks 16, bank_groups 2, bg_present 1,
//                     two_cycle_cmd 0
//     robust: excluded 10944  ->  576 live bins
//     weak:   excluded 10944  ->  IDENTICAL. The file was generated here.
//   cfg B (product):  banks 32, bank_groups 8, bg_present 1,
//                     two_cycle_cmd 1
//     robust: excluded  8112  -> 3408 live bins
//     weak:   excluded 10944  ->  576 live bins
//     newly_reachable(cfg B) = 2856 bins
//     of which 24 fall in 27.5 section 4's 96 INTERESTING bins.
//
//   gap: 2856 bins excluded while reachable, 24 of them interesting,
//   and the coverage report reads HIGHER on cfg B than on cfg A because
//   the same 576 bins fill faster on a bigger device.

The gap is 2,856 wrongly excluded bins, and the 24 is the number that matters. DERIVED: 27.5 §4 establishes that only 96 bins of the naive cross test anything, so 24 wrongly-excluded interesting bins is a quarter of the entire informative space — and the coverage figure went up.

That inversion is this item's whole difficulty and it is worth stating as a rule. DERIVED: coverage is a ratio, an exclusion reduces the denominator, and a stale exclusion therefore improves the headline number exactly when it becomes wrong. CURRICULUM-DERIVED from 33.2 §9's denominator-independence item — the same defect class, moved from a design's utilisation register into a project's coverage report, and the review question is identical: what would have to happen for this number to read low?

And the pass criterion has a sharp form: the exclusion set must be a function, not a file. DERIVED: a generated exclusion set re-derives on every elaboration and cannot go stale; a checked-in one is a snapshot of an argument whose premises are not recorded. CURRICULUM-DERIVED from 32.1 §15's variety 11 and 18.4 §1's grades: a static exclusion file is grade A evidence — documented for a named configuration — consumed as though it were grade B.

13. Review Item 8 — What Does This Supplied Component Not Check, Established How?

CURRICULUM-DERIVED from 27.6, which owns this and frames it exactly: the integration question “is not how to connect it” but “what you are now unable to see” — and it names the mechanism: a VIP's compliance claim is 27.1's unenumerated claim in a new place.

27.6 establishes the problem and the two integration modes. This item is the artifact that answers it, and the artifact is an experiment because no other method works. DERIVED: a datasheet lists what a component checks; only an injection establishes what it reports under the conditions your design produces.

// ROBUST ENVIRONMENT: an injection matrix over the obligation list,
// run against the SUPPLIED component, with the answer recorded.
package vip_observability_pkg;

  // The obligation list. CURRICULUM-DERIVED from 30.9 section 2's obligation
  // set for a DDR controller, taken as given and not re-derived.
  typedef enum int {
    OB_TRCD, OB_TRAS, OB_TRP, OB_TRRD, OB_TFAW, OB_TURN_RW,
    OB_TURN_WR, OB_REFRESH, OB_LEGAL_CMD, OB_ADDR_MAP,
    OB_DATA_INTEGRITY, OB_ORDERING, OB_ZQ
  } obligation_e;

  typedef enum int { CAUGHT, SILENT, UNTESTABLE } outcome_e;
endpackage

class vip_observability;
  import vip_observability_pkg::*;

  outcome_e result[obligation_e];
  string    note[obligation_e];

  function void record(obligation_e ob, outcome_e oc, string n);
    result[ob] = oc; note[ob] = n;
  endfunction

  function void classify(output int unsigned covered,
                         output int unsigned silent,
                         output int unsigned untestable,
                         output int unsigned unknown);
    covered = 0; silent = 0; untestable = 0; unknown = 0;
    for (obligation_e ob = ob.first(); 1; ob = ob.next()) begin
      if (!result.exists(ob))            unknown++;
      else case (result[ob])
        CAUGHT:     covered++;
        SILENT:     silent++;
        UNTESTABLE: untestable++;
      endcase
      if (ob == ob.last()) break;
    end
  endfunction

  // The correlated-failure check 27.6 names: if the VIP's model and the
  // design share a vendor interpretation, an injection of THAT
  // interpretation is caught by neither.
  function void record_shared_interpretation(obligation_e ob, string n);
    result[ob] = UNTESTABLE; note[ob] = n;
  endfunction
endclass

// INTENTIONALLY DEFECTIVE. WEAK ENVIRONMENT: the compliance claim is
// taken as the coverage statement.
//
//   // env.sv
//   // Vendor VIP is JEDEC-compliant per its datasheet section 2.1;
//   // all protocol checking is delegated. Our checkers cover the
//   // host-side interface only.
//
// CONTRACT VIOLATED: 27.1's completeness argument -- a compliance claim
// is unenumerable, so "compliant" does not enumerate what is checked.
//
// WHY IT SURVIVES: the VIP is good. It catches most things. The
// delegation is reasonable, documented, and made by experienced people.
// Nothing about it is careless.
//
// TRACE (ILLUSTRATIVE, 13 obligations injected against the VIP):
//   robust matrix result:
//     CAUGHT      9  (tRCD tRAS tRP tRRD tFAW tURN_RW tURN_WR
//                     OB_LEGAL_CMD OB_DATA_INTEGRITY)
//     SILENT      3  (OB_REFRESH -- reports per-bank but not the
//                     rolling window; OB_ADDR_MAP -- outside its view;
//                     OB_ORDERING -- it has no host-side request order)
//     UNTESTABLE  1  (OB_ZQ -- 7.7's unverifiable result: the interface
//                     does not report the outcome, so no injection can
//                     be observed)
//   weak claim: "13 of 13, the VIP is compliant"
//
//   gap: 3 obligations SILENT and believed covered; 1 obligation whose
//   unobservability is a property of the protocol and must be handled
//   some other way entirely.
//
//   And the one that matters most: OB_ADDR_MAP is SILENT because the
//   VIP sits at the DDR pins and an address-map error is a host-side
//   concept -- so BOTH the "delegated" note and the "host-side only"
//   note exclude it. Nobody checks it, and both notes are true.

The gap is 3 silent and 1 untestable, and the OB_ADDR_MAP row is the escape this item exists for. DERIVED: two correct scope statements, composed, leave an obligation with no owner — the VIP checks pins and cannot see an address map; the local checkers check the host side and delegate protocol. Neither statement is wrong and their union is not the obligation set.

CURRICULUM-DERIVED from 27.7, which owns the composition and names the same shape at environment scale: it identifies the device-level component that finally owns 27.4 §6's cross-bank obligations — an obligation that the distributed scoreboards left unowned precisely because each was correct about its own bank. DERIVED: this item and 27.7's finding are one phenomenon — correct components with correct scopes, composed, produce a gap that no component's review can see.

And the UNTESTABLE row must stay in the matrix rather than being dropped. CURRICULUM-DERIVED from 28.4 §2 and 7.7: for ZQ calibration, “did it work?” is not a question digital logic can answer at all. DERIVED: an obligation marked untestable is a standing entry in the residual-risk register, and an obligation silently absent from the matrix is the same risk with no record.

14. Review Item 9 — Is This Property Complete About the Mechanism and Silent About the Magnitude?

This is the twelfth variety, and §15 states it. This section is the model it was derived from.

CURRICULUM-DERIVED from 33.3 §18, which produced the evidence rather than the argument: three mutations — a sweep width, a staleness threshold, a drift fraction — kept every mechanism correct, passed all nineteen properties, kept all twelve covers non-zero, and made the design worse. Run 30.9 §7's three questions against the properties that let them through and all three answer cleanly.

// ROBUST ENVIRONMENT: each quantity a mechanism operates on is bound to
// an artifact, and the property set asserts the BOUND as well as the
// mechanism.
package quantity_bound_pkg;
  // 18.4 section 1's four evidence grades, made a type so a review can
  // audit category drift mechanically.
  typedef enum int { GRADE_A, GRADE_B, GRADE_C, GRADE_D } grade_e;

  typedef struct {
    string       quantity;      // the parameter
    string       artifact;      // what bounds it
    grade_e      grade;         // the grade that artifact holds
    grade_e      used_as;       // the grade it is CONSUMED at
    int unsigned lo;
    int unsigned hi;
  } bound_t;

  // ILLUSTRATIVE bounds for 33.3's three surviving mutations.
  bound_t BOUNDS[] = '{
    '{"sweep_taps",  "PHY hardware range register",   GRADE_B, GRADE_B, 32, 64},
    '{"stale_ticks", "thermal drift characterisation",GRADE_C, GRADE_C, 64, 512},
    '{"drift_num",   "eye-width vs temperature data", GRADE_C, GRADE_C,  1,   1},
    '{"drift_den",   "eye-width vs temperature data", GRADE_C, GRADE_C,  2,   8}
  };
endpackage

module quantity_bound #(
    parameter int SWEEP_TAPS  = 48,
    parameter int STALE_TICKS = 256,
    parameter int DRIFT_NUM   = 1,
    parameter int DRIFT_DEN   = 4
)(
    input  logic clk,
    input  logic rst_n,
    output logic bounds_ok,
    output logic grades_ok
);
  // The bound check, at elaboration. This is the whole item: a property
  // about the MECHANISM cannot express it, because the quantity is not
  // a signal.
  initial begin
    if (!(SWEEP_TAPS inside {[32:64]}))
      $error("sweep_taps %0d outside its bounding artifact's range [32:64]",
             SWEEP_TAPS);
    if (!(STALE_TICKS inside {[64:512]}))
      $error("stale_ticks %0d outside [64:512]", STALE_TICKS);
    if (!(DRIFT_DEN inside {[2:8]}))
      $error("drift_den %0d outside [2:8]", DRIFT_DEN);
    if (DRIFT_NUM != 1)
      $error("drift_num %0d: the characterisation supports 1 only", DRIFT_NUM);
  end

  // And the runtime companion: the quantity is PUBLISHED beside the
  // verdict, so a reviewer reading a green report sees the value that
  // made it green.
  always_comb begin
    bounds_ok = (SWEEP_TAPS  >= 32) && (SWEEP_TAPS  <= 64)
             && (STALE_TICKS >= 64) && (STALE_TICKS <= 512)
             && (DRIFT_DEN   >=  2) && (DRIFT_DEN   <=   8)
             && (DRIFT_NUM   ==  1);
    grades_ok = 1'b1;   // set false by the audit below on category drift
  end
endmodule

// INTENTIONALLY DEFECTIVE. WEAK ENVIRONMENT: the properties are
// complete about the mechanism and the quantities are unbounded.
//
//   // no BOUNDS table, no elaboration-time range checks. The property
//   // set is 33.3's nineteen, verbatim and correct:
//   assert property (p_start_only_when_permitted);   // mechanism: right
//   assert property (p_margin_fits_the_window);      // mechanism: right
//   assert property (p_failure_has_a_cause);         // mechanism: right
//   ...
//
// CONTRACT VIOLATED: none that the eleven varieties name. This is the
// GAP -- section 15 opens variety 12 for it.
//
// WHY IT SURVIVES: every property is correct, reachable, non-vacuous,
// independent, two-sided where 30.3 section 9 requires it, and covered on
// the dimension 31.2 section 14 requires. There is no property review
// finding to make. The property set is exemplary.
//
// TRACE (33.3's three surviving mutations, re-run against both):
//   M14  SWEEP_TAPS  48 -> 64   (== hw_taps: boot time up, no gain)
//        robust: elaboration ERROR? no -- 64 is inside [32:64].
//                bounds_ok 1. NOT CAUGHT, and correctly so: the bound
//                admits it. The finding is a BOOT-TIME trade, which is
//                Module 23's, not this gate's.
//        weak:   not caught.
//   M15  STALE_TICKS 256 -> 65535
//        robust: elaboration ERROR -- outside [64:512]. CAUGHT.
//        weak:   not caught. `trusted` becomes effectively permanent
//                and every property still passes.
//   M16  DRIFT_NUM/DEN -> 0/4   (zero margin budget)
//        robust: elaboration ERROR -- drift_num must be 1. CAUGHT.
//        weak:   not caught. Every margin becomes satisfiable and
//                p_margin_fits_the_window passes trivially --
//                which is variety 6 REACHED THROUGH a quantity.
//
//   gap: quantity mutations caught, robust 2 of 3, weak 0 of 3.
//   And M14's non-catch is the honest result: a bound cannot adjudicate
//   a trade-off, only a range.

The gap is 2 of 3, and the third is the finding. DERIVED: M15 and M16 are caught because they leave the bounding artifact's range; M14 stays inside it and is still a regression — it doubles boot time for no margin. A bound catches a quantity that is wrong. It cannot catch a quantity that is worse, because “worse” is a trade-off and a trade-off needs an objective.

M16 deserves its own line because of what it does to a correct property. Setting the drift budget to zero makes p_margin_fits_the_window pass trivially — margin_required becomes 0 and 0 fits every window. DERIVED: a quantity can render a correct, previously non-vacuous property vacuous without touching the property — so variety 6 is reachable through a parameter, and no antecedent cover changes. CURRICULUM-DERIVED from 27.2: vacuity is a property of the run, and this is a mechanism for producing it that the corpus measurement does not see, because the antecedent still fires.

15. The Twelfth Variety

The track has eleven named ways a green assertion proves nothing. This section adds the twelfth, and states plainly what evidence produced it.

12 — Complete about the mechanism, silent about the magnitude. The property correctly and exhaustively constrains what the design does, and says nothing about the quantities the doing operates on — so a design can be made materially worse by changing a number, with every property green, every antecedent hit, every checker independent, and no coverage gap.

Run 30.9 §7's three questions against p_margin_fits_the_window and watch all three pass. Which signal, if corrupted, would make this property fail? — window_low, window_high, chosen_valid; it names them. On which cycles is it non-vacuous? — every cycle a window is committed, and there is a cover. What does it not constrain? — and here the honest answer is “the value of DRIFT_DEN”, which is not a thing the question was shaped to elicit.

DERIVED: question 3's answer list in 30.9 §7 has three branches — safety without progress (variety 8), comparative obligations (variety 3), and derived statistics (variety 5). None of them is “a parameter.” So the taxonomy's own review procedure has a fourth branch it did not enumerate, and that is the strongest evidence that variety 12 is a genuine addition rather than a re-description.

Three consequences follow, and the third is the one worth carrying.

First, variety 12 is not detectable by any property review, because the finding is the absence of a constraint on something that is not a signal. The artifact is a parameter census, which is why §16 ranks this item by grep cost and not by simulation cost.

Second, variety 12 can manufacture variety 6. §14's M16 turned a correct, covered, non-vacuous property vacuous by changing a parameter, and the antecedent cover kept firing. DERIVED: the standard fix for vacuity — publish the antecedent as a cover — does not detect vacuity induced this way, which makes variety 12 the first entry in the taxonomy that interacts with another entry rather than sitting beside it.

Third — and this is the honest limit — variety 12's fix is a range, and a range is not an objective. §14's M14 stayed inside its bound and was still a regression. DERIVED: bounding every quantity closes the wrong-value case and leaves the worse-value case entirely open, and closing that needs a performance objective rather than a verification artifact. That is 33.5's gate, and §25 hands it over with the specific case named.

And one candidate was considered for a thirteenth and declined, with a reason. §7's finding — a correct property whose evidence a reviewer cannot obtain because the antecedent count is not in the signed-off report — is a defect in a report, not in a property. DERIVED: the eleven varieties classify properties; admitting report defects would make the taxonomy a list of everything that can go wrong in a project, and it would lose the property that makes it usable — that each entry names something you can find by looking at one property. It is recorded here as the reason variety 6 is under-detected in practice, and §7 is its review item. The thirteenth slot stays unopened.

16. The Review Assembled

Cost-ordered. DERIVED from §20's table. Unlike the three preceding gates, the cheap items here are cheap because they are lookups of artifacts that already exist — and the expensive ones are expensive because the artifact has to be built.

Four of the nine take minutes, and all four are greps or file lookups. DERIVED: §14 (the new variety), §12, §9 and §7 need no simulation at all — and between them they cover the twelfth variety, variety 10 applied to exclusions, variety 7, and variety 6's detectability. A reviewer with an hour and a shell finds four of this chapter's nine findings.

But the two most expensive items are the two that produce the findings nobody else can produce, and that asymmetry is this gate's central economics. DERIVED: items 8 and 9 are the only two whose method is injection, and injection is the only method that answers “could this have failed?” Every other item reasons about the environment's structure; these two test it. CURRICULUM-DERIVED from 27.3's cannot-fail failure mode: structure cannot distinguish a checker that passes from one that cannot fail, and only a fault can.

And three items compose into one artifact, which is the practical recommendation this chapter makes. Items 7, 8 and 10 all want the same thing: a per-property row carrying the antecedent count, the magnitude reached on its dimension, and the date of the run in which it last failed. DERIVED: one table with three columns closes three of nine items, and no tool produces it by default.

17. Quantitative Reasoning

Sort the gaps by what the weak environment's report showed and the pattern is the sharpest of the four gates.

DERIVED: seven of nine weak environments produce a report that is better-looking than the correct environment's, and that is not a coincidence — it is the definition of the failure. At the three preceding gates the weak build was silent; here the weak build is complimentary.

The mechanism is uniform and worth stating as this chapter's law. Every one of the seven removed a measurement, and the removed measurement was the one capable of producing an unflattering number. Deferral counts, antecedent counts, magnitudes, legal-set cardinalities, injection outcomes, re-derived denominators. DERIVED: a verification environment's quality is inversely correlated with how good its report looks, up to the point where the report starts publishing the quantities that could be bad.

CURRICULUM-DERIVED from 33.3 §16, which found the same inversion in three of nine PHY items and named its mechanism — a design that reports no failures of a check it does not perform is indistinguishable, in its telemetry, from a design that passes that check. DERIVED: at this gate the ratio is seven of nine rather than three of nine, because an environment is its reporting.

18. What the Assertions Prove

  // The unit under test here is an ENVIRONMENT, so most obligations are
  // class-level and checked by the audit functions above. These are the
  // ones that are genuinely temporal, plus the elaboration-time checks
  // that section 15's variety 12 requires -- and variety 12's whole point is
  // that some obligations are NOT properties.

  // ---- Section 6: configuration reach. The dimension census, asserted.
  property p_every_dimension_randomised;
    @(posedge clk) disable iff (!rst_n)
      cfg_applied |-> (dims_randomised == DIMS_DECLARED);
  endproperty
  assert property (p_every_dimension_randomised)
    else $error("a declared dimension is not randomised by the environment");

  property p_nonnominal_is_reached;
    @(posedge clk) disable iff (!rst_n)
      run_end |-> (nonnominal_runs > 0);
  endproperty
  assert property (p_nonnominal_is_reached)
    else $error("no run in this regression used a non-nominal configuration");

  // ---- Section 7: antecedent publication. The property that makes a
  // vacuous property VISIBLE rather than correct.
  property p_no_property_passes_unproven;
    @(posedge clk) disable iff (!rst_n)
      signoff |-> (unproven_count == '0);
  endproperty
  assert property (p_no_property_passes_unproven)
    else $error("a property passed with a zero antecedent count");

  property p_manifest_covers_every_implication;
    @(posedge clk) disable iff (!rst_n)
      signoff |-> (manifest_rows == implication_count);
  endproperty
  assert property (p_manifest_covers_every_implication)
    else $error("an implication has no manifest row: its vacuity is unmeasurable");

  // ---- Section 8: cover dimensions. Scale-vacuity, asserted rather than
  // inspected -- 31.2 section 14.
  property p_no_scale_vacuous_cover;
    @(posedge clk) disable iff (!rst_n)
      signoff |-> (scale_vacuous_count == '0);
  endproperty
  assert property (p_no_scale_vacuous_cover)
    else $error("a cover was hit but its dimension never reached its threshold");

  property p_threshold_has_a_mechanism;
    @(posedge clk) disable iff (!rst_n)
      cover_registered |-> (threshold_reason_len > 0);
  endproperty
  assert property (p_threshold_has_a_mechanism)
    else $error("a cover threshold was chosen with no stated mechanism");

  // ---- Section 9: model independence. Asserted as a MUTATION RESULT,
  // because independence is not a signal -- 27.3, and 30.6 section 11's
  // variety 3 in a new place: the obligation needs a model of the model.
  property p_model_catches_every_mutation;
    @(posedge clk) disable iff (!rst_n)
      audit_done |-> (mutations_caught == mutations_run);
  endproperty
  assert property (p_model_catches_every_mutation)
    else $error("the reference model agreed with a mutated design");

  // ---- Section 10: checker liveness.
  property p_no_inert_checker;
    @(posedge clk) disable iff (!rst_n)
      control_run_done |-> (inert_count == '0);
  endproperty
  assert property (p_no_inert_checker)
    else $error("a checker did not fire under its own injected fault");

  property p_every_checker_controlled;
    @(posedge clk) disable iff (!rst_n)
      control_run_done |-> (uncontrolled_count == '0);
  endproperty
  assert property (p_every_checker_controlled)
    else $error("a checker has no positive control in the matrix");

  // ---- Section 11: expected-set cardinality. Two-sided, because a set
  // that is too LARGE and one that is too SMALL are different bugs and
  // only one of them is loud.
  property p_reject_outside_legal_set;
    @(posedge clk) disable iff (!rst_n)
      (return_seen && !in_legal_set) |=> sb_rejected;
  endproperty
  assert property (p_reject_outside_legal_set)
    else $error("a return outside the computed legal set was accepted");

  property p_accept_inside_legal_set;
    @(posedge clk) disable iff (!rst_n)
      (return_seen && in_legal_set) |=> !sb_rejected;
  endproperty
  assert property (p_accept_inside_legal_set)
    else $error("a legal return was rejected: the set is too small");

  property p_cardinality_is_computed;
    @(posedge clk) disable iff (!rst_n)
      return_seen |-> (legal_card <= outstanding_count);
  endproperty
  assert property (p_cardinality_is_computed)
    else $error("the legal set is larger than the outstanding set: it is a superset");

  // ---- Section 12: exclusion provenance. Variety 10, mechanised.
  property p_exclusions_rederive;
    @(posedge clk) disable iff (!rst_n)
      cfg_changed |=> (excluded_count != $past(excluded_count))
                   || (cfg_equivalent);
  endproperty
  assert property (p_exclusions_rederive)
    else $error("the exclusion set did not change when the configuration did");

  property p_no_reachable_bin_excluded;
    @(posedge clk) disable iff (!rst_n)
      signoff |-> (newly_reachable_count == '0);
  endproperty
  assert property (p_no_reachable_bin_excluded)
    else $error("a bin is excluded as unreachable and is reachable here");

  // ---- Section 13: VIP observability.
  property p_no_unknown_obligation;
    @(posedge clk) disable iff (!rst_n)
      matrix_done |-> (unknown_count == '0);
  endproperty
  assert property (p_no_unknown_obligation)
    else $error("an obligation has no injection result: coverage is claimed, not shown");

  property p_silent_obligations_are_owned;
    @(posedge clk) disable iff (!rst_n)
      matrix_done |-> (silent_count == silent_owned_count);
  endproperty
  assert property (p_silent_obligations_are_owned)
    else $error("an obligation is silent in the VIP and owned by nobody");

  // ---- Section 14: quantity bounds. NOT a property of a signal, which is
  // the finding. These are elaboration-time, and that is the point.
  property p_quantities_within_bounds;
    @(posedge clk) disable iff (!rst_n) bounds_ok;
  endproperty
  assert property (p_quantities_within_bounds)
    else $error("a quantity lies outside the range its bounding artifact supports");

  property p_no_grade_drift;
    @(posedge clk) disable iff (!rst_n) grades_ok;
  endproperty
  assert property (p_no_grade_drift)
    else $error("a quantity is consumed at a higher evidence grade than it holds");

  // ---- COVERS. Each on the dimension its defect scales with, and two of
  // them are on dimensions that belong to the ENVIRONMENT'S MODEL --
  // which is section 6's whole item.
  // Section 6: a run with MORE THAN ONE non-nominal dimension. A single
  // non-nominal dimension is reachable by luck; two is a design choice.
  cover property (@(posedge clk) disable iff (!rst_n)
                  run_end && (nonnominal_count >= 2));
  // Section 7: a property that is PASSING and UNPROVEN simultaneously --
  // the state 27.2's documented instance was in, uncovered.
  cover property (@(posedge clk) disable iff (!rst_n)
                  signoff && (unproven_count > 0));
  // Section 8: a cover whose magnitude reached its threshold. The
  // dimension is MAGNITUDE, not occurrence -- 31.2 section 14.
  cover property (@(posedge clk) disable iff (!rst_n)
                  cover_registered && (max_seen_val >= threshold_val));
  // Section 9: a mutated design DISAGREEING with the model. Without this
  // cover, p_model_catches_every_mutation is vacuous when zero
  // mutations ran -- which is the default state of most projects.
  cover property (@(posedge clk) disable iff (!rst_n)
                  audit_done && (mutations_run > 0));
  // Section 10: a checker FIRING under injection. The positive control's
  // own positive control.
  cover property (@(posedge clk) disable iff (!rst_n)
                  control_run_done && (live_count == MATRIX_ROWS));
  // Section 11: a legal set of cardinality ONE -- the only case where a
  // superset checker and a correct checker must agree, and therefore the
  // case that proves the stimulus reached the interesting region.
  cover property (@(posedge clk) disable iff (!rst_n)
                  return_seen && (legal_card == 1) && (outstanding_count > 1));
  // Section 12: a SECOND configuration elaborated. The dimension is
  // configuration COUNT, and one configuration never reaches it.
  cover property (@(posedge clk) disable iff (!rst_n) cfg_changed);
  // Section 13: an obligation marked SILENT -- covered because a matrix
  // with no silent rows is more likely incomplete than perfect.
  cover property (@(posedge clk) disable iff (!rst_n)
                  matrix_done && (silent_count > 0));
  // Section 14: a quantity at the EDGE of its bound. The interior is
  // uninformative; the edge is where a bound is either right or wrong.
  cover property (@(posedge clk) disable iff (!rst_n)
                  bounds_checked && at_bound_edge);
  // And the mutation that variety 12 exists for: a quantity change with
  // every property still passing.
  cover property (@(posedge clk) disable iff (!rst_n)
                  quantity_mutated && all_properties_pass);

Reviewed against the now-twelve varieties, and three observations are worth recording because they are about this property set rather than about the items.

Variety 3 — the obligation is inexpressible without a model — governs §9, recursively, and that is not a wordplay. The obligation is the model is independent of the design, which requires comparing two algorithms, and no property compares algorithms. CURRICULUM-DERIVED from 30.6 §11: the obligation needs a model. DERIVED: here the thing needing a model is a model, so the artifact is a mutation harness — and p_model_catches_every_mutation is an assertion about the harness's output, not about the design.

Variety 6 governs four of this set's properties, and the covers written for them are unusual. p_model_catches_every_mutation, p_no_inert_checker, p_no_unknown_obligation and p_no_scale_vacuous_cover all have antecedents that are project activities — audit_done, control_run_done, matrix_done, signoff. DERIVED: in a project that never runs a mutation audit, p_model_catches_every_mutation is vacuous and green, which is precisely the state §10's weak environment was in for its whole life. So the cover mutations_run > 0 is not decoration — it is the only thing separating “the model is independent” from “nobody checked.”

And variety 12 governs its own section, which is the structural point of §15. p_quantities_within_bounds and p_no_grade_drift are runtime shadows of elaboration-time checks, written that way so a property-based sign-off flow can see them at all. DERIVED: the honest statement is that variety 12's real fix is not a property — it is the initial block in §14 and the BOUNDS table it reads, and the two properties here exist so that the finding appears in the same report as everything else.

19. Mutation Testing

Baseline first: all nineteen assertions pass and all ten covers are non-zero. Mutations are applied to the robust environment, which means each one is a plausible simplification a reviewer might wave through.

DERIVED: fourteen of seventeen killed, three survived — and the three survivors form a set with a single explanation, which is the same explanation §15 gave for variety 12's limit.

M8, M16 and M17 each weaken a quantity or a scope rather than a mechanism. One mutation instead of six is still a mutation audit; a bound of [0:2**32-1] is still a bound; dropping the grade-drift column still leaves the range check. All three keep every mechanism intact and make the environment materially weaker.

That is variety 12 applied to this chapter's own models, and it is the strongest confirmation the variety is real. DERIVED: the property set written to detect variety 12 is itself subject to variety 12, because p_quantities_within_bounds constrains the mechanism that a bound is checked and says nothing about how wide the bound is. A bound with no width requirement is a mechanism with no magnitude, which is the variety's definition.

M8 is the one to act on, and it has a concrete fix that no property can express. CURRICULUM-DERIVED from this track's standing mutation discipline: a mutation run needs a passing baseline or every mutation false-kills — and its companion here is a minimum mutation-set size, justified by the algorithm's branch count. DERIVED: §9's tracker has six distinguishable failure modes, so a six-mutation set is the smallest that exercises each; one mutation proves the harness runs and nothing else. That number belongs in a document, not a property.

And two mutations are killed only by a cover — M2 and M13, plus M11 which needs the cardinality-one cover. M13's is the sharpest: caching the exclusion set is invisible until a second configuration is elaborated, and the cover's dimension is configuration count. CURRICULUM-DERIVED from 31.2 §14: running one configuration for a year never reaches it, which is the same finding §6 makes about the design and §8 makes about covers — three items, one dimension, and it is the dimension a regression farm cannot buy.

20. Baseline Defects Found Before Mutation

Each of the nine weak environments run against the robust environment's property set and audits, before any mutation.

DERIVED: five of nine weak environments are visible without running anything — §6, §7, §11, §12 and §14. Four of those five are a single file lookup or a single grep.

That is the highest cheap-detection rate of the four gates, and the reason is worth stating because it is counter-intuitive. DERIVED: 33.2's gate found five of nine in source text; 33.3's found two of nine; this gate finds five of nine — and unlike 33.2's, these five are found in artifacts rather than in code. A localparam where a rand belongs, a missing manifest row, an absent legal-set function, a checked-in exclusion file, a parameter in no property. An environment's defects are unusually legible because an environment is mostly declaration.

And the four expensive items are expensive in a specific way: each needs an artifact that does not exist and whose absence is itself the finding. DERIVED: items 9, 10, 13 and 8 require a mutation harness, an injection matrix, a vendor injection matrix, and a magnitude column — so for each, the review's first output is not a verdict but a work item. CURRICULUM-DERIVED from 33.3 §15's finding that a PHY review must also produce a list of artifacts it could not obtain: at this gate the list is shorter and the items on it are ones the project could build itself, which makes them harder to defer and easier to refuse.

One more asymmetry, and it is the reason §10 is last in §16's ordering rather than third. Items 9, 10 and 13 all need a regression whose passing condition is failure. DERIVED: that is not a technical cost, it is an infrastructure cost — every piece of CI a project owns treats red as bad, and an injection suite inverts that for one job. The item most likely to be absent in a mature project is not the hardest one; it is the one that requires a green light to mean something different.

21. Silicon Observability

This gate's subject never reaches silicon, so this section reads the other way: what a silicon failure tells you about which item was skipped.

Three rows are diagnostic enough to name, and each points at exactly one item.

§9: the scoreboard was written for this bug and never reported it. DERIVED: that is not a coverage gap and not a stimulus gap — the stimulus reached it and the comparison agreed. CURRICULUM-DERIVED from 27.3's cannot-fail mode: the only remaining explanation is that the checker shares the design's computation, and the check is a grep of the model's imports.

§11: reordering-dependent corruption with a clean scoreboard. DERIVED: a correct scoreboard rejects an illegal order; a superset scoreboard accepts it. The signature is silicon-specific because reordering under real load explores orders the regression's distribution did not, and the escape is not a missing check but a check whose legal set was widened until it stopped complaining — 33.2 §14's rule, applied to the environment.

§14: legal, correct, and worse than specified. DERIVED: no assertion fires because nothing is illegal; no scoreboard mismatches because the data is right. CURRICULUM-DERIVED from 30.3 §9's variety 8 — safety cannot detect conservatism — and variety 12 is its generalisation: the quantity was in range for the mechanism and wrong for the system. The measurement that finds it is a bandwidth or margin number compared against a computed expectation, which is 33.5's instrument and not this gate's.

And one row is a warning about attribution rather than an observation: §7's. A green property beside a first-silicon bug is the most common shape of an escape, and it does not tell you which of the twelve varieties applies. DERIVED: the antecedent count separates variety 6 from the other eleven in one lookup — which is why §7's item is about the report rather than the property, and why its cost is minutes in §16's ordering.

22. Common Wrong Answers

1. “The regression is green, so the design is verified.” Seven of the nine weak environments here produce a green regression with a better-looking report than the correct one. Green is a statement about what ran, and §17's second table is the list of things it does not state.

2. “We ran ten billion transactions.” At one configuration. §6: 5 of 5 injected defects detected versus 0 of 5, at identical transaction counts. Verification effort and verification reach are different quantities, and only one of them is easy to publish.

3. “Our functional coverage is 96%.” Of what denominator? CURRICULUM-DERIVED from 27.5 §4: a naive DDR cross is 11,520 bins, 288 legal, 96 informative. 96% of 11,520 and 96% of 96 are different claims and the report does not distinguish them.

4. “Coverage went up on the product configuration, so we are in better shape.” §12: it went up because the stale exclusion file shrank the denominator while 2,856 bins became reachable. Coverage is a ratio, and an exclusion improves it exactly when it becomes wrong.

5. “All our properties passed.” CURRICULUM-DERIVED from 27.2: 78.5% of this curriculum's 843 properties are implications. A 100% pass rate over such a set is consistent with most of it proving nothing, and the pass rate cannot tell you which.

6. “We have covers for our antecedents.” Are their counts in the report you signed off? §7: six correct properties, six correct covers, three vacuous, and zero reviewer-verifiable — because the sign-off script exported pass/fail only.

7. “Every cover is hit, 100%.” §8: four of seven were hit and never reached their magnitude. CURRICULUM-DERIVED from 31.2 §14: a cover proves a condition occurred, not that it occurred at a scale where the defect is observable.

8. “We will run longer.” That fixes two of §8's four scale-vacuous covers and neither of the other two, whose dimensions are a configuration and a reset type. When the dimension belongs to the environment's model, duration is not a lever.

9. “The reference model is well-tested — we reused the design's tracker.” §9: 6 of 6 mutations caught versus 1 of 6, and the one was outside the shared code. Reuse is good engineering everywhere except between a design and its checker.

10. “The scoreboard has never reported a mismatch.” Consistent with a correct design and equally consistent with a scoreboard that cannot produce one (27.3). §10 found 2 of 7 checkers inert for the project's whole life.

11. “We do not need positive controls; our checkers are reviewed.” Both inert checkers in §10 were variety 7, which 30.9 §6 costs at read the checker's inputs. A cheap check that nobody runs has the same yield as an expensive one.

12. “The scoreboard used to report false failures and we fixed it.” Ask what the fix stopped rejecting. §11: the legal set became “anything outstanding” — 3.3× too large — and 9 of 64 illegal returns were accepted. The commit message was honest.

13. “The exclusion list was reviewed when it was written.” It was correct then. §12: variety 10 applied to an exclusion — a claim of unreachability is a claim about the parameterised state space, and it was sound at one elaboration. An exclusion set must be a function, not a file.

14. “The VIP is JEDEC-compliant, so protocol checking is covered.” CURRICULUM-DERIVED from 27.6 and 27.1: a compliance claim is an unenumerated claim in a new place. §13: 9 of 13 demonstrated, 3 silent, 1 untestable.

15. “We check the host side and the VIP checks the DDR side, so between us it is covered.” §13's OB_ADDR_MAP row: two true scope statements whose union is not the obligation set. CURRICULUM-DERIVED from 27.7's device-level component, which exists because distributed scoreboards each correct about their own bank left the cross-bank obligations unowned.

16. “An untestable obligation should come off the list.” It should stay on it, marked. CURRICULUM-DERIVED from 7.7 and 28.4 §2: for a mechanism whose outcome the interface does not report, “did it work?” is not a digital question. An obligation marked untestable is a residual-risk entry; one silently absent is the same risk with no record.

17. “Every property is correct, reachable, non-vacuous and independent, so the property set is done.” That is the twelfth variety's precondition, not its refutation. §14: three quantity mutations passed a nineteen-property set that satisfies all four conditions.

18. “If a parameter mattered, a property would mention it.” Inverted — the parameters that matter most are the ones no property mentions, because a property constrains relationships between signals and a parameter is not a signal. §16 ranks this check first, at grep cost.

19. “We bound our parameters, so variety 12 is handled.” M16: widening every bound to its type's range is still a bound. A mechanism with no magnitude requirement is the variety's definition, and the property set written to detect it is subject to it.

20. “A surviving mutation always means a missing property.” Three survivors here — M8, M16, M17 — and none has a property fix. A minimum mutation-set size, a bound width, and an evidence-grade column all belong in documents. CURRICULUM-DERIVED from this track's standing rule that a survivor is often a design finding rather than a coverage gap.

21. “This is all verification-team work, not design review.” Four of nine items are greps a designer can run in an hour — a config class's localparams, a model's imports, a checked-in exclusion file, a parameter list against property text. The expensive items need infrastructure; the cheap ones need somebody to look.

22. “We would have caught it in the next release.” §10's two inert checkers were inert for the project's life, and nothing in any release would have changed that — an inert checker is deterministic. The only event that finds it is an injection somebody decided to write.

23. Self-Check

1. A config class has three rand fields and five localparams. State the review finding in one sentence, and say which of 33.3's nine defects it lets through.
2. A sign-off report shows 240 properties, 100% passing. What is the second number you ask for, and what does its absence mean for 78.5% of the set?
3. A cover on dev_owns reads 100% on every run. The defect needs 256 held cycles. Name the phenomenon, and say which two of four such covers in §8 have a compute-time fix.
4. A reference model imports a class from the design's package. What is the mutation experiment, and what result would you expect if the import is the only problem?
5. A scoreboard has reported zero mismatches in three years. Give two hypotheses and the one experiment that separates them.
6. A scoreboard accepts any outstanding tag. What was the bug it was fixed to remove, what did the fix cost, and what single number would have exposed it?
7. An exclusion file is checked into the repository, dated, and was reviewed when written. Which of the twelve varieties applies, and why does the coverage number go up when the exclusion becomes wrong?
8. A VIP's datasheet claims JEDEC compliance and your team checks the host side. Name the obligation class that this arrangement leaves unowned, and say why both statements are true.
9. An obligation cannot be checked by any injection because the interface does not report the outcome. What do you do with it, and what is the cited precedent?
10. A nineteen-property set is correct, reachable, non-vacuous, independent, two-sided and covered on the right dimensions. A parameter change makes the design worse and everything stays green. Name the variety, the tell, and the artifact that fixes it.
11. Why is §7's finding not a twelfth variety, and what would admitting it cost the taxonomy?
12. Three mutations of this chapter's own environment survived. What do they have in common, and what is the general statement about property sets that follows?

24. The Residual Risk

What this gate cannot catch, stated plainly — and one of the limits is a result this chapter proved on itself.

It cannot adjudicate a quantity that is inside its bound and still wrong. §14's M14 widened a sweep from 48 taps to 64, stayed inside the bounding artifact's range, doubled boot time, and gained nothing. DERIVED: variety 12's fix closes the wrong-value case and leaves the worse-value case entirely open, because worse requires an objective and this gate has none. That is 33.5's subject.

It cannot verify its own quantities. M8, M16 and M17 survived: one mutation instead of six, a bound as wide as its type, a dropped grade column. DERIVED: the property set built to detect variety 12 is subject to variety 12, and the only remedy is a document — a minimum mutation-set size justified by branch count, a bound width justified by a characterisation range. Neither is expressible as a property, which is the variety's defining feature and therefore not a fixable gap.

It cannot tell you whether the obligation list is complete. Every item here is relative to a list of obligations taken from 30.9 §2. An obligation absent from that list is absent from §13's matrix, §7's manifest and §10's control set alike — so all nine items pass and nothing checks it. That is 33.1's gate, and its §12 commitment ledger is the instrument.

It cannot establish that a compliance claim is true. CURRICULUM-DERIVED from 27.1's completeness argument: a specification written by someone else is not enumerable, so §13's matrix measures what a component reports and never what the specification requires. A matrix reading 13 of 13 over an incomplete obligation list is the same escape one level up.

And it cannot prove that a green injection matrix stays green. DERIVED: §10's matrix is dated, and an environment refactor can make a live checker inert between releases with no test failing — the injection suite is the only thing that notices, and it notices only when re-run. The artifact this gate demands is therefore a cadence, not a document, and a cadence is the one thing a review cannot verify in a single sitting.

The honest summary: this gate's nine items decide whether an environment could have failed and whether its report would have said so. It cannot decide whether the obligations it checked were the right obligations, whether the quantities it bounded were the right quantities, or whether any of it is still true next month.

25. Where This Goes

This gate proved that an environment can be complete, green, and silent about a magnitude. The next gate is where magnitudes are the subject.

Chapter 33.5 reviews performance. The question changes from could this have failed to is this number the right number, and is it a measurement at all — and three findings from this chapter arrive at that gate as open items rather than as closed ones.

The first row is the one to carry, and it is the cleanest hand-off in this module. DERIVED: M14 is a design change that every gate so far would pass. The architecture gate has no obligation about boot time. The RTL gate sees a correct expression. The PHY gate sees a sweep inside the hardware range. This gate sees a quantity inside its bound. A regression that doubles boot time for no margin is invisible to all four, and the reason is that none of the four holds an objective — they hold contracts, and a contract is satisfied or not.

CURRICULUM-DERIVED from 30.3 §9, whose variety 8 is the special case this generalises: a design that is slower than required violates nothing, so safety properties cannot see conservatism. DERIVED: variety 12 extends that from timing conservatism to any quantity, and the extension is what makes a performance gate necessary rather than optional. 33.5 is the first gate in this module whose pass criterion is a comparison against a computed expectation rather than against a contract — and its first item is the one this chapter could not close: what does this number divide by, and what would have to happen for it to read low?