Name
Abstract | ||
|---|---|---|
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. |
Year | DOI | Venue |
|---|---|---|
2004 | 10.1007/978-3-540-30494-4_9 | Lecture Notes in Computer Science |
Keywords | Field | DocType |
branch prediction | Synchronization,Pipeline transport,Computer science,Program counter,Correctness,Computer Aided Design,Circuit design,Real-time computing,Theoretical computer science,Formal methods,Branch predictor | Conference |
Volume | ISSN | Citations |
3312 | 0302-9743 | 3 |
PageRank | References | Authors |
0.45 | 17 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Mark D. Aagaard | 1 | 119 | 8.91 |
| Nancy A. Day | 2 | 243 | 21.26 |
| Robert B. Jones | 3 | 434 | 39.17 |