Proofs do not start where simulation starts. Unless told otherwise, every register begins in an arbitrary state, history from before cycle 0 does not exist, and reset is just another input. This topic builds the harness that tames the first cycles: one reset sequence at the start, a history gate for properties that look back, and reset-aware checks that catch wrong reset values instead of disabling through them.
Lesson | After it you can... |
|---|---|
Write a harness with one reset sequence and read failures that start in impossible states. | |
Gate history reads so the first cycle and mid-run resets never lie. | |
Use disable iff without masking reset-time bugs, and state the async modelling caveat. |
Suggested order: top to bottom. The first lesson fixes the start of time, the second fixes the first history read, and the third fixes the reset-active window.
A free start includes states reset can never produce, so a good design fails on impossible traces; constraining step 0 to reset models power-up honestly.