{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,15]],"date-time":"2026-10-15T16:39:11Z","timestamp":1792082351244,"version":"4.4.0"},"reference-count":37,"publisher":"Springer Science and Business Media LLC","issue":"1-3","license":[{"start":{"date-parts":[[2019,2,26]],"date-time":"2019-02-26T00:00:00Z","timestamp":1551139200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2019,2,26]],"date-time":"2019-02-26T00:00:00Z","timestamp":1551139200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100002428","name":"Austrian Science Fund","doi-asserted-by":"publisher","award":["NFN S11408-N23 (RiSE)"],"award-info":[{"award-number":["NFN S11408-N23 (RiSE)"]}],"id":[{"id":"10.13039\/501100002428","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100002428","name":"Austrian Science Fund","doi-asserted-by":"publisher","award":["Y464-N18"],"award-info":[{"award-number":["Y464-N18"]}],"id":[{"id":"10.13039\/501100002428","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100002428","name":"Austrian Science Fund","doi-asserted-by":"publisher","award":["SFB F5004"],"award-info":[{"award-number":["SFB F5004"]}],"id":[{"id":"10.13039\/501100002428","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2020,12]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Verifying arithmetic circuits and most prominently multiplier circuits is an important problem which in practice still requires substantial manual effort. The currently most effective approach uses polynomial reasoning over pseudo boolean polynomials. In this approach a word-level specification is reduced by a Gr\u00f6bner basis which is implied by the gate-level representation of the circuit. This reduction returns zero if and only if the circuit is correct. We give a rigorous formalization of this approach including soundness and completeness arguments. Furthermore we present a novel incremental column-wise technique to verify gate-level multipliers. This approach is further improved by extracting full- and half-adder constraints in the circuit which allows to rewrite and reduce the Gr\u00f6bner basis. We also present a new technical theorem which allows to rewrite local parts of the Gr\u00f6bner basis. Optimizing the Gr\u00f6bner basis reduces computation time substantially. In addition we extend these algebraic techniques to verify the equivalence of bit-level multipliers without using a word-level specification. Our experiments show that regular multipliers can be verified efficiently by using off-the-shelf computer algebra tools, while more complex and optimized multipliers require more sophisticated techniques. We discuss in detail our complete verification approach including all optimizations.<\/jats:p>","DOI":"10.1007\/s10703-018-00329-2","type":"journal-article","created":{"date-parts":[[2019,2,27]],"date-time":"2019-02-27T01:43:07Z","timestamp":1551231787000},"page":"22-54","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":26,"title":["Incremental column-wise verification of arithmetic circuits using computer algebra"],"prefix":"10.1007","volume":"56","author":[{"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"}]},{"given":"Manuel","family":"Kauers","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2019,2,26]]},"reference":[{"key":"329_CR1","unstructured":"Agnarsson S, Kandri-Rody A, Kapur D, Narendran P, Saunders B (1984) Complexity of testing whether a polynomial ideal is nontrivial. In: 3rd MACSYMA user\u2019s conference, pp 452\u2013458"},{"key":"329_CR2","doi-asserted-by":"crossref","unstructured":"Beame P, Liew V (2017) Towards verifying nonlinear integer arithmetic. In: CAV, volume 10427 of LNCS. Springer, pp 238\u2013258","DOI":"10.1007\/978-3-319-63390-9_13"},{"key":"329_CR3","unstructured":"Berkeley Logic Synthesis and Verification Group. ABC: a system for sequential synthesis and verification. http:\/\/www.eecs.berkeley.edu\/~alanmi\/abc\/. Bitbucket Version 1.01, last change 27 Feb 2017"},{"key":"329_CR4","unstructured":"Biere A (2016) Collection of combinational arithmetic miters submitted to the SAT Competition 2016. In: SAT Competition 2016, volume B-2016-1 of Department of Computer Science Series of Publications B. University of Helsinki, pp 65\u201366"},{"key":"329_CR5","unstructured":"Biere A (2016) Splatz, Lingeling, Plingeling, Treengeling, YalSAT Entering the SAT Competition 2016. In: Proceedings of SAT Competition 2016\u2014solver and benchmark descriptions. University of Helsinki, pp 44\u201345"},{"key":"329_CR6","unstructured":"Biere A Weaknesses of CDCL solvers. http:\/\/www.fields.utoronto.ca\/talks\/weaknesses-cdcl-solvers, August 2016"},{"key":"329_CR7","unstructured":"Biere A, Heljanko K, Wieringa S (2011) AIGER 1.9 and beyond. Technical report, FMV Reports Series, Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr. 69, 4040 Linz, Austria"},{"key":"329_CR8","doi-asserted-by":"crossref","unstructured":"Biere A, Kauers M, Ritirc D (2017) Challenges in verifying arithmetic circuits using computer algebra. In: SYNASC. IEEE Computer Society, pp 9\u201315","DOI":"10.1109\/SYNASC.2017.00010"},{"issue":"8","key":"329_CR9","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"R Bryant","year":"1986","unstructured":"Bryant R (1986) Graph-based algorithms for boolean function manipulation. IEEE Trans Comput 35(8):677\u2013691","journal-title":"IEEE Trans Comput"},{"issue":"2","key":"329_CR10","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1007\/s100090100037","volume":"3","author":"R Bryant","year":"2001","unstructured":"Bryant R, Chen Y (2001) Verification of arithmetic circuits using binary moment diagrams. STTT 3(2):137\u2013155","journal-title":"STTT"},{"key":"329_CR11","unstructured":"Buchberger B (1965) Ein Algorithmus zum Auffinden der Basiselemente des Restklassenringes nach einem nulldimensionalen Polynomideal. Ph.D. thesis, University of Innsbruck"},{"issue":"10","key":"329_CR12","doi-asserted-by":"publisher","first-page":"7763","DOI":"10.4249\/scholarpedia.7763","volume":"5","author":"B Buchberger","year":"2010","unstructured":"Buchberger B, Kauers M (2010) Gr\u00f6bner basis. Scholarpedia 5(10):7763","journal-title":"Scholarpedia"},{"key":"329_CR13","doi-asserted-by":"crossref","unstructured":"Chen J, Chen Y (2001) Equivalence checking of integer multipliers. In: Goto S (ed) ASP-DAC 2001, pp 169\u2013174","DOI":"10.1145\/370155.370315"},{"key":"329_CR14","unstructured":"Chen Y, Bryant R (1995) Verification of arithmetic circuits with binary moment diagrams. In: DAC, pp 535\u2013541"},{"key":"329_CR15","doi-asserted-by":"crossref","unstructured":"Ciesielski M, Yu C, Brown W, Liu D, Rossi A (2015) Verification of gate-level arithmetic circuits by function extraction. In: DAC. ACM, pp 52:1\u201352:6","DOI":"10.1145\/2744769.2744925"},{"key":"329_CR16","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 (1997) Ideals, varieties, and algorithms. Springer, New York"},{"key":"329_CR17","unstructured":"Decker W, Greuel G-M, Pfister G, Sch\u00f6nemann H (2016) Singular 4-1-0. http:\/\/www.singular.uni-kl.de. Accessed Jan 2018"},{"key":"329_CR18","doi-asserted-by":"crossref","unstructured":"E\u00e9n N, Biere A (2005) Effective preprocessing in SAT through variable and clause elimination. In: SAT, volume 3569 of LNCS. Springer, pp 61\u201375","DOI":"10.1007\/11499107_5"},{"issue":"12","key":"329_CR19","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 (2006) Formal design of arithmetic circuits based on arithmetic description language. IEICE Trans 89\u2013A(12):3500\u20133509","journal-title":"IEICE Trans"},{"issue":"4","key":"329_CR20","doi-asserted-by":"publisher","first-page":"583","DOI":"10.1007\/s10817-011-9239-9","volume":"49","author":"M J\u00e4rvisalo","year":"2012","unstructured":"J\u00e4rvisalo M, Biere A, Heule M (2012) Simulating circuit-level simplifications on CNF. J Autom Reason 49(4):583\u2013619","journal-title":"J Autom Reason"},{"key":"329_CR21","unstructured":"Kandri-Rody A, Kapur D, Narendran P (1985) An ideal-theoretic approach to work problems and unification problems over finitely presented commutative algebras. In: RTA, volume 202 of LNCS. Springer, pp 345\u2013364"},{"key":"329_CR22","volume-title":"Computer arithmetic algorithms","author":"I Koren","year":"2001","unstructured":"Koren I (2001) Computer arithmetic algorithms, 2nd edn. A. K. Peters Ltd, Natick","edition":"2"},{"issue":"12","key":"329_CR23","first-page":"1377","volume":"21","author":"A Kuehlmann","year":"2002","unstructured":"Kuehlmann A, Paruthi V, Krohm F, Ganai M (2002) Robust boolean reasoning for equivalence checking and functional property verification. IEEE TCAD 21(12):1377\u20131394","journal-title":"IEEE TCAD"},{"issue":"9","key":"329_CR24","first-page":"1409","volume":"32","author":"J Lv","year":"2013","unstructured":"Lv J, Kalla P, Enescu F (2013) Efficient Gr\u00f6bner basis reductions for formal verification of Galois field arithmetic circuits. IEEE TCAD 32(9):1409\u20131420","journal-title":"IEEE TCAD"},{"key":"329_CR25","first-page":"53","volume":"9","author":"A Niemetz","year":"2014","unstructured":"Niemetz A, Preiner M, Biere A (2014) Boolector 2.0 system description. JSAT 9:53\u201358 (published 2015)","journal-title":"JSAT"},{"key":"329_CR26","volume-title":"Computer arithmetic: algorithms and hardware designs","author":"B Parhami","year":"2000","unstructured":"Parhami B (2000) Computer arithmetic: algorithms and hardware designs. Oxford University Press, Oxford"},{"key":"329_CR27","doi-asserted-by":"crossref","unstructured":"Pruss T, Kalla P, Enescu F (2014) Equivalence verification of large Galois field arithmetic circuits using word-level abstraction via Gr\u00f6bner bases. In: DAC. ACM, pp 152:1\u2013152:6","DOI":"10.1145\/2593069.2593134"},{"key":"329_CR28","doi-asserted-by":"crossref","unstructured":"Ritirc D, Biere A, Kauers M (2017) Column-wise verification of multipliers using computer algebra. In: Stewart D, Weissenbacher G (eds) FMCAD. IEEE, pp 23\u201330","DOI":"10.23919\/FMCAD.2017.8102237"},{"key":"329_CR29","doi-asserted-by":"crossref","unstructured":"Ritirc D, Biere A, Kauers M (2018) Improving and extending the algebraic approach for verifying gate-level multipliers. In: DATE. IEEE, pp 1556\u20131561","DOI":"10.23919\/DATE.2018.8342263"},{"key":"329_CR30","doi-asserted-by":"crossref","unstructured":"Sayed-Ahmed A, Gro\u00dfe D, K\u00fchne U, Soeken M, Drechsler R (2016) Formal verification of integer multipliers by combining Gr\u00f6bner basis with logic reduction. In: DATE. IEEE, pp 1048\u20131053","DOI":"10.3850\/9783981537079_0248"},{"key":"329_CR31","doi-asserted-by":"crossref","unstructured":"Sayed-Ahmed A, Gro\u00dfe D, Soeken M, Drechsler R (2016) Equivalence checking using Gr\u00f6bner bases. In: FMCAD. IEEE, pp 169\u2013176","DOI":"10.1109\/FMCAD.2016.7886676"},{"issue":"5","key":"329_CR32","first-page":"586","volume":"23","author":"D Stoffel","year":"2004","unstructured":"Stoffel D, Kunz W (2004) Equivalence checking of arithmetic circuits on the arithmetic bit level. IEEE TCAD 23(5):586\u2013597","journal-title":"IEEE TCAD"},{"key":"329_CR33","doi-asserted-by":"crossref","unstructured":"Wienand O, Wedler M, Stoffel D, Kunz W, Greuel G (2008) An algebraic approach for proving data correctness in arithmetic data paths. In: CAV, volume 5123 of LNCS. Springer, pp 473\u2013486","DOI":"10.1007\/978-3-540-70545-1_45"},{"key":"329_CR34","unstructured":"Wolfram Research, Inc. Mathematica, 2016. Version 10.4"},{"issue":"12","key":"329_CR35","first-page":"2131","volume":"35","author":"C Yu","year":"2016","unstructured":"Yu C, Brown W, Liu D, Rossi A, Ciesielski M (2016) Formal verification of arithmetic circuits by function extraction. IEEE TCAD 35(12):2131\u20132142","journal-title":"IEEE TCAD"},{"issue":"99","key":"329_CR36","first-page":"1","volume":"PP","author":"C Yu","year":"2017","unstructured":"Yu C, Ciesielski M, Mishchenko A (2017) Fast algebraic rewriting based on and-inverter graphs. IEEE TCAD PP(99):1","journal-title":"IEEE TCAD"},{"key":"329_CR37","doi-asserted-by":"crossref","unstructured":"Yu C, Ciesielski MJ (2017) Efficient parallel verification of Galois field multipliers. In: ASP-DAC. IEEE, pp 238\u2013243","DOI":"10.1109\/ASPDAC.2017.7858326"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-018-00329-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-018-00329-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-018-00329-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,1,18]],"date-time":"2021-01-18T11:01:18Z","timestamp":1610967678000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-018-00329-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,2,26]]},"references-count":37,"journal-issue":{"issue":"1-3","published-print":{"date-parts":[[2020,12]]}},"alternative-id":["329"],"URL":"https:\/\/doi.org\/10.1007\/s10703-018-00329-2","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,2,26]]},"assertion":[{"value":"26 February 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}