CXL Assertions

25.2 argued that a check has to be wide enough to see the bug. This chapter is about the other three dimensions: when it samples, how long it waits, and whether anybody is told when it fires.

The headline is section 6. A concurrent assertion written as an implication passes on every cycle its antecedent does not fire — so ten thousand cycles can produce ten thousand passes of which two hundred mean anything, and a pass count cannot tell the two apart.

1. The Engineering Problem — Four Ways To Write A Check That Cannot Fail

A concurrent check samples before the clock edge, not after. A rule written against the value the signal takes after the edge fails a correct design — a mismatch of four on hardware that is right. Section 5.

An implication whose antecedent never fires passes on every cycle. Ten thousand cycles, zero real evaluations, and a perfect score. Section 6.

A check gated off by every reset in the design is off for the cycles it was needed. A hundred cycles of its own reset becomes 2,100 gated — twenty-one percent of the run. Section 7.

A response window narrower than the protocol's worst legal case fails legal traffic. A 100-cycle window against a 200-cycle worst case flags a legal 150-cycle response; an unbounded one flags nothing at all. Section 8.

And a check that reports a warning leaves the run green. Twelve real failures, nine of them never read, and a regression that passes. Section 12.

This chapter against 25.2, stated precisely. That one owns the scope of an observation. This one owns its timing, its patience and its consequence — which is why every model here is about a check that runs and proves nothing, and why section 14's weak definition is a regression log with no failures in it.

2. The One-Sentence Model

A check suite is trustworthy when every antecedent has fired, nothing is gated off but the check's own reset, every window covers the worst legal case, one thread follows each outstanding request, and a firing stops the run — and "no check fired" is none of those five.

3. What This Chapter Owns

Deferred:

4. Teaching-Model Boundary

Icarus Verilog 13.0 has no concurrent assertion support, so nothing in this chapter is written as SVA. Every model is a small synchronous block that computes the consequence of one assertion-language decision — which region a value is read in, how many cycles a check is disabled, how many threads a rule spawns — and each is checked procedurally. The arithmetic is the teaching content; the syntax is in IEEE 1800 and is not reproduced here.

Three simplifications are worth stating. Section 5 models the preponed region as a single pre-edge value rather than the full four-region scheduler. Section 11 prices evaluation at a flat cost per check, where a real simulator's cost depends heavily on the property's shape. Section 13 treats proof depth as a single number, where a real engine reports different depths per property. 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 defensible-sounding choice: read the value after the edge, count every pass, gate on any reset, leave the window open, follow one thread, report a warning. None is a typo, and each has been argued for in a real review.

Figure 1 — Both populations reach the pass counter and only one reaches the evidence. Two percent of the run proved something, and no number in the report says so.

5. RTL 1 — A Concurrent Check Samples Before The Edge

