Skip to content
STIMSMITH

Hazard Detection

Concept WIKI v1 · 5/25/2026

Hazard detection is a pipeline-control concern in pipelined microprocessors: it identifies situations where overlapped instruction execution cannot safely proceed under the sequential ISA semantics and triggers handling such as stalling, forwarding, or cancellation. The provided evidence describes data hazards that stall decode, load/use hazards that can be handled by forwarding, and branch mispredictions that cancel in-flight instructions.

Overview

In a pipelined microprocessor, multiple instructions are overlapped to improve performance, even though the instruction set architecture (ISA) defines behavior as strict sequential execution over architectural state such as registers, the program counter, and memory. To keep pipelined execution faithful to those sequential ISA semantics, implementations use mechanisms such as interlocking and data forwarding. Hazard detection is the pipeline-control role that recognizes hazard conditions in this overlapped execution and initiates the appropriate response, such as stalling or using forwarding. [C1]

Role in pipelined execution

Pipelining creates the possibility that one instruction in an earlier stage depends on results or control decisions from instructions farther down the pipeline. The evidence describes these situations as hazard conditions that may require the pipeline to stop making progress for a cycle, or to cancel instructions after a branch misprediction. Such cycles can correspond to zero ISA-level progress while still preserving safety with respect to the sequential model. [C2]

Data hazards

A data hazard occurs when an instruction farther down the pipeline imposes a dependency on an instruction currently in decode. In the described STALL pipeline variant, no data forwarding is used; instead, an instruction can stall in the decode stage for up to three cycles whenever an instruction farther down the pipeline imposes a data hazard. [C3]

Forwarding can reduce the need for stalls. In the described LF variant, an additional forwarding path from the data-memory output to the pipeline register feeding the data-memory input allows some load/use hazards to be resolved by forwarding rather than stalling. [C4]

Control hazards and cancellation

The evidence also describes branch-prediction variants in which instructions may be canceled if a prediction is wrong. In the NT variant, branches are predicted not taken unless unconditional; in the BTFNT variant, lower-address branches are predicted taken and higher-address branches are predicted not taken unless unconditional. In both cases, up to two instructions must be canceled if the branch is mispredicted. [C5]

Verification implications

Formal verification of a pipelined processor must account for hazard behavior. Burch-Dill-style safety verification proves that each processor cycle has an effect consistent with some number of ISA steps, including k = 0, where the pipeline makes no ISA-level progress. The evidence explicitly gives pipeline stalls for hazard conditions and instruction cancellation after mispredicted branches as examples of such zero-progress cycles. [C2]

Safety alone is not enough: a processor that deadlocks, or does nothing forever, can satisfy a safety property. The evidence therefore states that liveness must also be verified to show that the processor cannot enter a state where it never makes forward progress, and specifically to show that the pipeline does not stall indefinitely. [C6]

Practical design pattern

Within the provided evidence, hazard handling appears as a combination of:

  • Stalling: holding an instruction in decode when a downstream instruction imposes a data hazard.
  • Forwarding: routing a value from a later pipeline point to avoid some stalls, including some load/use hazards.
  • Cancellation: removing in-flight instructions after a branch misprediction.

These mechanisms are part of the broader pipeline-control logic that preserves the ISA’s sequential semantics despite overlapped execution. [C1][C3][C4][C5]

LINKED ENTITIES

1 links
pipelining REQUIRES

CITATIONS

6 sources
6 citations
[1] C1: Pipelined processors overlap instructions, while interlocking and data forwarding help preserve sequential ISA semantics. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[2] C2: Pipeline stalls for hazard conditions and instruction cancellation after branch misprediction can be zero-progress cycles in safety verification. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[3] C3: In the STALL pipeline variant, an instruction stalls in decode for up to three cycles when a downstream instruction imposes a data hazard. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[4] C4: An added forwarding path can resolve some load/use hazards by forwarding rather than stalling. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[5] C5: Branch-prediction variants may cancel up to two instructions after a branch misprediction. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[6] C6: Liveness verification is needed to show that the processor cannot remain forever without forward progress and that the pipeline does not stall indefinitely. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5