formal.org

Binary Decision Diagrams with CUDDLearn binary decision diagrams: reduction, Apply, variable order, CUDD in C, equivalence checking and reachability, in eight modules of reading and katas.Modules (8)

Module 1 — Expand a Boolean function on its variables — 4 katas

Module 2 — Reduce a decision tree to an ROBDD — 4 katas

Module 3 — Combine BDDs with Apply and ITE — 4 katas

Module 4 — Choose a good variable order — 4 katas

Module 5 — Build BDDs in C with CUDD — 4 katas

Module 6 — Check two designs for equivalence — 4 katas

Module 7 — Compute the reachable states of a design — 4 katas

Module 8 — Compare BDD reachability with IC3 and PDR — 4 katas

Each module has a reading page and four katas, and the site checks each kata's answer. Module 5's katas are C programs, compiled and tested against CUDD.