Course map
- 1 lesson
Starts with How to Use This Course
- 1 lesson
Starts with Reading Paths
- 1 lesson
Starts with Glossary
- 1 lesson
Starts with Metrics Reference
- 1 lesson
Starts with Formal Cheat Sheet
- 19 lessons
Starts with Three Outcomes of a Formal Run
- 16 lessons
Starts with What a Proof Engine Does with SVA
- 19 lessons
Starts with Spec Sentence to Property
- 23 lessons
Starts with Transition Systems and Reachability
- 20 lessons
Starts with Table-Driven Connectivity Proof
- 14 lessons
Starts with Miter Construction
- 15 lessons
Starts with Antecedent Covers and Witness Traces
- 13 lessons
Starts with What Goes to Formal
- 15 lessons
Starts with Scoring Rubric and Structure
- 24 lessons
Starts with The Brief and Deliverables
About this course
Choose a learning path
This course teaches formal verification as it is practised on real blocks: writing properties that can fail, modelling a block together with its assumptions, running the proof, and reading the result honestly. Every lesson works on one of six small running designs, so the FIFO whose overflow you prove in the first section is the FIFO whose induction needs a helper in the fourth and whose signoff package you assemble in the seventh. A run has exactly three outcomes, and the course uses no other words for them: proven, counterexample, inconclusive.
Who it is for
Design engineers with three to fifteen years of experience who write properties for their own blocks and want those properties to mean something.
Verification engineers adding formal to a simulation plan: choosing what goes to formal, writing the harness, and reading the results.
Formal specialists and equivalence-check owners who prove properties, tame complexity, and defend a signoff.
Anyone preparing for a senior interview who must answer whiteboard questions on assumptions, induction, liveness, abstraction and signoff with evidence.
The three outcomes of a run
This table is the vocabulary of the whole course. Every lesson uses these words and no synonyms.
Outcome | Meaning | What it demands next |
|---|---|---|
Proven | The property holds for the stated model under the stated assumptions. | Record the assumptions beside the result. The proof belongs to that model and that revision only. |
Counterexample | A concrete trace that breaks the property: inputs, states and the earliest failing cycle. | Classify it as a design bug, a missing assumption, an abstraction artefact or an unreachable start, then repair the model or the design. |
Inconclusive | The run did not decide: time ran out, the induction step failed from an unreachable start, or the bound was reached with no counterexample. | Diagnose first, then reduce, split or strengthen. Report it as inconclusive, never as a pass. |
A bounded pass is written "bounded to N": no counterexample within N cycles. It is a sound, stated result and it is reported under inconclusive until the depth is justified or an inductive proof decides it.
Three paths through the course
Property writer on a block. Read How to Use This Course, then Formal Foundations for what a result means and what it assumes, then Properties and SVA for the proof engine's view of assertions, then Property Development and Constraints for writing properties and owning assumptions. Dip into Formal Applications for the property set of your kind of block: FIFO and handshake, registers, arbiter, pipeline. Finish with the capstone stage that matches your block.
Formal owner and signoff lead. Take the property-writer path, then Proof Engines and Convergence for induction, helpers and convergence tactics, Formal Coverage and Signoff for covers, vacuity, mutation and the signoff package, and Methodology and Debug for testplans, triage and regression. Read Equivalence Checking if you own a miter or an ECO. The capstone asks you to sign off all six designs.
Interview in two weeks. Read How to Use This Course for the study routine, skim the core lessons in the Reading Paths two-week plan, then work Interview Prep: the whiteboard framework, the four scenarios, the rapid-fire rounds and the numeric drills. Attempt every drill on paper before you read its answer.
What you can do after the course
Say precisely what a formal result means, and never over-claim it.
Model a block for a formal run: harness, reset, initial state, free inputs, assumptions as a contract, covers.
Write properties that can fail, and prove they can, by mutation and by antecedent covers.
Choose and read the engines: bounded checks, k-induction, and liveness through fairness and lassos, with the runnable bounded-response substitutes.
Read a counterexample and a counterexample to induction, classify it, and repair the model or the invariant.
Strengthen an induction with helper invariants, and discover them from a failing step.
Tame complexity with cones, data independence, abstraction, cut points, case splits and assume-guarantee reasoning.
Run the formal applications end to end: connectivity tables, register proofs, deadlock and starvation checks, reset determinism, handshake and data-integrity sets.
Build and read equivalence checks, and say what they do not prove.
Produce and defend a formal signoff: bounds, vacuity evidence, coverage, mutation score, assumption register, waivers, ledger.
Plan, schedule and regress formal in a project, and answer whiteboard questions with assumption, mechanism, trade-off and evidence.
Section map
Section | One line |
|---|---|
What a formal run is, what it promises, and the model it proves. | |
What a proof engine does with assertions, and the Boolean forms that run here. | |
Writing properties, owning assumptions, abstraction, and assume-guarantee proofs. | |
How the engines work, k-induction, liveness engines, and convergence tactics. | |
Connectivity, registers, deadlock and starvation, X and reset determinism, datapath sets. | |
Miters, sequential equivalence with retiming, RTL-to-gate assumptions, ECO checks. | |
Covers and vacuity, coverage metrics, bounded-proof justification, the signoff package. | |
Testplans, complexity management, counterexample triage, formal in regression. | |
The whiteboard framework, four scenarios, rapid-fire rounds, numeric drills, spot-the-bug. | |
Prove all six designs, find their planted bugs, and sign the ledger. |
The six running designs
Six small designs carry every lesson. Each is fixed: the same ports, reset and behaviour everywhere it appears, so a number you meet in one section still holds in the next.
Design | What it is | Where it appears most |
|---|---|---|
| 4-entry, 8-bit synchronous FIFO with full and empty flags. | Safety, induction with a helper, depth choice, the worked signoff. |
| 4-requester round-robin arbiter with a one-hot grant. | Bounded wait, fairness, starvation, ECO equivalence. |
| Valid and ready skid-register stage with backpressure. | Assumptions as a contract, harnesses, handshake property sets. |
| Four registers: read-write, write-1-to-clear, read-only, reset values. | Register proofs, access timing, hardware-set against software-clear races. |
| 3-stage arithmetic pipeline with a retimed twin. | Latency properties, cut points, sequential equivalence. |
| Decade counter, counts 0 to 9 with an enable. | The induction story: base case, step, unreachable states, helpers. |
The shape of the work
Show how the course is organised
Every lesson follows this loop. A requirement becomes a property; the property runs on a model together with its assumptions; the run reports one of the three outcomes; the outcome is kept as evidence with the assumptions beside it. When the evidence is thin, the loop turns again: a stronger property, a fairer model, a deeper run.
How to study
Read How to Use This Course, then the Reading Paths for your role.
Keep the Glossary open while you read: the glossary defines each term and links it to the lesson that teaches it.
Read each proof block with its header, then its bug variant, and read every counterexample cycle by cycle. To reproduce a block yourself, follow the appendix Appendix: Run It Yourself on an Open-Source Flow.
Answer every check-yourself before revealing its answer.
Keep the Metrics Reference and the Formal Cheat Sheet beside you.
Finish with the capstone: it spends the numbers and the properties of every earlier section.
Time and prerequisites
Allow about 31 hours to read, about 80 with the proofs and exercises. These are planning estimates computed from the length of the pages and the number of proof and Python blocks, not measurements of learners: see the Reading Paths for how they are built. If assertions, FIFOs and handshakes are new to you, start with the companions named in How to Use This Course before the property sections. Every number about a running design is quoted from the designs as built; invented numbers are labelled illustrative, and no value is typical of any product or process.
Check yourself A run reports no counterexample up to depth 12. What do you say, and what do you refuse to say?
You say the result is bounded to 12: sound and stated, but not a proof. You refuse to say proven until the depth is justified or an inductive proof decides it.