Skip to content
STIMSMITH

Satisfiability Modulo Theories (SMT)

Concept WIKI v1 · 5/26/2026

Satisfiability Modulo Theories (SMT) is used in UCLID5-based formal verification by solving verification-condition formulas over multiple theories such as uninterpreted data, integers, bit vectors, arrays, and other typed model elements. In the cited UCLID5 processor-verification workflow, SMT solvers report unsatisfiable, satisfiable, or indeterminate results, which respectively support proof, counterexample generation, or a need for less complex or more precise modeling.

Overview

In the UCLID5 verification workflow described in the evidence, Satisfiability Modulo Theories (SMT) is the solving technology invoked after UCLID5 generates verification conditions. Those verification conditions are formulas in a logic that supports multiple data types, described as theories, used in the model. The generated formulas are typically negations of the properties the user wants to verify.

Role in verification

UCLID5 uses a model and verification script to generate verification conditions, then invokes an SMT solver. In the reported work, UCLID5 could use several SMT solvers, and the experiments used the Z3 solver developed at Microsoft Research.

Because the generated formulas are often negated verification goals, solver results are interpreted in a verification-specific way:

  • Unsatisfiable: if the negated formula is unsatisfiable, the desired verification condition holds.
  • Satisfiable: the solver provides concrete values for all data elements appearing in the formula, including uninterpreted functions; UCLID5 uses these values to produce a counterexample.
  • Indeterminate: the solver finds no satisfying solution but also cannot prove unsatisfiability; this typically indicates that the model is too complex or requires more sophisticated reasoning than the SMT solver can provide.

Counterexamples and diagnostic use

When an SMT solver returns satisfiable for a verification condition encoded as a negated formula, UCLID5 can generate a counterexample: a sequence of model actions that violates the verification condition. The evidence identifies several possible interpretations of such counterexamples: a true design error, a model that is inaccurate or too abstract, or an incorrectly expressed verification condition.

Theories and abstraction choices

The cited report emphasizes that formal models can use different levels of abstraction. It describes models using uninterpreted terms, integers, and bit vectors, and notes that ALU and other data operations can range from uninterpreted functions to precise arithmetic. The report states a general modeling guideline: use the most abstract model possible that still captures the properties required for correctness.

This abstraction choice affects SMT solving. For example, an ALU increment/decrement property, (x+8)+−8 = x, was expressed in UCLID5 as an axiom imposed on an otherwise uninterpreted ALU function and provided as a constraint to the SMT solver. The report states that the SMT solver could not make effective use of this axiom, causing verification at that abstraction level to be unsuccessful. As a result, one pipeline variant required modeling data as either integers or bit vectors with a precise interpretation of addition.

Practical implication

Within this evidence, SMT is not only a backend decision procedure but also a constraint on modeling style. The same verification goal may succeed or fail depending on the theories selected, the precision of arithmetic modeling, and whether the solver can effectively use axioms over uninterpreted functions.

LINKED ENTITIES

4 links
UCLID5 invokes_smt_solver
Z3 is_smt_solver_used_with
Microsoft Research developed_z3_solver
Uninterpreted Functions used_in_smt_modeling

CITATIONS

12 sources
12 citations
[1] UCLID5 generates verification conditions as formulas in a logic supporting multiple data types, called theories, and invokes an SMT solver. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[2] Verification-condition formulas are typically negations of the properties being verified. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[3] In the reported work, UCLID5 used Z3 version 4.5.0 as the SMT solver, and Z3 is described as developed at Microsoft Research. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[4] An SMT solver invoked by UCLID5 can return unsatisfiable, satisfiable, or indeterminate. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[5] For negated verification formulas, unsatisfiability indicates that the desired verification condition holds. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[6] When a formula is satisfiable, the SMT solver provides concrete values for data elements, including uninterpreted functions, and UCLID5 uses them to generate a counterexample. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[7] A counterexample may indicate a true design error, an inaccurate or overly abstract model, or an incorrectly expressed verification condition. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[8] An indeterminate result means the solver found no satisfying solution but could not prove unsatisfiability, typically because the model is too complex or needs more sophisticated reasoning. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[9] The report recommends using the most abstract model possible that still captures the properties needed for correctness. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[10] Data in the cited models can be represented as uninterpreted terms, integers, or bit vectors, while ALU and data operations can range from uninterpreted functions to precise arithmetic. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[11] The ALU increment/decrement property was expressed as an axiom imposed on an otherwise uninterpreted ALU function and provided as a constraint to the SMT solver. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[12] The SMT solver could not effectively use that axiom, making verification at that abstraction level unsuccessful and requiring the SW variant to model data as integers or bit vectors with precise addition. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5