{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,11]],"date-time":"2026-05-11T11:19:41Z","timestamp":1778498381448,"version":"3.51.4"},"reference-count":9,"publisher":"Wiley","license":[{"start":{"date-parts":[[2010,2,1]],"date-time":"2010-02-01T00:00:00Z","timestamp":1264982400000},"content-version":"unspecified","delay-in-days":4414,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["LMS J. Comput. Math."],"published-print":{"date-parts":[[1998]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We describe a mechanically verified proof of correctness of the floating point multiplication, division, and square root instructions of the AMD-K7 microprocessor. The instructions are implemented in hardware and represented here by register-transfer level specifications, the primitives of which are logical operations on bit vectors. On the other hand, the statements of correctness, derived from IEEE Standard 754, are arithmetic in nature and considerably more abstract. Therefore, we begin by developing a theory of bit vectors and their role in floating point representations and rounding. We then present the hardware model and a rigorous proof of its correctness. All of our definitions, lemmas and theorems have been formally encoded in the ACL2 logic, and every step in the proof has been mechanically checked with the ACL2 prover.<\/jats:p>","DOI":"10.1112\/s1461157000000176","type":"journal-article","created":{"date-parts":[[2013,8,6]],"date-time":"2013-08-06T11:42:38Z","timestamp":1375789358000},"page":"148-200","source":"Crossref","is-referenced-by-count":95,"title":["A Mechanically Checked Proof of IEEE Compliance of the Floating Point Multiplication, Division and Square Root Algorithms of the AMD-K7<sup>\u2122<\/sup> Processor"],"prefix":"10.1112","volume":"1","author":[{"given":"David M.","family":"Russinoff","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"311","published-online":{"date-parts":[[2010,2,1]]},"reference":[{"key":"S1461157000000176_ref002","volume-title":"A computational logic handbook","author":"Boyer","year":"1988"},{"key":"S1461157000000176_ref008","article-title":"\u2018A mechanically checked proof of IEEE compliance of the AMD-K5 floating point square root microcode\u2019","author":"Russinoff","journal-title":"Formal Methods in System Design"},{"key":"S1461157000000176_ref006","doi-asserted-by":"publisher","DOI":"10.1109\/12.713311"},{"key":"S1461157000000176_ref007","unstructured":"7. Oberman S.F. , \u2018Division and square root for the AMD-K7 FPU\u2019 (Advanced Micro Devices, Milpitas, CA, March 1997)."},{"key":"S1461157000000176_ref001","doi-asserted-by":"publisher","DOI":"10.1147\/rd.111.0034"},{"key":"S1461157000000176_ref004","article-title":"a new approach for verifying arithmetic circuits\u2019","author":"Clarke","year":"1995","journal-title":"\u2018Word level symbolic model checking:"},{"key":"S1461157000000176_ref009","volume-title":"Common Lisp The Language","author":"Steele","year":"1990"},{"key":"S1461157000000176_ref005","unstructured":"5. Institute of Electrical and Electronic Engineers, \u2018IEEE Standard for Binary Floating Point Arithmetic\u2019, Std. 754-1985, (IEEE, New York, NY, 1985)."},{"key":"S1461157000000176_ref003","article-title":"\u2018Verification of arithmetic functions with binary moment diagrams\u2019","author":"Bryant","year":"1994","journal-title":"Technical Report CMU-CS-94-160"}],"container-title":["LMS Journal of Computation and Mathematics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S1461157000000176","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,6]],"date-time":"2019-06-06T16:03:48Z","timestamp":1559837028000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S1461157000000176\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"references-count":9,"alternative-id":["S1461157000000176"],"URL":"https:\/\/doi.org\/10.1112\/s1461157000000176","relation":{},"ISSN":["1461-1570"],"issn-type":[{"value":"1461-1570","type":"electronic"}],"subject":[],"published":{"date-parts":[[1998]]}}}