A formal owner reduces a proof effort to a short list of numbers that can be checked: how many properties are proved, how deep, what is reached, what the assumptions remove, and what the signoff rests on. This page defines each family, says how it is computed, names the trap, and points to the lesson that derives it. Every metric is read after the technique is taught. No value here is a target: acceptable limits are project decisions.
The ledger splits an inconclusive run into bounded (with justification) and inconclusive (no depth decision) so the depth can be read. The three run outcomes of the course are proven, counterexample and inconclusive; bounded is a finer status of the third.
Metric | Definition and computation | Trap | Taught in |
|---|---|---|---|
Proven count | Properties decided true for the stated model and assumptions by an unbounded proof. | Counting a run that only checked the base case. | |
Bounded count and depth reached | Properties with no counterexample up to N, each with its N and its justification. | Quoting N without the justification, or comparing N across different models. | |
Inconclusive count | Properties undecided after time, depth or strength ran out. | Counting them as passes, or ageing them silently into waivers. | |
Counterexample count | Properties with a concrete failing trace, each classified and owned. | Closing them by tightening an assumption instead of fixing the cause. |
Metric | Definition and computation | Trap | Taught in |
|---|---|---|---|
Covers reached | Cover directives with a witness trace, over all required covers. | A cover reached only in an over-constrained model. | |
Antecedent covers | One reached cover per implication trigger. Computed per property. | A proved property whose trigger never fires: a vacuous pass. | |
Activity covers | Covers of ordinary traffic: grants, stalls, skid use, contention. All must be reached. | A quiet model where everything proves because nothing happens. |
Metric | Definition and computation | Trap | Taught in |
|---|---|---|---|
Assumptions per property | Rows in the assumption register used by each proof. | A long list nobody reviews; every row needs an owner. | |
Assumptions without a discharging assertion | Assumptions with neither a discharging assertion nor a reviewed environment rule. Zero at signoff, or each carried by a waiver. | An assumption on a design output, which proves everything by assumption. | |
Assumption influence | Which assumptions each proof relied on, and the share of legal behaviour each removes. | An assumption nothing needs (delete it) or everything needs (review it twice). |
Metric | Definition and computation | Trap | Taught in |
|---|---|---|---|
Mutation score | Mutants killed by some property, over the master list of all mutants (state how many). Each survivor names missing behaviour. | Shrinking the mutant list inflates the score; the score is read against the registered master list, as the block shows. | |
Proof-core coverage | Union of proof cores over proven properties, against the blocks or flops of the design, stated. | High coverage at a shallow bound: pair it with the depth. | |
Cone coverage | Union of the cones of proven properties, against the blocks or flops of the design, stated. | Logic outside every cone is never checked by any property. | |
Ledger consistency | Every row has a known status, every bounded row a justification, every result a source hash. | A stale row after an RTL change. |
The block below summarises a small results ledger: per-status counts, the mutation score, and the problems a reviewer must see. Change a status, drop a mutant from the master list, or claim a score the master list does not support, and the check fails.
# A results ledger and a master list of mutants. A mutant counts as killed
# only if some property in the ledger names it; the denominator is the master list.
MASTER = {"m1", "m2", "m3", "m4", "m5", "m6", "m7", "m8"}
VALID = ("proven", "bounded", "counterexample", "inconclusive")
# (property, status, bound justified, mutants this property kills)
ledger = [
("a_range", "proven", True, {"m1", "m2", "m3"}),
("a_flags", "proven", True, {"m4", "m5"}),
("a_data", "bounded", True, {"m6", "m7"}),
("a_latency3", "inconclusive", False, set()),
]
def summarise(rows, master):
problems = []
counts = {s: 0 for s in VALID}
killed = set()
for name, status, justified, kills in rows:
if status not in VALID:
problems.append(name + ": unknown status " + status)
continue
counts[status] += 1
if status == "bounded" and not justified:
problems.append(name + ": bounded result without a justification")
if status == "inconclusive":
problems.append(name + ": inconclusive result is not evidence")
if not kills <= master:
problems.append(name + ": names a mutant that is not in the master list")
killed |= kills & master
for m in sorted(master - killed):
problems.append(m + ": surviving mutant")
score = len(killed) / len(master) if master else 0.0
return counts, score, problems
def check_claim(rows, master, claimed):
counts, score, problems = summarise(rows, master)
if abs(score - claimed) > 1e-9:
problems.append("claimed mutation score does not match the master list")
return counts, score, problems
counts, score, problems = summarise(ledger, MASTER)
assert counts == {"proven": 2, "bounded": 1, "counterexample": 0, "inconclusive": 1}
assert abs(score - 7 / 8) < 1e-9
assert problems == ["a_latency3: inconclusive result is not evidence", "m8: surviving mutant"]
# Hiding the survivor: quote the score over only the mutants some property kills.
# The same ledger against the master list still reports 7/8 and the survivor.
hidden_master = MASTER - {"m8"}
_, s2, p2 = summarise(ledger, hidden_master)
assert s2 == 1.0 and "m8: surviving mutant" not in p2
# Failing check: a reviewer compares against the registered master list, not the quoted one.
_, _, bad = check_claim(ledger, MASTER, s2)
assert any("does not match" in p for p in bad) and "m8: surviving mutant" in bad
print("PASS: score and survivors come from the master mutant list, so a hidden mutant is caught")Read the scope first: which properties, which model revision, which date.
Read the outcome split before the headline: proven, bounded with depths, inconclusive, counterexamples.
Read the covers: every antecedent reached, every activity reached, or the gap named.
Read the assumption register: every row discharged or waived, none on a design output.
Only then react to the mutation score and the coverage numbers.
What depth each bounded result carries with its justification, and whether every antecedent cover is reached: full cones with shallow bounds and quiet triggers prove nothing.