Welcome to Formal Verification

What you will learn

• Explain in one sentence what formal verification does that simulation cannot.
• Read a first SystemVerilog assertion and a counterexample waveform.
• Name the main ways formal is used on real chip projects.
• Describe the three possible outcomes of a formal run: proven, failed, inconclusive.

Lessons

1. 1.1What formal verification really isExhaustive, mathematical checking of a design against properties.✓
2. 1.2Your first formal bug huntA tiny credit counter, one assertion and a two-cycle counterexample.✓
3. 1.3Simulation and formal, side by sideDifferent questions, different strengths — and why teams use both.✓
4. 1.4Where formal fits in a chip projectDesign exploration, bug hunting, signoff and formal apps.✓
5. 1.5From theory to everyday toolA short history: logic, model checking, BDDs, SAT and assertion standards.✓
6. 1.6Limits, outcomes and the right mindsetState explosion, inconclusive results and why formal is only as good as its properties.✓
7. ✎Chapter quiz (5 questions)✓

Key takeaways