Reset determinism says the zeros and ones are determined; it says nothing about unknowns driven onto the bus by unreset memory, undriven nets, or clock-domain crossings sampled mid-flight. Those need an analysis that models X explicitly, with its two failure modes: pessimism that reports X where silicon resolves, and optimism that resolves X where silicon keeps it. Scoping that analysis honestly is this lesson's job.
A three-valued evaluator carries 0, 1 and X through the logic. AND with a 0 is exact: a controlling zero decides the output whatever the other input is. Pessimism is the evaluator reporting X where the silicon has a definite value: an XOR of a signal with itself is X in the evaluator and 0 in silicon, and a multiplexer with an unknown select whose data inputs agree is X in a naive evaluator and the agreed value in silicon. Optimism is the opposite, a definite answer where silicon may differ: an if on an unknown condition takes the else branch in RTL simulation, so an unknown reset can look like no reset at all. The analysis classifies each X source: undriven nets, unreset sequential elements read before written, and domain crossings, and each class has an owner and a fix. What remains, arrival-order and analogue effects, belongs in simulation with X modelling and on the bench.
The evaluator below implements the exact AND, a pessimistic XOR and multiplexer, and the RTL meaning of if. Each claim is an assert against the enumerated silicon behaviour: all values an unknown could take. The reset network at the end shows why optimism is the dangerous one, and an injected AND bug that propagates X through a controlling zero is caught:
X = "X"
def band(a, b): # exact: a controlling 0 decides
if a == 0 or b == 0:
return 0
return X if X in (a, b) else 1
def bxor(a, b): # pessimistic: ignores that both inputs may be the same net
return X if X in (a, b) else a ^ b
def mux_naive(sel, d0, d1): # pessimistic: an unknown select is always unknown
return X if sel == X else (d1 if sel else d0)
def mux3(sel, d0, d1): # exact three-valued mux: equal data resolve
if sel == X:
return d0 if d0 == d1 and d0 != X else X
return d1 if sel else d0
def if_rtl(cond, a, b): # RTL if: an unknown condition takes the else branch (optimism)
return a if cond == 1 else b
assert band(0, X) == 0 and band(1, X) == X
# pessimism: the evaluator says X, silicon has a definite value
assert bxor(X, X) == X and {a ^ a for a in (0, 1)} == {0}
assert mux_naive(X, 1, 1) == X and {mux_naive(s, 1, 1) for s in (0, 1)} == {1}
assert mux3(X, 1, 1) == 1 and mux3(X, 0, 1) == X
# optimism: RTL gives a definite answer, silicon may give either
assert if_rtl(X, 1, 0) == 0 and {if_rtl(c, 1, 0) for c in (0, 1)} == {0, 1}
# a reset network q = rst ? 0 : d with rst unknown and d = 1
assert if_rtl(X, 0, 1) == 1 and {if_rtl(r, 0, 1) for r in (0, 1)} == {0, 1}
assert mux3(X, 1, 0) == X # the three-valued evaluator flags it; the RTL if hides it
def band_bug(a, b):
return X if X in (a, b) else a and b
assert band_bug(0, X) == X != band(0, X)
print("PASS: AND is exact; XOR and naive mux are pessimistic; an unknown if is optimistic and hides an unknown reset")The properties below are concept, not runnable in the open flow: they need the dedicated analysis, and the headers say so. The runnable substitutes beside them are the two-copy determinism checks from the previous lesson, each with one sentence on which cycle it checks:
// not-run: needs a dedicated X-aware analysis, not a two-state proof
// assert_no_x_on_bus: every bus output is 0 or 1 one cycle after reset
// runnable substitute: the two-copy determinism check on valid and ready
// (judges the cycle after the reset cycle; says nothing about X itself)// not-run: needs X modelling of undriven nets and unreset memory
// undriven_net_check: every net has exactly one non-tristate driver
// runnable substitute: lint plus the two-copy determinism check
// (structural; run before any proof, and rerun on every netlist change)The X scope names which classes are analysed, with what tooling, and which are explicitly out of scope.
Every X source has an owner and a fix: reset clause, tie-off, synchroniser, or documented waiver.
Determinism proofs are not presented as X evidence: the two claims stay in separate columns.
Optimism is treated as the riskier of the two: an unknown reset that RTL simulation resolves quietly needs the three-valued view.
An X finding first asks its class: undriven net, unreset read-before-write, or crossing. The first two are fixed in RTL; the third is checked against the synchroniser protocol with the crossing abstracted, which is the CDC flow's job. A pessimistic report is disputed with silicon behaviour, never by weakening the analysis.
Probably not: a real multiplexer passes the agreed value regardless of the select, so this is the known pessimism of a naive analysis. Record it as pessimism with the justification, and keep the analysis strict everywhere else.