Much automatic pipeline verification research of the last decade has been based on some form of "Burch-Dill flushing" [BD94]. In this work, we study synchronization-at-retirement, an alternative formulation of correctness for pipelines. In this formulation, 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 establish by proof 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. © Springer-Verlag 2004.
CITATION STYLE
Aagaard, M. D., Day, N. A., & Jones, R. B. (2004). Synchronization-at-retirement for pipeline verification. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 3312, 113–127. https://doi.org/10.1007/978-3-540-30494-4_9
Mendeley helps you to discover research relevant for your work.