The course is organised as ten sections. Most sections have four to six topics, and most topics have a short hub page plus two to four lessons. The exceptions are the four interview scenarios, which are single pages, the capstone Solutions topic with eight lessons, and the capstone brief and appendix with two lessons each. A lesson is short enough to read in one sitting and is built to one pattern, so you always know where to look for the idea, the worked proof and the pitfall.
Five companions carry the mechanism this course spends. Read them before the sections that lean on them, not necessarily before the course.
If this is new | Read this first | Before sections |
|---|---|---|
What formal is, in one lesson | Formal Foundations | |
Formal beside simulation | Formal Foundations, Methodology | |
The assertion language | Properties and SVA, and every property lesson | |
A first formal run on a FIFO | Formal Foundations, Property Development | |
The equivalence-check flow | Equivalence Checking |
Part | What it gives you |
|---|---|
Why it matters | The problem the idea solves on a running design, usually a symptom or a decision. |
Core idea | How it works, with a table, a formula or a diagram. |
Worked example | A runnable proof with its failing partner, or a counterexample read cycle by cycle. |
What the review looks for | The checks a reviewer would apply to this step. |
How to verify or debug it | What to measure and where to look when the result is wrong. |
Pitfall callout | The common mistake with its symptom, cause, fix and how it is found. |
Interview callout | How the idea is asked in interviews and what a strong answer contains. |
Check yourself | A question with a hidden answer: answer it first. |
Related lessons | Links backwards and forwards, and to the owner course where the mechanics live. |
Section and topic hubs are shorter: a purpose paragraph, a table of what you can do after each page and a suggested order. The capstone is symptoms first: its stage lessons give symptoms and the checks to run, the design listings show each variant as a visible BUG == line to be read after the trace, and a Solutions lesson after the checks gives the causes. Its lessons follow the same shape and add a hint ladder, a graded sequence of hints for each planted bug.
A proof block is a small SystemVerilog module with its properties inside, and its first line is the proof header. The header says what was done with the block before it was published: which mode to run, how deep to go, and what outcome to expect. Here is a real one, from the decade counter lesson:
// formal: prove 20 expect unproven slang top mod10_counter define HELPER=0
// mode depth expected front end top module parameter variantEach word is explained once, here. A block that uses the front-end option also carries a line define FORMAL straight after the header, so that the properties inside the module are read.
Word | Meaning |
|---|---|
| The mode. |
Depth N | How many steps the bounded check unrolls. A counterexample at step N needs depth N plus 1. |
| The outcome the lesson claims. |
| Means not reached within the depth. That is inconclusive: it does not show the state is unreachable. Only a proved invariant makes a cover unreachable. |
| The front-end option: it selects the language front end that reads Boolean concurrent assertions with |
| Which module is the top when the block holds helpers or a harness wrapper. |
| A value for a top-module parameter. It selects a bug variant or switches a helper, so a proof and its counterexample come from the same module text. |
The result written in a header is the recorded result of a real run made before the lesson was published. A block whose result disagrees with its header is a mistake: report it. A block whose first line reads // not-run: followed by a reason is concept, not execution: textbook assertion operators that the front end cannot read are shown that way, always beside the runnable Boolean form that checks the same cycle. A block marked // snippet is a fragment for reading, not a complete module. A block marked // bad-example is deliberately wrong, and the lesson names its defect.
You cannot run a proof block on this site. To reproduce one, follow the appendix lesson Appendix: Run It Yourself on an Open-Source Flow. Python blocks run in any plain Python 3 interpreter.
The runnable blocks use a small open flow, and the lessons say so wherever a limit matters. Four limits recur:
Limit | What the course does instead |
|---|---|
No liveness engine | Eventually-style requirements are taught as concept; the runnable substitute is bounded response with a stated N, which is a safety property. |
No implication operators or sequences in the runnable form |
|
No gating argument on | A window of history needs a history register or a counter, not a third argument. |
Two-state model | There is no unknown value, so an unknown-check proves nothing; reset determinism is proved with two copies instead. |
The course teaches the textbook forms because reviewers and interviews speak them, and it runs the Boolean forms because the front end used here reads those. Every concept block is paired with the runnable equivalent written with sampled-value history, and the lesson says in one sentence which cycle each form checks. Never copy a concept block into a run: copy its runnable partner.
Answer every check-yourself before revealing its answer. A question you only read is not yet knowledge.
Read the Python blocks, and run them in any Python 3 interpreter if you want to change a number. Which assertion fails first tells you which relationship matters. Each block prints exactly one line starting with PASS when its assertions hold, and every check is written so it can fail: a second input or an injected bug shows the check catching it.
Worked arithmetic that cannot run is shown as text and marked accordingly. Read it with a pencil, not as output.
The word illustrative marks an invented number. It is consistent inside its lesson so the arithmetic checks, but it is not a target and not typical of anything.
sync_fifo, rr_arbiter, hs_bridge, csr_block, pipe3 with its retimed twin, and mod10_counter are defined once and reused everywhere: the hub table says what each is. Small lesson-local modules appear where a running design cannot show the point; each is named in its lesson and never reused elsewhere. One helper wrapper joins three designs for the connectivity lessons.
Aim | How to read |
|---|---|
A project starting now | Read the hub and how-to-use, then only the sections your task touches, top to bottom. Skim the worked traces even if you skip the proofs; the cycle tables carry the teaching. |
A project in six months | Follow your role path end to end. Read every proof block with its bug variant, reproduce the ones that matter to you through the appendix flow, read every counterexample, and do the capstone with the ledger, because the capstone is the closest thing to the job. |
An interview in two weeks | Read the hub, then the two-week plan on the reading-path page and Interview Prep. Say every answer aloud in the order assumption, mechanism, trade-off, evidence. |
Never skip the check-yourself questions or the interview callouts: they are the shortest way to find a gap. Cut breadth before depth: skip whole topics you will not use before skimming every topic.
Learner text never names formal tools, commands or products: it says the formal tool, the property checker, the equivalence checker, the solver, the front end. The single exception is the appendix lesson Appendix: Run It Yourself on an Open-Source Flow, clearly labelled, which names the open-source flow and its commands. Go there when you want to run something; its content is not repeated anywhere else.
If a number about a design disagrees between two lessons, the first lesson that introduces the design wins and the other is wrong: quote both pages, the two values, and which assertion fails. If a proof block's claimed outcome disagrees with a run on a fresh copy, quote the block, the header, and the first differing cycle. If a link points nowhere, quote the lesson and the link text. One report per message keeps each fix checkable.
You run the Boolean form: it is the one the front end reads. The textbook form gives you the review language and the cycle the check belongs to, stated in the lesson.