{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T10:35:44Z","timestamp":1725532544755},"publisher-location":"Dordrecht","reference-count":19,"publisher":"Springer Netherlands","isbn-type":[{"type":"print","value":"9781402097133"},{"type":"electronic","value":"9781402097140"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-1-4020-9714-0_17","type":"book-chapter","created":{"date-parts":[[2009,5,22]],"date-time":"2009-05-22T13:44:14Z","timestamp":1242999854000},"page":"257-272","source":"Crossref","is-referenced-by-count":0,"title":["A New Verification Technique for\u00a0Custom-Designed Components at\u00a0the\u00a0Arithmetic Bit Level"],"prefix":"10.1007","author":[{"given":"Evgeny","family":"Pavlenko","sequence":"first","affiliation":[]},{"given":"Markus","family":"Wedler","sequence":"additional","affiliation":[]},{"given":"Dominik","family":"Stoffel","sequence":"additional","affiliation":[]},{"given":"Wolfgang","family":"Kunz","sequence":"additional","affiliation":[]},{"given":"Oliver","family":"Wienand","sequence":"additional","affiliation":[]},{"given":"Evgeny","family":"Karibaev","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"17_CR1","doi-asserted-by":"crossref","unstructured":"G.\u00a0Audemard, P.\u00a0Bertoli, A.\u00a0Cimatti, A.\u00a0Kornilowicz, and R.\u00a0Sebastiani. A SAT-based approach for solving formulas over boolean and linear mathematical propositions. In Proc. International Conference on Automated Deduction (CAD), pages 195\u2013210, 2002.","DOI":"10.1007\/3-540-45620-1_17"},{"key":"17_CR2","unstructured":"Boolector. \n                    http:\/\/fmv.jku.at\/boolector\n                    \n                  ."},{"key":"17_CR3","doi-asserted-by":"publisher","first-page":"535","DOI":"10.1145\/217474.217583","volume-title":"DAC \u201995: Proceedings of the 32nd ACM\/IEEE Conference on Design Automation","author":"R.E. Bryant","year":"1995","unstructured":"R.E. Bryant and Y.-A. Chen. Verification of arithmetic circuits with binary moment diagrams. In DAC \u201995: Proceedings of the 32nd ACM\/IEEE Conference on Design Automation, pages 535\u2013541. Assoc. Comput. Mach., New York, 1995."},{"key":"17_CR4","doi-asserted-by":"crossref","unstructured":"D.\u00a0Chai and A.\u00a0Kuehlmann. A fast pseudo-boolean constraint solver. In Proc. International Design Automation Conference (DAC), pages 830\u2013835, 2003.","DOI":"10.1145\/775832.776041"},{"key":"17_CR5","doi-asserted-by":"crossref","unstructured":"M.\u00a0Ciesielski, Z.\u00a0Zeng, P.\u00a0Kalla, and B.\u00a0Rouzeyre. Taylor expansion diagrams: A compact, canonical representation with applications to symbolic verification. In Proc. International Conference on Design, Automation and Test in Europe (DATE), pages 285\u2013291, 2002.","DOI":"10.1109\/DATE.2002.998286"},{"key":"17_CR6","doi-asserted-by":"crossref","unstructured":"R.\u00a0Drechsler, B.\u00a0Becker, A.\u00a0Sarabi, M.\u00a0Theobald, and M.\u00a0Perkowski. Efficient representation and manipulation of switching functions based on ordered Kronecker functional decision diagrams. In Proc. International Design Automation Conference (DAC), pages 415\u2013419, 1994.","DOI":"10.1145\/196244.196444"},{"key":"17_CR7","doi-asserted-by":"crossref","unstructured":"H.\u00a0Ganzinger, G.\u00a0Hagen, R.\u00a0Nieuwenhuis, A.\u00a0Oliveras, and C.\u00a0Tinelli. DPLL(T): Fast decision procedures. In Proc. International Conference on Computer Aided Verification (CAV), pages 26\u201337, July 2004.","DOI":"10.1007\/978-3-540-27813-9_14"},{"key":"17_CR8","doi-asserted-by":"crossref","unstructured":"K.\u00a0Hamaguchi, A.\u00a0Morita, and S.\u00a0Yajima. Efficient construction of binary moment diagrams for verifying arithmetic circuits. In Proc. International Conference on Computer-Aided Design (ICCAD), pages 78\u201382, November 1995.","DOI":"10.1109\/ICCAD.1995.479995"},{"key":"17_CR9","doi-asserted-by":"crossref","unstructured":"U.\u00a0Kebschull, E.\u00a0Schubert, and W.\u00a0Rostenstiel. Multi-level logic based on functional decision diagrams. In Proc. European Design Automation Conference (EDAC), pages 43\u201347, 1992.","DOI":"10.1109\/EDAC.1992.205890"},{"key":"17_CR10","doi-asserted-by":"crossref","first-page":"398","DOI":"10.1109\/ASPDAC.2008.4483983","volume-title":"ASP-DAC \u201908: Proceedings of the 2008 Conference on Asia and South Pacific Design Automation","author":"U. Krautz","year":"2008","unstructured":"U.\u00a0Krautz, C.\u00a0Jacobi, K.\u00a0Weber, M.\u00a0Pflanz, W.\u00a0Kunz, and M.\u00a0Wedler. Verifying full-custom multipliers by boolean equivalence checking and an arithmetic bit level proof. In ASP-DAC \u201908: Proceedings of the 2008 Conference on Asia and South Pacific Design Automation, pages 398\u2013403. IEEE Comput. Soc., Los Alamitos, 2008."},{"key":"17_CR11","unstructured":"Onespin Solutions GmbH, Germany. OneSpin 360MV. \n                    www.onespin-solutions.com\n                    \n                  ."},{"issue":"7","key":"17_CR12","doi-asserted-by":"publisher","first-page":"1320","DOI":"10.1109\/TCAD.2006.888277","volume":"26","author":"N. Shekhar","year":"2007","unstructured":"N. Shekhar, P. Kalla, and F. Enescu. Equivalence verification of polynomial datapaths using ideal membership testing. IEEE Transactions on Computer-Aided Design, 26(7):1320\u20131330, 2007.","journal-title":"IEEE Transactions on Computer-Aided Design"},{"key":"17_CR13","unstructured":"Spear. \n                    http:\/\/www.domagoj-babic.com\n                    \n                  ."},{"issue":"5","key":"17_CR14","doi-asserted-by":"publisher","first-page":"586","DOI":"10.1109\/TCAD.2004.826548","volume":"23","author":"D. Stoffel","year":"2004","unstructured":"D. Stoffel and W. Kunz. Equivalence checking of arithmetic circuits on the arithmetic bit level. IEEE Transactions on Computer-Aided Design, 23(5):586\u2013597, 2004.","journal-title":"IEEE Transactions on Computer-Aided Design"},{"issue":"10","key":"17_CR15","doi-asserted-by":"publisher","first-page":"1401","DOI":"10.1109\/TC.2007.1073","volume":"56","author":"S. Vasudevan","year":"2007","unstructured":"S. Vasudevan, V. Viswanath, R.W. Sumners, and J.A. Abraham. Automatic verification of arithmetic circuits in RTL using stepwise refinement of term rewriting systems. IEEE Transactions on Computers, 56(10):1401\u20131414, 2007.","journal-title":"IEEE Transactions on Computers"},{"key":"17_CR16","doi-asserted-by":"crossref","unstructured":"Y.\u00a0Watanabe, N.\u00a0Homma, T.\u00a0Aoki, and T.\u00a0Higuchi. Application of symbolic computer algebra to arithmetic circuit verification. In Proc. International Conference on Computer Design (ICCD), pages 25\u201332, October 2007.","DOI":"10.1109\/ICCD.2007.4601876"},{"issue":"11","key":"17_CR17","doi-asserted-by":"publisher","first-page":"1909","DOI":"10.1109\/TCAD.2007.906458","volume":"26","author":"M. Wedler","year":"2007","unstructured":"M. Wedler, D. Stoffel, R. Brinkmann, and W. Kunz. A normalization method for arithmetic data-path verification. IEEE Transactions on Computer-Aided Design, 26(11):1909\u20131922, 2007.","journal-title":"IEEE Transactions on Computer-Aided Design"},{"key":"17_CR18","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1145\/330855.330957","volume-title":"GLSVLSI \u201900: Proceedings of the 10th Great Lakes symposium on VLSI","author":"S. Wefel","year":"2000","unstructured":"S. Wefel and P. Molitor. Prove that a faulty multiplier is faulty!? In GLSVLSI \u201900: Proceedings of the 10th Great Lakes symposium on VLSI, pages 43\u201346. Assoc. Comput. Mach., New York, 2000."},{"key":"17_CR19","doi-asserted-by":"crossref","unstructured":"O.\u00a0Wienand, M.\u00a0Wedler, G.-M. Greuel, D.\u00a0Stoffel, and W.\u00a0Kunz. An algebraic approach for proving data correctness in arithmetic data paths. In Proc. International Conference Computer Aided Verification (CAV), pages 473\u2013486. Princeton, NJ, USA, July 2008.","DOI":"10.1007\/978-3-540-70545-1_45"}],"container-title":["Lecture Notes in Electrical Engineering","Languages for Embedded Systems and their Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-1-4020-9714-0_17.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,29]],"date-time":"2021-04-29T05:56:21Z","timestamp":1619675781000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-1-4020-9714-0_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9781402097133","9781402097140"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-1-4020-9714-0_17","relation":{},"ISSN":["1876-1100","1876-1119"],"issn-type":[{"type":"print","value":"1876-1100"},{"type":"electronic","value":"1876-1119"}],"subject":[],"published":{"date-parts":[[2009]]}}}