{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,23]],"date-time":"2026-10-23T11:59:10Z","timestamp":1792756750984,"version":"4.5.0"},"reference-count":39,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2023,1,11]],"date-time":"2023-01-11T00:00:00Z","timestamp":1673395200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,1,11]],"date-time":"2023-01-11T00:00:00Z","timestamp":1673395200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"name":"TU Wien"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2023,4]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Verifying arithmetic circuits and most prominently multiplier circuits is an important problem which in practice is still considered to be challenging. One of the currently most successful verification techniques relies on algebraic reasoning. In this article, we present <jats:sc>AMulet2<\/jats:sc>, a fully automatic tool for verification of integer multipliers combining SAT solving and computer algebra. Our tool models multipliers given as and-inverter graphs as a set of polynomials and applies preprocessing techniques based on elimination theory of Gr\u00f6bner bases. Finally, it uses a polynomial reduction algorithm to verify the correctness of the given circuit. <jats:sc>AMulet2<\/jats:sc> is a re-factorization and improved re-implementation of our previous verification tool <jats:sc>AMulet1<\/jats:sc> and cannot only be used as a stand-alone tool but also serves as a polynomial reasoning framework. We present a novel XOR-based slicing approach and discuss improvements on the data structures including monomial sharing.\n<\/jats:p>","DOI":"10.1007\/s10009-022-00688-6","type":"journal-article","created":{"date-parts":[[2023,1,11]],"date-time":"2023-01-11T16:02:47Z","timestamp":1673452967000},"page":"133-144","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["Improving AMulet2 for verifying multiplier circuits using SAT solving and computer algebra"],"prefix":"10.1007","volume":"25","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5645-0292","authenticated-orcid":false,"given":"Daniela","family":"Kaufmann","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7170-9242","authenticated-orcid":false,"given":"Armin","family":"Biere","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2023,1,11]]},"reference":[{"key":"688_CR1","doi-asserted-by":"crossref","unstructured":"Beame, P., Impagliazzo, R., Kraj\u00edcek, J., Pitassi, T. and Pudl\u00e1k, P.: Lower bounds on Hilbert\u2019s Nullstellensatz and Propositional Proofs. In: Proc. London Math. Society, volume s3-73, pp. 1\u201326, (1996)","DOI":"10.1112\/plms\/s3-73.1.1"},{"key":"688_CR2","doi-asserted-by":"crossref","unstructured":"Becker, T., Weispfenning, V. and Kredel, H.: Gr\u00f6bner Bases, volume 141 of Grad. texts in math. Springer, (1993)","DOI":"10.1007\/978-1-4612-0913-3_5"},{"key":"688_CR3","unstructured":"Biere, A.: Collection of Combinational Arithmetic Miters Submitted to the SAT Competition 2016. In: SAT Competition 2016, volume B-2016-1 of Dep. of Computer Science Report Series B, pages 65\u201366. University of Helsinki, (2016)"},{"key":"688_CR4","unstructured":"Biere, A., Fazekas, K., Fleury, M., and Heisinger, M.: CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling entering the SAT Competition 2020. In Proc.\u00a0of SAT Competition 2020 \u2013 Solver and Benchmark Descriptions, volume B-2020-1 of Dep. of Computer Science Report Series B, pages 51\u201353. University of Helsinki, (2020)"},{"key":"688_CR5","unstructured":"Biere, A., Heljanko, K. and Wieringa, S.: AIGER 1.9 And Beyond. Technical report, FMV Reports Series, JKU Linz, Austria, (2011)"},{"issue":"2","key":"688_CR6","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1007\/s100090100037","volume":"3","author":"RE Bryant","year":"2001","unstructured":"Bryant, R.E., Chen, Y.: Verification of arithmetic circuits using binary moment diagrams. STTT 3(2), 137\u2013155 (2001)","journal-title":"STTT"},{"key":"688_CR7","unstructured":"Buchberger, B.: Ein Algorithmus zum Auffinden der Basiselemente des Restklassenringes nach einem nulldimensionalen Polynomideal. PhD thesis, Univ. of Innsbruck, (1965)"},{"issue":"6","key":"688_CR8","first-page":"1346","volume":"39","author":"MJ Ciesielski","year":"2020","unstructured":"Ciesielski, M.J., Su, T., Yasin, A., Yu, C.: Understanding algebraic rewriting for arithmetic circuit verification: a bit-flow model. IEEE TCAD 39(6), 1346\u20131357 (2020)","journal-title":"IEEE TCAD"},{"key":"688_CR9","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-41154-4","volume-title":"Ideals, Varieties, and Algorithms","author":"D Cox","year":"1997","unstructured":"Cox, D., Little, J., O\u2019Shea, D.: Ideals, Varieties, and Algorithms. Springer-Verlag, New York (1997)"},{"key":"688_CR10","unstructured":"Fleury, M.: Isabelle PAC formalization. Theory files at https:\/\/bitbucket.org\/isafol\/isafol\/src\/master\/PAC_Checker2\/, Accessed: 2021-07-28"},{"key":"688_CR11","unstructured":"Granlund, T. and the GMP development team. GNU MP: The GNU Multiple Precision Arithmetic Library, 2016. Version 6.1.2"},{"key":"688_CR12","unstructured":"Heule, M.J.H., Biere, A.: Proofs for satisfiability problems. In All about Proofs, Proofs for All Workshop, APPA 2014, volume\u00a055, pages 1\u201322. College Publications, (2015)"},{"key":"688_CR13","unstructured":"Hirsch, E., Itsykson, D., Kojevnikov, A., Kulikov, E. and Nikolenko, S.: Report on the Mixed Boolean-Algebraic Solver. Technical report, Laboratory of Mathematical Logic of St. Petersburg Dep. of Steklov Institute of Mathematics, (2005)"},{"issue":"12","key":"688_CR14","doi-asserted-by":"publisher","first-page":"3500","DOI":"10.1093\/ietfec\/e89-a.12.3500","volume":"89\u2013A","author":"N Homma","year":"2006","unstructured":"Homma, N., Watanabe, Y., Aoki, T., Higuchi, T.: Formal design of arithmetic circuits based on arithmetic description language. IEICE Trans. 89\u2013A(12), 3500\u20133509 (2006)","journal-title":"IEICE Trans."},{"key":"688_CR15","unstructured":"Kaufmann, D.: Amulet 1.5. https:\/\/github.com\/d-kfmnn\/amulet, (2020)"},{"key":"688_CR16","doi-asserted-by":"crossref","unstructured":"Kaufmann, D.: Artifact for AMulet2.0 for verifying multiplier circuits. http:\/\/fmv.jku.at\/amulet2_artifact, (2020)","DOI":"10.26226\/morressier.604907f41a80aac83ca25ce2"},{"key":"688_CR17","unstructured":"Kaufmann, D.: Formal Verification of Multiplier Circuits using Computer Algebra. PhD thesis, Informatik, Johannes Kepler University Linz, (2020)"},{"key":"688_CR18","doi-asserted-by":"crossref","unstructured":"Kaufmann, D.: AMulet2 for verifying multiplier circuits. https:\/\/github.com\/d-kfmnn\/amulet2, (2021)","DOI":"10.26226\/morressier.604907f41a80aac83ca25ce2"},{"key":"688_CR19","unstructured":"Kaufmann, D.: Practical algebraic calculus proof checker 2.0. https:\/\/github.com\/d-kfmnn\/pacheck2, (2021)"},{"key":"688_CR20","unstructured":"Kaufmann, D.: Artifact for AMulet2.1. https:\/\/zenodo.org\/record\/6637319, (2022)"},{"key":"688_CR21","doi-asserted-by":"crossref","unstructured":"Kaufmann, D. and Biere, A.: Nullstellensatz-proofs for multiplier verification. In CASC, volume 12291 of LNCS, pp. 368\u2013389. Springer, (2020)","DOI":"10.1007\/978-3-030-60026-6_21"},{"key":"688_CR22","doi-asserted-by":"crossref","unstructured":"Kaufmann, D. and Biere, A.: AMulet 2.0 for verifying multiplier circuits. In TACAS (2), volume 12652 of LNCS, pages 357\u2013364. Springer, (2021)","DOI":"10.1007\/978-3-030-72013-1_19"},{"key":"688_CR23","doi-asserted-by":"crossref","unstructured":"Kaufmann, D., Biere, A. and Kauers, M.: Verifying large multipliers by combining SAT and computer algebra. In FMCAD 2019, pp. 28\u201336. IEEE, (2019)","DOI":"10.23919\/FMCAD.2019.8894250"},{"key":"688_CR24","doi-asserted-by":"crossref","unstructured":"Kaufmann, D., Biere, A. and Kauers, M.: From DRUP to PAC and back. In DATE 2020, pp. 654\u2013657. IEEE (2020)","DOI":"10.23919\/DATE48585.2020.9116276"},{"key":"688_CR25","doi-asserted-by":"crossref","unstructured":"Kaufmann, D., Biere, A., Kauers, M.: Incremental Column-wise verification of arithmetic circuits using computer algebra. FMSD 56(1), 22\u201354 (2020)","DOI":"10.1007\/s10703-018-00329-2"},{"key":"688_CR26","unstructured":"Kaufmann, D., Biere, A. and Kauers, M.: SAT, Computer Algebra, Multipliers. In: Vampire 2018 and Vampire 2019, volume\u00a071 of EPiC Series in Computing, pp. 1\u201318. EasyChair, (2020)"},{"key":"688_CR27","unstructured":"Kaufmann, D., Fleury, M. and Biere, A.: Pacheck and Past\u00e8que, Checking Practical Algebraic Calculus Proofs. In FMCAD 2020, volume\u00a01 of FMCAD, pp. 264\u2013269. TU Vienna Academic Press, (2020)"},{"key":"688_CR28","doi-asserted-by":"crossref","unstructured":"Kaufmann, D., Fleury, M., Biere, A. and Kauers, M.: Practical Algebraic Calculus and Nullstellensatz with the Checkers Pacheck and Past\u00e8que and Nuss-Checker. FMSD, 2021. Submitted","DOI":"10.1007\/s10703-022-00391-x"},{"key":"688_CR29","unstructured":"Kaufmann, D., Kauers, M., Biere, A. and Cok, D.: Arithmetic Verification Problems Submitted to the SAT Race 2019. In SAT Race 2019, volume B-2019-1 of Dep. of Computer Science Report Series B, page\u00a049. University of Helsinki, (2019)"},{"issue":"12","key":"688_CR30","first-page":"1377","volume":"21","author":"A Kuehlmann","year":"2002","unstructured":"Kuehlmann, A., Paruthi, V., Krohm, F., Ganai, M.: Robust Boolean reasoning for equivalence checking and functional property verification. IEEE TCAD 21(12), 1377\u20131394 (2002)","journal-title":"IEEE TCAD"},{"issue":"1","key":"688_CR31","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1215\/ijm\/1380287466","volume":"56","author":"D Lichtblau","year":"2012","unstructured":"Lichtblau, D.: Effective computation of strong Gr\u00f6bner bases over Euclidean domains. Illinois J. Math. 56(1), 177\u2013194 (2012)","journal-title":"Illinois J. Math."},{"issue":"9","key":"688_CR32","first-page":"1409","volume":"32","author":"J Lv","year":"2013","unstructured":"Lv, J., Kalla, P., Enescu, F.: Efficient Gr\u00f6bner basis reductions for formal verification of Galois field arithmetic circuits. IEEE TCAD 32(9), 1409\u20131420 (2013)","journal-title":"IEEE TCAD"},{"key":"688_CR33","doi-asserted-by":"crossref","unstructured":"Mahzoon, A., Gro\u00dfe, D. and Drechsler, R.: PolyCleaner: clean your polynomials before backward rewriting to verify million-gate multipliers. In ICCAD 2018, pp. 129:1 \u2013 129:8. ACM, (2018)","DOI":"10.1145\/3240765.3240837"},{"key":"688_CR34","doi-asserted-by":"crossref","unstructured":"Mahzoon, A., Gro\u00dfe, D. and Drechsler, R.: RevSCA: using reverse engineering to bring light into backward rewriting for big and dirty multipliers. In DAC 2019, pp. 185:1\u2013185:6. ACM, (2019)","DOI":"10.1145\/3316781.3317898"},{"key":"688_CR35","doi-asserted-by":"crossref","unstructured":"Mahzoon, A., Gro\u00dfe, D., Scholl, C. and Drechsler, R.: Towards formal verification of optimized and industrial multipliers. In DATE, pp. 544\u2013549. IEEE, (2020)","DOI":"10.23919\/DATE48585.2020.9116485"},{"key":"688_CR36","unstructured":"Parhami, B.: Computer Arithmetic - Algorithms and Hardware designs. Oxford University Press, (2000)"},{"key":"688_CR37","unstructured":"Sharangpani, H. and Barton, M.L.: Statistical analysis of floating point flaw in the Pentium processor (1994)"},{"key":"688_CR38","unstructured":"Temel, M.: MultGen. https:\/\/github.com\/temelmertcan\/multgen, (2020)"},{"key":"688_CR39","doi-asserted-by":"crossref","unstructured":"Temel, M., Slobodov\u00e1, A. and Hunt, W.\u00a0A.: Automated and scalable verification of integer multipliers. In CAV, volume 12224 of LNCS, pp. 485\u2013507. Springer (2020)","DOI":"10.1007\/978-3-030-53288-8_23"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-022-00688-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10009-022-00688-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-022-00688-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,3,27]],"date-time":"2023-03-27T15:22:46Z","timestamp":1679930566000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10009-022-00688-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,1,11]]},"references-count":39,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2023,4]]}},"alternative-id":["688"],"URL":"https:\/\/doi.org\/10.1007\/s10009-022-00688-6","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,1,11]]},"assertion":[{"value":"4 November 2022","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"11 January 2023","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}