{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T22:16:26Z","timestamp":1725574586265},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540203636"},{"type":"electronic","value":"9783540397243"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/978-3-540-39724-3_7","type":"book-chapter","created":{"date-parts":[[2011,1,7]],"date-time":"2011-01-07T21:15:55Z","timestamp":1294434955000},"page":"51-65","source":"Crossref","is-referenced-by-count":15,"title":["Instantiating Uninterpreted Functional Units and Memory System: Functional Verification of the VAMP"],"prefix":"10.1007","author":[{"given":"Sven","family":"Beyer","sequence":"first","affiliation":[]},{"given":"Chris","family":"Jacobi","sequence":"additional","affiliation":[]},{"given":"Daniel","family":"Kr\u00f6ning","sequence":"additional","affiliation":[]},{"given":"Dirk","family":"Leinenbach","sequence":"additional","affiliation":[]},{"given":"Wolfgang J.","family":"Paul","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"7_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/3-540-44798-9_26","volume-title":"Correct Hardware Design and Verification Methods","author":"C. Berg","year":"2001","unstructured":"Berg, C., Jacobi, C.: Formal verification of the VAMP floating point unit. In: Margaria, T., Melham, T.F. (eds.) CHARME 2001. LNCS, vol.\u00a02144, pp. 325\u2013339. Springer, Heidelberg (2001)"},{"key":"7_CR2","unstructured":"Brock, B., Hunt, W.A., Kaufmann, M.: The FM9001 microprocessor proof. Technical Report Technical Report 86, Computational Logic Inc. (1994)"},{"key":"7_CR3","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.R. Burch","year":"1994","unstructured":"Burch, J.R., Dill, D.L.: Automatic verification of pipelined microprocessors control. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol.\u00a0818, pp. 68\u201380. Springer, Heidelberg (1994)"},{"key":"7_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/BFb0031797","volume-title":"Formal Methods in Computer-Aided Design","author":"Y.-A. Chen","year":"1996","unstructured":"Chen, Y.-A., Clarke, E.M., Ho, P.-H., Hoskote, Y., Kam, T., Khaira, M., O\u2019Leary, J.W., Zhao, X.: Verification of all circuits in a floating-point unit using word-level model checking. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol.\u00a01166, pp. 19\u201333. Springer, Heidelberg (1996)"},{"key":"7_CR5","first-page":"23","volume-title":"Charme IFIP WG10.5","author":"W. Damm","year":"1997","unstructured":"Damm, W., Pnueli, A.: Verifying out-of-order executions. In: Charme IFIP WG10.5, Montreal, Canada, pp. 23\u201347. Chapman & Hall, Boca Raton (1997)"},{"key":"7_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/3-540-49519-3_5","volume-title":"Formal Methods in Computer-Aided Design","author":"A.P. Eiriksson","year":"1998","unstructured":"Eiriksson, A.P.: The formal design of 1M-gate ASICs. In: Gopalakrishnan, G.C., Windley, P. (eds.) FMCAD 1998. LNCS, vol.\u00a01522, pp. 49\u201363. Springer, Heidelberg (1998)"},{"key":"7_CR7","volume-title":"Computer Architecture:A Quantitative Approach","author":"J.L. Hennessy","year":"1996","unstructured":"Hennessy, J.L., Patterson, D.A.: Computer Architecture:A Quantitative Approach, 2nd edn. Morgan Kaufmann, San Mateo (1996)","edition":"2"},{"key":"7_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1007\/3-540-48683-6_7","volume-title":"Computer Aided Verification","author":"R. Hosabettu","year":"1999","unstructured":"Hosabettu, R., Srivas, M., Gopalakrishnan, G.: Proof of correctness of a processor with reorder buffer using the completion functions approach. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 47\u201359. Springer, Heidelberg (1999)"},{"key":"7_CR9","unstructured":"Institute of Electrical and Electronics Engineers. ANSI\/IEEE standard 754\u20131985, IEEE Standard for Binary Floating-Point Arithmetic (1985)"},{"key":"7_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1007\/3-540-45657-0_23","volume-title":"Computer Aided Verification","author":"C. Jacobi","year":"2002","unstructured":"Jacobi, C.: Formal verification of complex out-of-order pipelines by combining modelchecking and theorem-proving. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, p. 309. Springer, Heidelberg (2002)"},{"key":"7_CR11","unstructured":"Jacobi, C.: Formal Verificaton of a fully IEEE compliant floating point unit. PhD thesis, Saarland University, Germany (2002)"},{"key":"7_CR12","unstructured":"Kroening, D.: Formal Verification of Pipelined Microprocessors. PhD thesis, Saarland University, Computer Science Department (2001)"},{"key":"7_CR13","unstructured":"Kr\u00f6ning, D., M\u00fcller, S., Paul, W.: Proving the correctness of pipelined micro-architectures. In: 3ITG-\/GI\/GMM-Workshop Methoden und Beschreibungsprachen zur Modellierung und Verifikation von Schaltungen und System, pp. 89\u201398. VDE Verlag (2000)"},{"key":"7_CR14","doi-asserted-by":"crossref","unstructured":"Kr\u00f6ning, D., M\u00fcller, S., Paul, W.: Proving the correctness of processors with delayed branch using delayed PCs. pp. 579\u2013588 (2000)","DOI":"10.1007\/978-1-4757-6048-4_46"},{"key":"7_CR15","first-page":"810","volume-title":"Proc. of the 38th Design Automation Conference","author":"D. Kr\u00f6ning","year":"2001","unstructured":"Kr\u00f6ning, D., Paul, W.: Automated pipeline design. In: Proc. of the 38th Design Automation Conference, pp. 810\u2013815. ACM Press, New York (2001)"},{"key":"7_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0028738","volume-title":"Computer Aided Verification","author":"K. McMillan","year":"1998","unstructured":"McMillan, K.: Verification of an implementation of Tomasulo\u2019s algorithm by compositional model checking. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol.\u00a01427, Springer, Heidelberg (1998)"},{"key":"7_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/3-540-44798-9_17","volume-title":"Correct Hardware Design and Verification Methods","author":"K. McMillan","year":"2001","unstructured":"McMillan, K.: Parameterized verification of the FLASH cache coherence protocol by compositional model checking. In: Margaria, T., Melham, T.F. (eds.) CHARME 2001. LNCS, vol.\u00a02144, p. 179. Springer, Heidelberg (2001)"},{"key":"7_CR18","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-04267-0","volume-title":"Computer Architecture. Complexity and Correctness","author":"S.M. Mueller","year":"2000","unstructured":"Mueller, S.M., Paul, W.J.: Computer Architecture. Complexity and Correctness. Springer, Heidelberg (2000)"},{"key":"7_CR19","unstructured":"O\u2019Leary, J., Zhao, X., Gerth, R., Seger, C.-J.H.: Formally verifying IEEE compliance of floating-point hardware. Intel Technology Journal\u00a0Q1 (1999)"},{"key":"7_CR20","series-title":"LNAI","first-page":"748","volume-title":"Automated Deduction - CADE-11","author":"S. Owre","year":"1992","unstructured":"Owre, S., Shankar, N., Rushby, J.M.: PVS:A prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS (LNAI), vol.\u00a0607, pp. 748\u2013752. Springer, Heidelberg (1992)"},{"key":"7_CR21","doi-asserted-by":"crossref","first-page":"148","DOI":"10.1112\/S1461157000000176","volume":"1","author":"D.M. Russinoff","year":"1998","unstructured":"Russinoff, D.M.: A mechanically checked proof of IEEE compliance of the floating point multiplication, division and square root algorithms of the AMD-K7 processor. LMS Journal of Computation and Mathematics\u00a01, 148\u2013200 (1998)","journal-title":"LMS Journal of Computation and Mathematics"},{"key":"7_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/3-540-40922-X_3","volume-title":"Formal Methods in Computer-Aided Design","author":"D.M. Russinoff","year":"2000","unstructured":"Russinoff, D.M.: A case study in formal verification of register-transfer logic withACL2: The floating point adder of the AMD Athlon processor. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol.\u00a01954, pp. 3\u201336. Springer, Heidelberg (2000)"},{"key":"7_CR23","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"J. Sawada","year":"1997","unstructured":"Sawada, J., Hunt, W.A.: Trace table based approach for pipelined microprocessor verification. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, Springer, Heidelberg (1997)"},{"key":"7_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0028740","volume-title":"Computer Aided Verification","author":"J. Sawada","year":"1998","unstructured":"Sawada, J., Hunt, W.A.: Processor verification with precise exceptions and speculative execution. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol.\u00a01427, Springer, Heidelberg (1998)"},{"key":"7_CR25","doi-asserted-by":"crossref","unstructured":"Shen, X., Arvind, Rudolph, L.: CACHET: an adaptive cache coherence protocol for distributed shared-memory systems. In: International Conference on Supercomputing (1999)","DOI":"10.1145\/305138.305187"},{"key":"7_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/3-540-45251-6_4","volume-title":"FME 2001: Formal Methods for Increasing Software Productivity","author":"J. Stoy","year":"2001","unstructured":"Stoy, J., Shen, X., Arvind: Proofs of correctness of cache-coherence protocols. In: Oliveira, J.N., Zave, P. (eds.) FME 2001. LNCS, vol.\u00a02021, p. 43. Springer, Heidelberg (2001)"},{"key":"7_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/3-540-48153-2_5","volume-title":"Correct Hardware Design and Verification Methods","author":"M.N. Velev","year":"1999","unstructured":"Velev, M.N., Bryant, R.E.: Superscalar processor verification using efficient reductions of the logic of equality with uninterpreted functions to propositional logic. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol.\u00a01703, pp. 37\u201353. Springer, Heidelberg (1999)"},{"key":"7_CR28","volume-title":"DAC","author":"M.N. Velev","year":"2000","unstructured":"Velev, M.N., Bryant, R.E.: Formal verification of superscale microprocessors with multicycle functional units, exception, and branch prediction. In: DAC, ACM, New York (2000)"}],"container-title":["Lecture Notes in Computer Science","Correct Hardware Design and Verification Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-39724-3_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,7]],"date-time":"2019-06-07T14:03:34Z","timestamp":1559916214000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-39724-3_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540203636","9783540397243"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-39724-3_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2003]]}}}