Skip to content
STIMSMITH

PIPE Pipeline Processor

Concept

PIPE is the pipelined Y86-64 processor implementation discussed in formal verification work comparing seven PIPE variants against the sequential SEQ reference processor. PIPE overlaps instruction execution for performance and relies on pipeline registers plus PIPE-specific control logic, while sharing functional blocks such as instruction decoding and the ALU with SEQ.

First seen 5/26/2026
Last seen 5/26/2026
Evidence 11 chunks
Wiki v1

WIKI

Overview

PIPE is a pipelined implementation of the Y86-64 processor family used in the Bryant-O’Hallaron instructional architecture and in later formal-verification work. The Y86-64 ISA defines programmer-visible architectural state including registers, the program counter, condition codes, data memory, and an exception status word. Unlike a sequential ISA model, a pipelined implementation overlaps multiple instructions and must use mechanisms such as interlocking and data forwarding to preserve the sequential semantics of the ISA. [Y86-64-state] [pipeline-semantics]

Relationship to SEQ

READ FULL ARTICLE →

NEIGHBORHOOD

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

explore full graph →

RELATIONSHIPS

9 connections
Pipeline Stall uses → 100% 2e
PIPE uses pipeline stalls to handle hazard conditions when data forwarding is insufficient.
Pipeline Flushing uses → 100% 2e
PIPE uses pipeline flushing to bring the pipeline to a quiescent state during exceptional conditions.
Sequential Reference Model (SEQ) compares with → 100% 2e
Verification checks that PIPE and SEQ are functionally equivalent for all possible programs.
Data Forwarding uses → 100% 2e
PIPE uses data forwarding to resolve hazard conditions between instructions in the pipeline.
Bryant-O'Hallaron Computer Systems Textbook ← introduces 100% 1e
The Bryant-O'Hallaron textbook presents the PIPE pipelined processor implementation of Y86-64.
Hardware Control Language (HCL) uses → 100% 1e
The control logic for PIPE is described in HCL.
Y86-64 part of → 95% 1e
PIPE is the pipelined implementation of the Y86-64 instruction set.
Branch Prediction uses → 100% 1e
PIPE uses branch prediction to speculatively fetch instructions.
Instruction Pipeline Register ← part of 100% 1e
PIPE contains pipeline registers to enable multiple instructions to flow through the pipeline simultaneously.

LINKED ENTITIES

4 links
Y86-64 instruction_set_architecture PIPE is described as a pipelined implementation of a Y86-64 processor and is verified against the Y86-64 ISA semantics.
UCLID5 formal_verification_tool The verification work constructs UCLID5 models and scripts for a system combining a pipelined microprocessor and a sequential reference implementation.
Burch-Dill Correspondence Checking verification_method The evidence describes the Burch-Dill approach and says the verification script carries out Burch-Dill correspondence checking.
Z3 SMT solver solver_used_for_verification_conditions The evidence states that UCLID5 invokes SMT solvers and that the work used the Z3 solver.

CITATIONS

11 sources
11 citations — click to expand
[1] Y86-64-state Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[2] pipeline-semantics Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[3] PIPE-vs-SEQ Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[4] seven-variants Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[5] HCL-control Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[6] UCLID5-generation Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[7] UCLID5-role Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[8] correspondence-checking Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[9] term-level-modeling Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[10] SMT-solving Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[11] safety-liveness Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5