{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,22]],"date-time":"2025-03-22T04:18:41Z","timestamp":1742617121896,"version":"3.40.2"},"publisher-location":"Berlin, Heidelberg","reference-count":8,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540600459"},{"type":"electronic","value":"9783540494133"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/3-540-60045-0_35","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T17:36:30Z","timestamp":1330277790000},"page":"1-3","source":"Crossref","is-referenced-by-count":0,"title":["Multipliers and dividers: Insights on arithmetic circuit verification (extended abstract)"],"prefix":"10.1007","author":[{"given":"Randal E.","family":"Bryant","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"issue":"No.10","key":"1_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, \u201cHigher-radix division using estimates of the divisor and partial remainder,\u201d IEEE Transactions on Computers, Vol. C-17, No. 10 (October, 1968), pp. 925\u2013934.","journal-title":"IEEE Transactions on Computers"},{"issue":"No.2","key":"1_CR2","doi-asserted-by":"crossref","first-page":"205","DOI":"10.1109\/12.73590","volume":"40","author":"R. E. Bryant","year":"1991","unstructured":"R. E. Bryant, \u201cOn the complexity of VLSI implementations and graph representations of Boolean functions with application to integer multiplication,\u201d IEEE Transactions on Computers, Vol. 40, No. 2 (February, 1991), pp. 205\u2013213.","journal-title":"IEEE Transactions on Computers"},{"issue":"No.3","key":"1_CR3","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1145\/136035.136043","volume":"24","author":"R. E. Bryant","year":"1992","unstructured":"R. E. Bryant, \u201cSymbolic Boolean manipulation with ordered binary decision diagrams,\u201d ACM Computing Surveys, Vol. 24, No. 3 (September, 1992), pp. 293\u2013318.","journal-title":"ACM Computing Surveys"},{"key":"1_CR4","doi-asserted-by":"crossref","unstructured":"R. E. Bryant, and Y.-A. Chen, \u201cVerification of arithmetic circuits with binary moment diagrams,\u201d 32nd Design Automation Conference, 1995.","DOI":"10.1145\/217474.217583"},{"key":"1_CR5","unstructured":"E. M. Clarke, J. R. Burch, K. L. McMillan, and D. L. Dill, \u201cSequential circuit verification using symbolic model checking,\u201d 27th Design Automation Conference, June 1990."},{"key":"1_CR6","doi-asserted-by":"crossref","unstructured":"Y.-T. Lai, and S. Sastry, \u201cEdge-valued binary decision diagrams for multi-level hierarchical verification,\u201d 29th Design Automation Conference, June, 1992, pp. 608\u2013613.","DOI":"10.1109\/DAC.1992.227813"},{"key":"1_CR7","unstructured":"H. P. Sharangpani, M. L. Barton, \u201cStatistical analysis of floating point flaw in the Pentium processor(1994),\u201d Intel Technical Report, Nov. 30, 1994."},{"issue":"No.1","key":"1_CR8","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/BF01383955","volume":"4","author":"D. Verkest","year":"1994","unstructured":"D. Verkest, L. Claesen, and H. DeMan, \u201cA proof of the nonrestoring division algorithm and its implementation on an ALU,\u201d Formal Methods in System Design, Vol. 4, No. 1 (January, 1994), pp. 5\u201332.","journal-title":"Formal Methods in System Design"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-60045-0_35.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,21]],"date-time":"2025-03-21T22:51:38Z","timestamp":1742597498000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-60045-0_35"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540600459","9783540494133"],"references-count":8,"URL":"https:\/\/doi.org\/10.1007\/3-540-60045-0_35","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1995]]}}}