{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T20:35:30Z","timestamp":1761597330375,"version":"3.40.2"},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540631668"},{"type":"electronic","value":"9783540691952"}],"license":[{"start":{"date-parts":[[1997,1,1]],"date-time":"1997-01-01T00:00:00Z","timestamp":852076800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/3-540-63166-6_12","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T23:13:11Z","timestamp":1330297991000},"page":"95-106","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["Automatic datapath extraction for efficient usage of HDD"],"prefix":"10.1007","author":[{"given":"Gila","family":"Kamhi","sequence":"first","affiliation":[]},{"given":"Osnat","family":"Weissberg","sequence":"additional","affiliation":[]},{"given":"Limor","family":"Fix","sequence":"additional","affiliation":[]},{"given":"Ziv","family":"Binyamini","sequence":"additional","affiliation":[]},{"given":"Ze'ev","family":"Shtadler","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,7]]},"reference":[{"key":"12_CR1","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, IEEE Computer Society Press"},{"key":"12_CR2","unstructured":"E.Clarke, X.Zhao. Word Level Symbolic Model Checking, CMU-CS-95-161"},{"key":"12_CR3","doi-asserted-by":"crossref","unstructured":"Y.Chen, E.Clarke, Pei-Hsin Ho, Y. Hoskote, T. Kam, M. Khaira, J. O'Leary, X. Zhao. Verification of All Circuits in a Floating-Point Unit Using Word-Level Model Checking, In Proceedings of the International Conference on Formal Methods in Computer-Aided Design, November 1996","DOI":"10.1007\/BFb0031797"},{"key":"12_CR4","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"},{"issue":"8","key":"12_CR5","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"c-35","author":"R.E. Bryant","year":"1986","unstructured":"R.E. Bryant. Graph-based Algorithms for Boolean Function Manipulation. IEEE Transactions on Computers, c-35(8):677\u2013691, Aug. 1986","journal-title":"IEEE Transactions on Computers"},{"key":"12_CR6","doi-asserted-by":"crossref","unstructured":"Laurent Arditi. *BMDs Can Delay the Use of Theorem Proving for Verifying Arithmetic Assembly Instructions, In Proceedings of the International Conference on Formal Methods in Computer-Aided Design, November 1996","DOI":"10.1007\/BFb0031798"},{"key":"12_CR7","doi-asserted-by":"crossref","unstructured":"R.Hojati, R.K.Brayton. Automatic Datapath Abstraction In Hardware Systems, In Proceedings of the International Conference on Computer-Aided Verification Conference, 1995","DOI":"10.1007\/3-540-60045-0_43"},{"key":"12_CR8","unstructured":"A.Aziz et.al. HSIS: A BDD-Based Environment for Formal Verification, In Proceedings of the 31st Design Automation Conference, IEEE Computer Society Press"},{"key":"12_CR9","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 International Conference on Computer-Aided-Design, pages 78\u201382, San Jose, CA, November 1995.","DOI":"10.1109\/ICCAD.1995.479995"},{"key":"12_CR10","doi-asserted-by":"crossref","unstructured":"K.Ravi, A.Pardo, G.Hachtel, F.Somenzi. Modular Verification of Multipliers. In Proceedings of the International Conference on Formal Methods in Computer-Aided Design, Palo Alto, CA, November 1996","DOI":"10.1007\/BFb0031799"},{"key":"12_CR11","doi-asserted-by":"crossref","unstructured":"M.Fujita. Verification of Arithmetic Circuits by Comparing Two Similiar Circuits. In Proceedings of the International Conference on Computer-Aided Verification, 1996","DOI":"10.1007\/3-540-61474-5_66"},{"key":"12_CR12","unstructured":"K.S.Brace, R.L.Rudell, and R.E.Bryant. Efficient Implementation of a BDD Package. In Proceedings of the Design Automation Conference, pages 535\u2013541, San Francisco, CA, June 1995."},{"key":"12_CR13","unstructured":"E.M.Clarke, M. Khaira, and X.Zhao. Word Level 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."},{"issue":"10","key":"12_CR14","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":"12_CR15","volume-title":"Note on the Complexity of Binary Moment Diagram Representations","author":"R. Enders","year":"1994","unstructured":"R. Enders. Note on the Complexity of Binary Moment Diagram Representations. unpublished paper, Siemens AG, Munich Germany, 1994."},{"key":"12_CR16","unstructured":"K.L.McMillan. Symbolic Model Checking, Kluwer Academic Publishers."}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-63166-6_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,21]],"date-time":"2025-03-21T23:38:53Z","timestamp":1742600333000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-63166-6_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540631668","9783540691952"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/3-540-63166-6_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1997]]},"assertion":[{"value":"7 June 2005","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}