Passing properties are not coverage. A suite can prove every line it looks at while looking at half the design, leaning on every assumption, and checking nothing that can fail. This topic builds the four views that keep a sign-off honest: the cone each property could depend on, the proof core it actually used, the assumptions it relied on, and the mutants it kills. Each view has a precise definition before first use, and each number comes with the companion metric that stops it being misread.
Lesson | After it you can... |
|---|---|
Separate what a property could depend on from what its proof used, and spot uncovered logic. | |
Tabulate which proofs lean on which assumptions and how much behaviour each excludes. | |
Run a fault-injection gate over the property set and close the gaps it finds. | |
Pair every coverage number with its bound and assumption context before signing. |
Suggested order: top to bottom. Cone and core first, because they define the vocabulary; assumption influence next, because it qualifies every number the first lesson produces; mutation next, because it is the strongest evidence; the sceptical last lesson, because it is read at sign-off time.
Everything that makes the number meaningful: the depth each proof reached, which assumptions were active, and whether any injected fault survives. Coverage without those companions is decoration.