Overview

UCLID5 is a formal verification tool described as the most recent in a series of tools developed at Carnegie Mellon University and the University of California, Berkeley. It provides both a modeling language for describing a system to be verified and a command language for creating verification scripts that specify initialization, operation, and verification conditions.

In a documented microprocessor-verification case study, UCLID5 was used to formally verify variants of the Y86-64 pipelined microprocessor against a sequential reference implementation. The study reports that UCLID5 was used to evaluate modeling and verification capabilities for hardware designs and that the verified pipeline processors generated the same results as the sequential reference model for all possible programs.

Modeling model

UCLID5 is designed to support models combining synchronous hardware and software. Hardware is expressed as state machines that compute a next state from the current state and transition to it. Software is expressed as sequences of operations that update parts of the system state. In the Y86-64 processor study, only UCLID5's hardware-modeling aspects were used.

The tool supports multiple data types useful for hardware modeling, including:

• Uninterpreted types, suitable for term-level modeling and uninterpreted functions with arbitrary but consistent functionality.
• Integers, used as mathematical unbounded integers for abstract hardware representations.
• Bit vectors, fixed-width groups of bits with arithmetic, logical, and comparison operations.
• Enumerated types, useful for register identifiers, operation codes, and other small hardware encodings.
• Booleans, used for single Boolean signals.
• Arrays, useful for register files, data memories, and other memory arrays.

UCLID5 can combine these types in functions and arrays. For example, the cited Y86-64 work models branch-decision logic as an uninterpreted function returning a Boolean value from an enumerated function-code argument and an uninterpreted condition-code argument.

Verification workflow

Given a model and verification script, UCLID5 generates verification conditions as formulas over the theories used in the model. These formulas are typically negations of the properties being verified. UCLID5 then invokes a satisfiability modulo theories (SMT) solver; in the Y86-64 case study, Z3 was used as the SMT solver.

When invoked through UCLID5, the SMT solver may report:

1. Unsatisfiable, indicating that the negated verification condition cannot hold and therefore the desired condition holds.
2. Satisfiable, providing concrete values for data elements and uninterpreted functions; UCLID5 uses these values to generate a counterexample trace that may indicate a design error, an inaccurate or overly abstract model, or an improperly stated verification condition.
3. Indeterminate, indicating that the solver found no satisfying solution but could not prove unsatisfiability, typically because the model is too complex or requires stronger reasoning than the SMT solver can provide.

Use in Y86-64 microprocessor verification

The report Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5 describes a case study using UCLID5 to verify several variants of the Y86-64 pipelined microprocessor. The methodology translated control logic into UCLID5 format automatically and modeled the pipelined processor and sequential reference implementation with as much modularity as possible. The work is presented as both confidence-building evidence for the processor designs in the Bryant-O'Hallaron textbook and a case study in UCLID5's capabilities and performance.

The same report used UCLID5 version 0.9.5 and Z3 version 4.5.0 for its experimental results.