Senior Verification Strategy

“How would you verify a DDR memory controller?” The answer that fails is “build a UVM environment, add assertions, add functional coverage.”

It fails because it names three tools and zero obligations. Every one of the three is correct and none of them is an answer: a tool cannot be evaluated without the claim it is supposed to support.

The question behind the question, and the one this chapter is built on:

What does this assertion actually prove?

Start from the obligations — the things that must be true — then ask what kind of evidence each kind of truth requires. Some obligations need an assertion; some need an independent model; some need only a cover; and some are best caught by lint before simulation starts.

Five chapters of this module have each produced a different reason a passing property proves nothing, and the curriculum supplies three more. §6 collects all eight, and the collection is the deliverable: a checklist, not an insight.

1. Why the Tool Answer Fails

Three things are graded, and the tool answer scores on none of them.

And there is a fourth, which is the interview's real purpose: can you tell a colleague that their passing regression proves nothing, and show them why? That is a reviewing skill, and §6 is its checklist.

The reframe to say in the first thirty seconds: before choosing tools, I would write down what must be true about this controller — and then, for each one, what would constitute evidence. That sentence answers the question, because everything after it is derivable.

2. The Obligations

A DDR controller's obligations fall into five kinds, and the kind determines the evidence.

Two observations that make this a senior list.

The five kinds need five different instruments, and conflating them is the tool answer's real error. A safety obligation is an assertion's natural shape. A functional obligation needs an independent expected value, which is a model. A progress obligation needs a bound and cannot be an unbounded liveness property. A discharge obligation needs a ledger that is compared. And a performance obligation needs a measurement with a reference — 30.8 §11 — which no assertion supplies.

And the fifth row is the one candidates omit entirely. A controller that is correct and 40% below its bandwidth model is a failed controller, and no amount of assertion work discovers that. Naming performance as a verification obligation rather than a tuning afterthought is the clearest single signal of seniority in the answer.

3. What Each Tool Can Prove

Row seven is the one nobody lists and it caught two of this module's defects. CURRICULUM-DERIVED from 30.7 §9 — a trained input declared and never read — and 30.8 §10 — the same tell on any_outstanding. Both were findable before a testbench existed, and naming the cheapest tool that would have found a bug is a legitimate verification answer.

And row four carries the sharpest published warning in the curriculum. CURRICULUM-DERIVED from 27.5 §1: a coverage model dominated by uninformative axes reports a high percentage early, which licenses a sign-off argument that nothing supports — and that is the mechanism by which a coverage-driven lab reached 100% with a data-corruption bug still in the design.

4. The Evidence Architecture

Two edges carry the architecture.

DUT → monitor, labelled pins only. CURRICULUM-DERIVED from 27.3, which owns the independence requirement with its cannot-fail failure mode: a monitor that reads design internals agrees with the design by construction. §9's checker is that requirement violated in the timing domain.

vacuity report → verdict, labelled gates. The vacuity report is not an appendix. It decides whether the assertion results mean anything at all — §11.

And the obligation list appears twice, on purpose. It determines what the monitor watches and what the coverage model must hit. A coverage model derived from the design's signals rather than from the obligation list measures the design against itself — which is 27.5's argument for choosing axes by information content rather than by availability.

5. Working the Question

Q1 (establishing). How would you verify a DDR controller?

Answer in the order of §2 and §3, and do it in four sentences:

   1  I'd write the obligation list: safety, functional, progress,
      obligation-discharge, performance. Five kinds, five instruments.

   2  Safety obligations become bindable properties on the COMMITTED
      command stream -- the commit point (17.1), because timing is
      measured between commits and not between requests.

   3  The functional obligation needs an INDEPENDENT expected value,
      which for DDR is a memory model, and it is distributed because
      the obligations are per-bank with cross-bank leftovers (27.4).

   4  Then the instruments that make the first three believable:
      antecedent covers for every implication, a check-count on the
      scoreboard, a bandwidth measurement against a model, and lint.