// RTL 1 - sampling semantics. A concurrent check samples its operands in the
// preponed region, so it sees the value before the clock edge, not after.
module sampling_region #(parameter int SAMPLE_AFTER_EDGE = 0) (
  input  logic clk, rst_n,
  input  logic        eval_it,
  input  logic [15:0] value_before, value_after, wanted,
  output logic [15:0] sampled, mismatch,
  output logic        rule_holds,
  output logic [7:0]  n_evals, n_failures,
  output logic        late_sample_err
);
  // The preponed region is the value as it stood before the edge.
  assign sampled = (SAMPLE_AFTER_EDGE != 0) ? value_after : value_before;
  assign mismatch = (sampled > wanted) ? (sampled - wanted) : (wanted - sampled);
  assign rule_holds = (mismatch == 16'd0);
  // A check reading the post-edge value, which no concurrent check can see.
  assign late_sample_err = eval_it && (value_before != value_after)
                           && (sampled == value_after);

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      n_evals <= 8'd0; n_failures <= 8'd0;
    end else if (eval_it) begin
      n_evals <= n_evals + 8'd1;
      if (!rule_holds) n_failures <= n_failures + 8'd1;
    end
  end
endmodule

Five evaluations.

One failure with preponed sampling; three with post-edge sampling.

A concurrent assertion reads the value that was there before the edge, always. That is not a subtlety to be worked around — it is the semantics that make an assertion deterministic regardless of where the procedural code that drives the signal happens to be scheduled. Every value an assertion sees is one clock old by construction.

Row three is the bug report that arrives every time. The rule was written thinking of the value after the edge, the design is correct, and the assertion fires on a mismatch of four. A day is spent on the RTL before anybody looks at the check, and the fix is to shift the property rather than the hardware.

Row two is why the mistake survives. When the signal does not change across the edge the two regions agree, and most signals do not change on most cycles. A check written against the wrong region passes for a long time and then fires on exactly the cycles that matter.

6. RTL 2 — An Implication That Never Fires Passes Every Cycle

// RTL 2 - vacuity. An implication whose antecedent never fires passes on every
// cycle, and a pass count cannot tell the two kinds of pass apart.
module vacuity #(parameter int COUNT_ALL_PASSES = 0) (
  input  logic clk, rst_n,
  input  logic        measure,
  input  logic [15:0] cycles_run, antecedent_fires, real_passes,
  output logic [15:0] reported_passes, vacuous_passes, real_pct,
  output logic        meaningful,
  output logic [7:0]  n_measures, n_vacuous,
  output logic        vacuity_hidden_err
);
  logic [31:0] p_q;
  // A pass on a cycle the antecedent did not fire proves nothing.
  assign vacuous_passes = (cycles_run > antecedent_fires)
                          ? (cycles_run - antecedent_fires) : 16'd0;
  assign reported_passes = (COUNT_ALL_PASSES != 0) ? cycles_run : real_passes;
  assign p_q = (cycles_run == 16'd0) ? 32'd0
             : (({16'd0, real_passes} * 32'd100) / {16'd0, cycles_run});
  assign real_pct = (p_q > 32'd65535) ? 16'hFFFF : p_q[15:0];
  assign meaningful = (antecedent_fires != 16'd0);
  // Vacuous passes counted as evidence.
  assign vacuity_hidden_err = measure && (vacuous_passes != 16'd0)
                              && (reported_passes == cycles_run);

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      n_measures <= 8'd0; n_vacuous <= 8'd0;
    end else if (measure) begin
      n_measures <= n_measures + 8'd1;
      if (reported_passes != real_passes) n_vacuous <= n_vacuous + 8'd1;
    end
  end
endmodule

Five measurements. Ten thousand cycles unless stated.

The real count never disagrees with itself; the all-passes count disagrees three times of five.

Vacuity is not a corner case; it is the normal condition of an implication. A rule of the form "if a request is issued then a response follows" is evaluated on every cycle, and on the overwhelming majority of them there is no request. Those cycles pass, correctly and meaninglessly, and a tool that reports "10,000 passes, 0 failures" has told you nothing about the 9,800.

Row two is the check that cannot fail. The antecedent never fired once in ten thousand cycles — perhaps the signal was misnamed, perhaps the stimulus never reached that state — and the report is indistinguishable from a rule that held perfectly. The only number that separates them is the firing count, and it is the number least often looked at.

Row three is the exemption, and it is rare. An antecedent that fires on every cycle makes vacuity impossible and the two models agree exactly. That happens for unconditional rules — "this signal is never X" — which are the minority of any real suite and the ones least likely to be wrong.

7. RTL 3 — A Gate That Covers Every Reset Covers Too Much

// RTL 3 - the gating condition. A check gated off by reset must be gated for
// exactly the cycles reset is active, and gating too widely disables it.
module gate_scope #(parameter int GATE_ON_ANY_RESET = 0) (
  input  logic clk, rst_n,
  input  logic        evaluate,
  input  logic [15:0] total_cycles, reset_cycles, other_gated_cycles,
  output logic [15:0] gated_cycles, live_cycles, gated_pct,
  output logic        adequately_live,
  output logic [7:0]  n_evals, n_dead,
  output logic        overgated_err
);
  logic [31:0] g_q, p_q;
  // Gating on any reset in the design gates on resets this check does not care
  // about, and every gated cycle is a cycle the check is not running.
  assign g_q = (GATE_ON_ANY_RESET != 0)
             ? ({16'd0, reset_cycles} + {16'd0, other_gated_cycles})
             : {16'd0, reset_cycles};
  assign gated_cycles = (g_q > 32'd65535) ? 16'hFFFF : g_q[15:0];
  assign live_cycles = (total_cycles > gated_cycles)
                       ? (total_cycles - gated_cycles) : 16'd0;
  assign p_q = (total_cycles == 16'd0) ? 32'd0
             : (({16'd0, gated_cycles} * 32'd100) / {16'd0, total_cycles});
  assign gated_pct = (p_q > 32'd65535) ? 16'hFFFF : p_q[15:0];
  assign adequately_live = (gated_pct <= 16'd10);
  // Cycles gated off that no reset of this check's own required. No guard on
  // other_gated_cycles is needed: gated_cycles can only exceed reset_cycles
  // when other_gated_cycles is non-zero, in either build.
  assign overgated_err = evaluate && (gated_cycles > reset_cycles);

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

Five evaluations. Ten thousand cycles unless stated.

One inadequately live with a narrow gate; two with a wide one.

A gating condition is written to suppress false failures during reset, and it suppresses everything it names. Gating on a global "any reset active" signal is the convenient thing to write, and in a design with several reset domains it turns a hundred cycles of suppression into 2,100 — twenty-one percent of the run in which the check is not a check.

Rows three and four are the policy threshold and it is inclusive. Exactly ten percent gated is adequate and eleven is not. The number matters less than having one, because without it "the check is disabled during reset" is a statement with no quantity attached and nobody notices when the quantity grows.

Row five is the degenerate case worth stating. A run of no cycles gates nothing and reports as live, which is arithmetically right and substantively empty. A liveness metric computed over zero cycles is not evidence, and the model reports it as such rather than dividing by zero.

8. RTL 4 — A Window Is Wrong In Both Directions

// RTL 4 - the response window. A bounded window fails a response that was
// legal but late; an unbounded one never fails and never finishes.
module response_window #(parameter int UNBOUNDED_WINDOW = 0) (
  input  logic clk, rst_n,
  input  logic        judge,
  input  logic [15:0] window_max, actual_latency, worst_legal_latency,
  output logic [15:0] slack, false_failures, missed_failures,
  output logic        flags_it, window_correct,
  output logic [7:0]  n_judgements, n_wrong,
  output logic        unflagged_violation_err
);
  // A window shorter than the worst legal latency fails legal traffic; an
  // unbounded window flags nothing at all.
  assign flags_it = (UNBOUNDED_WINDOW != 0) ? 1'b0 : (actual_latency > window_max);
  assign slack = (window_max > actual_latency) ? (window_max - actual_latency) : 16'd0;
  assign false_failures = (UNBOUNDED_WINDOW == 0)
                          && (window_max < worst_legal_latency)
                          && (actual_latency > window_max)
                          && (actual_latency <= worst_legal_latency) ? 16'd1 : 16'd0;
  assign missed_failures = (UNBOUNDED_WINDOW != 0)
                           && (actual_latency > worst_legal_latency) ? 16'd1 : 16'd0;
  assign window_correct = (window_max >= worst_legal_latency)
                          && (UNBOUNDED_WINDOW == 0);
  // A latency past the protocol's own worst case that no window flagged.
  assign unflagged_violation_err = judge && (actual_latency > worst_legal_latency)
                                   && !flags_it;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      n_judgements <= 8'd0; n_wrong <= 8'd0;
    end else if (judge) begin
      n_judgements <= n_judgements + 8'd1;
      if (false_failures != 16'd0 || missed_failures != 16'd0)
        n_wrong <= n_wrong + 8'd1;
    end
  end
endmodule

Five judgements. A worst legal latency of 200 cycles.

One wrong with a bounded window — the false failure; two with an unbounded one, both real violations.

A response window encodes a number the protocol already fixed, and getting it wrong fails in opposite directions. Too narrow and legal traffic is flagged — noise, which trains the team to ignore the check. Left unbounded, the property waits forever and never fails at all, which is silence.

Row one is how a check acquires a waiver. The window is 100 and the protocol permits 200, so legal responses at 150 fire the assertion. The fix that gets applied under schedule pressure is $assertoff or an unbounded window, and the check that was too strict becomes a check that cannot fail.

Row three is the boundary the window must be written on. A response at exactly the worst legal latency is legal, so the comparison is inclusive — a window of 200 must not flag 200. That is the same off-by-one that section 9 finds in the implication operator, arriving from the latency side instead.

9. RTL 5 — Overlapping Or Not Is An Off-By-One In Every Check

// RTL 5 - overlapping against non-overlapping implication. The consequent
// starts on the antecedent's own cycle or on the next one, and the choice is
// an off-by-one in every check that uses it.
module implication_offset #(parameter int OVERLAP_IT = 0) (
  input  logic clk, rst_n,
  input  logic        evaluate,
  input  logic [15:0] antecedent_cycle, response_cycle,
  output logic [15:0] check_starts, gap, expected_gap,
  output logic        aligned,
  output logic [7:0]  n_evals, n_misaligned,
  output logic        offset_wrong_err
);
  // A non-overlapping implication starts the consequent one cycle later.
  assign check_starts = (OVERLAP_IT != 0) ? antecedent_cycle
                      : (antecedent_cycle + 16'd1);
  assign gap = (response_cycle > check_starts)
               ? (response_cycle - check_starts) : 16'd0;
  assign expected_gap = (response_cycle > antecedent_cycle)
                        ? (response_cycle - antecedent_cycle) : 16'd0;
  assign aligned = (check_starts <= response_cycle);
  // A consequent evaluated on the antecedent's own cycle, when the response
  // cannot legally arrive until the next one.
  assign offset_wrong_err = evaluate && (response_cycle > antecedent_cycle)
                            && (check_starts == antecedent_cycle);

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

Four evaluations. An antecedent on cycle 10.

One misaligned with a non-overlapping check; none with an overlapping one.

The two implication operators differ by exactly one cycle and there is no way to tell from the failure which one you wanted. A response that cannot arrive before the next cycle needs the non-overlapping form; a response that may arrive combinationally on the same cycle needs the overlapping one. Rows one and two are the same protocol under the two conventions, and each form is wrong for the other's traffic.

Row two is the failure that reads as a hardware bug. The response arrives on the antecedent's own cycle, the non-overlapping check starts looking after it has gone, and the assertion reports a missing response that was there. Nothing in the message says "off by one".

Rows three and four show why the error scales invisibly. At a gap of five the two forms differ by one in twenty percent; at a gap of one they differ by one in a hundred. The larger the real latency, the smaller the proportional difference — and the less likely the mistake is to be noticed before it matters.

10. RTL 6 — Checks Are Evaluated Every Cycle On Every Instance

// RTL 6 - what checks cost to run. Concurrent checks are evaluated every cycle
// on every instance, and the bill arrives as regression wall-clock.
module check_cost #(parameter int CHECKS_ARE_FREE = 0) (
  input  logic clk, rst_n,
  input  logic        budget,
  input  logic [15:0] checks_per_block, blocks, cost_per_check_ns,
  input  logic [15:0] base_runtime_min, budget_min,
  output logic [15:0] total_checks, added_min, runtime_min, overrun,
  output logic        affordable,
  output logic [7:0]  n_budgets, n_over,
  output logic        check_cost_ignored_err
);
  logic [31:0] c_q, a_q, r_q;
  assign c_q = {16'd0, checks_per_block} * {16'd0, blocks};
  assign total_checks = (c_q > 32'd65535) ? 16'hFFFF : c_q[15:0];
  assign a_q = (CHECKS_ARE_FREE != 0) ? 32'd0
             : (({16'd0, total_checks} * {16'd0, cost_per_check_ns}) / 32'd60);
  assign added_min = (a_q > 32'd65535) ? 16'hFFFF : a_q[15:0];
  assign r_q = {16'd0, base_runtime_min} + {16'd0, added_min};
  assign runtime_min = (r_q > 32'd65535) ? 16'hFFFF : r_q[15:0];
  assign overrun = (runtime_min > budget_min) ? (runtime_min - budget_min) : 16'd0;
  assign affordable = (runtime_min <= budget_min);
  // Checks that run on every cycle, costed at nothing.
  assign check_cost_ignored_err = budget && (total_checks != 16'd0)
                                  && (cost_per_check_ns != 16'd0)
                                  && (added_min == 16'd0);

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      n_budgets <= 8'd0; n_over <= 8'd0;
    end else if (budget) begin
      n_budgets <= n_budgets + 8'd1;
      if (!affordable) n_over <= n_over + 8'd1;
    end
  end
endmodule

Five budgets. Forty checks in each of thirty blocks, at 3 ns each, on a 120-minute base.

Two over budget when the checks are charged; none when they are not.

A concurrent assertion is evaluated on every clock, in every instance, for the whole run. Twelve hundred of them at three nanoseconds each is sixty minutes on a two-hour regression — fifty percent. That is the number that decides whether the suite runs nightly or weekly, and it is not in any assertion plan.

Row one is the trade nobody states. The choice is not "assertions or no assertions"; it is how many, on which instances, and in which regression tier. A suite that runs on a tenth of the instances in the nightly and all of them weekly is a decision with a number behind it — and the number is section 10's.

Row five is the saturation case, and it is a modelling honesty point rather than a design one. Ninety thousand checks exceeds the counter and saturates at 65,535 rather than wrapping to a small number. A cost model that wrapped here would report a large design as cheap.

11. RTL 7 — A Rule About Outstanding Requests Needs A Thread Each

// RTL 7 - pipelined checks. A rule about a request and its response has one
// live thread per outstanding request, and a single-threaded check follows the
// first one only.
module threaded_rule #(parameter int SINGLE_THREAD = 0) (
  input  logic clk, rst_n,
  input  logic        evaluate,
  input  logic [15:0] outstanding, violating_txn,
  output logic [15:0] threads, tracked, untracked,
  output logic        catches_it,
  output logic [7:0]  n_evals, n_missed,
  output logic        thread_lost_err
);
  // One thread per outstanding request, or one thread total.
  assign threads = (SINGLE_THREAD != 0) ? 16'd1 : outstanding;
  assign tracked = (threads > outstanding) ? outstanding : threads;
  assign untracked = (outstanding > tracked) ? (outstanding - tracked) : 16'd0;
  // The check catches a violation only if that transaction has a thread.
  assign catches_it = (violating_txn != 16'd0) && (violating_txn <= tracked);
  // Outstanding requests with no thread following them. No guard on
  // outstanding is needed: untracked is non-zero only when outstanding
  // exceeds one, since tracked equals outstanding in every other case.
  assign thread_lost_err = evaluate && (untracked != 16'd0);

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

Five evaluations.

Two evaluations with nothing caught because nothing was wrong; three when only one request is followed.

A property about a request and its response spawns a thread each time the antecedent fires. With eight requests outstanding there are eight live evaluations, each waiting for its own response. A check written to follow one — a flag, a single register, a non-pipelined property — tracks the first and drops seven.

Row three is why the defect passes bring-up. The violating transaction happens to be the one the single thread is following, so the check catches it and looks correct. Every early directed test has one outstanding request, which is exactly the regime in which the two designs are indistinguishable.

Row one is the number that matters at scale. Seven of eight requests are unwatched, so the check's probability of catching a random violation is one in eight — and it will eventually catch one, report a real bug, and thereby confirm to everybody that it works.

Figure 3 — The same eight requests under two checks. The single-threaded check is not disabled and not wrong — it evaluates the right rule, on one transaction in eight, and catches enough violations over a project to look like it works.

12. RTL 8 — A Warning Is A Failure Nobody Counts

// RTL 8 - severity. A check that reports a warning is a check whose failures
// are counted by nobody, and the regression stays green.
module severity_policy #(parameter int WARN_ONLY = 0) (
  input  logic clk, rst_n,
  input  logic        report_it,
  input  logic [15:0] firings, warnings_read_pct,
  output logic [15:0] stops_run, warnings, noticed, unnoticed,
  output logic        run_fails,
  output logic [7:0]  n_reports, n_silent,
  output logic        severity_too_low_err
);
  logic [31:0] n_q;
  // An error stops the run; a warning is read at whatever rate warnings are.
  assign stops_run = (WARN_ONLY != 0) ? 16'd0 : firings;
  assign warnings = (WARN_ONLY != 0) ? firings : 16'd0;
  assign n_q = ({16'd0, warnings} * {16'd0, warnings_read_pct}) / 32'd100;
  assign noticed = stops_run + ((n_q > 32'd65535) ? 16'hFFFF : n_q[15:0]);
  assign unnoticed = (firings > noticed) ? (firings - noticed) : 16'd0;
  assign run_fails = (stops_run != 16'd0);
  // A real failure that leaves the run green.
  assign severity_too_low_err = report_it && (firings != 16'd0) && !run_fails;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      n_reports <= 8'd0; n_silent <= 8'd0;
    end else if (report_it) begin
      n_reports <= n_reports + 8'd1;
      if (!run_fails) n_silent <= n_silent + 8'd1;
    end
  end
endmodule

Five reports.

One silent report with a fatal severity — the one with no firing; all five with a warning.

A check's severity decides whether its failures are facts or opinions. An error stops the run and appears in the regression summary; a warning appears in a log file that is read at whatever rate log files are read. Twelve real protocol violations, nine of them never seen by anybody, and the dashboard is green.

Row three is the sharpest row in the chapter. Even at a hundred percent warning-read rate — a team that genuinely reads every line — the run is still green. Being read is not being counted. The regression's pass/fail signal is what gates a release, and a warning does not touch it.

Row one is where the severity choice comes from. Warnings are chosen when a check is new and its false-failure rate is unknown, which is a reasonable temporary position. The failure is that it is temporary and nothing expires it — section 22's review question exists because nothing in the flow ever asks again.

13. RTL 9 — A Bounded Proof Proves A Rule As Far As It Reached

// RTL 9 - proof depth. A bounded proof establishes a rule up to a depth, and a
// bug that needs more cycles than that is not disproved, only unreached.
module proof_depth #(parameter int DEPTH_IS_PROOF = 0) (
  input  logic clk, rst_n,
  input  logic        evaluate,
  input  logic [15:0] proof_depth_cycles, bug_depth_cycles, sim_cycles,
  output logic [15:0] reach, shortfall, sim_advantage,
  output logic        rule_proven, bug_reachable_by_proof,
  output logic [7:0]  n_evals, n_unproven,
  output logic        bounded_as_full_err
);
  assign reach = proof_depth_cycles;
  assign bug_reachable_by_proof = (bug_depth_cycles <= proof_depth_cycles)
                                  && (bug_depth_cycles != 16'd0);
  assign shortfall = (bug_depth_cycles > proof_depth_cycles)
                     ? (bug_depth_cycles - proof_depth_cycles) : 16'd0;
  assign sim_advantage = (sim_cycles > proof_depth_cycles)
                         ? (sim_cycles - proof_depth_cycles) : 16'd0;
  // A bounded proof proves the rule only as far as it reached.
  assign rule_proven = (DEPTH_IS_PROOF != 0) ? 1'b1 : (shortfall == 16'd0);
  // A rule reported proven past the depth the proof actually reached.
  assign bounded_as_full_err = evaluate && (shortfall != 16'd0) && rule_proven;

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

Five evaluations. A bug reachable in 35 cycles, against 50,000 simulated.

Two unproven when the depth is respected; none when it is taken as a proof.

A bounded proof is a statement with a number attached, and the number is usually dropped in the retelling. "The property is proven" almost always means "no counterexample was found within twenty cycles" — and a bug that needs thirty-five is not disproved, merely unreached. Simulation, meanwhile, went 49,980 cycles further and proved nothing anywhere.

Rows three and four are the boundary and it is exact. A proof reaching exactly the bug's depth finds it; one cycle less does not. The depth is a hard edge, not a gradient — which is why "we increased the depth and it still passes" is only meaningful alongside the depth it reached.

Row five is the honest failure. With no known bug depth the shortfall is zero and the rule reads as proven — the model is missing an input rather than making a claim. It is worth separating from row two, where the depth genuinely covers a known-reachable bug: the two produce the same verdict from completely different evidence.

14. RTL 10 — A Check Suite Assembled

// RTL 10 - a check suite assembled. Everything that must hold before "the
// checks pass" is a statement about the design rather than about the checks.
module check_signoff #(parameter int CHECKS_PASS = 0) (
  input  logic clk, rst_n,
  input  logic       evaluate,
  input  logic       checks_pass,      // no check fired
  input  logic       non_vacuous,      // every antecedent fired
  input  logic       gated_narrowly,   // nothing gated off but this reset
  input  logic       windows_correct,  // every window covers the worst legal case
  input  logic       threads_tracked,  // one thread per outstanding request
  input  logic       severity_fatal,   // a firing stops the run
  output logic       trustworthy,
  output logic [5:0] fail_mask,
  output logic [7:0] n_eval, n_trusted,
  output logic       false_trust_err
);
  assign fail_mask[0] = ~checks_pass;
  assign fail_mask[1] = ~non_vacuous;
  assign fail_mask[2] = ~gated_narrowly;
  assign fail_mask[3] = ~windows_correct;
  assign fail_mask[4] = ~threads_tracked;
  assign fail_mask[5] = ~severity_fatal;
  // The checks-pass build is what a regression log reports.
  assign trustworthy = (CHECKS_PASS != 0) ? checks_pass : (fail_mask == 6'd0);
  assign false_trust_err = evaluate && trustworthy && (fail_mask != 6'd0);

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

Seven configurations.

One trusted under the full model; six under the log.

Row six is the one that makes the point without argument. A firing that only warns produces a green log by definition — the check ran, found the bug, reported it, and the regression passed. The log is not being fooled; it is reporting exactly what it measures, which is whether anything stopped the run.

The other four are checks that could not have fired. A vacuous antecedent, a gated-off window, an over-narrow window later waived, a single thread following one request of eight. None of them is disabled, which is why an audit that greps for $assertoff finds nothing.

These six are not 25.2's six. That chapter's failures are checks that were too narrow to see a violation; these are checks that were never in a position to evaluate one. A suite can pass both chapters' standards and still fail 25.1's, which asks whether the rule was written at all.

Figure 4 — Vacuity is asked first because it is the only failure with no observable symptom at all; severity is asked last because it is the only one where the check did its job and the report threw the answer away. Every exit above is a green regression.

15. Quantitative Reasoning

Sampling. A concurrent check reads the preponed value, one region old, always. A rule written against the post-edge value fails a correct design by 4 on three evaluations of five.

Vacuity. Ten thousand cycles with two hundred firings is 9,800 vacuous passes and a real share of 2%; an antecedent that never fires reports a perfect score on zero evidence.

Gating. A hundred cycles of a check's own reset becomes 2,100 gated on an any-reset condition — 21% of the run against a 10% policy line.

Windows. A 100-cycle window against a 200-cycle worst legal case flags legal traffic at 150; an unbounded window misses a violation at 201, the smallest it can lose.

Implication offset. The two forms differ by exactly one cycle — at a gap of five that is 20%, at a gap of one it is 100%, and neither failure message says "off by one".

Evaluation cost. Twelve hundred checks at 3 ns is 60 minutes on a 120-minute base — fifty percent — and 90,000 checks saturates rather than wraps.

Threading. Eight outstanding requests followed by one thread is seven untracked, and a one-in-eight chance of catching a random violation.

Severity. Twelve firings as warnings at a 25% read rate is nine unnoticed; at a 100% read rate it is zero unnoticed and a green run.

Proof depth. A proof reaching twenty cycles against a bug at thirty-five is fifteen short, while simulation ran 49,980 cycles further and proved nothing.

The assembled model. Six properties, seven configurations, one trustworthy. The log called six trustworthy.

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.

Before mutating, every model's outputs were listed and each confirmed to appear in an equality — 25.2 §18's step rather than its principle. It found one gap immediately: tracked in section 11 was computed, driven and never asserted, which is the same class that produced three of the previous chapter's four survivors. The step took two minutes and the principle had already failed twice.

Alongside it: every inclusive threshold at exactly equal, every ceiling on and off its boundary, every floor past it, and both builds asserted on every degenerate case.

Sampling. The gap across the edge is driven rising and falling, which is what an absolute difference requires.

chk(sBm == 16'd4, "and the post-edge value is off by four the other way");

Vacuity. An antecedent firing on every cycle is asserted to make the two models agree — the one configuration in which vacuity is impossible.

Gating. Exactly ten percent gated is asserted adequate and eleven percent is not.

Windows. A response at exactly the worst legal latency is asserted not flagged, and a violation one cycle past it is asserted flagged.

chk(rGx == 1'b0,  "a response at exactly the worst legal latency is not flagged");
chk(rBm == 16'd1, "and still missed by an unbounded window");

Implication offset. A response on the antecedent's own cycle is driven, which is the only configuration in which the non-overlapping form is the wrong one.

Evaluation cost. A budget exactly equal to the runtime is driven, and the saturating check count is asserted to clamp rather than wrap.

Threading. The violation is driven inside the tracked set and outside it, and the inside case is asserted caught by both builds.

Severity. A 100% warning-read rate is driven and asserted to leave the run green — the case that separates being read from being counted.

Proof depth. A depth exactly equal to the bug's is asserted proven and one cycle less is not.

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: 261 checks across two testbenches, 124 on the front five models and 137 on the back five, all passing on the unmutated sources.

17. Mutation Testing

Eighty-three mutations were injected one at a time. 83 injected, 83 killed, after two survivors.

Both survivors were dominated guards, and both were deleted rather than covered. Section 7's overgated_err carried a guard on other_gated_cycles != 0, and section 11's thread_lost_err carried one on outstanding > 1. Neither is reachable false while the rest of its expression is true: gated cycles can only exceed the reset cycles when another reset contributed, and untracked requests only exist when more than one is outstanding. Each was deleted with a comment naming the dominating condition, and each mutation replaced with one that changes an operand.

That is six dead guards across two chapters — four in the previous batch, two here — and the rate is stable at roughly a quarter of survivors. A campaign that only ever adds stimulus would have shipped all six.

The survivor class that dominated the previous chapter did not appear at all here, because §16's step ran before the campaign rather than after it. It found tracked unasserted in two minutes. The rule cost one chapter to learn as a principle and one line of process to actually apply.

18. Verification Strategy

What a testbench for an assertion-semantics model must cover.

Run the output-listing step before mutating, not after. It caught this chapter's only instance of the previous chapter's dominant survivor class, at a cost of two minutes. Principles held while writing have now failed twice; a step performed afterwards has worked once.

Delete a dominated guard, do not contrive a case for it. Two here, four in the previous batch. The test to apply is whether the guard can be false while the rest of the expression is true — if not, it is dead code with a comment's worth of value and a mutation's worth of noise.

Drive both directions of every difference. §5's mismatch is an absolute value, so a testbench in which the signal only ever rises across the edge executes half of it.

The cases where the broken build is right. A signal that does not change across the edge. An antecedent that fires every cycle. A design with one reset. A violation inside the tracked set. One outstanding request. A run with no firings. Six exemptions across nine models, each a real configuration and each the reason the wrong choice survives review.

Separate what a check measures from what it reports. §12's noticed and run_fails are different outputs because a warning that is read is still a warning that does not fail the run — and the whole section is the distance between those two facts.

Counters as a second signature. Ten models, ten pairs of totals, differing in all ten.

What a real assertion suite needs that these models do not have. The full four-region scheduler for §5, a per-property cost model for §10, and per-property proof depths for §13. All three are abbreviations that preserve the conclusion, and section 26 exercises 1, 6 and 9 are where they come back.

19. Synthesis and Implementation Reality

Assertions are not synthesised, and that is exactly why they rot. Nothing downstream consumes them, so a property that stopped matching the RTL two revisions ago produces no error anywhere — it produces vacuous passes, which is section 6 and is invisible.

disable iff is evaluated asynchronously and takes precedence over everything. That is what makes section 7's over-gating so effective at silencing a check: the condition does not need to be true at the sampling edge, only during the evaluation, so a wide gate suppresses attempts already in flight.

A property with an unbounded window holds a thread open until the end of simulation. Section 8's unbounded build is not only silent — it accumulates state, and a suite of them on a busy interface is a real memory cost as well as a real coverage hole.

Section 11's threading is automatic in SVA and manual in everything else. A concurrent property spawns a thread per antecedent match without being asked; the same rule written as procedural code in a monitor does not, which is where single-threaded checks come from.

Severity is a runtime decision as well as a compile-time one. $assertoff, elaboration-time filters and per-instance controls all disable checks without editing them, so section 12's audit has to read the runtime configuration, not the source.

Formal and simulation fail on opposite axes. A bounded proof covers every input for twenty cycles; a regression covers one input sequence for fifty thousand. Section 13's sim_advantage is that asymmetry as a number, and it is the argument for running both rather than choosing.

20. Silicon Observability

"Properties with zero firings across the whole regression" is the cheapest high-value audit in this chapter. It requires no new instrumentation — the firing counts already exist in every simulator's coverage database — and it is the direct detector for the failure with no other symptom. A property that never fired in a full regression is either unreachable, misnamed, or checking something that never happens, and all three are worth a morning.

21. Debug Lab

Symptom. A CXL device passes its full assertion suite for six months. At first silicon: a completion returns with the wrong tag under sustained load, roughly once an hour. The suite has a property for exactly this rule, written on day one, and it has never fired.

Step 1 — did the property ever run? Section 6. The firing count for the tag-uniqueness property across the entire regression is zero. Six months of green is six months of vacuous passes, and the audit that would have shown it is a column in the coverage database.

Step 2 — why did it never fire. The antecedent names req_valid && req_ready && !cfg_mode, and cfg_mode was tied high in the environment's default configuration eighteen months ago for an unrelated reason. The property was correct, the rule was correct, and the antecedent was unreachable.

Step 3 — the second property. A related rule does fire, and passes. Its window is ##[1:16], written from an early latency estimate. The protocol's worst legal case is 200 cycles. Section 8. It was flagging legal traffic during bring-up, and the fix applied at the time was to change its severity to a warning rather than widen the window.

Step 4 — how many warnings. Section 12. That property has fired 1,847 times across the regression. Every one is in a log; the run has been green every time. At a realistic read rate, nine in ten were never seen by a person.

Step 5 — the threading. The tag-uniqueness rule, once the antecedent is fixed, tracks one outstanding request. Section 11. The device runs thirty-two outstanding, so even repaired the check watches one transaction in thirty-two — which is why the first fixed run still passed.

Step 6 — what the tag bug actually is. A tag freed one cycle early under a specific retry sequence. It needs forty cycles of setup to reach. Section 13: the formal run on this block reached a depth of twenty and reported the property proven. Twenty cycles of exhaustive proof, and the bug is at forty.

The finding. One hardware bug and four independent reasons the suite could not report it: an unreachable antecedent, a real failure demoted to a warning, a single-threaded check on a 32-deep pipeline, and a bounded proof that stopped short. None of the four is a disabled check, which is why every audit that looked for disabled checks found nothing.

The fix. In the RTL, hold the tag until the retry window closes. In the environment: fail the regression on any property with zero firings, restore the demoted property's severity and widen its window to 200, re-write the tag rule as a properly threaded concurrent property, and re-run the proof to a depth argued from the deepest known sequence rather than from the default.

What made this hard. Every one of the six months was honestly green. The suite contained a correct property for the exact rule that broke, and it had never once been evaluated.

22. Design Review

1. How many properties fired zero times in the last full regression? The audit is a database column and it is almost never run. Sections 6 and 20.

2. For each property, what is the antecedent's firing count? A pass count without it is not evidence. Section 6.

3. What does each property's disable iff name, and how many cycles was it gated? A global reset condition gates twenty-one percent of the run. Section 7.

4. Where did each response window's bound come from? An early estimate that flags legal traffic becomes a waiver. Section 8.

5. Which properties are warnings, who decided, and when does that expire? Nothing in the flow ever asks again. Section 12.

6. Which properties are disabled at runtime rather than in source? A source audit will not find them. Section 19.

7. How many threads does each pipelined property hold at peak? One thread on thirty-two outstanding requests. Section 11.

8. Which implication form does each property use, and does it match the protocol's response timing? An off-by-one whose message never says so. Section 9.

9. What depth did each proof reach, and what is the deepest known sequence? "Proven" is a claim with a number attached. Section 13.

10. What does a green regression establish? Section 14 exists because the answer is the last property only.

23. How This Appears In Real Engineering

A verification engineer writes properties that pass, and a property that passes looks finished. Nothing in the ordinary workflow distinguishes a property that holds from one that never ran — which is why section 6's audit has to be a gate rather than a habit.

A verification lead owns the severity policy, usually by inheriting it. Demotions to warning are made for good reasons under schedule pressure and are never revisited, and section 12's 1,847 firings is what that looks like after a year.

A formal engineer reports proof depths precisely and watches them get rounded to "proven" one meeting later. Section 13's shortfall is the number that survives the retelling, and stating it alongside the verdict is the whole intervention.

A designer meets this chapter as the sinking feeling in section 21 — a correct property, for the exact rule that broke, that never ran. The corrective is not more properties; it is the firing count next to each one.

24. Common Misconceptions

"The property passes, so the rule holds." It holds on the cycles the antecedent fired, which may be none. Ten thousand passes and two hundred evaluations look identical in every report that does not print the firing count (section 6).

"The check is enabled — I can see it in the source." Enabled is not the same as live. A wide disable iff gates twenty-one percent of the run (section 7), and runtime controls disable properties the source knows nothing about (section 19).

"We made it a warning until the false failures settle down." Reasonable, temporary, and nothing expires it. 1,847 firings later the run is still green, and even at a hundred percent read rate it would be (section 12).

"The property is proven." To a depth. A bug at forty cycles is not disproved by a proof that reached twenty (section 13) — and the depth is the first thing dropped when the result is repeated.

"Assertions are free — they don't synthesise." They cost simulation. Twelve hundred at 3 ns is sixty minutes on a two-hour regression (section 10), which is the real reason suites get thinned.

"An assertion sees what the RTL sees." It sees the preponed value, one region old, always (section 5) — and a rule written against the post-edge value fails a design that is right.

25. Interview Reasoning

"Your assertion suite is 100% passing. What do you check next?" The firing counts. A property that never fired is indistinguishable from a property that held, and the two have opposite meanings. A candidate who reaches for coverage has answered a different and later question; the antecedent count comes first because it costs nothing.

"Why did this assertion fire on correct hardware?" Section 5 is the first hypothesis: the rule was written against the value after the edge, and a concurrent check samples before it. The second is section 9 — the wrong implication form, off by one cycle. Both look like design bugs and neither is.

"How would you choose a response window bound?" From the protocol's worst legal latency, not from measured behaviour. Measured behaviour gives you a window that flags legal traffic the first time the design gets slower, and the fix under pressure is a waiver (section 8). Ask back: what happens at exactly the worst legal value?

"When is a warning the right severity for a check?" Almost never, and the useful answer names an expiry. A demotion with a date and an owner is a decision; one without is section 12's 1,847 firings.

"Formal says the property is proven. Are you done?" To what depth, and what is the deepest sequence you know how to construct? A bounded proof is a statement with a number attached, and the number is what makes it comparable to the fifty thousand cycles simulation ran.

26. Exercises

1. Model the full scheduler. §5 uses one pre-edge value. Add the preponed, active, observed and reactive regions, and find which of them a procedural monitor reads compared with a concurrent property.

2. Audit for vacuity. Given a suite of 400 properties over a 10,000-cycle run, write the report that separates real from vacuous passes and say what fraction of a typical suite you expect to be unreachable.

3. Price the gate. For a design with four reset domains, compute the gated percentage for a per-check gate and a global one, and find the number of domains at which the global gate crosses a 10% policy line.

4. Write the window from the specification. Take a rule with a 200-cycle worst legal latency. State the bound, the comparison, and what the property does at exactly 200 — then say what changes if the specification is later relaxed to 260.

5. Find the off-by-one. Construct a response protocol where the overlapping form is correct and one where it is not, and write the failure message that would distinguish them. Why does the default message not?

6. Build a per-property cost model. §10 uses a flat cost. Price a simple boolean property, a two-cycle sequence and an unbounded one separately, and re-derive the regression budget.

7. Thread a rule properly. For 32 outstanding requests, compute the catch probability of a single-threaded check against a violation at a uniformly random transaction, and the number of runs to reach 95% confidence of catching it.

8. Give warnings an expiry. Design a policy that permits a demotion to warning and guarantees it is revisited, and state what the regression does when the date passes.

9. Argue a proof depth. For a bug needing 40 cycles of setup, state the evidence that would justify a depth of 50 and what it costs. What do you do when the engine will not reach it?

10. Add the seventh property. Propose one none of §14's six implies, name its section, and construct the configuration where the six hold and it fails. A property that cannot fail alone is not a seventh property.

27. Summary

A concurrent check samples one region before the edge, always. A rule written against the post-edge value fails a correct design on exactly the cycles the signal moves — which is exactly when the rule is interesting.

An implication passes on every cycle its antecedent does not fire. Ten thousand cycles with two hundred firings is 9,800 vacuous passes and a real share of two percent, and a pass count cannot separate them.

An antecedent that never fires reports a perfect score. It is indistinguishable, in every report that omits the firing count, from a rule that held on every cycle of a six-month regression.

A gate that names every reset gates twenty-one percent of the run. A hundred cycles of a check's own reset becomes 2,100, and every gated cycle is a cycle the check is not a check.

A window is wrong in both directions. Too narrow and it flags legal traffic at 150 against a 200-cycle worst case — noise that earns a waiver. Unbounded and it misses a real violation at 201 — silence.

The two implication forms differ by exactly one cycle, and neither failure message says so. At a gap of five that is twenty percent; at a gap of one it is the whole answer.

Checks cost simulation. Twelve hundred at 3 ns is sixty minutes on a 120-minute base, which is the real reason suites get thinned and the number that should decide which tier they run in.

A pipelined rule needs a thread each. Eight outstanding requests followed by one thread is seven unwatched and a one-in-eight catch rate — and it catches enough to look like it works.

A warning is a failure nobody counts. Twelve firings at a 25% read rate is nine unnoticed; at a 100% read rate the run is still green, because being read is not being counted.

And a bounded proof proves a rule as far as it reached. Twenty cycles against a bug at thirty-five is fifteen short and not a disproof — while simulation ran 49,980 cycles further and proved nothing anywhere.

Both mutation survivors were dominated guards and both were deleted. That is six across two chapters, a stable quarter of survivors — and a campaign that only adds stimulus ships every one of them. Meanwhile the previous chapter's dominant survivor class did not appear once, because 25.2 §18's step was run before the campaign instead of learned from it.

"No check fired" is one property of six. The regression log called six of seven configurations trustworthy when one was — and §21 is a device six months green with a correct property, for the exact rule that broke, that had never once been evaluated.

25.4 — CXL Scoreboards takes the other half of the environment. This chapter's checks all evaluate at a clock; a scoreboard evaluates when two things match — and every argument here about timing becomes an argument about keys, ordering and what happens to a transaction that never finds its partner.