Every proof in this course works on the same mathematical object: a set of states, a set of inputs, and a rule that maps a state plus inputs to the next state. The design, the properties, and the three directives all make sense once that object is visible. This topic builds it for the decade counter and the FIFO, defines safety as an invariant over reachable states, and fixes the three roles assume, assert, and cover play in every later proof.
Lesson | After it you can... |
|---|---|
Describe any design as a transition system and enumerate its reachable states. | |
Write a safety property as an invariant and read its counterexample as a finite path. | |
Place each directive on the right side of the interface and predict what misplacement does. | |
Compute state counts and input-space fractions, and explain why enumeration is impractical. |
Suggested order: top to bottom. The first lesson builds the model, the second states properties over it, the third drives the engine with the three directives, and the fourth counts what cannot be counted by visiting.
The induction step starts from arbitrary states, so it can begin in the unreachable region and step into the bad state even when no real run can get there.