Pipeline Flushing

Concept

Pipeline flushing is a mechanism used to stop fetching new instructions while allowing instructions already in a processor pipeline to complete, thereby bringing the pipeline to an empty or quiescent state. In Burch-Dill correspondence checking, flushing is used to compute an abstraction from an arbitrary pipelined state to the architectural state that would result after all partially executed instructions finish.

First seen 5/26/2026

Last seen 5/26/2026

Evidence 3 chunks

Wiki v1

WIKI

Definition

Pipeline flushing is the process of driving a pipelined processor for enough cycles to complete instructions already present in the pipeline while preventing new instructions from being fetched. In the Burch-Dill verification setting, an arbitrary pipeline state may contain partially executed instructions in its pipeline registers; flushing for a sufficiently large number of steps n guarantees that those partially executed instructions have completed, yielding the corresponding architectural state. [C1]

Role in Burch-Dill correspondence checking

READ FULL ARTICLE →

NEIGHBORHOOD

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

explore full graph →

RELATIONSHIPS

3 connections

Burch-Dill Correspondence Checking ← uses 100% 2e

Burch-Dill verification computes the abstraction function by symbolically simulating the processor as it flushes instructions out of the pipeline.

PIPE Pipeline Processor ← uses 100% 2e

PIPE uses pipeline flushing to bring the pipeline to a quiescent state during exceptional conditions.

Abstraction Function ← uses 100% 2e

The abstraction function is computed by flushing instructions from the pipeline during symbolic simulation.

LINKED ENTITIES

1 links

UCLID5 models_pipeline_flushing The evidence describes implementing Burch-Dill verification with UCLID5 and adding a force_flush control signal to the pipeline framework.

CITATIONS

6 sources

6 citations — click to expand

[1] A general pipeline state can contain partially executed instructions, and flushing for sufficiently many steps maps it to the architectural state after those instructions complete. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5

[2] Burch-Dill verification computes the abstraction function by symbolically simulating the microprocessor as it flushes instructions out of the pipeline. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5

[3] The correspondence check compares a normal PIPE step followed by flushing with flushing followed by a SEQ step, and accepts either one sequential step of effect or no architectural effect. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5

[4] In the UCLID5 framework, flushing is implemented with a force_flush control signal that stops fetching new instructions and injects bubbles into the decode stage until the pipeline is empty. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5

[5] Pipeline registers in the UCLID5 model can initialize, stall, inject a bubble, or load their input on each step. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5

[6] Correct flushing should not stall the fetch stage in a way that fixes the program counter, and in the SW variant flushing must be disabled for one cycle during dynamic popq conversion. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5