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

Burch-Dill verification relies on an abstraction function α that maps a microprocessor pipeline state to an architectural state. The cited Y86-64 verification work describes computing this abstraction by symbolically simulating the processor while it flushes instructions out of the pipeline. [C2]

For a general pipeline state P₀, flushing is used to define:

α(P₀) = S

where S is the architectural state obtained after all partially executed instructions in P₀ have been completed. [C1]

The correspondence check compares two symbolic simulation sequences:

σₐ = Init(P₀), Pipe, Flush(n), SaveAP(Sᵃ)
σᵦ = Init(P₀), Flush(n), Xfer, SaveS(S₀ᵇ), Seq, SaveS(S₁ᵇ)

The first sequence performs one normal pipeline step and then flushes. The second sequence flushes first, transfers the architectural state to the sequential model, and then performs one sequential step. The verification condition is:

Sᵃ = S₁ᵇ  ∨  Sᵃ = S₀ᵇ

The Sᵃ = S₁ᵇ case corresponds to a pipeline cycle that fetches an instruction that is eventually completed and should match one step of the sequential model. The Sᵃ = S₀ᵇ case corresponds to a cycle with no architectural effect, such as a stall or a fetched instruction later canceled because of a mispredicted branch. [C3]

Implementation mechanism

In the UCLID5 Y86-64 verification framework, flushing required extending the pipeline model with an input control signal named force_flush. When asserted, flushing stops the fetching of new instructions while completing instructions already in the pipeline. The implementation injects a bubble into the decode stage each cycle until the pipeline is empty. This dynamically injects nop instructions and sets the status register to SBUB, indicating a pipeline bubble. [C4]

The same framework models pipeline registers as elements that, on each step, can initialize, stall, inject a bubble, or load their input. This register behavior provides the basic modeling support needed for bubble injection during flushing. [C5]

Subtleties

The cited implementation identifies two important subtleties:

1. Flushing should not stall the fetch stage by forcing the program counter to remain fixed. If the fetch stage were stalled in that way, a ret or jXX instruction could be prevented from setting the program counter to the return or jump destination. [C6]
2. In the SW variant, the pipeline stalls for one cycle to dynamically convert a popq instruction into a two-instruction sequence; flushing must be disabled for that cycle. [C6]

Verification significance

Pipeline flushing is central to correspondence checking because it lets the verifier compare a pipelined implementation against a sequential instruction-set model without manually defining the full abstraction from in-flight pipeline state to architectural state. For a single-issue microprocessor, the verification task becomes proving equivalence between a simulation that flushes and then executes one ISA instruction, and a simulation that executes one normal pipeline cycle and then flushes. [C2]