Overview

Z3 is a satisfiability modulo theories (SMT) solver developed at Microsoft Research. In the cited Y86-64 processor-verification report, UCLID5 generated verification conditions and invoked an SMT solver; the reported work used Z3 for that solver role. [C1]

Role in UCLID5 verification

In the described workflow, UCLID5 takes a model and verification script, generates verification conditions as formulas over the theories used in the model, and typically formulates those conditions as negations of the properties to be verified. It then invokes an SMT solver. The report states that UCLID5 can use several SMT solvers and that this work used Z3. [C2]

When invoked by UCLID5, the SMT solver can return three classes of result: unsatisfiable, satisfiable, or indeterminate. An unsatisfiable result indicates that the desired verification condition holds because the formula is the negation of the property. A satisfiable result provides concrete values that usually indicate a failed verification condition, which UCLID5 can use to generate a counterexample. An indeterminate result indicates that the solver found no satisfying solution but also could not prove unsatisfiability. [C3]

Use in the Y86-64 processor-verification study

The report Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5 used UCLID5 version 0.9.5 and Z3 version 4.5.0 as the SMT solver for its experimental results. The experiments were run on an eight-core 2.20 GHz Intel Xeon E5-1660, and the report notes that Z3 gained a small benefit from multi-core parallelism, making wall-clock run times slightly shorter than total CPU time used. [C4]

Technical context

The verification task involved UCLID5 models of Y86-64 processor variants. The report describes how UCLID5 formulas may involve multiple theories corresponding to model data types, including uninterpreted functions and arrays with arbitrary index and data types. Z3 was the solver used for these verification conditions in the reported experiments. [C2]