Each lesson answers one part of one of the course's sixteen questions. It starts with a concrete situation, shows why the obvious approach fails, and builds the idea from there. Tools and standards appear as evidence for the reasoning; the courses that teach them are linked.
Block | What it is for |
|---|---|
Header | Level badge, the question the lesson answers, and what to read first |
Hook | A short scene that ends on the lesson's question |
The obvious answer, and why it breaks | The first approach most engineers try, and the case where it fails |
The idea and the picture | The idea, drawn as stimulus, design, checker and coverage, or as a plot from a model |
Worked numbers | Probabilities, costs and sizes with numbers that add up. Numbers not taken from a published source are marked illustrative. |
Build it and watch it run | Runnable code, a model or a proof, and its real output |
Design space and how real teams do it | The options, what each costs, and which practices and standards chose which |
What breaks | A failure told as a short story: symptom, evidence, root cause, fix |
Senior or Principal lens | The second-order effect, or the question a reviewer would ask |
Interview corner | The question as interviewers ask it, a weak answer, a strong answer, and follow-ups |
Check yourself, takeaways, next | Scenario questions with reasoned answers, three lines to remember, and the problem the next lesson solves |
Badges F, W, S and P mark the lowest level a lesson serves: Foundation, Working, Senior, Principal. Senior readers should not skip foundation lessons: the lens at the end of each one is written for them.
DCRouter is a small 4-port packet router written for this course (Meet DCRouter). It contains 24 planted bugs, each switched on by a define. In the parts marked below, you apply one technique to DCRouter and record which bugs it catches, building a bug-catch matrix: measured evidence of which technique finds which kind of bug.
Step | Part | What you add |
|---|---|---|
1 | build and run a smoke test of the bug-free DCRouter. | |
2 | sort the 24 Bug Zoo entries by class and predict which technique will catch each. | |
3 | a Python reference model of DCRouter that predicts every output packet. | |
4 and 5 | directed tests, then a constrained-random hunt through the Bug Zoo. | |
6 and 7 | assertions and a scoreboard for DCRouter; which zoo bugs now fail. | |
8 | a coverage model for DCRouter; correlate coverage holes with uncaught zoo bugs. | |
9 | prove DCRouter's arbiter and credit counters; see which zoo bugs fall to proof. | |
10 | a full verification plan for DCRouter. | |
11 | the complete evidence ledger and bug-catch matrix, presented as a sign-off review. |
Verilog and SystemVerilog listings are complete testbenches that print a line starting with PASS. Constrained-random and assertion listings run in Verilator (verilator --binary --timing --assert file.sv); simple ones also run in Icarus Verilog.
DCRouter testbenches start with // uses: dcrouter. Put them in one file after the DCRouter RTL from the DCRouter page; a line such as // uses: dcrouter BUG_5 means "with ` define BUG_5`` at the top".
Formal proofs start with // formal: bmc 20 or // formal: prove 20. They run with Yosys and yosys-smtbmc using the z3 solver; each lesson shows the commands.
Python models use only the standard library; run them with python3 file.py. They check their own results and print PASS.
Listings that start with // snippet are fragments; // bad-example marks code shown as a mistake.
Read the hook and stop. Decide what you would do before reading on.
Before each Bug Zoo run, predict which bugs the technique will catch; then compare.
Answer the check-yourself questions out loud before opening them.
Once a part is done, try its drills page from memory.