Sentence four is what distinguishes the answer, because sentences one to three are what a good candidate says and sentence four is what a reviewer says.

Q2 (applying). Which obligation is hardest, and why?

Progress, and the reason is a property-shape argument rather than a DDR argument.

A progress obligation is naturally liveness — eventually — and an unbounded liveness property is not usable: it cannot fail in a finite simulation, and in formal it requires fairness assumptions that are themselves unverified claims about the environment. CURRICULUM-DERIVED from 27.2 §9, which records that this curriculum's corpus uses no sequence operator at all and states why.

So the obligation must be converted into a bound:

   NOT  "every accepted request eventually completes"
   BUT  "every accepted request completes within N cycles"

   and then N must be JUSTIFIED, not chosen:
     N >= the worst legitimate wait
        = tRAS + tRP + tRCD in the conflict case
        + the refresh drain and occupancy
        + contention from the other queue entries
   -- 17.4 §9 owns that derivation, and 30.5 §8 is the interview form.

And the qualification that makes it senior: a bound that is too loose is satisfied by a design that starves in practice, so the bound must be tight enough to fail on the starvation case 17.4 §8 demonstrates. A progress property nobody has watched fail is a progress property nobody has tested.

6. Eight Reasons a Green Assertion Proves Nothing

This is the chapter's checklist, and every entry was derived from a working defect earlier in this module.

Eight entries, and the last three come from the curriculum rather than from this module — which is the point: the list is not a clever observation, it is a review procedure, and its length is why it has to be written down rather than remembered.

Variety 6 is the largest in volume and the curriculum has measured it. CURRICULUM-DERIVED from 27.2: of 843 named properties in this curriculum, 78.5% are implications and therefore vacuity-exposed, 74 lack a reset guard, and 89 chapters contain no cover at all — 84 of them Modules 1 to 13, which wrote 343 assertions and zero covers. So every implication in that range is vacuity-exposed with no instrument that would reveal it, and that is a measurement of a real corpus rather than a caution.

And variety 6 has a documented instance with a published report. Chapter 27.2 §3 records a legal-only testbench in which three forbidden-transition properties passed while their antecedents never became true, so they held trivially and constrained nothing — and the only evidence was a coverage report nobody was reading.

7. Three Questions to Ask of Any Property

A review procedure that takes under a minute per property and finds every variety in §6.

   1  WHICH SIGNAL, if corrupted, would make this property fail?
        -- no answer  -> variety 2. it is about something else.
        -- the answer is a CONSTANT shared with the design
                      -> variety 4. it is a consistency check.

   2  ON WHICH CYCLES is it non-vacuous, and how often do they occur?
        -- unknown    -> variety 6. publish the antecedent as a cover.
        -- one cycle where a window was meant
                      -> variety 1.

   3  WHAT DOES IT NOT CONSTRAIN?
        -- it forbids, so it says nothing about progress or speed
                      -> variety 8. a bound or a measurement is needed.
        -- the obligation is comparative ("best", "widest", "fewest")
                      -> variety 3. it needs a model, not a property.
        -- the value is DERIVED (a rate, a percentage, an average)
                      -> variety 5. assert its range.

Question one is the highest-yield and it takes seconds. A property whose author cannot name the signal it protects is a property about the design's shape, and shape properties are the most common thing in a real assertion set because they are the easiest to write.

Question three is the one that changes designs rather than testbenches, because its answers are usually obligations nobody wrote down — which sends you back to §2's list with a gap identified.

8. Reviewing a Candidate's Property Set

A candidate offers these five properties as their verification plan for a DDR controller's command interface. Review them.

