Module 6 — SMT: Bit-Vectors, Arrays, Uninterpreted Functions

SMT theories for hardware reasoning. Model register files with arrays, arithmetic with bit-vectors, and opaque sub-modules with uninterpreted functions in a unified solver framework.

Katas in this module (3)

• Kata 6.1 — Bit-Vector Property
• Kata 6.2 — Array Property
• Kata 6.3 — Abstract with an Uninterpreted Function

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