We present a novel method for pipeline verification using SMT
solvers. It is based on a non-deterministic ``mother pipeline''
machine (\mam) that abstracts the instruction set architecture
(\isa). The \mam\ vs.~\isa\ correctness theorem splits naturally
into a large number of simple subgoals. This theorem reduces
proving the correctness of a given pipelined implementation of the
\isa\ to verifying that each of its transitions can be modeled as a
sequence of \mam\ state transitions.