The proof passes and the silicon shows X on an output. Both are telling the truth about different models: the formal tool reasons over zeros and ones with unreset registers free to be either, while the silicon and the X-aware simulator propagate unknowns. This topic teaches the boundary precisely: what two-state formal can show, which is reset determinism, what it cannot show, which is X propagation, and what to run instead for the X question.
Lesson | After it you can... |
|---|---|
Say exactly what a two-state proof claims about X, and what it does not. | |
Prove the state after reset is independent of free initial values, on running designs. | |
Scope a dedicated X analysis, its pessimism and optimism, and its simulation complement. |
Suggested order: top to bottom. The boundary first, because everything else assumes it; the determinism proof, which is the runnable substitute; the X-aware analysis, which says what the substitute does not cover. For the simulation-side discipline that complements these proofs, see the X-propagation discipline lesson.
No: different models. The proof says the reset state is determined over zeros and ones; the run says an unknown propagates in four-state modelling. Trust both, then run the X analysis the last lesson scopes.