Decision Procedures for Hardware Formal Verification

An 8-module course on the solvers that power formal verification. BDDs, SAT/CDCL, SMT bit-vectors, bounded model checking, k-induction, and IC3/PDR — implemented and applied to real hardware properties.

Modules (8)

• Module 1 — Binary Decision Diagrams (BDDs)
• Module 2 — Symbolic Image Computation & Reachability
• Module 3 — Fixed-Point CTL Model Checking — 1 kata
• Module 4 — Boolean Satisfiability & CDCL
• Module 5 — Bounded Model Checking — 3 katas
• Module 6 — SMT: Bit-Vectors, Arrays, Uninterpreted Functions — 3 katas
• Module 7 — Bit-Vector Arithmetic — 3 katas
• Module 8 — k-Induction & IC3/PDR — 3 katas

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