The course has 243 pages in ten sections, which is more than anyone needs for one goal. This page gives three routes. Each is an ordered table of the essential lessons with the reason to read it and an approximate time, so you can plan a week instead of guessing. Every route assumes you have read How to Use This Course. Essential means the lessons that carry the core path: read those in section order, and treat the rest as depth you add when a lesson leaves a question.
A lesson read once takes about 10 minutes. Lessons with a longer proof or a program to run are listed at 12 or 15. Working every proof, reading every counterexample and answering every check-yourself takes roughly two and a half times as long as reading. The course totals quoted on the hub come from the page text itself: about 971,000 characters of prose and tables read at about 1,000 characters a minute, and about 2,161,000 characters of code read at about 2,500 a minute, give about 31 hours to read. Adding 3 minutes for each of the 691 proof blocks (re-read its bug variant), 3 minutes for each of the 132 Python blocks, and 2 minutes for the check-yourself and exercise of each of the 243 pages gives about 80 hours with the proofs and exercises. These are planning estimates built from the lesson counts, not measurements of learners. Treat them as the size of the job, and expect the first few lessons to run slower while the design names settle.
Section | Pages | Essential lessons |
|---|---|---|
25 | Outcomes, assumptions, invariants, reset, cone, harness | |
21 | Monitor view, Boolean translation, implication, safety and liveness, mutation | |
25 | Spec to property, tracked items, assumption contract, data independence, assume-guarantee, checkers | |
30 | Reachability, BMC depth, induction and helpers, IC3 intuition, fairness and lassos, diagnosis | |
27 | Connectivity, registers, deadlock and starvation, reset determinism, FIFO set | |
19 | Miter, sequential equivalence, LEC assumptions, ECO flow | |
20 | Antecedent covers, over-constraint, proof core, mutation, bound justification, checklist | |
18 | Testplan, bring-up, slow-proof diagnosis, triage, regression | |
20 | Framework, scenarios, rapid-fire, drills, spot-the-bug | |
32 | Brief, four stages, solutions, appendix flow |
You write RTL and want properties for it. This route takes the ideas a designer is missing: that a result is relative to its assumptions, that a property must be able to fail, and that the harness is part of the proof. It follows the course in section order, apart from the mutation check, which comes once you have properties and assumptions to test, and it ends with the capstone stage for your kind of block.
Lesson | Why you read it | Minutes |
|---|---|---|
The vocabulary every later lesson uses. | 10 | |
The model every result is about: state, free inputs and one step. | 10 | |
The same assertion proves, passes vacuously or fails with the assumption set. | 15 | |
What each directive means to the engine, and which side of a port each belongs on. | 10 | |
The harness must create one reset sequence, or the proof starts anywhere. | 12 | |
Parameters, free inputs, one reset, assumptions, assertions and covers in one place. | 12 | |
What each line of a result says, and what it leaves out. | 10 | |
An assertion is a small monitor added to the model. | 10 | |
The translation table the rest of the course relies on. | 15 | |
The most common off-by-one in review. | 10 | |
One attempt per cycle against one per edge. | 10 | |
From the failing cycle back to the attempt that started it. | 12 | |
Turn a requirement into a property that can fail. | 12 | |
Data integrity without a scoreboard. | 12 | |
Assumed at the input that depends on it, asserted at the output that owes it. | 10 | |
List, classify, discharge, and probe every assumption. | 12 | |
Reuse a property set without hierarchical references. | 12 | |
A property is only as good as the bugs it kills. | 12 | |
Connectivity is a table, proved for all configurations. | 12 | |
The register table generates the property set. | 12 | |
The three register behaviours that hide bugs. | 12 | |
The full property set of one design, with the depth each needs. | 12 | |
Start the capstone stage for your block. | 15 | |
Pick the stage lesson that matches your block: stage 1 for a FIFO or handshake. | 15 | |
Stage 2 for a register block. | 15 | |
Stage 3 for a pipeline. | 15 |
You prove properties and defend the proofs. This route assumes route 1, or equivalent experience, for properties and assumptions, and concentrates on engines, convergence, applications, equivalence, coverage, the signoff evidence and the capstone that signs off all six designs.
Lesson | Why you read it | Minutes |
|---|---|---|
What a bounded check is, as constraints. | 12 | |
Why cutting to the cone changes no result. | 10 | |
Depth is derived, not guessed. | 12 | |
A pass needs both, to the same k. | 12 | |
Read a failing step and decide spurious or real. | 15 | |
Exclude the unreachable region so the property turns inductive. | 12 | |
Measure first then choose: reduce, split, strengthen. | 12 | |
Measure cone, depth and engine progress before touching anything. | 12 | |
A liveness violation is an infinite trace that loops. | 12 | |
Three different failures that need three different checks. | 10 | |
The rule that makes a split proof sound. | 12 | |
The one way a split proof lies. | 12 | |
Equivalence as a safety property on a miter. | 12 | |
States differ, outputs agree: the cut invariant. | 12 | |
Own a miter or an ECO: the flow and its intended differences. | 12 | |
Activity covers expose a proof that is true by assumption. | 12 | |
The surviving mutants are your uncovered behaviour. | 12 | |
When a bounded result may carry signoff weight. | 12 | |
Every line of the package with its evidence. | 10 | |
Decide in a fixed order: legal start, assumption, artefact, bug. | 12 | |
Choose the blocks and properties that earn a formal run. | 10 | |
Reset, harness, covers, then properties. | 10 | |
Per-commit and nightly sets, the ledger as the build output. | 10 | |
The capstone stage that asks for helpers and a ledger across the designs. | 15 | |
Review the whole ledger and call readiness. | 15 | |
Read it after your own attempt: the answers for the ledger and the final manifest. | 12 |
Fourteen days, about half an hour a day (never more than 50 minutes). The plan adds the interview pages that test each subject, so some lessons are not on the other routes. Each day pairs the lessons that teach a subject with the interview-prep page that tests it. Say the answers aloud in the order assumption, mechanism, trade-off, evidence: an answer you only read is not yet an answer. If you have less time, keep days 1, 2, 3, 4, 5 and 10.
Day | Lesson | Why you read it | Minutes |
|---|---|---|---|
Day 1 | The answer shape the later days reuse. | 10 | |
Day 1 | Open with what a result means. | 10 | |
Day 2 | The over-constraint story, with the trace. | 15 | |
Day 2 | Everything proves and nothing is reached: find it. | 15 | |
Day 3 | The forms interviewers quiz. | 15 | |
Day 3 | Fast proof, assume versus assert, bounded pass, induction, FIFO, arbiter. | 25 | |
Day 4 | Both obligations, same k. | 12 | |
Day 4 | Spurious or real: the reading routine. | 15 | |
Day 5 | How an invariant closes a step. | 12 | |
Day 5 | Depth, k, helpers, inconclusive. | 20 | |
Day 6 | Fairness constrains the environment only. | 12 | |
Day 6 | Within N cycles is safety; eventually is liveness. | 12 | |
Day 7 | The window arithmetic for four requesters. | 12 | |
Day 7 | Cycle of waits against absence of progress. | 15 | |
Day 8 | When one tagged bit stands for all data. | 12 | |
Day 8 | One-to-one states, scan off, consistent constants. | 10 | |
Day 9 | The miter question, with the mismatch read. | 12 | |
Day 9 | Setup difference against real difference. | 15 | |
Day 10 | Every implication gets a cover. | 10 | |
Day 10 | The evidence behind a signoff claim. | 10 | |
Day 11 | Triage, memory, disable-iff, equivalence, wrong tool, signoff. | 25 | |
Day 11 | Diagnose under deadline, report honestly. | 15 | |
Day 12 | Practise the arithmetic aloud. | 25 | |
Day 12 | Cones, lassos, clauses, assumption share. | 25 | |
Day 13 | Six flawed answers, each with the defect named. | 20 | |
Day 13 | Six flawed claims, each corrected. | 20 | |
Day 14 | Review the whole ledger and call readiness. | 15 |
Keep the framework and the first whiteboard set, since they train the answer shape, plus one subject day each on assumptions, induction and signoff. Give up the rapid-fire pages and the scenario days, which reward breadth you cannot build in three days.