CXL Protocol Verification

Module 24 built a device: a link interface, a transaction pipeline, a memory controller, and the boundaries between them. Every one of those chapters ended on a debug lab in which the design was correct and the evidence was missing.

This chapter is about the evidence. Not about writing checkers — about what a passing suite entitles anyone to believe, which turns out to be a much smaller claim than a green regression report suggests.

Nine things stand between "a rule exists in the specification" and "that rule is verified", and a suite can fail every one of them while passing every test it contains.

1. The Engineering Problem — Nine Filters Between A Rule And Its Verification

A rule with no checker is unverified. A hundred and twenty specification rules against ninety checkers is 75% coverage, and a plan with no traceability reports a hundred. Section 5.

A checker no stimulus reaches has never spoken. Ninety checkers of which seventy-two ever evaluated is 80%, and the other eighteen have passed every regression without running. Section 6.

A vacuous pass checked nothing. A thousand evaluations of which four hundred had a false antecedent is 60% meaningful, and a pass counter reports a thousand. Section 7.

Illegal stimulus produces failures that are not defects. Fifty illegal stimuli against twenty real defects is seventy failures at 28% signal, and every one costs the same to triage. Section 8.

And a check on a range accepts every value in it. A span of ten in a hundred-value space misses nine wrong values; a check on a value misses none. Section 9.

This chapter against Module 24, stated precisely. Those four chapters own what a device must do. This one owns what it takes to know that it does — which is why every model here scores a verification effort rather than a design, and why section 14's weak definition is a regression report.

2. The One-Sentence Model

A suite that passes has proved something when every specification rule has a checker, every checker evaluated at least once, vacuous evaluations are excluded from the pass count, error paths were made reachable, and the suite itself was scored against deliberately broken designs — and every defect below is a green report over an unverified device.

3. What This Chapter Owns

Deferred:

4. Teaching-Model Boundary

Every model is a small synchronous block isolating one filter between a rule and its verification. A real verification environment is a testbench, a set of agents, a scoreboard, a coverage model, a constraint solver and a regression farm, and none of that is reproduced. What is reproduced is the arithmetic each demands, and the shape of the mistake when it is skipped.

Three simplifications are worth stating. Section 9 treats a check's strength as the size of the value set it accepts, which is a first-order stand-in for something that depends on the failure distribution. Section 13 assigns a fixed triage cost per false failure. Section 12's mutation score treats all mutants as equally meaningful, which they are not. In each case the conclusion is the same and the model is abbreviated.

Each model is built twice — a correct build and a broken build selected by a parameter. Every broken build here is a line from a status report: every rule is checked, every checker runs, every pass is meaningful, the stimulus is legal, the errors are covered, the suite is trusted because it passes. None of them is a lie — each is a claim nobody measured, and section 14 is what happens when five of six are unmeasured at once.

Figure 1 — Three filters in series, each of them a percentage nobody measures, and a report at the top right that skips all three. The chapter's arithmetic is what survives the chain.

5. RTL 1 — A Rule With No Checker Is Unverified

