{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,13]],"date-time":"2025-11-13T18:11:39Z","timestamp":1763057499363,"version":"3.37.0"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642026577"},{"type":"electronic","value":"9783642026584"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-02658-4_32","type":"book-chapter","created":{"date-parts":[[2009,6,22]],"date-time":"2009-06-22T11:00:16Z","timestamp":1245668416000},"page":"414-429","source":"Crossref","is-referenced-by-count":55,"title":["Replacing Testing with Formal Verification in Intel $^{\\scriptsize\\circledR}$ CoreTM i7 Processor Execution Engine Validation"],"prefix":"10.1007","author":[{"given":"Roope","family":"Kaivola","sequence":"first","affiliation":[]},{"given":"Rajnish","family":"Ghughal","sequence":"additional","affiliation":[]},{"given":"Naren","family":"Narasimhan","sequence":"additional","affiliation":[]},{"given":"Amber","family":"Telfer","sequence":"additional","affiliation":[]},{"given":"Jesse","family":"Whittemore","sequence":"additional","affiliation":[]},{"given":"Sudhindra","family":"Pandav","sequence":"additional","affiliation":[]},{"given":"Anna","family":"Slobodov\u00e1","sequence":"additional","affiliation":[]},{"given":"Christopher","family":"Taylor","sequence":"additional","affiliation":[]},{"given":"Vladimir","family":"Frolov","sequence":"additional","affiliation":[]},{"given":"Erik","family":"Reeber","sequence":"additional","affiliation":[]},{"given":"Armaghan","family":"Naik","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"32_CR1","unstructured":"First the Tick, Now the Tock: Next Generation Intel\u00ae Microarchitecture (Nehalem) Intel Corp., http:\/\/www.intel.com\/technology\/architecture-silicon\/next-gen\/whitepaper.pdf"},{"key":"32_CR2","unstructured":"IA-32 Intel\u00ae Architecture Software Developer\u2019s Manual, Vol. 2A and 2B. Intel Corp."},{"key":"32_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/3-540-40922-X_17","volume-title":"Formal Methods in Computer-Aided Design","author":"M.D. Aagaard","year":"2000","unstructured":"Aagaard, M.D., Jones, R.B., Melhan, T.F., O\u2019Leary, J.W., Seger, C.-J.H.: A methodology for large-scale hardware verification. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol.\u00a01954, pp. 263\u2013282. Springer, Heidelberg (2000)"},{"key":"32_CR4","doi-asserted-by":"crossref","first-page":"806","DOI":"10.1145\/1391469.1391675","volume-title":"DAC 2008: Proc. of the 45th annual conf. on Design automation","author":"R. Beers","year":"2008","unstructured":"Beers, R.: Pre-RTL formal verification: an Intel experience. In: DAC 2008: Proc. of the 45th annual conf. on Design automation, pp. 806\u2013811. ACM, New York (2008)"},{"key":"32_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/11513988_2","volume-title":"Computer Aided Verification","author":"B. Bentley","year":"2005","unstructured":"Bentley, B.: Validating a modern microprocessor. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 2\u20134. Springer, Heidelberg (2005)"},{"key":"32_CR6","doi-asserted-by":"crossref","unstructured":"Flaisher, A., Gluska, A., Singerman, E.: Case study: Integrating FV and DV in the verification of the Intel CoreTM 2 Duo microprocessor. In: FMCAD, Formal Methods in Computer-Aided Design, pp. 192\u2013195 (2007)","DOI":"10.1109\/FAMCAD.2007.38"},{"issue":"2","key":"32_CR7","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1017\/S0956796805005757","volume":"16","author":"J. Grundy","year":"2006","unstructured":"Grundy, J., Melhan, T., O\u2019Leary, J.: A reflective functional language for hardware design and theorem proving. Journal of Functional Programming\u00a016(2), 157\u2013196 (2006)","journal-title":"Journal of Functional Programming"},{"key":"32_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/3-540-63475-4_1","volume-title":"Formal Hardware Verification","author":"S. Hazelhurst","year":"1997","unstructured":"Hazelhurst, S., Seger, C.-J.H.: Symbolic trajectory evaluation. In: Kropf, T. (ed.) Formal Hardware Verification. LNCS, vol.\u00a01287, pp. 3\u201378. Springer, Heidelberg (1997)"},{"key":"32_CR9","unstructured":"Hinton, G., Sager, D., Upton, M., Boggs, D., Carmean, D., Kyker, A., Roussel, P.: The microarchitecture of the Pentium\u00ae 4 processor. Intel. Technology Journal\u00a0Q1 (February 2001)"},{"key":"32_CR10","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-1101-4","volume-title":"Symbolic Simulation Methods for Industrial Formal Verification","author":"R.B. Jones","year":"2002","unstructured":"Jones, R.B.: Symbolic Simulation Methods for Industrial Formal Verification. Kluwer Academic Publishers, Dordrecht (2002)"},{"key":"32_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"170","DOI":"10.1007\/11513988_19","volume-title":"Computer Aided Verification","author":"R. Kaivola","year":"2005","unstructured":"Kaivola, R.: Formal verification of Pentium\u00ae 4 components with symbolic simulation and inductive invariants. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 170\u2013184. Springer, Heidelberg (2005)"},{"key":"32_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"338","DOI":"10.1007\/3-540-44659-1_21","volume-title":"Theorem Proving in Higher Order Logics","author":"R. Kaivola","year":"2000","unstructured":"Kaivola, R., Aagaard, M.D.: Divider circuit verification with model checking and theorem proving. In: Aagaard, M.D., Harrison, J. (eds.) TPHOLs 2000. LNCS, vol.\u00a01869, pp. 338\u2013355. Springer, Heidelberg (2000)"},{"key":"32_CR13","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1007\/s10009-002-0081-6","volume":"4","author":"R. Kaivola","year":"2003","unstructured":"Kaivola, R., Kohatsu, K.: Proof engineering in the large: formal verification of Pentium\u00ae 4 floating-point divider. Int\u2019l J. on Software Tools for Technology Transfer\u00a04, 323\u2013334 (2003)","journal-title":"Int\u2019l J. on Software Tools for Technology Transfer"},{"key":"32_CR14","doi-asserted-by":"crossref","unstructured":"Kaivola, R., Naik, A.: Formal verification of high-level conformance with symbolic simulation. In: HLDVT, High-Level Design Validation and Test, pp. 153\u2013159 (2005)","DOI":"10.1109\/HLDVT.2005.1568830"},{"key":"32_CR15","doi-asserted-by":"crossref","unstructured":"Kaivola, R., Narasimhan, N.: Formal verification of the Pentium\u00ae 4 floating-point multiplier. In: DATE, Design, Automation and Test in Europe, pp. 20\u201327 (2002)","DOI":"10.1109\/DATE.2002.998245"},{"key":"32_CR16","unstructured":"O\u2019Leary, J.: Using a reflective functional language for hardware verification and theorem proving. In: Third Workshop on Applied Semantics (APPSEM 2005), September 12\u201315, 2005, pp. 12\u201315 (2005)"},{"key":"32_CR17","unstructured":"O\u2019Leary, J.W., Zhao, X., Gerth, R., Seger, C.-J.H.: Formally verifying IEEE compliance of floating-point hardware. Intel. Technology Journal\u00a0Q1 (Feburary 1999)"},{"key":"32_CR18","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511811326","volume-title":"ML for the Working Programmer,","author":"L. Paulson","year":"1996","unstructured":"Paulson, L.: ML for the Working Programmer. Cambridge University Press, Cambridge (1996)"},{"key":"32_CR19","first-page":"1","volume-title":"DAC 2003: Proceedings of the 40th conference on Design automation","author":"T. Schubert","year":"2003","unstructured":"Schubert, T.: High level formal verification of next-generation microprocessors. In: DAC 2003: Proceedings of the 40th conference on Design automation, pp. 1\u20136. ACM Press, New York (2003)"},{"issue":"2","key":"32_CR20","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/BF01383966","volume":"6","author":"C.-J.H. Seger","year":"1995","unstructured":"Seger, C.-J.H., Bryant, R.E.: Formal verification by symbolic evaluation of partially-ordered trajectories. Formal Methods in System Design\u00a06(2), 147\u2013189 (1995)","journal-title":"Formal Methods in System Design"},{"key":"32_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-70952-7_1","volume-title":"Formal Methods: Applications and Technology","author":"A. Slobodova","year":"2007","unstructured":"Slobodova, A.: Challenges for formal verification in industrial setting. In: Brim, L., Haverkort, B.R., Leucker, M., van de Pol, J. (eds.) FMICS 2006 and PDMC 2006. LNCS, vol.\u00a04346, pp. 1\u201322. Springer, Heidelberg (2007)"},{"key":"32_CR22","doi-asserted-by":"crossref","unstructured":"Slobodova, A.: Formal verification of hardware support for advanced encryption standard. In: FMCAD, Formal Methods in Computer-Aided Design, pp. 61\u201364 (2008)","DOI":"10.1109\/FMCAD.2008.ECP.12"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-02658-4_32","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,10]],"date-time":"2025-02-10T07:58:28Z","timestamp":1739174308000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-02658-4_32"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642026577","9783642026584"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-02658-4_32","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}