Much automatic pipeline verification research of the last decade has been based on some form of "Burch-Dill flushing". In this work, we study synchronization-at-retirement, an alternative formulation of correctness for pipelines, in which the proof obligations can also be verified automatically but have significantly-reduced verification complexity compared to flushing. We present an approach for systematically generating invariants, addressing one of the most difficult aspects of pipeline verification. We prove that synchronization-at-retirement and the Burch-Dill flushing correctness statements are equivalent under reasonable side conditions. Finally, we provide experimental evidence of the reduced complexity of our approach for a pipelined processor with ALU operations, memory operations, stalls, jumps, and branch prediction.