// RTL 1 - rule coverage. A rule with no checker is a rule nobody is verifying,
// and the specification's rule count is the only honest denominator.
module rule_coverage #(parameter int ASSUME_ALL_CHECKED = 0) (
  input  logic clk, rst_n,
  input  logic [15:0] spec_rules, checkers_written,
  input  logic        assess,
  output logic [15:0] unchecked_rules, coverage_pct,
  output logic        adequate,
  output logic [7:0]  n_assessments, n_short,
  output logic        coverage_assumed_err
);
  logic [31:0] c_q;
  logic [15:0] eff_checkers;
  // Claiming every rule is checked is what a plan with no traceability does.
  assign eff_checkers = (ASSUME_ALL_CHECKED != 0) ? spec_rules : checkers_written;
  assign unchecked_rules = (spec_rules > eff_checkers)
                           ? (spec_rules - eff_checkers) : 16'd0;
  assign c_q = (spec_rules == 16'd0) ? 32'd100
             : (({16'd0, eff_checkers} * 32'd100) / {16'd0, spec_rules});
  assign coverage_pct = (c_q > 32'd65535) ? 16'hFFFF : c_q[15:0];
  assign adequate = (coverage_pct >= 16'd95);
  // Rules with no checker, reported as covered.
  assign coverage_assumed_err = assess && (checkers_written < spec_rules)
                                && (unchecked_rules == 16'd0);

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      n_assessments <= 8'd0; n_short <= 8'd0;
    end else if (assess) begin
      n_assessments <= n_assessments + 8'd1;
      if (!adequate) n_short <= n_short + 8'd1;
    end
  end
endmodule

Five assessments. A hundred and twenty extracted specification rules.

One short when the rules are traced; none when they are assumed covered.

The denominator is the whole model. Ninety checkers is ninety checkers whichever way it is reported; what makes it 75% is dividing by a rule count somebody sat down and extracted from the specification. Without that extraction there is no denominator, and every coverage figure is a numerator with a percent sign after it.

Row five is the failure that produces the most confident wrong answer. With no rules extracted, coverage is a hundred percent by construction — and it is exactly what a project that never did the traceability work reports. The vacuous hundred and the earned hundred are indistinguishable in the number.

Row four is worth driving because a checker count above the rule count is normal, not an error: several checkers per rule is good practice. The floor reports nothing unchecked rather than wrapping, and the coverage figure above a hundred is honest about what happened.

6. RTL 2 — A Checker No Stimulus Reaches Has Never Spoken

// RTL 2 - a checker no stimulus reaches. A check that never evaluates is a
// check that has never said anything, and it counts as coverage anyway.
module checker_reachability #(parameter int ASSUME_REACHABLE = 0) (
  input  logic clk, rst_n,
  input  logic        assess,
  input  logic [15:0] checkers_written, checkers_reached,
  output logic [15:0] unreached, effective_checkers, reach_pct,
  output logic        adequate,
  output logic [7:0]  n_assessments, n_short,
  output logic        reach_assumed_err
);
  logic [31:0] r_q;
  // A plan that assumes every checker runs counts the ones that never did.
  assign effective_checkers = (ASSUME_REACHABLE != 0) ? checkers_written
                            : ((checkers_reached > checkers_written)
                               ? checkers_written : checkers_reached);
  // No floor is needed here: effective_checkers is a minimum against
  // checkers_written, so the subtraction is never negative.
  assign unreached = checkers_written - effective_checkers;
  assign r_q = (checkers_written == 16'd0) ? 32'd100
             : (({16'd0, effective_checkers} * 32'd100) / {16'd0, checkers_written});
  assign reach_pct = (r_q > 32'd65535) ? 16'hFFFF : r_q[15:0];
  assign adequate = (reach_pct >= 16'd95);
  // Checkers that never evaluated, counted as having passed.
  assign reach_assumed_err = assess && (checkers_reached < checkers_written)
                             && (unreached == 16'd0);

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      n_assessments <= 8'd0; n_short <= 8'd0;
    end else if (assess) begin
      n_assessments <= n_assessments + 8'd1;
      if (!adequate) n_short <= n_short + 8'd1;
    end
  end
endmodule

Five assessments.

One short when reach is measured; none when it is assumed.

A checker that never evaluates passes every regression. It contributes to the pass count, to the checker count, and to any coverage figure derived from either — and it has never once expressed an opinion about the design. Eighteen such checkers is eighteen rules that appear verified and are not.

This is the batch's own finding turned into a model. Every chapter of batches 021 through 023 produced mutation survivors that were exactly this: a guard, a threshold or a branch that no stimulus reached, and which therefore could not distinguish a correct design from a broken one. Section 12 is the instrument that finds them; this section is the quantity it finds.

Row five is the vacuous hundred again, in a second guise: a suite with no checkers has reached all of them. Two of this chapter's nine models can report a hundred percent by having nothing to measure, which is why section 14's mask requires several properties rather than a single figure.

7. RTL 3 — A Vacuous Pass Checked Nothing

// RTL 3 - a vacuous pass. An implication whose antecedent never held did not
// check its consequent, and a pass count that includes it is inflated.
module vacuous_pass #(parameter int COUNT_VACUOUS = 0) (
  input  logic clk, rst_n,
  input  logic        assess,
  input  logic [15:0] evaluations, vacuous_evaluations,
  output logic [15:0] meaningful, vacuous_pct, meaningful_pct,
  output logic        adequate,
  output logic [7:0]  n_assessments, n_weak,
  output logic        vacuity_counted_err
);
  logic [31:0] v_q, m_q;
  logic [15:0] eff_vacuous;
  // Counting vacuous passes as checks is what a pass counter does by default.
  assign eff_vacuous = (COUNT_VACUOUS != 0) ? 16'd0
                     : ((vacuous_evaluations > evaluations) ? evaluations
                        : vacuous_evaluations);
  assign meaningful = evaluations - eff_vacuous;
  assign v_q = (evaluations == 16'd0) ? 32'd0
             : (({16'd0, eff_vacuous} * 32'd100) / {16'd0, evaluations});
  assign vacuous_pct = (v_q > 32'd65535) ? 16'hFFFF : v_q[15:0];
  assign m_q = (evaluations == 16'd0) ? 32'd0
             : (({16'd0, meaningful} * 32'd100) / {16'd0, evaluations});
  assign meaningful_pct = (m_q > 32'd65535) ? 16'hFFFF : m_q[15:0];
  assign adequate = (meaningful_pct >= 16'd80);
  // Vacuous evaluations counted as checks.
  assign vacuity_counted_err = assess && (vacuous_evaluations != 16'd0)
                               && (evaluations != 16'd0) && (eff_vacuous == 16'd0);

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      n_assessments <= 8'd0; n_weak <= 8'd0;
    end else if (assess) begin
      n_assessments <= n_assessments + 8'd1;
      if (!adequate) n_weak <= n_weak + 8'd1;
    end
  end
endmodule

Seven assessments. A thousand evaluations.

Five weak when vacuity is excluded; two when it is counted.

A check written as "if this happens, then that must be true" passes silently whenever the first half does not happen. Four hundred vacuous evaluations of a thousand is four hundred passes that examined nothing — and the pass counter cannot tell them apart from the six hundred that did.

Row four is the state a checker reaches when its antecedent is impossible. Every evaluation vacuous means the check is structurally unable to fail, and it will contribute a growing pass count forever. That is section 6's unreached checker with one extra step of disguise — it evaluates, it passes, and it still says nothing.

Row seven is an inconsistent report and the model says so. More vacuous evaluations than evaluations is a tool or a merge error; the cap keeps the meaningful count at zero rather than wrapping, and section 17 records that this case was demanded by a surviving mutation.

Seven passes and two evaluations that meant anything. The pass count is the number every regression report leads with, and it is the sum of two quantities with completely different value — which is why section 14's mask separates "the suite passes" from "the passes are meaningful."

8. RTL 4 — Illegal Stimulus Produces Failures That Are Not Defects

// RTL 4 - illegal stimulus. A testbench that drives what the protocol forbids
// produces failures that are not defects, and they cost the same to debug.
module stimulus_legality #(parameter int ALLOW_ILLEGAL = 0) (
  input  logic clk, rst_n,
  input  logic        run,
  input  logic [15:0] stimuli, illegal_stimuli, real_defects,
  output logic [15:0] admitted_illegal, failures, false_failures, signal_pct,
  output logic        trustworthy,
  output logic [7:0]  n_runs, n_noisy,
  output logic        legality_ignored_err
);
  logic [31:0] s_q;
  // A constrained generator refuses what the protocol forbids; an unconstrained
  // one drives it and blames the design.
  assign admitted_illegal = (ALLOW_ILLEGAL != 0)
                            ? ((illegal_stimuli > stimuli) ? stimuli
                               : illegal_stimuli) : 16'd0;
  assign false_failures = admitted_illegal;
  assign failures = real_defects + false_failures;
  assign s_q = (failures == 16'd0) ? 32'd100
             : (({16'd0, real_defects} * 32'd100) / {16'd0, failures});
  assign signal_pct = (s_q > 32'd65535) ? 16'hFFFF : s_q[15:0];
  assign trustworthy = (signal_pct >= 16'd90);
  // Illegal stimulus admitted and its failures reported as defects. No separate
  // illegal-count guard is needed: admitted_illegal is a minimum against
  // illegal_stimuli, so it can only be non-zero when that one is.
  assign legality_ignored_err = run && (admitted_illegal != 16'd0);

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      n_runs <= 8'd0; n_noisy <= 8'd0;
    end else if (run) begin
      n_runs <= n_runs + 8'd1;
      if (!trustworthy) n_noisy <= n_noisy + 8'd1;
    end
  end
endmodule

Five runs. Five hundred stimuli.

None noisy when the stimulus is constrained; three when it is not.

Twenty-eight percent signal means seven of ten failures are the testbench's fault, and the team cannot tell which without debugging all of them. A false failure costs the same as a real one to triage — section 13 prices that directly — and it costs more than that in the credibility of the next failure.

Row three is the worst case and it is not rare. A design with no defects and an unconstrained generator produces fifty failures, all of them false, none of them dismissible without investigation. That is a suite that consumes a team and finds nothing.

Row five is the trust boundary. Two false failures in twenty is exactly ninety percent signal — which is roughly where a team stops assuming a failure is a testbench problem and starts assuming it is a design problem. Below it, the default assumption inverts, and real defects start being dismissed.

9. RTL 5 — A Check On A Range Accepts Every Value In It

// RTL 5 - the strength of a check. A check against a range accepts every value
// in it; a check against a value accepts one, and the difference is detection.
module checker_strength #(parameter int BOUNDS_NOT_VALUES = 0) (
  input  logic clk, rst_n,
  input  logic        assess,
  input  logic [15:0] value_space, accepted_span, wrong_values_caught,
  output logic [15:0] accepted, missed, detection_pct,
  output logic        is_strong,
  output logic [7:0]  n_assessments, n_weak,
  output logic        bounds_used_err
);
  logic [31:0] d_q;
  // A bounds check accepts the whole declared span; an exact check accepts one.
  assign accepted = (BOUNDS_NOT_VALUES != 0)
                    ? ((accepted_span > value_space) ? value_space : accepted_span)
                    : 16'd1;
  assign missed = (accepted > 16'd1) ? (accepted - 16'd1) : 16'd0;
  assign d_q = (value_space <= 16'd1) ? 32'd100
             : ((({16'd0, value_space} - {16'd0, accepted}) * 32'd100)
                / ({16'd0, value_space} - 32'd1));
  assign detection_pct = (d_q > 32'd65535) ? 16'hFFFF : d_q[15:0];
  assign is_strong = (detection_pct >= 16'd99);
  // A span accepted where a single value was the specification. No separate
  // span guard is needed: accepted is a minimum against accepted_span, so it
  // can only exceed one when the span does.
  assign bounds_used_err = assess && (value_space > 16'd1) && (accepted > 16'd1);

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      n_assessments <= 8'd0; n_weak <= 8'd0;
    end else if (assess) begin
      n_assessments <= n_assessments + 8'd1;
      if (!is_strong) n_weak <= n_weak + 8'd1;
    end
  end
endmodule

Six assessments.

None weak when the check names a value; three when it names a span.

This is the rule every prompt in this batch has carried: assert exact values, never bounds or relations. A check that the result is "between 40 and 50" passes for eleven values of which ten are wrong; a check that it is 45 passes for one. The difference is not stylistic — it is ninety percent detection against a hundred.

Row three is the check that has no strength at all. A span as wide as the value space accepts everything and detects nothing, while still appearing in the checker count, the coverage figure and the pass count. It is section 6's unreached checker and section 7's vacuous pass in a third guise: present, running, evaluating, and unable to fail.

Row two is the case that makes the check honest. A span of one is an exact check, so a bounds-shaped check with a degenerate range is not weak — the shape is not the defect; the width is.

10. RTL 6 — Error Paths Need Injection

// RTL 6 - error paths need injection. A path that only runs when something goes
// wrong never runs in a testbench where nothing does.
module error_injection #(parameter int NO_INJECTION = 0) (
  input  logic clk, rst_n,
  input  logic        assess,
  input  logic [15:0] error_paths, injectable_paths,
  output logic [15:0] exercised, unexercised, exercised_pct,
  output logic        adequate,
  output logic [7:0]  n_assessments, n_short,
  output logic        injection_assumed_err
);
  logic [31:0] e_q;
  // Without an injection mechanism no error path is reachable at all.
  assign exercised = (NO_INJECTION != 0) ? 16'd0
                   : ((injectable_paths > error_paths) ? error_paths
                      : injectable_paths);
  assign unexercised = error_paths - exercised;
  assign e_q = (error_paths == 16'd0) ? 32'd100
             : (({16'd0, exercised} * 32'd100) / {16'd0, error_paths});
  assign exercised_pct = (e_q > 32'd65535) ? 16'hFFFF : e_q[15:0];
  assign adequate = (exercised_pct >= 16'd90);
  // Injectable paths that were never injected into.
  assign injection_assumed_err = assess && (injectable_paths != 16'd0)
                                 && (error_paths != 16'd0) && (exercised == 16'd0);

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      n_assessments <= 8'd0; n_short <= 8'd0;
    end else if (assess) begin
      n_assessments <= n_assessments + 8'd1;
      if (!adequate) n_short <= n_short + 8'd1;
    end
  end
endmodule

Six assessments. Twenty error paths.

Two short when injection is measured; five when there is none.

An error path is unreachable by construction in a testbench where nothing goes wrong, and a healthy testbench is one where nothing goes wrong. The two requirements are in direct opposition, which is why injection has to be built deliberately rather than emerging from good stimulus.

This is 24.2 §12's poison path exactly. That chapter's debug lab found one corrupted line every nine hours from a dropped poison marker, and the finding was that it needs an injected fault and a scoreboard that knows what was injected. Section 6's unreached checkers and this section's unexercised paths are the same eighteen-percent-shaped hole seen from two sides.

Row six is where most projects start, and it is worth stating plainly: with no injection mechanism the error-path coverage is not low, it is zero — and every error-handling line in the design is unverified regardless of how good the rest of the suite is.

11. RTL 7 — Bins Say It Happened, Crosses Say It Happened Together

// RTL 7 - coverage closure. Hitting every bin says each thing happened; hitting
// every cross says they happened together, which is where the bugs are.
module coverage_closure #(parameter int BINS_ONLY = 0) (
  input  logic clk, rst_n,
  input  logic        assess,
  input  logic [15:0] bin_total, bin_hits, cross_total, cross_hits,
  output logic [15:0] bin_pct, cross_pct, reported_pct,
  output logic        closed,
  output logic [7:0]  n_assessments, n_open,
  output logic        cross_ignored_err
);
  logic [31:0] b_q, c_q;
  assign b_q = (bin_total == 16'd0) ? 32'd100
             : (({16'd0, bin_hits} * 32'd100) / {16'd0, bin_total});
  assign bin_pct = (b_q > 32'd65535) ? 16'hFFFF : b_q[15:0];
  assign c_q = (cross_total == 16'd0) ? 32'd100
             : (({16'd0, cross_hits} * 32'd100) / {16'd0, cross_total});
  assign cross_pct = (c_q > 32'd65535) ? 16'hFFFF : c_q[15:0];
  // Closure is the weaker of the two; a bin count alone reports the stronger.
  assign reported_pct = (BINS_ONLY != 0) ? bin_pct
                      : ((cross_pct < bin_pct) ? cross_pct : bin_pct);
  assign closed = (reported_pct >= 16'd95);
  // Crosses that were declared and left out of the closure figure.
  assign cross_ignored_err = assess && (cross_total != 16'd0)
                             && (cross_pct < bin_pct) && (reported_pct == bin_pct);

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      n_assessments <= 8'd0; n_open <= 8'd0;
    end else if (assess) begin
      n_assessments <= n_assessments + 8'd1;
      if (!closed) n_open <= n_open + 8'd1;
    end
  end
endmodule

Five assessments. Sixty-four bins and sixteen crosses.

Two open when both are counted; one when only the bins are.

Ninety-six percent of bins and twenty-five percent of crosses is a suite that has seen everything happen and almost nothing happen together. 24.1 §21 is the chapter-length version: every protocol worked alone, and all three defects needed two protocols busy at once — which is a cross, not a bin.

Row four is the vacuous hundred for a third time. A model with no crosses declared reports full cross coverage, so closure becomes the bin figure — and a coverage model with no crosses in it is exactly the model that produced row one's problem. The absence is not visible in the number.

Row five is the case that keeps the check honest. When the bins are the weaker half, taking the weaker figure gives the bin figure, and the bins-only model is right by accident — which is why cross_ignored_err requires the cross share to actually be lower.

12. RTL 8 — What A Passing Suite Proves

// RTL 8 - what a passing suite proves. A suite that passes on a deliberately
// broken design has proved nothing, and the kill rate is the measurement.
module regression_signal #(parameter int TRUST_THE_PASS = 0) (
  input  logic clk, rst_n,
  input  logic        assess,
  input  logic [15:0] mutants_injected, mutants_killed,
  output logic [15:0] survivors, kill_pct, blind_spots,
  output logic        trustworthy,
  output logic [7:0]  n_assessments, n_weak,
  output logic        pass_trusted_err
);
  logic [31:0] k_q;
  logic [15:0] eff_killed;
  // A suite that is trusted because it passed reports every mutant killed.
  assign eff_killed = (TRUST_THE_PASS != 0) ? mutants_injected
                    : ((mutants_killed > mutants_injected) ? mutants_injected
                       : mutants_killed);
  assign survivors = mutants_injected - eff_killed;
  assign blind_spots = survivors;
  assign k_q = (mutants_injected == 16'd0) ? 32'd0
             : (({16'd0, eff_killed} * 32'd100) / {16'd0, mutants_injected});
  assign kill_pct = (k_q > 32'd65535) ? 16'hFFFF : k_q[15:0];
  assign trustworthy = (kill_pct >= 16'd100);
  // Mutants that survived, reported as killed.
  assign pass_trusted_err = assess && (mutants_killed < mutants_injected)
                            && (survivors == 16'd0);

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      n_assessments <= 8'd0; n_weak <= 8'd0;
    end else if (assess) begin
      n_assessments <= n_assessments + 8'd1;
      if (!trustworthy) n_weak <= n_weak + 8'd1;
    end
  end
endmodule

Five assessments. A hundred deliberately injected defects.

Three untrustworthy when the suite is measured; one when the pass is trusted.

A suite that passes on a design you deliberately broke has told you nothing about the design you did not break. That is the entire content of this model, and it is the instrument that produced every finding in this batch: 316 mutations in batch 022 and 316 in this one, with every survivor a place where the checks could not tell correct from incorrect.

Row three is a threshold that is deliberately unforgiving. Ninety-nine percent is not trustworthy here, because the one survivor is not a rounding error — it is a specific, named, reproducible blind spot, and the whole value of the measurement is that it points at exactly which one.

Row five is the state a project is in before it runs this. Zero mutants injected gives a zero kill rate rather than a hundred: an unmeasured suite is not a trustworthy suite that happens to lack a number, and reporting it as anything above zero would be the same vacuous hundred that sections 5, 6 and 11 each produce.

What a survivor is worth is not always a stimulus gap. Across this batch, survivors have been: a threshold never driven at equality, a ceiling never driven off its boundary, a floor never driven past it, a guard for a configuration outside the model's premise, two inputs the testbench always tied together, a case driven and half observed, and a guard that was genuinely dominated and should be deleted. The last category is the one that improves the design rather than the testbench.

13. RTL 9 — What A Check Costs

// RTL 9 - what a check costs. Writing it is the small half; debugging what it
// reports is the large one, and a noisy check costs more than it finds.
module verification_cost #(parameter int IGNORE_DEBUG_TIME = 0) (
  input  logic clk, rst_n,
  input  logic        price,
  input  logic [15:0] checkers, write_hours_each, false_failures,
  input  logic [15:0] debug_hours_each,
  output logic [15:0] write_hours, debug_hours, total_hours, debug_share_pct,
  output logic        acceptable,
  output logic [7:0]  n_pricings, n_costly,
  output logic        debug_ignored_err
);
  logic [31:0] w_q, d_q, t_q, s_q;
  assign w_q = {16'd0, checkers} * {16'd0, write_hours_each};
  assign write_hours = (w_q > 32'd65535) ? 16'hFFFF : w_q[15:0];
  // Every false failure is triaged by a person before it is dismissed.
  assign d_q = (IGNORE_DEBUG_TIME != 0) ? 32'd0
             : ({16'd0, false_failures} * {16'd0, debug_hours_each});
  assign debug_hours = (d_q > 32'd65535) ? 16'hFFFF : d_q[15:0];
  assign t_q = {16'd0, write_hours} + {16'd0, debug_hours};
  assign total_hours = (t_q > 32'd65535) ? 16'hFFFF : t_q[15:0];
  assign s_q = (total_hours == 16'd0) ? 32'd0
             : (({16'd0, debug_hours} * 32'd100) / {16'd0, total_hours});
  assign debug_share_pct = (s_q > 32'd65535) ? 16'hFFFF : s_q[15:0];
  assign acceptable = (debug_share_pct <= 16'd50);
  // False failures that were triaged and costed at nothing.
  assign debug_ignored_err = price && (false_failures != 16'd0)
                             && (debug_hours_each != 16'd0) && (debug_hours == 16'd0);

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      n_pricings <= 8'd0; n_costly <= 8'd0;
    end else if (price) begin
      n_pricings <= n_pricings + 8'd1;
      if (!acceptable) n_costly <= n_costly + 8'd1;
    end
  end
endmodule

Six pricings. Ninety checkers at two hours each to write.

Two costly when the triage is counted; none when it is not.

Fifty-seven percent of the effort is triage, and every hour of it is spent on a failure that was not a defect. Section 8's twenty-eight percent signal and this section's fifty-seven percent triage are the same number from opposite ends — an unconstrained generator produces false failures, and false failures produce triage.

Row five is a suite that costs more than it finds. At seventy-two percent triage, the team is spending nearly three hours dismissing noise for every hour spent writing a check — and the ratio worsens as the suite grows, because more checkers on the same noisy stimulus produce more false failures.

Row three is the boundary worth defending. Half the effort on triage is roughly where a verification team's throughput stops improving with headcount, because the added people are absorbed by the noise. Constraining the stimulus is cheaper than hiring.

Figure 3 — Two hundred and forty hours that no verification plan contains, caused by a stimulus decision rather than by a checker decision. The plan estimates the left branch and the schedule is set by the right one.

14. RTL 10 — A Verification Effort Assembled

// RTL 10 - a CXL protocol verification effort assembled. Everything that must
// hold before a suite that passes is a suite that proved something.
module verification_model #(parameter int SUITE_PASSES = 0) (
  input  logic clk, rst_n,
  input  logic       evaluate,
  input  logic       suite_passes,        // every test in the suite passed
  input  logic       rules_checked,       // every specification rule has a checker
  input  logic       checkers_reached,    // every checker evaluated at least once
  input  logic       passes_meaningful,   // vacuous evaluations are excluded
  input  logic       errors_injected,     // error paths were made reachable
  input  logic       suite_measured,      // the suite was scored against mutants
  output logic       proves_something,
  output logic [5:0] fail_mask,
  output logic [7:0] n_eval, n_proves,
  output logic       false_proof_err
);
  assign fail_mask[0] = ~suite_passes;
  assign fail_mask[1] = ~rules_checked;
  assign fail_mask[2] = ~checkers_reached;
  assign fail_mask[3] = ~passes_meaningful;
  assign fail_mask[4] = ~errors_injected;
  assign fail_mask[5] = ~suite_measured;
  // The suite-passes build is what a regression report says.
  assign proves_something = (SUITE_PASSES != 0) ? suite_passes
                                                : (fail_mask == 6'd0);
  assign false_proof_err = evaluate && proves_something && (fail_mask != 6'd0);

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      n_eval <= 8'd0; n_proves <= 8'd0;
    end else if (evaluate) begin
      n_eval <= n_eval + 8'd1;
      if (proves_something) n_proves <= n_proves + 8'd1;
    end
  end
endmodule

One configuration of six proves something, and four false claims.

"The suite passes" is what a regression report says and it is right about one of the six. The other five are all upstream of the report and invisible to it — a report reads the outcome of the tests that ran, and every property here is about which tests exist, whether they ran, and whether running them meant anything.

Row five is the one this batch has the most direct evidence for: a suite that has never been scored against deliberately broken designs has no measured detection ability at all, and every survivor found across batches 021 to 023 was a blind spot that a green report had been hiding.

Figure 4 — Four questions, and a passing suite is the entry condition rather than the answer. The order is by how early each filter acts: a rule with no checker was never going to be verified, and a suite that was never scored might be perfect and nobody knows.

15. Quantitative Reasoning

Rule coverage. A hundred and twenty rules against ninety checkers is 75%, and 114 is exactly the 95% threshold.

Reachability. Ninety checkers of which seventy-two evaluated is 80% — eighteen checkers that have passed every regression without running.

Vacuity. A thousand evaluations with four hundred vacuous is 60% meaningful, and all thousand vacuous is a suite that proved nothing while passing.

Stimulus legality. Fifty illegal stimuli and twenty real defects is seventy failures at 28% signal; with no defects it is fifty failures, every one false.

Checker strength. A span of ten in a hundred-value space misses nine wrong values — 90% detection; an exact check misses none.

Error injection. Twenty error paths with twelve injectable is 60%; with no injection mechanism it is zero.

Closure. Ninety-six percent of bins against twenty-five percent of crosses is closure of 25%, and the bins-only figure reports 96.

Mutation score. A hundred mutants with eighty-five killed is fifteen named blind spots; ninety-nine killed is still one.

Cost. Ninety checkers at two hours is 180; sixty false failures at four hours is 240 — 57% of the effort is triage.

The assembled model. Six properties, six configurations, one proves something. The regression report reported five.

16. Assertions

Every check is an explicit comparison against an exact value. Icarus Verilog 13.0 has no concurrent assertion support, so each is a procedural comparison against 1'b1, and every one is an equality.

Every inclusive threshold is driven at exactly equal, and every capped quantity is driven past its cap — the rules this batch has accumulated, applied to a chapter about exactly that discipline.

Rule coverage. Coverage of exactly 95% is constructed from 114 checkers, and more checkers than rules is asserted to floor at zero unchecked.

Reachability. A reach of exactly 95% is constructed, and a report claiming more checkers ran than exist is asserted capped.

Vacuity. A meaningful share of exactly 80% is constructed, every evaluation vacuous is driven, and a vacuous count reported against no evaluations at all is driven.

chk(wGm == 16'd0, "still nothing meaningful");
chk(wGe == 1'b0,  "which is an inconsistent report, not counted vacuity");

Stimulus legality. A signal ratio of exactly 90% is constructed from two false failures in twenty, and more illegal stimuli than stimuli is asserted capped.

Checker strength. A span of one is asserted to be an exact check, a span wider than the space is asserted to detect nothing, and a detection rate of exactly 99% is constructed from a 101-value space.

chk(kBd == 16'd99, "at exactly ninety-nine percent detection");
chk(kBs == 1'b1,   "which is exactly strong");

Error injection. Coverage of exactly 90% is constructed, and a design with no error paths is asserted vacuously complete.

Closure. Both figures at exactly 95% are driven, and the case where the bins are the weaker half is asserted as not an ignored cross.

Mutation score. A single survivor is asserted untrustworthy, and no mutants injected at all is asserted to give a zero kill rate rather than a hundred.

Cost. A triage share of exactly 50% is constructed from 45 false failures.

The assembled model. Every fail mask is asserted as an exact six-bit value, and each of the six bits is driven false alone.

Totals: 270 checks across two testbenches, 132 on the front five models and 138 on the back five, all passing on the unmutated sources.

17. Mutation Testing

Sixty-four mutations were injected one at a time. 64 injected, 64 killed, after six survivors — the most of any chapter in this batch, which is a fitting result for the chapter about measuring suites.

Six survivors in two even classes, and the split is the finding.

Three were genuinely dominated guards, deleted with comments naming the domination. Section 6's unreached floor, section 8's illegal-count guard and section 9's span guard were each redundant for the same structural reason: the quantity being guarded is a minimum against the quantity in the guard, so it can never exceed it. Each was replaced with a mutation that changes an operand rather than removing a guard.

Three were stimulus gaps, and one of them needed nothing but an assertion. A vacuous count reported against no evaluations; a detection rate of exactly 99% (which needed a 101-value space to construct — no value space of 100 produces it); and section 7's zero-evaluation guard, which was already driven and had its vacuous-share output unasserted.

The even split is worth recording. Across this batch's five chapters, eleven survivors were stimulus gaps and six were dominated guards — which means roughly a third of the time, a surviving mutation is telling you the design has a line that does nothing, not that the testbench has a hole. A campaign that only adds stimulus in response to survivors would have shipped six dead guards.

The complete set was re-run after every stimulus change, per standing discipline, and all sixty-four held.

18. Verification Strategy

What a testbench for a verification-methodology model must cover — and the chapter is unusually self-referential about it.

Ask whether a guard is dominated before adding stimulus for it. Six of this batch's seventeen survivors were dead guards. The test is structural: if the guarded quantity is a minimum against the quantity in the guard, the guard can never fire. Three of this chapter's own guards failed that test.

Construct the equality rather than searching for it. Section 9's 99% detection is impossible in a hundred-value space and trivial in a hundred-and-one-value one; the case had to be solved for backwards, and no sweep over round numbers would have found it.

Assert every output on every degenerate case. One survivor here needed no new stimulus at all — the case was driven and one of its three outputs was unchecked. That is the third time in this batch.

The cases where the status report is right. Every rule checked. Every checker reached. No vacuous evaluations. Constrained stimulus. A span of one. Every error path injectable. Every mutant killed. Seven cases across nine models, each exempted explicitly — and each one a state a good verification effort is genuinely in.

Watch for the vacuous hundred. Sections 5, 6, 11 and section 10's row five all report a hundred percent by having nothing to measure. Four of nine models can produce a perfect score from an empty denominator, which is the strongest argument in this chapter for section 14's mask over any single figure.

Counters as a second signature. Ten models, ten pairs of totals, differing in all ten — one short against none, five weak against two, three noisy against none, three untrustworthy against one.

19. Synthesis and Implementation Reality

Nothing in this chapter is hardware. Every model is arithmetic a verification lead performs, and the failure mode is a sign-off decision rather than a timing violation.

Section 5's rule extraction is the most expensive item here and the least automatable. Reading a specification and enumerating its testable rules is human work, and it is the denominator every other coverage figure depends on — which is why projects that skip it can never produce an honest coverage number afterwards.

Section 6's reachability is free to measure and almost never measured. Every assertion language reports evaluation counts; the number exists and nobody looks at it.

Section 7's vacuity is reported by most tools and disabled by most projects, because vacuous passes are noisy in a log. Turning the report off does not turn the vacuity off.

Section 10's injection needs design support, not just testbench support: a fault-injection path into ECC, a poison-forcing register, a way to corrupt a flit's CRC. Those are RTL features that must be argued for on a schedule that is measuring area.

Section 12's mutation campaign is the most mechanisable item in this chapter and the one with the least tool support. A script that patches one line, rebuilds and re-runs is a day's work, and it is what produced every finding in this batch.

20. Silicon Observability

"The named survivors" is the entry that changes behaviour. A kill rate of 85% is a number to argue about; fifteen named, reproducible cases where the suite cannot distinguish correct from broken is a work list. Every finding in batches 021 through 023 arrived that way — as a specific mutation with a label, not as a percentage.

21. Debug Lab

Symptom. A CXL device's verification sign-off reports 100% functional coverage, 12,000 tests passing, zero failures for six weeks. First silicon has four defects in the first month, and all four are in areas the report marked fully covered.

Step 1 — what is the coverage a percentage of? The coverage model has 64 bins and no crosses. Section 11, and closure is the bin figure by default because there is nothing weaker to report. The first defect was two protocols busy at once, which is a cross that was never declared.

Step 2 — how many rules were extracted? There is no rule list. The checker count is 90 and the denominator is the checker count — so coverage is 90 of 90. Section 5's row five exactly: the vacuous hundred, produced by having nothing to divide by.

Step 3 — did the checkers run? Evaluation counts, read for the first time: 18 checkers have an evaluation count of zero. Section 6. Two of them cover the error-handling paths the second defect is in.

Step 4 — did the passes mean anything? Vacuity reporting was disabled in the tool configuration eighteen months ago to reduce log noise. Re-enabled and re-run: 41% of evaluations are vacuous. Section 7, and the third defect is behind a checker whose antecedent requires an error response that the stimulus never produces.

Step 5 — were the error paths reachable at all? There is no fault-injection mechanism in the RTL. Section 10's row six: error-path coverage is zero, not low, and the fourth defect is in a retry path that has never once executed.

Step 6 — what would have caught any of this? A mutation campaign. Injecting a hundred single-line defects into the RTL and re-running the suite would have produced survivors for every one of the four areas — and would have taken a week against six weeks of a passing regression that proved nothing.

The finding. Five of section 14's six properties failed. The suite passed, and it was the only one of the six that held. No individual decision was unreasonable: nobody extracted rules because the schedule was tight, nobody read evaluation counts because the coverage was green, and vacuity reporting was disabled because the logs were noisy.

The fix, in the order that recovers the most. Extract the rule list — it is the denominator everything else needs. Re-enable vacuity reporting and fix the 41%. Declare the crosses. Add an injection mechanism, which is an RTL change and therefore the slowest. And run the mutation campaign first, because it names which of the others matters most for this design.

What made this hard. Every number in the report was computed correctly. Four of the five failures were empty denominators or unread outputs, and the fifth was a tool option turned off for a good reason a year and a half earlier.

22. Design Review

1. How many testable rules does the specification contain, and where is that list? It is the denominator for everything else. Section 5.

2. What is the evaluation count of every checker, and how many are zero? Free to collect and almost never read. Section 6.

3. Is vacuity reporting enabled, and what is the vacuous share? Disabling the report does not remove the vacuity. Section 7.

4. How many failures in the last quarter were testbench issues? Below ninety percent signal the default assumption inverts. Section 8.

5. How many checkers assert a value, and how many assert a range? A ten-wide span misses nine wrong values. Section 9.

6. Is there a fault-injection mechanism in the RTL, and what does it reach? With none, error-path coverage is zero rather than low. Section 10.

7. Are crosses reported separately from bins? 96% of bins and 25% of crosses closes at 25%. Section 11.

8. What is the mutation kill rate, and what are the survivors called? The names are the work list. Section 12.

9. What share of verification hours is triage? Above half, headcount stops helping. Section 13.

10. Which of the six properties does "the suite passes" imply? Section 14 exists because the answer is the first one only.

23. How This Appears In Real Engineering

A verification lead owns all ten models and typically inherits a plan built around section 13's left branch — checkers to write, hours to write them. The right branch, triage, is the half that sets the schedule, and it is a consequence of the stimulus constraints rather than of the checker count.

A design engineer owns section 10 without usually being asked to. Fault injection is an RTL feature: a way to force poison, corrupt a CRC, or fail an ECC decode. It costs area, it appears on no requirement list, and without it every error-handling line the designer wrote is unverified.

A project manager meets the vacuous hundred. Four of nine models here can report a perfect score from an empty denominator, and a status report reading 100% is compatible with having measured nothing — which is why section 14's six-property mask is the useful artefact and a single percentage is not.

And anyone running a mutation campaign meets section 17's split. A third of survivors are dead guards rather than testbench holes, so the campaign improves the design as well as the suite — which is a return nobody budgets for and the strongest argument for running one.

24. Common Misconceptions

"We have 100% coverage." Of what denominator? Sections 5 and 21.

"The checkers all pass." Eighteen of them have never evaluated. Section 6.

"Twelve thousand passing tests." Forty-one percent of the evaluations checked nothing. Section 7.

"The design keeps failing." Seven of ten failures are the testbench. Section 8.

"The check verifies the result is in range." It accepts every value in that range. Section 9.

"Error handling is covered." Without injection it is unreachable, so coverage is zero. Section 10.

"Coverage is closed at 96%." Of bins. Crosses are at 25%. Section 11.

"The suite passed, so the design is good." Or the suite cannot tell. Section 12.

"Ninety checkers at two hours each is 180 hours." Plus 240 of triage. Section 13.

"The suite passes." One property of six. Section 14.

25. Interview Reasoning

Q. A report says 100% functional coverage. What do you ask?

What the denominator is. If coverage is checkers-hit over checkers-written, it is a hundred percent by construction and says nothing — the honest denominator is the count of testable rules extracted from the specification, which is human work that projects under schedule pressure skip. A hundred percent with no rule list and a hundred percent with one are the same number and completely different claims.

Q. What is a vacuous pass and why does it matter?

An implication whose antecedent never held. The checker evaluated, reported a pass, and examined nothing — and a pass counter cannot distinguish it from a pass that checked something. Four hundred vacuous of a thousand means the suite did 60% of the work its pass count claims, and the report reads identically either way.

Q. Your team is drowning in failures that turn out to be testbench issues. What is the number?

The signal ratio — real defects over total failures. Fifty illegal stimuli and twenty real defects is 28% signal, and below about ninety percent a team's default assumption inverts from "this is a bug" to "this is the testbench," at which point real defects start being dismissed. The fix is constraining the generator, which is cheaper than the triage it saves.

Q. Why is checking a range weaker than checking a value?

Because it accepts every value in the range. A ten-wide span in a hundred-value space accepts ten values of which nine are wrong — ninety percent detection against a hundred. The check still appears in the checker count, the coverage figure and the pass count, and it is nine times less able to fail.

Q. How do you know a passing suite is worth anything?

Break the design deliberately and see if the suite notices. Inject a hundred single-line defects, re-run, and count the survivors — each survivor is a named, reproducible case where the suite cannot distinguish correct from broken. A kill rate is a number to argue about; the survivor names are a work list.

Q. You run a mutation campaign and a mutation survives. What does that tell you?

Usually that the testbench has a gap — a threshold never driven at equality, a boundary never crossed, a configuration outside the model's premise. But about a third of the time it tells you the design has a guard that can never fire, because the quantity it guards is already bounded by the quantity in the guard. That one is a design improvement rather than a testbench one, and adding stimulus for it would be wrong.

26. Exercises

1. Extract the testable rules from one section of a protocol specification and compute a real coverage figure against an existing checker set.

2. Read the evaluation count of every checker in an existing environment and list the ones at zero.

3. Re-enable vacuity reporting on a suite that has it disabled and compute the meaningful share.

4. Classify a quarter's failures into real and testbench, and compute the signal ratio.

5. Count the checkers in an environment that assert a value against those that assert a range, and estimate the detection loss.

6. Enumerate the error paths in one block and list which have an injection mechanism.

7. Add crosses to a bin-only coverage model and re-compute closure.

8. Build a mutation harness for one module: patch one line, rebuild, re-run, record the verdict.

9. Model section 21 end to end: no rule list, unread evaluation counts, disabled vacuity, no crosses, no injection.

10. Add a seventh property to RTL 10. If it is implied by one of the six, say which; if not, give the suite it catches that the current mask calls sufficient.

27. Summary

Module 24 built a device across four chapters, and every one of them ended on a debug in which the design was correct and the evidence was missing. This chapter is the evidence, and its finding is that a passing suite is the beginning of an argument rather than the end of one.

A rule with no checker is unverified. A hundred and twenty rules against ninety checkers is 75% — and a project with no rule list divides by the checker count and reports a hundred.

A checker no stimulus reaches has never spoken. Eighteen of ninety with an evaluation count of zero have passed every regression without once expressing an opinion.

A vacuous pass checked nothing. Four hundred of a thousand evaluations with a false antecedent is 60% meaningful, and the pass count reads a thousand either way.

Illegal stimulus produces failures that are not defects. Fifty illegal stimuli against twenty real defects is seventy failures at 28% signal, and each false one costs a full triage.

A check on a range accepts every value in it. A ten-wide span misses nine wrong values — which is why every prompt in this batch said to assert exact values and never bounds.

Error paths need injection. With no mechanism, error-path coverage is zero rather than low, and every error-handling line the designer wrote is unverified.

Bins say it happened; crosses say it happened together. 96% of bins against 25% of crosses closes at 25% — and 24.1's three defects all needed two protocols busy at once.

And a suite that passes on a design you broke has told you nothing. A hundred mutants with fifteen survivors is fifteen named blind spots, and ninety-nine of a hundred is still one.

Triage is the half of verification nobody plans. Ninety checkers at two hours is 180; sixty false failures at four hours is 240 — 57% of the effort, caused by a stimulus decision rather than a checker decision.

Four of nine models here can report a hundred percent by having nothing to measure, which is the strongest argument in the chapter for a six-property mask over any single figure.

Six mutations survived and the split was even: three dominated guards and three stimulus gaps. Across this batch, six of seventeen survivors were dead guards — so about a third of the time a survivor improves the design rather than the testbench, and a campaign that only adds stimulus would have shipped all six.

A suite that passes is one property of six. The regression report every project leads with called five of six efforts sound when one was — and section 21 is a sign-off at 100% coverage, 12,000 passing tests and six weeks green, with four escapes in the first month of silicon.

25.2 — Coherency Verification takes this methodology to the one property a device cannot check locally: that every cache in a system agrees about what memory says, which no single block's checker can see.