This section says what a formal run is and what it promises, and it is the start of the course. It assumes the reader has met formal once in one of the on-ramp lessons and starts where they stop: with results that must be defended. The running designs are a 4-entry FIFO, a decade counter, a skid stage, a register block, a pipelined pair, and an arbiter, and every number about them comes from counted runs, never from habit.
Topic | Lessons | After it you can... |
|---|---|---|
4 | Read any result as proven, counterexample, or inconclusive, and split work with simulation. | |
4 | Model a block as states and rules, write invariants, and place each directive correctly. | |
3 | Harness the first cycles so reset and history never lie. | |
4 | Compute cones, trust their exactness, read their sizes, and price them. | |
4 | Build harnesses, run tasks, read reports, and name model fidelity limits. |
Suggested order: topics top to bottom, lessons top to bottom inside each topic. The first topic fixes the vocabulary, the second the model, the third the start of time, the fourth the cost, and the fifth the machinery. Later sections assume all of it, especially the three outcomes and the assumption discipline.
The model, the assumption list, and the depth or proof form: a verdict without them cannot be trusted or reproduced. A bounded pass is a sound result with a stated bound, but it is not a proof.