Industrial Practice: Scaling Formal Verification

A 5-module course on industrial-scale formal verification. State explosion, abstraction, CEGAR, assume-guarantee reasoning, and equivalence checking — the techniques used in production chip verification flows.

Modules (5)

• Module 1 — State Explosion & Symmetry Reductions — 3 katas
• Module 2 — Abstraction: Black-Boxing & Data Abstraction — 3 katas
• Module 3 — CEGAR & Predicate Abstraction — 1 kata
• Module 4 — Compositional Verification & Assume-Guarantee — 3 katas
• Module 5 — Combinational & Sequential Equivalence Checking — 3 katas

Every kata runs SymbiYosys in the browser: write the properties, run the proof, read the counterexample.