Module 7 — Bit-Vector Arithmetic

Bit-vector decision procedures for hardware. Reason about overflow detection, signed and unsigned comparison, bit-field extraction, and mixed-width operations in the SMT bit-vector theory.

Katas in this module (3)

• Kata 7.1 — Modular Addition
• Kata 7.2 — Two's Complement Symmetry
• Kata 7.3 — Multiplier Difficulty

Part of Decision Procedures for Hardware Formal Verification on formal.org.