Proving one property on a small block is a skill; shipping a verified block is a method. This section is the method: which requirements get a formal obligation, in which order a harness comes up, what to do when a proof slows down, how to read each of the three failing traces, and how formal lives in regression beside simulation. Every lesson works on the same running designs as the rest of the course, and every verdict uses the same three words: proven, counterexample, or inconclusive.
Topic | Lessons | After it you can... |
|---|---|---|
3 | Choose formal-shaped requirements, bring a harness up stage by stage, and write a plan with evidence per row. | |
3 | Diagnose a slow proof from measurements, split work and parameters, and set budgets that never hide a timeout. | |
4 | Triage any failing trace to bug, missing assumption, or abstraction artefact, and tell counterexamples, induction counterexamples, and lassos apart. | |
3 | Run per-commit and nightly formal sets, triage new failures from a ledger, and map the course flow onto any formal tool. |
Suggested order: topics top to bottom. The testplan decides what to prove, complexity management keeps the proofs moving, debugging reads what fails, and regression keeps the answers true as the RTL changes. Readers preparing for interviews can take the first lesson of the first and third topics plus the regression lessons as a short path.
The same checks as for any result: trigger covers reached, the cone holds the intended logic, the property fails under mutation, and every assumption is listed and reviewed.