Skip to content
STIMSMITH

Instruction Pipeline Register

Concept WIKI v1 · 5/26/2026

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.

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.

Function in a pipelined processor

In the PIPE model, pipeline registers cause normal instruction flow to advance only one stage at a time. This staged advancement is not the entire timing story, because some signals can still flow combinationally between stages. For example, data read in the memory stage can feed forwarding logic in the decode stage. In the cited UCLID5 model, stage procedures are ordered to respect these combinational dependencies and are followed by procedures that update the control logic and then update the pipeline registers.

Register update modes

A modeled pipeline register can take one of several next-state values:

  • Input value: the normal operation, loading the register input.
  • Old value: used when the pipeline stalls, preserving the previous register contents.
  • Empty value: used when a bubble is injected into the stage.
  • Initial value: used for the initial verification state, typically as an uninterpreted value indicating that the value may be arbitrary.

The UCLID5 word_register definition gives these modes a priority order. On each step, the register first checks whether it should initialize. If not initializing, it checks whether it should stall and retain the old value. If not stalled, it checks whether it should inject a bubble and take the empty value. If none of those conditions applies, it loads the input value.

Role in hazards, stalls, and bubbles

Pipeline registers are part of the mechanism that lets PIPE handle hazard conditions. The PIPE design requires additional data connections and control logic to resolve cases where data or control must pass between instructions already in the pipeline. In the standard PIPE variant, data hazards for execute-stage operands are handled by forwarding into decode; a one-cycle decode-stage stall is required for a load/use hazard, and a three-cycle stall is required for the return instruction. Branches are predicted as taken, and up to two instructions are canceled when a misprediction is detected.

The register update modes directly support these behaviors. A stall keeps the old register value. A bubble injects an empty value into a stage. During flushing for Burch-Dill verification, the pipeline framework uses bubble injection into the decode stage on each cycle until the pipeline is empty; this dynamically injects nop instructions and sets the status register to SBUB, indicating a pipeline bubble.

Verification context

The cited source models PIPE in UCLID5 for formal verification against the sequential SEQ processor. In that model, a pipeline register is represented as a procedure parameterized by control signals such as initialize, stall, and bubble, as well as values for the input, empty state, initial state, and old state. The same abstraction supports both ordinary pipeline execution and verification-specific mechanisms such as initialization and flushing.

CITATIONS

8 sources
8 citations
[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