Free, practical, chapter-by-chapter
Prove your design is right — for every input, every cycle.
Learn formal verification the practical way — SVA, FPV, equivalence and signoff, chapter by chapter.
- 12 chapters
- 72 lessons
- 42 runnable example files
- 50 quiz questions
Learning path
Welcome to Formal Verification
What formal verification is, how it differs from simulation, where it fits in a chip project and what its limits are.
How Formal Engines Think
Boolean models, reachability, cones of influence, BDDs, SAT, bounded model checking and induction — the ideas inside every formal tool.
SystemVerilog Assertions Essentials
The SVA you need for formal: assert/assume/cover, immediate vs concurrent assertions, sampling, sequences, implication, local variables and good style.
Formal Property Verification (FPV) Basics
Bring up a complete FPV environment for a small periodic timer: covers, assumptions, assertions, running the tool and debugging counterexamples.
Exploring New RTL with Formal
Use formal as a designer's microscope: ask "can this happen?" with covers, poke at behaviours, and find spec holes before any testbench exists — on a 4-floor lift controller.
FPV for Bug Hunting and Signoff
Build a complete, reviewable FPV plan for a synchronous FIFO: goals, property set, end-to-end data checking with a tracked item, complexity staging and quality checks.
Formal Apps for Everyday Problems
Targeted formal flows that solve common problems with little effort: connectivity, control/status registers, reusable protocol checkers, unreachable coverage, X-propagation and post-silicon debug.
Formal Equivalence Verification
Prove two models behave identically: combinational vs sequential equivalence, key-point mapping, RTL-to-netlist and RTL-to-RTL flows, constraints, don't-cares and mismatch debug.
When Proofs Lie: Avoiding False Positives
The ways a formal environment can report "proven" while a real bug survives — over-constraints, vacuity, reset mistakes, wrong configurations, shallow bounds — and the habits that catch them.
Taming Complexity
What to do when proofs do not converge: measure, reduce, cut, abstract, add helper invariants, decompose with assume-guarantee, split cases and choose engines — with worked examples.
Formal Signoff on Real Projects
Running formal at project scale: choosing blocks, planning and staffing, the FV plan template, formal coverage metrics, reviews, regressions and the final signoff report.
Your Formal-Aware Workflow
Make formal part of everyday design work: designer assertions, team habits, practice problems with solutions, and where to go next.
How every lesson works
Small, original examples
Every concept is shown on a tiny design you can read in one screen — arbiters, FIFOs, locks, counters — with design, properties and a run script.
Waveforms, not walls of text
Timing-heavy ideas such as implication, sampling and liveness are drawn as cycle-by-cycle waveforms.
Quiz at the end of each chapter
Check yourself with short questions; every answer comes with an explanation.
Report & flag anything
Found a bug in the text or the code? Every page and every code block has a report button that goes straight to the editors.