Part of the book series:Lecture Notes in Computer Science ((LNCS,volume 3312))
Included in the following conference series:
622Accesses
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 studysynchronization-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.
This is a preview of subscription content,log in via an institution to check access.
Access this chapter
Subscribe and save
- Get 10 units per month
- Download Article/Chapter or eBook
- 1 Unit = 1 Article or 1 Chapter
- Cancel anytime
Buy Now
- Chapter
- JPY 3498
- Price includes VAT (Japan)
- eBook
- JPY 5719
- Price includes VAT (Japan)
- Softcover Book
- JPY 7149
- Price includes VAT (Japan)
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Aagaard, M.D., Cook, B., Day, N.A., Jones, R.B.: A framework for superscalar microprocessor correctness statements. Software Tools for Technology Transfer 4(3), 298–312 (2003)
Aagaard, M.D., Day, N.A., Jones, R.B.: Equivalence of sync-at-fetch and syncat-retire correctness for pipeline circuits. Technical Report CS2004-31, University of Waterloo, School of Computer Science (September 2004)
Arons, T., Pnueli, A.: Verifying Tomasulo’s algorithm by refinement. Technical report, Dept. of Computer Science, Weizmann Institute (October 1998)
Arons, T., Pnueli, A.: A comparison of two verification methods for speculative instruction execution with exceptions. In: Schwartzbach, M.I., Graf, S. (eds.) TACAS 2000. LNCS, vol. 1785, pp. 487–502. Springer, Heidelberg (2000)
Arvind, Shen, X.: Using term rewriting systems to design and verify processors. IEEE Micro 19(3), 36–46 (1999)
Barrett, C., Berezin, S.: CVC Lite: A new implementation of the cooperating validity checker. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 515–518. Springer, Heidelberg (2004)
Burch, J., Dill, D.: Automatic verification of pipelined microprocessor control. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 68–80. Springer, Heidelberg (1994)
Barrett, C., Dill, D., Levitt, J.: Validity checking for combinations of theories with equality. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol. 1166, pp. 187–201. Springer, Heidelberg (1996)
Fox, A., Harman, N.: Algebraic models of correctness for microprocessors. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol. 1166, pp. 346–361. Springer, Heidelberg (1996)
Fox, A., Harman, N.: Algebraic models of correctness for abstract pipelines. The Journal of Algebraic and Logic Programming 57, 71–107 (2003)
Hosabettu, R., Gopalakrishnan, G., Srivas, M.K.: Formal verification of a complex pipelined processor. Formal Methods in System Design 23(2), 171–213 (2003)
Jhala, R., McMillan, K.L.: Microarchitecture verification by compositional model checking. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 396–410. Springer, Heidelberg (2001)
Lahiri, S.K., Seshia, S.A., Bryant, R.E.: Modeling and verification of out-of-order microprocessors in UCLID. In: Aagaard, M.D., O’Leary, J.W. (eds.) FMCAD 2002. LNCS, vol. 2517, pp. 142–158. Springer, Heidelberg (2002)
Milner, R.: An algebraic definition of simulation between programs. In: Joint Conf. on AI, pp. 481–489. British Computer Society (1971)
Manolios, P., Srinivasan, S.K.: Automatic verification of safety and liveness for Xscale-like processor models using web refinements. In: DATE, pp. 168–175 (2004)
Pnueli, A., Arons, T.: Verification of data-insensitive circuits: An in-orderretirement case study. In: Gopalakrishnan, G.C., Windley, P. (eds.) FMCAD 1998. LNCS, vol. 1522, pp. 351–368. Springer, Heidelberg (1998)
Author information
Authors and Affiliations
Electrical and Computer Engineering, University of Waterloo, Waterloo, ON, Canada
Mark D. Aagaard
Computer Science, University of Waterloo,
Nancy A. Day
Strategic CAD Labs, Intel Corporation, Hillsboro, OR, USA
Robert B. Jones
- Mark D. Aagaard
You can also search for this author inPubMed Google Scholar
- Nancy A. Day
You can also search for this author inPubMed Google Scholar
- Robert B. Jones
You can also search for this author inPubMed Google Scholar
Editor information
Editors and Affiliations
Computer Science Department, University of British Columbia,
Alan J. Hu
IBM Austin Research Laboratory, 11400 Burnet Rd, MS 904-6H004, TX 78758-3493, Austin, USA
Andrew K. Martin
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Aagaard, M.D., Day, N.A., Jones, R.B. (2004). Synchronization-at-Retirement for Pipeline Verification. In: Hu, A.J., Martin, A.K. (eds) Formal Methods in Computer-Aided Design. FMCAD 2004. Lecture Notes in Computer Science, vol 3312. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30494-4_9
Download citation
Publisher Name:Springer, Berlin, Heidelberg
Print ISBN:978-3-540-23738-9
Online ISBN:978-3-540-30494-4
eBook Packages:Springer Book Archive
Share this paper
Anyone you share the following link with will be able to read this content:
Sorry, a shareable link is not currently available for this article.
Provided by the Springer Nature SharedIt content-sharing initiative