Lesson 9.6 · When Proofs Lie: Avoiding False PositivesA false-positive checklist
| # | Check | Done when… |
|---|
| 1 | Reset and clocks | A cover trace shows the design leaving reset and state changing in every clock domain |
| 2 | Covers | Every planned cover is reachable; trace lengths are plausible |
| 3 | Vacuity | Tool vacuity check clean; antecedent covers hit for key assertions |
| 4 | Assumptions | Each one has a spec reference and an owner who asserts it elsewhere; no assumptions on DUT outputs |
| 5 | Conflicts | No assumption conflicts / dead-ends reported |
| 6 | Configuration | Parameters and defines match the shipped instantiations, or reductions are justified in writing |
| 7 | Depth | Bounded results justified by covers or abstraction |
| 8 | Mutation | Deliberate bugs are caught |
| 9 | Files & settings | Compiled file list and revision logged; no assertions excluded by mistake; warnings reviewed |
| 10 | Review | A second engineer reviewed properties and assumptions against the spec |
Chapter takeaways
Was this page helpful?Thanks — noted!
Tip: select any text on the page before clicking Report and it will be quoted in your report.
