Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5

Paper

Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5 is an October 2018 CMU technical report by Randal E. Bryant describing a UCLID5-based case study for verifying pipelined Y86-64 processor variants against a sequential reference model. The work uses Burch-Dill correspondence checking, UCLID5 modeling and verification scripts, and the Z3 SMT solver, and reports successful verification that the pipeline processors generate the same results as the sequential model for all possible programs.

First seen 5/25/2026

Last seen 5/25/2026

Evidence 3 chunks

Wiki v1

WIKI

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.

READ FULL ARTICLE →

NEIGHBORHOOD

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

explore full graph →

LINKED ENTITIES

7 links

Randal E. Bryant AUTHORED Extracted graph relationship

UCLID5 USES Extracted graph relationship

Z3 USES Extracted graph relationship

Y86-64 VERIFIES Extracted graph relationship

Burch-Dill Correspondence Checking APPLIES Extracted graph relationship

Semiconductor Research Corporation FUNDED Extracted graph relationship

National Science Foundation FUNDED Extracted graph relationship

CITATIONS

14 sources

14 citations — click to expand

[1] The report is titled Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5, is CMU-CS-18-122, was authored by Randal E. Bryant, and is dated October 2018. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5

[2] The work reports on verification of a CISC processor named Y86-64, styled after the Intel64 instruction set, using the UCLID5 verifier. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5

[3] The case study aimed to verify several Y86-64 pipelined microprocessor variants from the Bryant-O'Hallaron textbook and to evaluate UCLID5 for hardware modeling and verification. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5

[4] The reported verification succeeded in showing that the different pipeline processors generate the same results as the sequential reference model for all possible programs. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5

[5] The modeled system combines a pipelined microprocessor with a sequential reference implementation, and the verification script performs Burch-Dill correspondence checking. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5

[6] The paper argues that safety alone can allow a deadlocked or inactive processor to pass, so it also verifies liveness to show the pipeline does not stall indefinitely. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5

[7] UCLID5 provides a modeling language and a command language, and for this processor verification work only its hardware modeling aspects were used. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5

[8] UCLID5 supports multiple data types relevant to hardware modeling, including uninterpreted values, integers, bit vectors, enumerations, Booleans, tuples and records, and arrays. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5

[9] The report recommends using the most abstract model that still captures the correctness-critical properties of the system. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5

[10] UCLID5 generates verification conditions and invokes an SMT solver; this work used the Z3 solver. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5

[11] The SMT solver outcomes described are unsatisfiable, satisfiable with counterexample generation, and indeterminate. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5

[12] The report covers seven Y86-64 pipeline variants derived from the textbook implementation and homework modifications. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5

[13] The experimental results were measured using UCLID5 version 0.9.5 and Z3 version 4.5.0. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5

[14] The work was supported in part by the Semiconductor Research Corporation under contract 2637.001 and the National Science Foundation under STARSS grant 1525527. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5