A dashboard showed forty passing lines and the block was signed off; three of the forty were time-outs the summary had counted as passes, and one of them covered the overflow rule. The report had said exactly what happened, but nobody read past the colour. This lesson teaches what a formal run looks like on paper, so the counting is honest before any metric is built on it.
Job of this lesson: show what a run reports per property and per cover, and give a parser that classifies a generic report and refuses mislabelled lines.
A run reports, per property: the verdict (proven for the stated model and assumptions, counterexample at a stated step, or inconclusive with the reason), the proof form or depth behind it, the cone size, and the assumptions in force; and, for a proof, the proof core, the part of the model the proof used (a later lesson). Covers report reached with a witness step, or not reached within the bound, which is inconclusive unless an engine proved unreachability. The report below is an illustrative generic format; the values are measured on the running FIFO and the decade counter, so the lesson is the fields, not the format.
# not-run: illustrative generic report format, not executable here
# run 1: sync_fifo, helper invariant removed
# property a_range : PROVEN (induction, k=1) cone=3 flops
# property a_push_inc : PROVEN (induction, k=2)
# property a_data : INCONCLUSIVE (base case passed to depth 12, induction step failed at k=12)
# cover c_full : REACHED at step 5
# assumptions: reset at step 0 (1), tracked slot held constant (1)
# proof core: listed per proven property (a later lesson)
# run 2: sync_fifo with the overflow bug
# property a_range : COUNTEREXAMPLE at step 6
# property a_ovf_ign : COUNTEREXAMPLE at step 7
# run 3: mod10_counter
# cover c_ten : NOT REACHED within 20 (inconclusive)Property | Kind | Earliest failing step | Why that step |
|---|---|---|---|
a_range | Current state (combinational) | 6 | Reports the step where the bad state exists: the count reads 5. |
a_ovf_ign | Looks back with $past (clocked) | 7 | Judged at its closing edge, so one step later. |
The parser sorts each line into proven, counterexample, inconclusive or cover-reached, and raises an error on a line that claims a proof while saying it was bounded, unknown or timed out, or that claims a proof with no proof form. Bounded passes, unproven results with a failed induction step, and unreached covers all count as inconclusive. The self-test holds realistic lines, including five realistic lines that naive parsers misfile; the check is applied to the parser and to a naive one, which it catches.
import re
INCONCLUSIVE_WORDS = ("BOUNDED", "UNKNOWN", "TIMEOUT", "TIME-OUT", "UNPROVEN", "INCONCLUSIVE", "STEP FAILED", "NOT REACHED", "UNREACHED")
class Mislabelled(ValueError):
pass
def classify(line):
up = line.upper()
weak = any(word in up for word in INCONCLUSIVE_WORDS)
claims_proof = bool(re.search(r"\bPROVEN\b", up))
if claims_proof and (weak or "INDUCTION" not in up):
raise Mislabelled(line)
if weak:
return "inconclusive"
if "CEX" in up or "COUNTEREXAMPLE" in up:
return "counterexample"
if "REACHED" in up:
return "cover-reached"
if claims_proof:
return "proven"
raise Mislabelled(line)
def naive(line):
up = line.upper()
if "CEX" in up or "FAIL" in up:
return "counterexample"
if "REACHED" in up and "NOT" not in up:
return "cover-reached"
if "PROVEN" in up or "PASS" in up:
return "inconclusive" if ("TIMEOUT" in up or "UNKNOWN" in up) else "proven"
return "inconclusive"
CASES = [
("property a_range : PROVEN (induction, k=1)", "proven"),
("property a_ovf_ign : COUNTEREXAMPLE at step 7", "counterexample"),
("property a_data : INCONCLUSIVE (base case passed to depth 12, induction step failed at k=12)", "inconclusive"),
("property a_x : PASS (bounded to 12)", "inconclusive"),
("property a_y : UNPROVEN (base case passed, induction step FAILED)", "inconclusive"),
("cover c_full : REACHED at step 5", "cover-reached"),
("cover c_ten : NOT REACHED within 20", "inconclusive"),
("cover c_q : UNREACHED within 12", "inconclusive"),
]
REFUSED = ["property a_z : PROVEN (bounded to 12)", "property a_t : PROVEN (timeout after 60s)", "property a_u : PROVEN"]
def check(fn):
for line, want in CASES:
assert fn(line) == want, line
for line in REFUSED:
try:
fn(line)
except Mislabelled:
continue
raise AssertionError("accepted: " + line)
check(classify)
counts = {}
for line, _ in CASES:
kind = classify(line)
counts[kind] = counts.get(kind, 0) + 1
assert counts == {"proven": 1, "counterexample": 1, "inconclusive": 5, "cover-reached": 1}
caught = False
try:
check(naive)
except AssertionError:
caught = True
assert caught
print("PASS: report classified 1 proven, 1 counterexample, 5 inconclusive, 1 cover reached; mislabelled lines are refused and the naive parser is caught")Report says | Count as | Demands next |
|---|---|---|
Proven with model, assumptions and proof form | Proven | Keep the assumption list; rerun on RTL change. |
Counterexample at step K | Counterexample | Triage the trace; fix design or model. |
Bounded pass to N | Inconclusive (bounded to N) | A sound result, not a proof: justify the bound or strengthen. |
Time-out, unknown, induction step failed | Inconclusive | Diagnose; never file as a pass. |
Cover reached at step K | Witness | File as exercised. |
Cover not reached within N | Inconclusive | Prove unreachable or extend the bound. |
Three separate counts, proven, counterexample, inconclusive, with the depth beside every bounded line; covers counted as reached or inconclusive, never as proven.
Every proven property names its model, assumptions and proof form, and a counterexample table gives the earliest failing step per property.
Run the parser over every report before signoff and confirm the counts add up to the property list. Inject a mislabelled line periodically to confirm the check still refuses it. When a count moves between runs, diff the assumption list first: results move when models move.
At most 37 proven, 3 inconclusive and 0 counterexamples: the time-outs are not passes, and the signoff waits for them.
Only that no witness appeared within 12 steps: inconclusive. Unreachable needs an engine proof or a separate argument, not a missed bound.