{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,2]],"date-time":"2025-03-02T05:45:50Z","timestamp":1740894350479,"version":"3.38.0"},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540204619"},{"type":"electronic","value":"9783540398936"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/978-3-540-39893-6_13","type":"book-chapter","created":{"date-parts":[[2011,1,7]],"date-time":"2011-01-07T15:35:57Z","timestamp":1294414557000},"page":"206-225","source":"Crossref","is-referenced-by-count":3,"title":["Modeling SystemC Fixed-Point Arithmetic in HOL"],"prefix":"10.1007","author":[{"given":"Behzad","family":"Akbarpour","sequence":"first","affiliation":[]},{"given":"Sofi\u00e8ne","family":"Tahar","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"13_CR1","doi-asserted-by":"crossref","unstructured":"Aagaard, M.D., Seger, C.-J.H.: The Formal Verification of a Pipelined Double- Precision IEEE Floating-Point Multiplier. In: International Conference on Computer Aided Design, San Francisco, CA, USA, November 1995, pp. 7\u201310 (1995)","DOI":"10.1109\/ICCAD.1995.479878"},{"key":"13_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1007\/3-540-47884-1_11","volume-title":"Integrated Formal Methods","author":"B. Akbarpour","year":"2002","unstructured":"Akbarpour, B., Tahar, S., Dekdouk, A.: Formalization of Cadence SPW Fixed- Point Arithmetic in HOL. In: Butler, M., Petre, L., Sere, K. (eds.) IFM 2002. LNCS, vol.\u00a02335, pp. 185\u2013204. Springer, Heidelberg (2002)"},{"issue":"5","key":"13_CR3","doi-asserted-by":"publisher","first-page":"611","DOI":"10.1109\/32.24710","volume":"SE-15","author":"G. Barrett","year":"1989","unstructured":"Barrett, G.: Formal Methods Applied to a Floating Point Number System. IEEE Transactions on Software Engineering\u00a0SE-15(5), 611\u2013621 (1989)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"13_CR4","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":"13_CR5","first-page":"129","volume-title":"Theorem Provers in Circuit Design","author":"R. Boulton","year":"1992","unstructured":"Boulton, R., Gordon, A., Gordon, M., Harrison, J., Herbert, J., Van-Tassel, J.: Experience with Embedding Hardware Description Languages in HOL. In: Theorem Provers in Circuit Design, pp. 129\u2013156. North-Holland, Amsterdam (1992)"},{"key":"13_CR6","unstructured":"Carreno, V.A.: Interpretation of IEEE-854 Floating-Point Standard and Definition in the HOL System. NASA Technical Memorandum 110189 (September 1995)"},{"key":"13_CR7","series-title":"A Guide to Platform-Based Design","volume-title":"Surviving the SoC Revolution","author":"H. Chang","year":"1999","unstructured":"Chang, H., et al.: Surviving the SoC Revolution. A Guide to Platform-Based Design. Kluwer Academic Publishers, Boston (1999)"},{"key":"13_CR8","first-page":"1","volume":"Q2","author":"M. Cornea-Hasegan","year":"1998","unstructured":"Cornea-Hasegan, M.: Proving the IEEE Correctness of Iterative Floating-Point Square Root, Divide, and Remainder Algorithms. Intel Technology Journal Q2, 1\u201311 (1998)","journal-title":"Intel Technology Journal"},{"key":"13_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"488","DOI":"10.1007\/BFb0028769","volume-title":"Computer Aided Verification","author":"Y.-A. Chen","year":"1998","unstructured":"Chen, Y.-A., Bryant, R.E.: Verification of Floating Point Adders. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 488\u2013499. Springer, Heidelberg (1998)"},{"key":"13_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/3-540-44755-5_13","volume-title":"Theorem Proving in Higher Order Logics","author":"M. Daumas","year":"2001","unstructured":"Daumas, M., Rideau, L., Thry, L.: A Generic Library for Floating-Point Numbers and its Application to Exact Computing. In: Boulton, R.J., Jackson, P.B. (eds.) TPHOLs 2001. LNCS, vol.\u00a02152, pp. 169\u2013184. Springer, Heidelberg (2001)"},{"key":"13_CR11","volume-title":"Introduction to HOL: A Theorem Proving Environment for Higher-Order Logic","author":"M.J.C. Gordon","year":"1993","unstructured":"Gordon, M.J.C., Melham, T.F.: Introduction to HOL: A Theorem Proving Environment for Higher-Order Logic. Cambridge University Press, Cambridge (1993)"},{"key":"13_CR12","unstructured":"Harrison, J.R.: Theorem Proving with the Real Numbers. Technical Report 408, University of Cambridge Computer Laboratory, New Museums Site, Pembroke Street, Cambridge, CB2 3QG, UK (December 1996)"},{"issue":"3","key":"13_CR13","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1023\/A:1008712907154","volume":"16","author":"J.R. Harrison","year":"2000","unstructured":"Harrison, J.R.: Floating-Point Verification in HOL Light: The Exponential Function. Formal Methods in System Design\u00a016(3), 271\u2013305 (2000)","journal-title":"Formal Methods in System Design"},{"key":"13_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/3-540-48256-3_9","volume-title":"Theorem Proving in Higher Order Logics","author":"J.R. Harrison","year":"1999","unstructured":"Harrison, J.R.: A Machine-Checked Theory of Floating-Point Arithmetic. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Th\u00e9ry, L. (eds.) TPHOLs 1999. LNCS, vol.\u00a01690, pp. 113\u2013130. Springer, Heidelberg (1999)"},{"key":"13_CR15","unstructured":"IEEE, Standard for Binary Floating-Point Arithmetic, ANSI\/IEEE Standard 754- 1985, The Institute of Electrical and Electronic Engineers, Inc., 345 East 47th Street, New York, NY 10017, USA (1985)"},{"key":"13_CR16","unstructured":"IEEE, Standard for Radix-Independent Floating-Point Arithmetic, ANSI\/IEEE Std 854-1987, The Institute of Electrical and Electronic Engineers, Inc., 345 East 47th Street, New York, NY 10017, USA (1987)"},{"key":"13_CR17","doi-asserted-by":"crossref","unstructured":"Inacio, C., Ombres, D.: The DSP Decision: Fixed Point or Floating? IEEE Spectrum, 0018-9234 (September 1996)","DOI":"10.1109\/6.535397"},{"key":"13_CR18","unstructured":"Intel Inc., Pentium Processors, Statistical Analysis of Floating-Point Flaw, Intel White Paper, Sec. 3 (November 1994)"},{"key":"13_CR19","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1145\/307988.307989","volume":"4","author":"C. Kern","year":"1999","unstructured":"Kern, C., Greenstreet, M.: Formal Verification in Hardware Design: A Survey. ACM Transactions on Design Automation of Electronic Systems\u00a04, 123\u2013193 (1999)","journal-title":"ACM Transactions on Design Automation of Electronic Systems"},{"key":"13_CR20","doi-asserted-by":"crossref","unstructured":"Leeser, M., O\u2019Leary, J.: Verification of a Subtractive Radix-2 Square Root Algorithm and Implementation. In: International Conference on Computer Design, Cambridge, MA, USA, October 1995, pp. 526\u2013531 (1995)","DOI":"10.1109\/ICCD.1995.528918"},{"key":"13_CR21","first-page":"1","volume":"Q1","author":"J. O Leary","year":"1999","unstructured":"O Leary, J., Zhao, X., Gerth, R., Seger, C.-J.H.: Formally Verifying IEEE Compliance of Floating-Point Hardware. Intel Technology Journal\u00a0Q1, 1\u201314 (1999)","journal-title":"Intel Technology Journal"},{"key":"13_CR22","unstructured":"Melham, T.F.: The HOL pred sets Library. University of Cambridge, Computer Laboratory (February 1992)"},{"key":"13_CR23","doi-asserted-by":"crossref","unstructured":"Melham, T.: Higher Order Logic and Hardware Verification. Cambridge Tracts in Theoretical Computer Science\u00a031. Cambridge University Press (1993)","DOI":"10.1017\/CBO9780511569845"},{"key":"13_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1007\/BFb0031800","volume-title":"Formal Methods in Computer-Aided Design","author":"P.S. Miner","year":"1996","unstructured":"Miner, P.S., Leathrum, J.F.: Verification of IEEE Compliant Subtractive Division Algorithms. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol.\u00a01166, pp. 64\u201378. Springer, Heidelberg (1996)"},{"key":"13_CR25","unstructured":"Miner, P.S.: Defining the IEEE-854 Floating-Point Standard in PVS. Technical Memorandum 110167, NASA, Langley Research Center, Hampton, VA 236810001, USA (June 1995)"},{"key":"13_CR26","doi-asserted-by":"publisher","first-page":"913","DOI":"10.1109\/12.713311","volume":"47","author":"J.S. Moore","year":"1998","unstructured":"Moore, J.S., Lynch, T., Kaufmann, M.: A Mechanically Checked Proof of the Correctness of the Kernel of the AMD5K86 Floating-Point Division Algorithm. IEEE Transactions on Computers\u00a047, 913\u2013926 (1998)","journal-title":"IEEE Transactions on Computers"},{"key":"13_CR27","series-title":"Complexity and Correctness","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-04267-0","volume-title":"Computer Architecture","author":"S.M. Mueller","year":"2000","unstructured":"Mueller, S.M., Paul, W.J.: Computer Architecture. Complexity and Correctness. Springer, Heidelberg (2000)"},{"key":"13_CR28","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 with ACL2: 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":"13_CR29","unstructured":"Signal Processing WorkSystem (SPW) User\u2019s Guide, Cadence Design Systems, Inc. (July 1999)"},{"key":"13_CR30","unstructured":"Swan, S.: An Introduction to System Level Modeling in SystemC 2.0, Cadence Design Systems, Inc. (May 2001)"},{"key":"13_CR31","unstructured":"http:\/\/www.systemc.org\/"},{"key":"13_CR32","unstructured":"CoCentric TM System Studio User\u2019s Guide, Synopsys, Inc., USA (August 2001)"},{"key":"13_CR33","unstructured":"CoCentric Fixed-Point Designer User\u2019s Guide, Synopsys, Inc., USA (August 2002)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-39893-6_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,1]],"date-time":"2025-03-01T14:26:26Z","timestamp":1740839186000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-39893-6_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540204619","9783540398936"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-39893-6_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2003]]}}}