Uninterpreted Functions

Concept

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.

First seen 5/25/2026

Last seen 6/8/2026

Evidence 8 chunks

Wiki v1

WIKI

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

READ FULL ARTICLE →

NEIGHBORHOOD

No graph connections found for this entity yet. It may appear in future ingestion runs.

explore full graph →

RELATIONSHIPS

3 connections

UCLID5 ← uses 100% 2e

UCLID5 supports uninterpreted functions for term-level modeling of hardware blocks.

ALU Abstraction Modeling ← uses 100% 2e

The most abstract ALU model defines the ALU as an uninterpreted function.

Synthesizing Instruction Selection Rewrite Rules from RTL using SMT ← uses 100% 1e

The paper uses uninterpreted functions to abstract complex operations like floating-point arithmetic.

LINKED ENTITIES

2 links

UCLID5 APPLIES Extracted graph relationship

Term-Level Modeling USES Extracted graph relationship

CITATIONS

5 sources

5 citations — click to expand

[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