Why it matters

The nightly ledger turns red on three properties the morning after an RTL change. One is a genuine bug the change introduced. One is an assumption the change silently invalidated. One ran on a machine whose memory limit changed overnight. Reverting the RTL fixes the first, breaks nothing for the second, and misses the third entirely. Triage tells the three apart before anyone acts.

Job of this lesson: classify ledger changes and read the inconclusive trend.

The core idea

A new counterexample after an RTL change is a real bug until the triage order says otherwise: replay the old trace, check the assumptions against the new RTL, check the setup and the revision hashes. Assumption drift shows as a failure under an environment rule the change altered. It is accepted as drift only when the neighbour block's updated guarantee is recorded; a rule changed in the same commit as the RTL, with no such guarantee, is an unreviewed change and is treated as a bug, because that is how a bug hides as drift. A setup change shows as identical RTL and rules with different outcomes; the fix is the environment, not the design. A newly inconclusive property is a slow proof wearing a new revision's clothes: triage it as one. The trend of inconclusive counts over releases is the project's early warning:

Worked example: the ledger diff

The script below diffs two nightly runs and classifies each change. The injected regression is a_hold: its RTL changed and its interface rule changed in the same commit, and it fails. A naive classifier calls that drift and moves on; this one calls it an unreviewed assumption change, and the test pins that down, along with the same row once the neighbour's guarantee is recorded. The setup-change row has identical RTL and rule, so only the environment differs. The trend function flags a rise over three consecutive releases:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42

def classify(o, n):
    if n["status"] == "counterexample":
        if n["rtl"] == o["rtl"] and n["rule"] == o["rule"] and n["setup"] != o["setup"]:
            return "setup-change"
        if n["rule"] != o["rule"]:
            if n.get("rule_discharged"):
                return "assumption-drift"
            return "unreviewed-assumption-change (treat as bug)"
        if n["rtl"] != o["rtl"]:
            return "candidate-bug"
        return "unexplained: rerun"
    if n["status"] == "inconclusive" and o["status"] == "proven":
        return "newly-inconclusive"
    return "unchanged"

def entry(name, status, rtl, rule, setup, **extra):
    return dict({"name": name, "status": status, "rtl": rtl, "rule": rule, "setup": setup}, **extra)

old = {n: entry(n, "proven", "r100", "v1", "s1") for n in ("a_conserve", "a_hold", "a_ready", "a_data", "a_flags", "a_reset")}
new = [
    entry("a_conserve", "counterexample", "r101", "v1", "s1"),
    entry("a_hold", "counterexample", "r101", "v2", "s1"),
    entry("a_ready", "counterexample", "r101", "v2", "s1", rule_discharged=True),
    entry("a_data", "inconclusive", "r101", "v1", "s1"),
    entry("a_flags", "counterexample", "r100", "v1", "s2"),
    entry("a_reset", "proven", "r101", "v1", "s1"),
]
result = {n["name"]: classify(old[n["name"]], n) for n in new}
assert result["a_conserve"] == "candidate-bug"
assert result["a_hold"].startswith("unreviewed-assumption-change")      # the bug hiding as drift
assert result["a_ready"] == "assumption-drift"                          # same change, guarantee recorded
assert result["a_data"] == "newly-inconclusive"
assert result["a_flags"] == "setup-change"
assert result["a_reset"] == "unchanged"

def rising(trend, releases=3):
    last = trend[-releases:]
    return len(last) == releases and all(a < b for a, b in zip(last, last[1:]))

assert rising([0, 0, 1, 1, 2, 3])
assert not rising([3, 2, 1, 1, 0, 0]) and not rising([0, 1, 1, 2])
print("PASS: bug, hidden bug, drift, setup change and new inconclusiveness each classified; trend flagged")

What the review looks for

• Every ledger change names its class and the test that decided it.

• Assumption updates are reviewed with the neighbour's guarantee, never silent; setup changes rerun before any RTL action.

• The inconclusive trend is plotted per release and has an owner when it rises.

Verify and debug

When a change classifies as drift, demand the neighbour's updated guarantee before accepting the new assumption; drift accepted on one side without the other side's proof is over-constraint waiting to happen. When the same commit changes RTL and rule, split the commit and rerun with the old rule first. When the trend rises for two releases running, schedule complexity work, not more machines: the proofs are losing to the design's growth.

Related topics

• Earlier: CI for Formal

• Next: From the Open Flow to Any Formal Tool

• Hardware Debug: Equivalence Failures