// A CANDIDATE'S PROPERTY SET, offered as a verification plan.
// CLASSIFICATION: illustrative review material. Each property is
// SYNTACTICALLY VALID and each has a defect of a DIFFERENT variety
// from §6. The corrected set follows.

  // P1
  property p_cmd_onehot;
    @(posedge clk) disable iff (!rst_n) $onehot0({act, pre, rd, wr, ref_cmd});
  endproperty
  assert property (p_cmd_onehot);

  // P2
  property p_no_act_before_trcd;
    @(posedge clk) disable iff (!rst_n)
      (rd && dut_bank_ready[rd_bank]) |-> 1'b1;
  endproperty
  assert property (p_no_act_before_trcd);

  // P3
  property p_read_returns_data;
    @(posedge clk) disable iff (!rst_n) rd |-> ##CL dq_valid;
  endproperty
  assert property (p_read_returns_data);

  // P4
  property p_request_completes;
    @(posedge clk) disable iff (!rst_n) req_accepted |-> s_eventually resp_valid;
  endproperty
  assert property (p_request_completes);

  // P5
  property p_efficiency_sane;
    @(posedge clk) disable iff (!rst_n) win_done |-> (eff_pct <= 100);
  endproperty
  assert property (p_efficiency_sane);

The review, one verdict per property:

