{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,6]],"date-time":"2025-01-06T12:40:11Z","timestamp":1736167211138,"version":"3.32.0"},"publisher-location":"Berlin, Heidelberg","reference-count":21,"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\/bfb0031799","type":"book-chapter","created":{"date-parts":[[2005,12,11]],"date-time":"2005-12-11T06:59:01Z","timestamp":1134284341000},"page":"49-63","source":"Crossref","is-referenced-by-count":5,"title":["Modular verification of multipliers"],"prefix":"10.1007","author":[{"given":"Kavita","family":"Ravi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Abelardo","family":"Pardo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gary D.","family":"Hachtel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Fabio","family":"Somenzi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,25]]},"reference":[{"doi-asserted-by":"crossref","unstructured":"P. Ashar, A. Ghosh, and S. Devadas. Boolean satisfiability and equivalence checking using general binary decision diagrams. In Proceedings of the International Conference on Computer Design, pages 259\u2013264, Cambridge, MA, October 1991.","key":"4_CR1","DOI":"10.1109\/ICCD.1991.139893"},{"doi-asserted-by":"crossref","unstructured":"R. I. Bahar, E. A. Frohm, C. M. Gaona, G. D. Hachtel, E. Macii, A. Pardo, and F. Somenzi. Algebraic decision diagrams and their applications. In Proceedings of the International Conference on Computer-Aided Design, pages 188\u2013191, Santa Clara, CA, November 1993.","key":"4_CR2","DOI":"10.1109\/ICCAD.1993.580054"},{"doi-asserted-by":"crossref","unstructured":"K. S. Brace, R. L. Rudell, and R. E. Bryant. Efficient implementation of a BDD package. In Proceedings of the 27th Design Automation Conference, pages 40\u201345, Orlando, FL, June 1990.","key":"4_CR3","DOI":"10.1145\/123186.123222"},{"doi-asserted-by":"crossref","unstructured":"D. Brand. Verification of large synthesized designs. In Proceedings of the International Conference on Computer-Aided Design, pages 534\u2013537, Santa Clara, CA, November 1993.","key":"4_CR4","DOI":"10.1109\/ICCAD.1993.580110"},{"unstructured":"R. K. Brayton et al. VIS: A system for verification and synthesis. Technical Report UCB\/ERL M95\/104, Electronics Research Lab, Univ. of California, December 1995.","key":"4_CR5"},{"doi-asserted-by":"crossref","unstructured":"R. Bryant and Y.-A. Chen. Verification of arithmetic circuits with binary moment diagrams. In Proceedings of the Design Automation Conference, pages 535\u2013541, San Francisco, CA, June 1995.","key":"4_CR6","DOI":"10.1145\/217474.217583"},{"issue":"8","key":"4_CR7","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, August 1986.","journal-title":"IEEE Transactions on Computers"},{"issue":"2","key":"4_CR8","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, February 1991.","journal-title":"IEEE Transactions on Computers"},{"doi-asserted-by":"crossref","unstructured":"J. R. Burch. Using BDDs to verify multipliers. In Proceedings of the Design Automation Conference, pages 408\u2013412, San Francisco, CA, June 1991.","key":"4_CR9","DOI":"10.1145\/127601.127703"},{"doi-asserted-by":"crossref","unstructured":"E. M. Clarke, O. Grumberg, and D. E. Long. Model checking and abstraction. In Proceedings of the 19th ACM Symposium on Principles of Programming Languages, January 1992.","key":"4_CR10","DOI":"10.1145\/143165.143235"},{"doi-asserted-by":"crossref","unstructured":"E. M. Clarke, K. L. McMillan, X. Zhao, M. Fujita, and J. C.-Y. Yang. Spectral transforms for large boolean functions with applications to technology mapping. In Proceedings of the Design Automation Conference, pages 54\u201360, Dallas, TX, June 1993.","key":"4_CR11","DOI":"10.1145\/157485.164569"},{"key":"4_CR12","volume-title":"An Introduction to Algorithms","author":"T. H. Cormen","year":"1990","unstructured":"T. H. Cormen, C. E. Leiserson, and R. L. Rivest. An Introduction to Algorithms. McGraw-Hill, New York, 1990."},{"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.","key":"4_CR13","DOI":"10.1109\/ICCAD.1995.479995"},{"doi-asserted-by":"crossref","unstructured":"J. Jain, M. Abadir, J. Bitner, D. S. Fussell, and J. A. Abraham. IBDDs: An efficient functional representation for digital circuits. In Proceedings of the European Conference on Design Automation, pages 440\u2013446, Brussels, Belgium, March 1992.","key":"4_CR14","DOI":"10.1109\/EDAC.1992.205973"},{"doi-asserted-by":"crossref","unstructured":"J. Jain, R. Mukherjee, and M. Fujita. Advanced verification techniques based on learning. In Proceedings of the Design Automation Conference, pages 420\u2013426, San Francisco, CA, June 1995.","key":"4_CR15","DOI":"10.1145\/217474.217564"},{"doi-asserted-by":"crossref","unstructured":"U. Kebshull, E. Schubert, and W. Rosenstiel. Multilevel logic synthesis based on functional decision diagrams. In Proceedings of the European Conference on Design Automation, pages 43\u201347, Brussels, March 1992.","key":"4_CR16","DOI":"10.1109\/EDAC.1992.205890"},{"doi-asserted-by":"crossref","unstructured":"S. Kimura. Residue BDD and its application to the verification of arithmetic circuits. In Proceedings of the Design Automation Conference, pages 542\u2013545, San Francisco, CA, June 1995.","key":"4_CR17","DOI":"10.1145\/217474.217584"},{"doi-asserted-by":"crossref","unstructured":"Y.-T. Lai and S. Sastry. Edge-valued binary decision diagrams for multi-level hierarchical verification. In Proceedings of the Design Automation Conference, pages 608\u2013613, Anaheim, CA, June 1992.","key":"4_CR18","DOI":"10.1109\/DAC.1992.227813"},{"doi-asserted-by":"crossref","unstructured":"S.-I. Minato. Zero-suppressed BDDs for set manipulation in combinatorial problems. In Proceedings of the Design Automation Conference, pages 272\u2013277, Dallas, TX, June 1993.","key":"4_CR19","DOI":"10.1145\/157485.164890"},{"issue":"2","key":"4_CR20","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1007\/BF01384083","volume":"4","author":"B. Plessier","year":"1994","unstructured":"B. Plessier, G. Hachtel, and F. Somenzi. Extended BDDs: Trading off canonicity for structure in verification algorithms. Journal of Formal Methods in System Design, 4(2):167\u2013185, February 1994.","journal-title":"Journal of Formal Methods in System Design"},{"doi-asserted-by":"crossref","unstructured":"S. M. Reddy, W. Kunz, and D. K. Pradhan. Novel verification framework combining structural and OBDD methods in a synthesis environment. In Proceedings of the Design Automation Conference, pages 414\u2013419, San Francisco, CA, June 1995.","key":"4_CR21","DOI":"10.1145\/217474.328705"}],"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\/BFb0031799","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,6]],"date-time":"2025-01-06T12:11:30Z","timestamp":1736165490000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0031799"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540619376","9783540495673"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/bfb0031799","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}