Instruction Pipeline Register

Concept

An instruction pipeline register is a state element used between stages of a pipelined processor. In the PIPE Y86-64 implementation, pipeline registers allow multiple instructions to occupy different pipeline stages at the same time, and their modeled behavior includes normal loading, stalling, bubble injection, and initialization.

First seen 5/26/2026

Last seen 5/26/2026

Evidence 4 chunks

Wiki v1

WIKI

Overview

An instruction pipeline register is a pipeline state element that carries instruction-related values between adjacent stages of a pipelined processor. In the PIPE implementation of the Y86-64 instruction set, pipeline registers are the additional state elements that distinguish the pipelined design from the sequential SEQ design: they allow up to five instructions to flow through the pipeline simultaneously, with each instruction in a different stage.

PIPE is organized as a five-stage pipeline. Its stages correspond to the familiar instruction-processing steps shown for the sequential implementation: fetch, decode, execute, memory, and writeback. Pipeline registers sit in this staged organization and hold the values needed as an instruction advances one stage per cycle.

READ FULL ARTICLE →

NEIGHBORHOOD

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

explore full graph →

RELATIONSHIPS

2 connections

PIPE Pipeline Processor part of → 100% 1e

PIPE contains pipeline registers to enable multiple instructions to flow through the pipeline simultaneously.

UCLID5 Pipeline Register Definition ← implements 100% 1e

The UCLID5 pipeline register definition implements the pipeline registers used in the PIPE model.

CITATIONS

8 sources

8 citations — click to expand

[1] PIPE contains additional state elements in the form of pipeline registers, enabling up to five instructions to flow through the pipeline simultaneously, each in a different stage. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5

[2] PIPE is a five-stage pipeline implementing the Y86-64 instruction set, with stages corresponding to fetch, decode, execute, memory, and writeback. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5

[3] Pipeline registers cause normal instruction flow to advance only one stage at a time, while some signals still flow combinationally between stages. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5

[4] In the UCLID5 model, the pipeline register supports input value, old value, empty value, and initial value modes. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5

[5] On each step, the UCLID5 pipeline-register definition can initialize, stall, inject a bubble, or load its input, with the shown conditional structure selecting among those outcomes. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5

[6] PIPE uses additional data connections and control logic to resolve hazard conditions where data or control must pass between instructions in the pipeline. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5

[7] In the standard PIPE variant, forwarding handles data hazards for execute-stage arguments, a one-cycle decode-stage stall is required for load/use hazards, a three-cycle stall is required for return, and up to two instructions are canceled on branch misprediction. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5

[8] For Burch-Dill verification, flushing is implemented by injecting a bubble into the decode stage each cycle until the pipeline is empty, dynamically injecting nop instructions and setting the status register to SBUB. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5