Overview
Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5 is a technical report identified as CMU-CS-18-122, authored by Randal E. Bryant and dated October 2018. The report studies formal verification of the Y86-64 processor, described as a CISC processor styled after the Intel64 instruction set, using the UCLID5 verifier.
The paper frames the work as a case study in formally verifying several variants of the pipelined Y86-64 microprocessor from the third edition of the Bryant-O'Hallaron computer systems textbook. Its stated goals were to check that the processor designs are correct and to evaluate UCLID5 for modeling and verifying hardware designs.
Verification objective
The report verifies pipelined processor implementations against a sequential reference version. The modeled system combines a pipelined microprocessor with the sequential reference implementation, and the verification script carries out Burch-Dill correspondence checking. The successful outcome reported in the introduction is that the different pipeline processors generate the same results as the sequential reference model for all possible programs.
The paper also notes a limitation of safety-only correspondence checking: a processor that deadlocks, or even a device that does nothing, could satisfy a safety property. To address this, the report adds a liveness argument, described as a simple and effective approach that builds on the safety property to show that the pipeline does not stall indefinitely.
UCLID5 modeling approach
UCLID5 is described as providing both a modeling language for describing the system and a command language for verification scripts that initialize the system, operate it, and check verification conditions. For the processor work, only UCLID5's hardware modeling aspects were used.
The report emphasizes abstraction choices in building formal models. UCLID5 supports data types including uninterpreted values, integers, bit vectors, enumerations, Booleans, tuples and records, and arrays. In the hardware models, uninterpreted functions are used where detailed functionality is unnecessary as long as behavior is consistent between the pipeline and sequential reference model; arrays are useful for register files, data memories, and other memory arrays. The report states a general modeling rule: use the most abstract model that still captures the properties required to guarantee correctness.
SMT solving 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 checked. UCLID5 then invokes an SMT solver; in this work, the solver used was Z3 from Microsoft Research.
The report describes three possible solver outcomes. If the formula is unsatisfiable, the desired verification condition holds because the checked formula is the negation of the property. If the formula is satisfiable, UCLID5 can produce a counterexample, which may indicate a true design error, an inaccurate or overly abstract model, or an incorrectly expressed verification condition. If the solver returns indeterminate, the model may be too complex or may require reasoning beyond the solver's capability.
Scope and experimental setup
The report states that the Bryant-O'Hallaron textbook presents the Y86-64 instruction set, a pipelined implementation, and homework modifications that yield a total of seven variants; the report describes verifying all of these variants. It also describes construction of UCLID5 processor models, verification efforts, performance aspects of UCLID5, and related work involving an earlier version of UCLID.
All experimental results reported in the paper were measured using UCLID5 version 0.9.5 and Z3 version 4.5.0 as the SMT solver.
Funding
The work was supported in part by the Semiconductor Research Corporation under contract 2637.001 and the National Science Foundation under STARSS grant 1525527.