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
In formal verification of pipelined processors, the goal is to prove that pipelined execution faithfully implements the sequential semantics of the instruction set architecture (ISA). The ISA model describes the effect of each instruction on architectural state, including registers, the program counter, and memory, under strict sequential execution. [C2]
Burch and Dill's approach uses pipeline flushing as part of an automatically computed abstraction function, denoted α, that maps concrete microprocessor states to architectural ISA states. Their key contribution was showing that this abstraction function could be computed by symbolically simulating the microprocessor while it flushes instructions out of the pipeline. [C3]
Use in correspondence checking
For a single-issue microprocessor, the verification task is described as proving equivalence between two symbolic simulations:
- flush the pipeline, then execute one instruction in the ISA model; and
- operate the pipeline for one normal cycle, then flush the pipeline.
The source identifies this verification method as correspondence checking. [C4]
Verification implications
The same source explains that Burch-Dill verification establishes a safety property: every cycle of processor operation has an effect consistent with some number of ISA steps, including zero steps. Zero-step behavior can occur when a pipeline stalls for a hazard condition or when instructions are canceled because of a mispredicted branch. However, safety alone does not establish liveness; additional verification is needed to show the processor cannot remain forever in a non-progressing state. [C5]