Module 5 — Combinational & Sequential Equivalence Checking

Prove two RTL implementations compute the same function using miter circuits and SAT-based equivalence checking, extended to sequential retiming.

Katas in this module (3)

• Kata 5.1 — Miter the Adders
• Kata 5.2 — Sequential Equivalence, Different Encodings
• Kata 5.3 — Find the Differentiating Input

Part of Industrial Practice: Scaling Formal Verification on formal.org.