The corrected set, with what changed and why:

  // P1' unchanged -- it was correct, only mislabelled. A shape
  // property is worth having; it is not timing verification.

  // P2' the real obligation, with an INDEPENDENT timing model. Note
  // `mdl_` rather than `dut_`: variety 7 is fixed by the prefix.
  // And the consequent is a real claim, not 1'b1.
  property p_trcd_respected;
    @(posedge clk) disable iff (!rst_n)
      (rd && mdl_same_bank_act_seen[rd_bank]) |->
        (mdl_since_act[rd_bank] >= TRCD);
  endproperty
  assert property (p_trcd_respected)
    else $error("column command issued before tRCD elapsed");

  // P2'' the antecedent, published. Without this, P2' can pass
  // because no read ever targeted a bank with a prior activate.
  cover property (@(posedge clk) disable iff (!rst_n)
                  rd && mdl_same_bank_act_seen[rd_bank]);

  // P2''' the BOUNDARY, covered rather than asserted -- variety 8:
  // a safety property cannot detect a controller that waits too long.
  cover property (@(posedge clk) disable iff (!rst_n)
                  rd && (mdl_since_act[rd_bank] == TRCD));

  // P3' the WINDOW, not the arrival cycle -- variety 1.
  property p_read_data_window;
    @(posedge clk) disable iff (!rst_n) rd |-> ##CL dq_valid[*OCC];
  endproperty
  assert property (p_read_data_window)
    else $error("read data did not occupy the full burst window");

  // P4' the BOUND, with its derivation named -- §5 Q2.
  // MAX_LAT is justified from 17.4 §9's worst legitimate wait, not
  // chosen to make the test pass.
  property p_request_completes_bounded;
    @(posedge clk) disable iff (!rst_n)
      req_accepted |-> ##[1:MAX_LAT] resp_valid;
  endproperty
  assert property (p_request_completes_bounded)
    else $error("request exceeded the justified completion bound");

  // P5' unchanged, plus its sibling: the check COUNT, so a clean
  // report is distinguishable from an empty one -- 27.4's discipline.
  property p_checks_were_performed;
    @(posedge clk) disable iff (!rst_n) win_done |-> (checks_done != '0);
  endproperty
  assert property (p_checks_were_performed)
    else $error("a window closed having compared nothing");

The set went from five properties to eight items, and three of the new items are covers. That ratio is the shape of a real plan, and CURRICULUM-DERIVED from 27.2 §6, which owns why the cover is not optional: the fix for a vacuous property is not a better property — the property is correct — it is a cover on the antecedent.

And P5''s sibling is the item most easily forgotten. A window that closed having compared nothing reports zero mismatches, and zero mismatches is what a passing regression looks like.

9. RTL Review — A Checker That Samples Late

The intended contract:

1. Observe the committed command stream only. No signal from inside the design. CURRICULUM-DERIVED from 27.3's independence requirement.
2. Maintain the checker's own per-bank elapsed-cycle state, advanced from the observed stream.
3. Evaluate a column command against the state as it stood on the command's own commit cycle, before that command's own effect is applied — 30.2's classification rule.
4. Report a rule mask, not a single rule id, because several rules can fail at once — 30.3 §4.
5. Count checks performed, so a zero-violation report is distinguishable from a zero-check report.

// ---------------------------------------------------------------------
// ddr_timing_check -- INTENTIONALLY DEFECTIVE, for review (§9).
//
// CLASSIFICATION: verification-only, ILLUSTRATIVE, CONTAINS A BUG.
//
// WHAT IT IS MEANT TO DO: the five-clause contract above -- an
// INDEPENDENT observer of the committed command stream that flags a
// column command issued too soon after an activate to the same bank.
//
// WHY IT EXISTS HERE: §6's variety 1 and 7 concern properties. This
// is the same failure one level down, in the INSTRUMENT: a checker
// whose sampling is off by one produces both false failures and
// false passes, and only one of the two gets investigated.
//
// HOW TO RUN IT: commit ACT to bank b, then a column command to bank
// b at exactly TRCD-1 cycles later.
// EXPECTED RESULT under clause 3: a violation, rule mask bit 0.
// EXPECTED TRACE: the evaluation must use the elapsed count as it
// stood on the column command's OWN commit cycle.
//
// SYNTHESIS: none -- verification only. No DUT signal appears on the
// port list, which clause 1 requires and which is checkable by
// inspection.
// LIMITATIONS: models the row-to-column rule ONLY. A complete checker
// takes the MAXIMUM over every applicable rule (30.3 §3), and the
// single-rule scope is why clause 4's mask is one bit wide here.
// ---------------------------------------------------------------------
module ddr_timing_check #(
  parameter int BANKS  = 16,
  parameter int TRCD   = 14,       // ILLUSTRATIVE
  // "Fixed" during bring-up when the checker produced false failures.
  // §10 is about what this parameter actually did.
  parameter int SLACK  = 1,
  parameter int CNT_W  = 8
)(
  input  logic                      clk,
  input  logic                      rst_n,

  // Observed, committed command stream. No DUT internals -- clause 1.
  input  logic                      obs_act,
  input  logic [$clog2(BANKS)-1:0]  obs_act_bank,
  input  logic                      obs_col,
  input  logic [$clog2(BANKS)-1:0]  obs_col_bank,

  output logic                      viol,
  output logic [0:0]                viol_mask,
  output logic [CNT_W-1:0]          checks_done
);
  initial begin
    if (CNT_W < $clog2(TRCD + 1))
      $fatal(1, "ddr_timing_check: CNT_W too narrow for TRCD");
  end

  logic [CNT_W-1:0] since_act [BANKS];
  logic             seen_act  [BANKS];

  // Registered copy of the observed column command -- clause 3 is
  // about WHEN this is evaluated.
  logic                      col_q;
  logic [$clog2(BANKS)-1:0]  col_bank_q;

  always_ff @(posedge clk) begin
    if (!rst_n) begin
      for (int b = 0; b < BANKS; b++) begin
        since_act[b] <= '0;
        seen_act[b]  <= 1'b0;
      end
      col_q       <= 1'b0;
      checks_done <= '0;
    end else begin
      for (int b = 0; b < BANKS; b++)
        if (seen_act[b] && since_act[b] != {CNT_W{1'b1}})
          since_act[b] <= since_act[b] + 1'b1;

      if (obs_act) begin
        since_act[obs_act_bank] <= '0;
        seen_act[obs_act_bank]  <= 1'b1;
      end

      col_q      <= obs_col;
      col_bank_q <= obs_col_bank;

      if (col_q && seen_act[col_bank_q] && checks_done != {CNT_W{1'b1}})
        checks_done <= checks_done + 1'b1;
    end
  end

  // The check. col_q is LAST cycle's command; since_act is THIS
  // cycle's state.
  always_comb begin
    viol      = 1'b0;
    viol_mask = 1'b0;
    if (col_q && seen_act[col_bank_q]) begin
      if (since_act[col_bank_q] + SLACK[CNT_W-1:0] < TRCD[CNT_W-1:0]) begin
        viol      = 1'b1;
        viol_mask = 1'b1;
      end
    end
  end
endmodule

Before reading on: which clause, and what did SLACK actually do?

10. The Defect, and What the “Fix” Did

The violated clause is 3, and the defect is the registered col_q: the command is delayed by one cycle while the elapsed counter is not.

So the checker compares last cycle's command against this cycle's state, and since_act has already advanced. Every evaluation sees one more cycle of elapsed time than actually elapsed — which makes the checker one cycle too lenient.

   ILLUSTRATIVE TRCD = 14, SLACK = 0 for this trace.
   ACT to bank 5 committed at cycle 100. since_act[5] <= 0.

   a column command to bank 5 committed at cycle 113 is ILLEGAL:
   only 13 cycles elapsed (30.3 §5's stated convention).

   cycle 113   obs_col=1; col_q <= 1
               since_act[5] = 13
   cycle 114   col_q = 1 (last cycle's command)
               since_act[5] = 14   <-- already advanced
               check: 14 < 14 is FALSE -> NO VIOLATION

   the illegal command passes. the checker is one cycle LENIENT.

And now the part the review is for: what did SLACK = 1 do?

During bring-up this checker produced false failures, because the same one-cycle error is strict at the other boundary — a command legal by exactly one cycle in one direction reports a violation depending on where the counter reset lands relative to the registered command. SLACK was added to stop the noise, and it worked: the false failures stopped.

It also made the checker two cycles lenient instead of one.

A checker adjusted until it stopped complaining has been calibrated against the design rather than against the specification. The false failures were the evidence, and tuning them away destroyed it.

That is this chapter's sharpest result and it is a process finding rather than a code finding. The false failures were real information: they said the checker and the design disagreed about a boundary — 30.3 §5's three readings — and the correct response was to establish which convention was normative, not to add a tolerance.

The correction, and both halves are needed:

  // CORRECTED. Clause 3: evaluate the command against the state as it
  // stood on the command's OWN commit cycle. Either sample the state
  // alongside the command, or evaluate combinationally from the
  // observed command -- this takes the second, which needs no extra
  // registers and cannot drift.
  //
  // SLACK is DELETED, not set to zero: a tolerance parameter on a
  // checker is a place for the next person to hide a disagreement.
  // If a convention is genuinely ambiguous, STATE it (30.3 §5) and
  // encode the stricter reading -- do not parameterise it.
  always_comb begin
    viol      = 1'b0;
    viol_mask = 1'b0;
    if (obs_col && seen_act[obs_col_bank]) begin
      if (since_act[obs_col_bank] < TRCD[CNT_W-1:0]) begin
        viol      = 1'b1;
        viol_mask = 1'b1;
      end
    end
  end

And the clause-5 observation that makes the whole block reviewable: checks_done must be compared against expectation. A checker reporting viol = 0 with checks_done = 0 is indistinguishable from a working one, and this block's registered col_q means its check count is also off by one — so the count that was meant to validate the checker was computed by the same defective logic. Independence applies to an instrument's own self-checks too.

11. Vacuity as a Deliverable

Q3 (the senior turn). Your regression is green. What do you hand to a sign-off review?

Not the pass rate. CURRICULUM-DERIVED from 27.5, which owns what a coverage number licenses: its closure model refuses to produce a single percentage, and a coverage number licenses nothing without checking present.

Four artifacts, and the second and third are the ones nobody brings:

Row two turns the corpus statistic in §6 into an operational requirement. With 78.5% of properties vacuity-exposed, an assertion report without antecedent counts is a report about 21.5% of the property set — and that arithmetic is a sentence worth having ready.

Row four's second half is a discipline the curriculum publishes. CURRICULUM-DERIVED from 27.5 §8: the exclusion list goes stale. An exclusion written because a bin was unreachable in one configuration silently hides a reachable bin after a parameter change, so an exclusion without a recorded reason is a hole with a lid on it.

The follow-up an interviewer should ask: what if the antecedent counts are all healthy and coverage is closed? Then you have evidence about the space you stated, and the remaining question is whether the obligation list was complete — which is not a verification question at all, and saying so is the honest end of the answer. CURRICULUM-DERIVED from 27.5's legal / reachable / interesting distinction: closure over the interesting set is the goal, and interesting is a human judgement that no tool supplies.

12. A Bug Escaped to Silicon

Q4 (diagnosing). A DDR controller bug was found in silicon. What does that tell you about the verification plan?

The tempting answer is we need more coverage, and it is the one answer that cannot be acted on. An escape is evidence about a specific mechanism, and the mechanism determines the fix — which is the same reframe 30.8 §8 applied to a regression.

Five escape mechanisms, and each implies a different repair:

Row five is the only case the reflexive answer fits, and it is rarely the case. Four of the five mechanisms are plan or review defects that no additional stimulus would have found — and distinguishing them is what the escape analysis is for.

The discriminating procedure, cheapest first:

   1  is the obligation in the plan?        -- read the plan. minutes.
   2  is there a property for it?           -- grep. minutes.
   3  did that property's antecedent occur? -- the vacuity report,
                                                IF one exists (§11)
   4  does the property survive §7's three questions?
   5  only then: did the stimulus reach the state?

Steps one to three take under an hour and settle most escapes. And step three is the one that is impossible without §11's antecedent counts — which is the operational argument for collecting them, rather than the principled one.

The follow-up that separates levels: what if step three cannot be answered because no vacuity report exists? Then the escape has already told you the most important thing — that the programme cannot distinguish a checked property from a trivially satisfied one — and that finding outranks the individual bug. CURRICULUM-DERIVED from 27.2 §3's published instance, where three properties passed vacuously and the only evidence was a coverage report nobody was reading.

And the honest thing to say about blame: an escape is a property of the plan, not of the engineer who wrote the property that missed it. A review procedure that only runs after an escape is not a procedure; §7 exists so that the eight varieties are caught at review time, when they cost a minute each.

13. What Would You Measure?

Q. What metrics would you track through a DDR verification programme?

Row four is the instrument that audits the instruments. A deliberate error injected into the design that no checker reports is a survivor, and a survivor is a finding about the testbench. A verification programme with no mutation result has never tested its own checkers.

Row seven is the cheapest and the most often absent. An obligation with zero properties is a plan defect, and it is visible without running anything — which makes it the first thing to compute, not the last.

And row eight is a one-line grep with a real yield. Every SLACK, TOLERANCE, FUDGE or _ADJ parameter in a checker is a place where somebody's disagreement was parameterised instead of resolved — §10.

14. Common Wrong Answers

“Build a UVM environment, add assertions, add coverage.” §1. Three tools, zero obligations. None can be evaluated without the claim it supports.

“We have 800 assertions.” §6. A count is not evidence. CURRICULUM-DERIVED from 27.2: 78.5% of this curriculum's 843 are vacuity-exposed, so the number that matters is how many antecedents occurred.

“Coverage is at 100%.” §3, §11. A coverage number licenses nothing without checking present — 27.5 — and a model dominated by uninformative axes reports high early.

“The regression is green.” §11. Green over what antecedents, with how many checks performed? Both are reportable and neither is in a pass rate.

“Assertions verify timing.” §3, §6 variety 8. They verify that nothing happened too early. A controller one cycle too conservative satisfies every one of them.

“The scoreboard reported no mismatches.” §8. Against how many comparisons? Zero mismatches over zero checks is what an unwired scoreboard reports.

“I'd assert that every request eventually completes.” §5 Q2. Unbounded liveness cannot fail in simulation and needs unstated fairness assumptions in formal. Bound it, and justify the bound.

“p_x |-> 1'b1 documents the intent.” §8 P2. It is a checker that cannot fail, and a comment claiming otherwise is worse than no property.

“The monitor reads the controller's bank-state array — it's simpler.” §9, and 27.3 owns the correction: a checker that reads the design's state agrees with it by construction, so an error in that state cancels.

“The checker was producing false failures so we added tolerance.” §10. The false failures were the evidence. Establish which convention is normative; do not parameterise the disagreement.

“We reviewed every property and they all look right.” §7. Looks right is not a review. Name the signal each one protects, the cycles on which it is non-vacuous, and what it does not constrain.

“Performance is a tuning task, not a verification obligation.” §2. A correct controller 40% below its model is a failed controller, and no assertion discovers that.

“The exclusion list is fine, it was reviewed last year.” §11. It goes stale — 27.5 §8. An exclusion without a recorded reason is a hole with a lid on it.

“A bug escaped, so we need more coverage.” §12. Only one of five escape mechanisms is a coverage gap. The other four are plan or review defects that no extra stimulus would have found.

“Formal proved it.” §3. Formal proved a property over the reachable states under the constraints you wrote, and the constraints are unverified claims about the environment. Report them alongside the proof.

“We use a commercial VIP, so protocol compliance is covered.” A VIP checks what it checks, and 27.6 owns what integrating one does and does not settle. The obligation list is still yours, and the useful question is which of its rows the VIP covers — which is §2 again, with a procurement decision attached.

15. Self-Check

1. Write the five kinds of obligation and, for each, the instrument that can support it and one that cannot.

2. State what each of the seven tools in §3 proves and cannot prove. Then name the two defects in this module that lint would have found before simulation.

3. Reproduce §6's list from memory. For each variety, give the one-sentence test from §7 that detects it.

4. Review P1 through P5 in §8 without reading the verdict table. Assign each a variety and say what you would change.

5. Convert “every accepted request eventually completes” into a usable obligation, and justify the bound from named chapters rather than choosing it.

6. Find the defect in §9 without reading §10. State the direction of the error and why only one of its two symptoms was investigated.

7. Explain what SLACK = 1 accomplished, and state the general rule about tolerance parameters in checker code.

8. A bug escaped to silicon. List the five mechanisms from §12 in the order you would check them, and say which single one “more coverage” addresses.

9. You are asked to sign off a green regression. List the four artifacts you would require, and say what each would reveal that a pass rate does not.

16. Where This Goes

A verification question is an evidence question. Enumerate the obligations before naming a tool; match each obligation's kind to the evidence its kind admits; convert liveness into a justified bound; publish every antecedent as a cover, because 78.5% of a real corpus is vacuity-exposed; keep every checker independent of the design's state; and treat performance as an obligation rather than a tuning task.

Three results carry forward. A checker adjusted until it stopped complaining has been calibrated against the design, and the false failures it was silenced for were the evidence. A clean report over zero checks is what a passing regression looks like. And the eight varieties in §6 are a review procedure rather than an insight — which is why the answer to what does this assertion actually prove is three questions asked in under a minute, not a judgement call.

Chapter 30.10 closes the module where verification stops. In simulation you can see every signal; in a lab you can see almost nothing, and the part does not stop. The question is walk me through a bring-up debug session, and it is the only question in the module with no right answer at all — because the graded output is not a diagnosis but a sequence of decisions, each one justified by the evidence available at the time it was taken, with the cheapest discriminator chosen first.