{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,23]],"date-time":"2025-02-23T05:13:35Z","timestamp":1740287615864,"version":"3.37.3"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540237389"},{"type":"electronic","value":"9783540304944"}],"license":[{"start":{"date-parts":[[2004,1,1]],"date-time":"2004-01-01T00:00:00Z","timestamp":1072915200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-30494-4_9","type":"book-chapter","created":{"date-parts":[[2010,6,29]],"date-time":"2010-06-29T18:42:14Z","timestamp":1277836934000},"page":"113-127","source":"Crossref","is-referenced-by-count":2,"title":["Synchronization-at-Retirement for Pipeline Verification"],"prefix":"10.1007","author":[{"given":"Mark D.","family":"Aagaard","sequence":"first","affiliation":[]},{"given":"Nancy A.","family":"Day","sequence":"additional","affiliation":[]},{"given":"Robert B.","family":"Jones","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"3","key":"9_CR1","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/s10009-002-0087-0","volume":"4","author":"M.D. Aagaard","year":"2003","unstructured":"Aagaard, M.D., Cook, B., Day, N.A., Jones, R.B.: A framework for superscalar microprocessor correctness statements. Software Tools for Technology Transfer\u00a04(3), 298\u2013312 (2003)","journal-title":"Software Tools for Technology Transfer"},{"key":"9_CR2","unstructured":"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)"},{"key":"9_CR3","doi-asserted-by":"crossref","unstructured":"Arons, T., Pnueli, A.: Verifying Tomasulo\u2019s algorithm by refinement. Technical report, Dept. of Computer Science, Weizmann Institute (October 1998)","DOI":"10.1109\/ICVD.1999.745165"},{"key":"9_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"487","DOI":"10.1007\/3-540-46419-0_33","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T. Arons","year":"2000","unstructured":"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.\u00a01785, pp. 487\u2013502. Springer, Heidelberg (2000)"},{"issue":"3","key":"9_CR5","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1109\/40.768501","volume":"19","author":"Arvind","year":"1999","unstructured":"Arvind, Shen, X.: Using term rewriting systems to design and verify processors. IEEE Micro\u00a019(3), 36\u201346 (1999)","journal-title":"IEEE Micro"},{"key":"9_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"515","DOI":"10.1007\/978-3-540-27813-9_49","volume-title":"Computer Aided Verification","author":"C. Barrett","year":"2004","unstructured":"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.\u00a03114, pp. 515\u2013518. Springer, Heidelberg (2004)"},{"key":"9_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"68","DOI":"10.1007\/3-540-58179-0_44","volume-title":"Computer Aided Verification","author":"J. Burch","year":"1994","unstructured":"Burch, J., Dill, D.: Automatic verification of pipelined microprocessor control. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol.\u00a0818, pp. 68\u201380. Springer, Heidelberg (1994)"},{"key":"9_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/BFb0031808","volume-title":"Formal Methods in Computer-Aided Design","author":"C. Barrett","year":"1996","unstructured":"Barrett, C., Dill, D., Levitt, J.: Validity checking for combinations of theories with equality. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol.\u00a01166, pp. 187\u2013201. Springer, Heidelberg (1996)"},{"key":"9_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"346","DOI":"10.1007\/BFb0031820","volume-title":"Formal Methods in Computer-Aided Design","author":"A. Fox","year":"1996","unstructured":"Fox, A., Harman, N.: Algebraic models of correctness for microprocessors. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol.\u00a01166, pp. 346\u2013361. Springer, Heidelberg (1996)"},{"key":"9_CR10","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1016\/S1567-8326(03)00041-9","volume":"57","author":"A. Fox","year":"2003","unstructured":"Fox, A., Harman, N.: Algebraic models of correctness for abstract pipelines. The Journal of Algebraic and Logic Programming\u00a057, 71\u2013107 (2003)","journal-title":"The Journal of Algebraic and Logic Programming"},{"issue":"2","key":"9_CR11","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1023\/A:1024716316140","volume":"23","author":"R. Hosabettu","year":"2003","unstructured":"Hosabettu, R., Gopalakrishnan, G., Srivas, M.K.: Formal verification of a complex pipelined processor. Formal Methods in System Design\u00a023(2), 171\u2013213 (2003)","journal-title":"Formal Methods in System Design"},{"key":"9_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"396","DOI":"10.1007\/3-540-44585-4_40","volume-title":"Computer Aided Verification","author":"R. Jhala","year":"2001","unstructured":"Jhala, R., McMillan, K.L.: Microarchitecture verification by compositional model checking. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 396\u2013410. Springer, Heidelberg (2001)"},{"key":"9_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1007\/3-540-36126-X_9","volume-title":"Formal Methods in Computer-Aided Design","author":"S.K. Lahiri","year":"2002","unstructured":"Lahiri, S.K., Seshia, S.A., Bryant, R.E.: Modeling and verification of out-of-order microprocessors in UCLID. In: Aagaard, M.D., O\u2019Leary, J.W. (eds.) FMCAD 2002. LNCS, vol.\u00a02517, pp. 142\u2013158. Springer, Heidelberg (2002)"},{"key":"9_CR14","unstructured":"http:\/\/www.cs.uwaterloo.ca\/~nday\/microbox"},{"key":"9_CR15","unstructured":"Milner, R.: An algebraic definition of simulation between programs. In: Joint Conf. on AI, pp. 481\u2013489. British Computer Society (1971)"},{"key":"9_CR16","doi-asserted-by":"crossref","unstructured":"Manolios, P., Srinivasan, S.K.: Automatic verification of safety and liveness for Xscale-like processor models using web refinements. In: DATE, pp. 168\u2013175 (2004)","DOI":"10.1109\/DATE.2004.1268844"},{"key":"9_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1007\/3-540-49519-3_23","volume-title":"Formal Methods in Computer-Aided Design","author":"A. Pnueli","year":"1998","unstructured":"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.\u00a01522, pp. 351\u2013368. Springer, Heidelberg (1998)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods in Computer-Aided Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-30494-4_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,22]],"date-time":"2025-02-22T09:56:57Z","timestamp":1740218217000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-30494-4_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540237389","9783540304944"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-30494-4_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}