Pipeline Flushing

Technique

Pipeline flushing is a technique in pipelined microprocessor designs that drains or removes in-flight instructions to bring the pipeline to a quiescent architectural state. In Burch-Dill-style correspondence checking, symbolic simulation of this flushing process is used to automatically compute an abstraction function from microprocessor states to ISA architectural states.

First seen 5/25/2026

Last seen 5/25/2026

Evidence 1 chunks

Wiki v1

WIKI

Overview

Pipeline flushing is a technique used in pipelined microprocessor designs to remove instructions from the pipeline and bring the processor to a quiescent state. The cited evidence describes this as a mechanism that most pipelined processor designs already provide, because it is needed when handling exceptional conditions such as halting or interrupts. [C1]

Role in formal verification

READ FULL ARTICLE →

NEIGHBORHOOD

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

explore full graph →

LINKED ENTITIES

1 links

Burch-Dill Correspondence Checking USES Extracted graph relationship

CITATIONS

5 sources

5 citations — click to expand

[1] Pipeline flushing brings a pipelined processor to a quiescent state and is commonly needed for exceptional conditions such as halting or interrupts. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5

[2] ISA models describe architectural state including registers, program counter, and memory under strict sequential instruction execution. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5

[3] Burch and Dill showed that an abstraction function from microprocessor states to architectural states can be computed by symbolically simulating pipeline flushing. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5

[4] For a single-issue microprocessor, correspondence checking compares a flush-then-ISA-step simulation with a normal-cycle-then-flush simulation. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5

[5] Burch-Dill verification proves a safety property but must be supplemented with liveness verification to rule out non-progressing deadlock-like behavior. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5