{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,29]],"date-time":"2025-09-29T12:06:56Z","timestamp":1759147616799},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540619376"},{"type":"electronic","value":"9783540495673"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/bfb0031797","type":"book-chapter","created":{"date-parts":[[2005,12,11]],"date-time":"2005-12-11T06:59:01Z","timestamp":1134284341000},"page":"19-33","source":"Crossref","is-referenced-by-count":22,"title":["Verification of all circuits in a floating-point unit using word-level model checking"],"prefix":"10.1007","author":[{"given":"Yirng-An","family":"Chen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Edmund","family":"Clarke","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pei-Hsin","family":"Ho","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yatin","family":"Hoskote","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Timothy","family":"Kam","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Manpreet","family":"Khaira","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"John","family":"O'Leary","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xudong","family":"Zhao","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,25]]},"reference":[{"issue":"10","key":"2_CR1","doi-asserted-by":"crossref","first-page":"925","DOI":"10.1109\/TC.1968.226439","volume":"C-17","author":"D. E. Atkins","year":"1968","unstructured":"D. E. Atkins. Higher-radix division using estimates of the divisor and partial remainders. IEEE Transactions on Computers, C-17(10):925\u2013934, October 1968.","journal-title":"IEEE Transactions on Computers"},{"key":"2_CR2","doi-asserted-by":"crossref","unstructured":"R.E. I. Beer, S. Ben-David, C. Eisner, and Avner Landver. Rulebase: an industry-oriented formal verification tool. In Proceedings of the 33rd Design Automation Conference. IEEE Computer Society Press, June 1996.","DOI":"10.1145\/240518.240642"},{"key":"2_CR3","doi-asserted-by":"crossref","unstructured":"R. E. Bryant and Y. A. Chen. Verification of arithmetic functions with binary moment diagrams. In Proceedings of the 32nd ACM\/IEEE Design Automation Conference, pages 535\u2013541. IEEE Computer Society Press, June 1995.","DOI":"10.1145\/217474.217583"},{"issue":"2","key":"2_CR4","doi-asserted-by":"crossref","first-page":"205","DOI":"10.1109\/12.73590","volume":"40","author":"R. E. Bryant","year":"1991","unstructured":"R. E. Bryant. On the complexity of vlsi implementations and graph representations of boolean functions with application to integer multiplication. IEEE Transactions on Computers, 40(2):205\u2013213, 1991.","journal-title":"IEEE Transactions on Computers"},{"key":"2_CR5","doi-asserted-by":"crossref","unstructured":"R.E. Bryant. Bit-level analysis of an srt divider circuit. Technical report, Carnegie Mellon University, 1995.","DOI":"10.21236\/ADA294842"},{"key":"2_CR6","doi-asserted-by":"crossref","unstructured":"M. Birman, A. Samuels, G. Chu, T. Chuk, L. Hu, J. McLeod, and J. Barnes. Developing the wtl3170\/3171 sparc floating-point coprocessors. IEEE Micro, pages 55\u201364, February 1990.","DOI":"10.1109\/40.46769"},{"key":"2_CR7","doi-asserted-by":"crossref","unstructured":"J. Bannur and A. Varma. The vlsi implementation of a square root algorithm. In Proceedings of the 7th Symposium on Computer Arithmetic, pages 159\u2013165. IEEE Computer Society Press, 1985.","DOI":"10.1109\/ARITH.1985.6158929"},{"key":"2_CR8","doi-asserted-by":"crossref","unstructured":"E. M. Clarke, M. Fujita, and X. Zhao. Hybrid decision diagrams \u2014 overcoming the limitations of mtbdds and bmds. In Proceedings of the 1995 Proceedings of the IEEE International Conference on Computer Aided Design, pages 159\u2013163. IEEE Computer Society Press, November 1995.","DOI":"10.21236\/ADA296684"},{"key":"2_CR9","unstructured":"E. M. Clarke, M. Khaira, and X. Zhao. Word level symbolic model checking \u2014 a new approach for verifying arithmetic circuits. In Proceedings of the 33rd ACM\/IEEE Design Automation Conference. IEEE Computer Society Press, June 1996."},{"key":"2_CR10","doi-asserted-by":"crossref","unstructured":"E. M. Clarke, K. McMillan, X. Zhao, M. Fujita, and J. Yang. Spectral transforms for large boolean functions with applications to technology mapping. In Proceedings of the 30th ACM\/IEEE Design Automation Conference, pages 54\u201360. IEEE Computer Society Press, June 1993.","DOI":"10.1145\/157485.164569"},{"issue":"4","key":"2_CR11","first-page":"129","volume":"20","author":"T. Coe","year":"1995","unstructured":"T. Coe. Inside the pentium fdiv bug. Dr. Dobbs Journal, 20(4):129\u2013135, April 1995.","journal-title":"Dr. Dobbs Journal"},{"key":"2_CR12","doi-asserted-by":"crossref","unstructured":"C. V. Frieman. Statistical analysis of certain arithmetic binary division algorithms. IRE Transaction, pages 91\u2013103, January 1961.","DOI":"10.1109\/JRPROC.1961.287780"},{"key":"2_CR13","doi-asserted-by":"crossref","unstructured":"K. Hamaguchi, A. Morita, and S. Yajima. Efficient construction of binary moment diagrams for verifying arithmetic circuits. In Proceedings of the 1995 IEEE International Conference on Computer Aided Design, pages 78\u201382, November 1995.","DOI":"10.1109\/ICCAD.1995.479995"},{"key":"2_CR14","unstructured":"J. L. Hennessy and D. A. Patterson. Computer Architecture: A Quantitative Approach. Morgan Kaufmann, 1996."},{"key":"2_CR15","doi-asserted-by":"crossref","unstructured":"R. P. Kurshan and L. Lamport. Verification of a multiplier: 64 bits and beyond. In C. Courcoubetis, editor, Proceedings of the Fifth Workshop on Computer-Aided Verification, June\/July 1993.","DOI":"10.1007\/3-540-56922-7_14"},{"key":"2_CR16","doi-asserted-by":"crossref","unstructured":"K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"2_CR17","doi-asserted-by":"crossref","unstructured":"J. O'Leary, M. Leeser, J. Hickey, and M. Aagaard. Non-restoring integer square root: a case study in design by principled optimization. In Proceedings of the Theorem Provers in Circuit Design '94, volume 901 of Lecture Notes in Computer Science. Springer-Verlag, 1995.","DOI":"10.1007\/3-540-59047-1_42"},{"key":"2_CR18","doi-asserted-by":"crossref","unstructured":"R. Rudell. Dynamic variable ordering for ordered binary decision diagrams. In Intl. Conf. on Computer Aided Design, Santa Clara, Ca., November 1993.","DOI":"10.1109\/ICCAD.1993.580029"},{"key":"2_CR19","unstructured":"H. P. Sharangpani and M. L. Barton. Statistical analysis of floating point flaw in the pentium processor(1994). Technical report, Intel Corporation, November 1994."},{"key":"2_CR20","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1007\/BF01383955","volume":"4","author":"D. Verkest","year":"1994","unstructured":"D. Verkest, L. Claesen, and H. De Man. A proof of the nonrestoring division algorithm and its implementation on an alu. Formal Methods in System Design, 4:5\u201331, January 1994.","journal-title":"Formal Methods in System Design"}],"container-title":["Lecture Notes in Computer Science","Formal Methods in Computer-Aided Design"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0031797","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,7,21]],"date-time":"2021-07-21T07:34:57Z","timestamp":1626852897000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0031797"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540619376","9783540495673"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/bfb0031797","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}