Hardware Formal Verification

A 10-module hands-on course in hardware formal verification using SymbiYosys, Yosys, and open-source solvers. Write SVA properties, run BMC and k-induction, and prove correctness of real RTL designs.

Modules (10)

• Module 1 — Introduction to FV — 6 katas
• Module 2 — assert / assume / cover — 3 katas
• Module 3 — Bounded MC — 3 katas
• Module 4 — SVA Operators and Bind — 3 katas
• Module 5 — What a Proof Claims — 6 katas
• Module 6 — Strengthening Induction — 3 katas
• Module 7 — Clock Domain Crossing — 3 katas
• Module 8 — Liveness and Fairness — 3 katas
• Module 9 — AXI4-Lite Protocol and Security — 6 katas
• Module 10 — Capstone — 3 katas

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