Two engineers read the same conservation failure on the skid stage. One spent a week in the RTL before noticing the trace began with the counters at arbitrary values, a harness gap. The other spent ten minutes: unreachable start, so fix the harness, rerun, and only then ask whether the design is guilty. Triage is that ten minutes, done the same way every time.
Job of this lesson: classify any failure into one of four classes and prescribe the fix plus its regression.
Four classes, checked in order. An illegal initial state means the harness is wrong: the trace is discarded, not debugged. A trace the assumptions should have excluded means the environment model is wrong: add the documented rule, and check the neighbour owes it. A trace that does not replay on the unabstracted design means the abstraction is wrong: constrain the cut or the black box with a proven contract. A trace that survives all three is a design bug: fix the RTL, keep the failing property, and add a cover that pins the scenario. Each class leaves a regression behind, an assert plus a cover, so it cannot silently return:
Class | Test that names it | Fix | Regression left behind |
|---|---|---|---|
Illegal start | First cycle unreachable from reset | Fix reset and initial state | Reset cover, no step-0 failure |
Missing assumption | A spec rule the environment owes would have excluded it | Add the documented rule, exactly as written | Neighbour assert discharging it, plus a cover that legal traffic survives |
Abstraction artefact | No replay on the real design | Constrain with a proven contract | Contract asserted on the real block |
Design bug | Survives all three tests | Fix the RTL | Failing property plus scenario cover |
The script below encodes the skid stage's environment rules as data and tests a trace against them. The rule is the valid/ready rule: a source whose valid was high while ready was low must keep valid high in the next cycle. It is not the rule that valid is held while the output is stalled, because while the output is stalled the skid register may be empty, ready is high, the word is accepted, and the source may then legally stop. The test uses that legal trace to show the difference: the right rule passes it, the over-strong rule flags it, and so would over-constrain the proof. A trace with a real drop is flagged by the right rule with its name, and a checker that inspects only the first cycle misses it:
def valid_held(t):
# valid/ready rule: valid and not ready in one cycle means valid again in the next
return all(not (a["in_valid"] and not a["in_ready"]) or b["in_valid"] for a, b in zip(t, t[1:]))
def valid_held_while_output_stalled(t):
# too strong: it also forbids a legal stop after a word was accepted during a stall
return all(not (a["out_stalled"] and a["in_valid"]) or b["in_valid"] for a, b in zip(t, t[1:]))
rules = [
("reset-first", lambda t: t[0]["rst"] == 1),
("valid-held", valid_held),
]
def broken_rules(trace, rule_list=rules):
return [name for name, holds in rule_list if not holds(trace)]
def cycle(rst, v, r, s):
return {"rst": rst, "in_valid": v, "in_ready": r, "out_stalled": s}
legal = [cycle(1, 0, 1, 0), cycle(0, 1, 1, 0), cycle(0, 1, 1, 1), cycle(0, 0, 0, 1)] # word accepted, then valid stops
assert broken_rules(legal) == []
assert broken_rules(legal, [("too-strong", valid_held_while_output_stalled)]) == ["too-strong"]
drop = [cycle(1, 0, 1, 0), cycle(0, 1, 1, 0), cycle(0, 1, 0, 0), cycle(0, 0, 0, 0)] # offer waiting, then valid stops
assert broken_rules(drop) == ["valid-held"]
def blind_checker(trace):
return [] if trace[0]["rst"] == 1 else ["reset-first"]
assert blind_checker(drop) == [] and blind_checker(drop) != broken_rules(drop)
print("PASS: the legal stop is accepted, the real drop is named, the first-cycle checker is blind to it")Every triaged failure names its class and the test that decided it.
Missing assumptions map to a neighbour guarantee and are written as the documented rule, not as a tighter local constraint.
Each fix carries a regression: the property plus a cover pinning the scenario, and for an assumption a cover showing legal traffic is still reachable.
Replay the trace on the unabstracted design before changing anything: if it does not replay, the abstraction is the suspect, not the RTL. Record the classification in the ledger next to the outcome; a failure with no class is a failure that will be triaged twice. Adding an assumption is the one repair that can hide a bug, so every added rule is listed with its owner: the assumptions lesson covers the register.
Missing assumption: add the documented rule, check the neighbour owes it, and prove the property again under the corrected environment.
Everything downstream: the replaying one is a candidate design bug; the other is an abstraction artefact until its cut or black box carries a proven contract.