Why it matters

A proof that leans on twelve assumptions is a different asset from one that leans on two, and a report that lists neither is asking for trust without evidence. Worse, each assumption deletes part of the input space, and the deleted classes are exactly where the next bug hides. This lesson makes both visible: which proofs used which assumptions, and what share of legal behaviour each assumption excludes.

The core idea

Assumption influence is the mapping from each assumption to the properties whose proofs relied on it. A proof relies on an assumption when removing it changes the result: the proof fails, goes inconclusive, or needs a deeper bound. From the mapping come the two review rules. An assumption nothing needs is deleted: it constrains the environment for no benefit and can only hide behaviour. An assumption everything needs is reviewed twice: it is load-bearing for the whole suite, so its justification must be the strongest document in the package.

Worked example: how much each assumption deletes

The arithmetic below is exact for an illustrative input space: a 4-bit opcode where only values below 12 except 5 are exercised, plus a word-aligned address rule on a 32-bit bus. Eleven of sixteen opcodes remain, one address in four remains, and the combined space is eleven sixty-fourths, about 17.2 per cent. About 83 per cent of the input space (53 of 64) is excluded, so a bug triggered only by opcode 5 or an unaligned address is invisible to every proof under these assumptions, and the report must say where those classes are verified instead. The script then computes the two review rules from an influence table instead of restating them, and shows each rule firing on an injected bad table.

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

# exact input-space shares from the illustrative assumption set
opcodes_total, opcodes_kept = 16, 11  # op < 12 and op != 5
addr_total, addr_kept = 4, 1           # addr[1:0] == 0 keeps one in four
op_share = opcodes_kept / opcodes_total
addr_share = addr_kept / addr_total
combined = op_share * addr_share
assert abs(op_share - 0.6875) < 1e-12
assert abs(addr_share - 0.25) < 1e-12
assert abs(combined - 11 / 64) < 1e-12
assert abs((1 - combined) - 53 / 64) < 1e-12

# influence[a] = properties whose result changed when assumption a was removed
all_props = ["p_alu", "p_mem", "p_csr"]

def review(influence):
    unused = sorted(a for a, ps in influence.items() if not ps)
    load_bearing = sorted(a for a, ps in influence.items() if len(ps) == len(all_props))
    return unused, load_bearing

influence = {"a_aligned": ["p_alu", "p_mem", "p_csr"], "a_op_legal": ["p_alu"],
             "a_burst_len": []}
assert review(influence) == (["a_burst_len"], ["a_aligned"])
# a clean table: every assumption is used, none is used by everything
clean = {"a_op_legal": ["p_alu"], "a_aligned": ["p_mem", "p_csr"]}
assert review(clean) == ([], [])
# injected fault: a_op_legal stops being needed, and a_aligned becomes load-bearing
bad = {"a_op_legal": [], "a_aligned": ["p_alu", "p_mem", "p_csr"]}
assert review(bad) == (["a_op_legal"], ["a_aligned"])
print("PASS: kept 11/64 = 17.2 pct, excluded 53/64; unused assumption found, load-bearing one flagged")

Read the table as a contract with the rest of verification: every excluded class names the method that covers it, or it is an uncovered hole. An assumption that hides a real bug, such as forbidding writes to a full FIFO instead of asserting the design tolerates them, is caught here because the excluded class contains the failing input and no other method claims it.

What the reviewer looks for

• The influence table lists every assumption against the properties that relied on it, verified by removing each assumption once.

• Each assumption states the excluded input class and where that class is verified instead.

• Assumptions used by nothing are gone; assumptions used by everything carry the strongest justification.

Verify and debug

Recompute influence by subtraction: remove one assumption, rerun the suite, and record what changes. If nothing changes, the assumption is dead weight. If a proof that should be independent suddenly needs it, the property is weaker than believed. Pay special attention to assumptions on outputs or internal signals: they prune the design rather than the environment and almost always hide behaviour.

Related topics

• Next: Mutation-Based Formal Coverage

• Formal: Assumptions and Constraints