We present a systematic approach to decompose and incrementally build
the proof of correctness of pipelined microprocessors. The central idea
is to construct the abstraction function using completion functions, one
per unfinished instruction, each of which specify the effect (on the
observables) of completing the instruction. In addition to avoiding
term-size and case explosion as could happen for deep and complex
pipelines during flushing and helping localize errors, our method can
also handle stages with iterative loops. The technique is illustrated on
pipelined- as well as a superscalar pipelined implementations of a
subset of the DLX architecture.