Skip to content
STIMSMITH

Uninterpreted Functions

Concept WIKI v1 · 5/25/2026

Uninterpreted functions are used in UCLID5 formal models as typed function symbols whose concrete behavior is left to the SMT-level verification problem. In the cited Y86-64 verification work, they are used to abstract processor logic such as branch-condition evaluation while still allowing UCLID5 and an SMT solver to reason about verification conditions.

Overview

In the UCLID5-based verification workflow described for pipelined Y86-64 microprocessors, an uninterpreted function may have multiple arguments, each with its own type, and may return a value of another type. The report gives branch-decision logic as an example: whether a branch should be taken is modeled as an uninterpreted function returning a Boolean value, with arguments including an enumerated function-code type and an uninterpreted condition-code type.

Role in modeling abstraction

The report frames these typed modeling constructs as part of the abstraction choices available when constructing a formal model. It states a general modeling rule: use the most abstract model that still captures the correctness-relevant properties of the system. In this setting, uninterpreted functions can support abstraction by representing behavior such as branch-condition evaluation without requiring all implementation details to be expanded in the model.

Use in UCLID5 verification

Given a model and verification script, UCLID5 generates verification conditions as formulas in logics supporting the theories used by the model. These formulas are typically negations of the properties being verified, and UCLID5 invokes an SMT solver to check them. In the cited work, UCLID5 used the Z3 SMT solver.

When the SMT solver finds such a formula satisfiable, it provides concrete values for all data elements appearing in the formula, including uninterpreted functions. UCLID5 can then use those values to produce a counterexample: a sequence of model actions that violates a verification condition. The report notes that such counterexamples may indicate a real design error, an inaccurate or overly abstract model, or an incorrectly stated verification condition.

Verification outcomes

The cited UCLID5 workflow distinguishes three SMT-solver outcomes:

  • Unsatisfiable: because the checked formula is usually the negation of the property, unsatisfiability indicates that the desired verification condition holds.
  • Satisfiable: concrete values, including for uninterpreted functions, are produced and may lead to a counterexample.
  • Indeterminate: the solver cannot find a satisfying solution but also cannot prove unsatisfiability, often suggesting that the model is too complex or requires reasoning beyond the solver's capability.

LINKED ENTITIES

2 links
UCLID5 APPLIES
Term-Level Modeling USES

CITATIONS

5 sources
5 citations
[1] Uninterpreted functions in the cited UCLID5 modeling setting can have multiple typed arguments and a separately typed return value. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[2] Branch-decision logic is modeled as an uninterpreted function returning a Boolean value from an enumerated function-code type and an uninterpreted condition-code type. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[3] The report recommends using the most abstract model that still captures the system properties needed for correctness. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[4] UCLID5 generates verification conditions and invokes an SMT solver; the cited work used Z3. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[5] If an SMT query is satisfiable, the solver provides concrete values for all data elements in the formula, including uninterpreted functions, and UCLID5 can use them to generate a counterexample. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5