{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,5]],"date-time":"2026-06-05T15:48:04Z","timestamp":1780674484512,"version":"3.54.1"},"reference-count":50,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2024,5,24]],"date-time":"2024-05-24T00:00:00Z","timestamp":1716508800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,5,24]],"date-time":"2024-05-24T00:00:00Z","timestamp":1716508800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100001659","name":"German Research Foundation","doi-asserted-by":"crossref","award":["Project VerA (SCHO 894\/5-1, GR 3104\/6-1 and DR 297\/37-1)"],"award-info":[{"award-number":["Project VerA (SCHO 894\/5-1, GR 3104\/6-1 and DR 297\/37-1)"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100001659","name":"German Research Foundation","doi-asserted-by":"crossref","award":["Project VerA (SCHO 894\/5-1, GR 3104\/6-1 and DR 297\/37-1)"],"award-info":[{"award-number":["Project VerA (SCHO 894\/5-1, GR 3104\/6-1 and DR 297\/37-1)"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100001659","name":"German Research Foundation","doi-asserted-by":"crossref","award":["Project VerA (SCHO 894\/5-1, GR 3104\/6-1 and DR 297\/37-1)"],"award-info":[{"award-number":["Project VerA (SCHO 894\/5-1, GR 3104\/6-1 and DR 297\/37-1)"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100001659","name":"German Research Foundation","doi-asserted-by":"crossref","award":["Project VerA (SCHO 894\/5-1, GR 3104\/6-1 and DR 297\/37-1)"],"award-info":[{"award-number":["Project VerA (SCHO 894\/5-1, GR 3104\/6-1 and DR 297\/37-1)"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100001659","name":"German Research Foundation","doi-asserted-by":"crossref","award":["Project VerA (SCHO 894\/5-1, GR 3104\/6-1 and DR 297\/37-1)"],"award-info":[{"award-number":["Project VerA (SCHO 894\/5-1, GR 3104\/6-1 and DR 297\/37-1)"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"crossref"}]},{"name":"LIT Secure and Correct Systems Lab"},{"name":"Albert-Ludwigs-Universit\u00e4t Freiburg im Breisgau"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2025,10]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Recent methods based on <jats:italic>Symbolic Computer Algebra<\/jats:italic> (SCA) have shown great success in formal verification of multipliers and\u2014more recently\u2014of dividers as well. In this paper we enhance known approaches by the computation of <jats:italic>satisfiability don\u2019t cares for so-called Extended Atomic Blocks (EABs)<\/jats:italic> and by <jats:italic>Delayed Don\u2019t Care Optimization (DDCO)<\/jats:italic> for optimizing polynomials during backward rewriting. Using those novel methods we are able to extend the applicability of SCA-based methods to further divider architectures which could not be handled by previous approaches. We successfully apply the approach to the fully automatic formal verification of large dividers (with bit widths up to 512).<\/jats:p>","DOI":"10.1007\/s10703-024-00452-3","type":"journal-article","created":{"date-parts":[[2024,5,24]],"date-time":"2024-05-24T12:01:42Z","timestamp":1716552102000},"page":"106-142","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Divider verification using symbolic computer algebra and delayed don\u2019t care optimization: theory and practical implementation"],"prefix":"10.1007","volume":"67","author":[{"given":"Alexander","family":"Konrad","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Christoph","family":"Scholl","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Alireza","family":"Mahzoon","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Daniel","family":"Gro\u00dfe","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Rolf","family":"Drechsler","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2024,5,24]]},"reference":[{"key":"452_CR1","unstructured":"Balyo T, Heule M, Iser M et\u00a0al (eds) (2023) Proceedings of SAT competition 2023: Solver, Benchmark and Proof Checker Descriptions. Department of Computer Science Series of Publications B, Department of Computer Science, University of Helsinki, Finland"},{"key":"452_CR2","unstructured":"Berkeley Logic Synthesis and Verification Group (2019) ABC: a system for sequential synthesis and verification. available at https:\/\/people.eecs.berkeley.edu\/alanmi\/abc\/"},{"key":"452_CR3","doi-asserted-by":"crossref","unstructured":"Brayton RK, Mishchenko A (2010) ABC: an academic industrial-strength verification tool. In: Computer Aided Verification. Springer, pp 24\u201340","DOI":"10.1007\/978-3-642-14295-6_5"},{"issue":"8","key":"452_CR4","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"RE Bryant","year":"1986","unstructured":"Bryant RE (1986) Graph-based algorithms for Boolean function manipulation. IEEE Trans Comp 35(8):677\u2013691","journal-title":"IEEE Trans Comp"},{"key":"452_CR5","doi-asserted-by":"crossref","unstructured":"Bryant RE (1996) Bit-level analysis of an SRT divider circuit. In: Design Automation Conf., pp 661\u2013665","DOI":"10.1109\/DAC.1996.545657"},{"issue":"2","key":"452_CR6","first-page":"137","volume":"3","author":"RE Bryant","year":"2001","unstructured":"Bryant RE, Chen Y (2001) Verification of arithmetic circuits using binary moment diagrams. Softw Tools Technol Transf 3(2):137\u2013155","journal-title":"Softw Tools Technol Transf"},{"key":"452_CR7","doi-asserted-by":"crossref","unstructured":"Bryant RE, Chen YA (1995) Verification of arithmetic circuits with binary moment diagrams. In: Design Automation Conf. ACM Press, pp 535\u2013541","DOI":"10.1145\/217474.217583"},{"key":"452_CR8","doi-asserted-by":"crossref","unstructured":"Burch JR (1991) Using BDDs to verify multipliers. In: Design Automation Conf. ACM, pp 408\u2013412","DOI":"10.1145\/127601.127703"},{"key":"452_CR9","doi-asserted-by":"crossref","unstructured":"Ciesielski M, Yu C, Liu D et\u00a0al (2015) Verification of gate-level arithmetic circuits by function extraction. In: Design Automation Conf. ACM, pp 52:1\u201352:6","DOI":"10.1145\/2744769.2744925"},{"key":"452_CR10","doi-asserted-by":"crossref","unstructured":"Clarke EM, Khaira M, Zhao X (1996) Word level model checking\u2014avoiding the Pentium FDIV error. In: Design Automation Conf. ACM Press, pp 645\u2013648","DOI":"10.1109\/DAC.1996.545654"},{"issue":"1","key":"452_CR11","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1023\/A:1008665528003","volume":"14","author":"EM Clarke","year":"1999","unstructured":"Clarke EM, German SM, Zhao X (1999) Verifying the SRT division algorithm using theorem proving techniques. Formal Methods Syst Design Int J 14(1):7\u201344","journal-title":"Formal Methods Syst Design Int J"},{"issue":"4","key":"452_CR12","first-page":"129","volume":"20","author":"T Coe","year":"1995","unstructured":"Coe T (1995) Inside the Pentium FDIV bug. Dr Dobbs J 20(4):129\u2013135","journal-title":"Dr Dobbs J"},{"key":"452_CR13","doi-asserted-by":"crossref","unstructured":"Coudert O, Madre JC (1990) A unified framework for the formal verification of sequential circuits. In: International conference on computer-aided design. IEEE Computer Society, pp 126\u2013129","DOI":"10.1109\/ICCAD.1990.129859"},{"key":"452_CR14","doi-asserted-by":"crossref","unstructured":"E\u00e9n N, S\u00f6rensson N (2003) An extensible SAT-solver. In: Theory and Applications of Satisfiability Testing. Springer, pp 502\u2013518","DOI":"10.1007\/978-3-540-24605-3_37"},{"issue":"2","key":"452_CR15","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1016\/j.micpro.2015.01.007","volume":"39","author":"F Farahmandi","year":"2015","unstructured":"Farahmandi F, Alizadeh B (2015) Gr\u00f6bner basis based formal verification of large arithmetic circuits using gaussian elimination and cone-based polynomial extraction. Microprocess Microsyst 39(2):83\u201396","journal-title":"Microprocess Microsyst"},{"key":"452_CR16","doi-asserted-by":"crossref","unstructured":"Goldberg EI, Prasad MR, Brayton RK (2001) Using SAT for combinational equivalence checking. In: Design, Automation and Test in Europe. IEEE Computer Society, pp 114\u2013121","DOI":"10.1109\/DATE.2001.915010"},{"key":"452_CR17","unstructured":"Gurobi Optimization LLC (2020) Gurobi optimizer reference manual. http:\/\/www.gurobi.com"},{"key":"452_CR18","doi-asserted-by":"crossref","unstructured":"Hamaguchi K, Morita A, Yajima S (1995) Efficient construction of binary moment diagrams for verifying arithmetic circuits. In: International conference on computer-aided design. IEEE Computer Society \/ ACM, pp 78\u201382","DOI":"10.1109\/ICCAD.1995.479995"},{"key":"452_CR19","doi-asserted-by":"crossref","unstructured":"Kaufmann D, Biere A, Kauers M (2019) Verifying large multipliers by combining SAT and computer algebra. In: Int\u2019l Conf. on Formal Methods in CAD. IEEE, pp 28\u201336","DOI":"10.23919\/FMCAD.2019.8894250"},{"key":"452_CR20","doi-asserted-by":"crossref","unstructured":"Kaufmann D, Beame P, Biere A, et\u00a0al (2022) Adding dual variables to algebraic reasoning for gate-level multiplier verification. In: Design, automation and test in Europe. IEEE, pp 1431\u20131436","DOI":"10.23919\/DATE54114.2022.9774587"},{"key":"452_CR21","unstructured":"Konrad A, Scholl C, Mahzoon A et\u00a0al (2022a) Benchmarks and binaries. https:\/\/abs.informatik.uni-freiburg.de\/src\/projects_view.php?projectID=24"},{"key":"452_CR22","unstructured":"Konrad A, Scholl C, Mahzoon A, et\u00a0al (2022b) Divider verification using symbolic computer algebra and delayed don\u2019t care optimization. In: Griggio A, Rungta N (eds) Int\u2019l Conf. on Formal Methods in CAD. IEEE, pp 1\u201310"},{"key":"452_CR23","volume-title":"Computer arithmetic algorithms","author":"I Koren","year":"1993","unstructured":"Koren I (1993) Computer arithmetic algorithms. Prentice Hall, Upper Saddle River"},{"issue":"9","key":"452_CR24","doi-asserted-by":"publisher","first-page":"1409","DOI":"10.1109\/TCAD.2013.2259540","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 Trans Comput Aided Design Circuits Syst 32(9):1409\u20131420","journal-title":"IEEE Trans Comput Aided Design Circuits Syst"},{"key":"452_CR25","doi-asserted-by":"crossref","unstructured":"Mahzoon A, Gro\u00dfe D, Drechsler R (2018) PolyCleaner: clean your polynomials before backward rewriting to verify million-gate multipliers. In: International conference on computer-aided design. ACM, pp 129:1\u2013129:8","DOI":"10.1145\/3240765.3240837"},{"key":"452_CR26","doi-asserted-by":"crossref","unstructured":"Mahzoon A, Gro\u00dfe D, Drechsler R (2019) RevSCA: using reverse engineering to bring light into backward rewriting for big and dirty multipliers. In: Design Automation Conf. ACM, pp 185:1\u2013185:6","DOI":"10.1145\/3316781.3317898"},{"key":"452_CR27","doi-asserted-by":"crossref","unstructured":"Mahzoon A, Gro\u00dfe D, Scholl C et\u00a0al (2020) Towards formal verification of optimized and industrial multipliers. In: Design, automation and test in Europe. IEEE, pp 544\u2013549","DOI":"10.23919\/DATE48585.2020.9116485"},{"issue":"5","key":"452_CR28","doi-asserted-by":"publisher","first-page":"1573","DOI":"10.1109\/TCAD.2021.3083682","volume":"41","author":"A Mahzoon","year":"2022","unstructured":"Mahzoon A, Gro\u00dfe D, Drechsler R (2022) RevSCA-2.0: SCA-based formal verification of nontrivial multipliers using reverse engineering and local vanishing removal. IEEE Trans Comput Aided Design Circuits Syst 41(5):1573\u20131586","journal-title":"IEEE Trans Comput Aided Design Circuits Syst"},{"key":"452_CR29","doi-asserted-by":"crossref","unstructured":"Mahzoon A, Gro\u00dfe D, Scholl C et\u00a0al (2022b) Formal verification of modular multipliers using symbolic computer algebra and Boolean satisfiability. In: Design automation Conf. ACM, pp 1183\u20131188","DOI":"10.1145\/3489517.3530605"},{"key":"452_CR30","doi-asserted-by":"crossref","unstructured":"Malik S, Wang AR, Brayton RK et\u00a0al (1988) Logic verification using binary decision diagrams in a logic synthesis environment. In: International conference on computer-aided design. IEEE Computer Society, pp 6\u20139","DOI":"10.1109\/ICCAD.1988.122451"},{"key":"452_CR31","first-page":"1","volume":"Q1","author":"J O\u2019Leary","year":"1999","unstructured":"O\u2019Leary J, Zhao X, Gerth R et al (1999) Formally verifying IEEE compliance of floating point hardware. Intel Technol J Q1:1\u201310","journal-title":"Intel Technol J"},{"key":"452_CR32","doi-asserted-by":"crossref","unstructured":"Pan P, Lin C (1998) A new retiming-based technology mapping algorithm for lut-based fpgas. In: Cong J, Kaptanoglu S (Eds) Proceedings of the ACM\/SIGDA sixth international symposium on field programmable gate arrays. ACM, pp 35\u201342","DOI":"10.1145\/275107.275118"},{"key":"452_CR33","doi-asserted-by":"crossref","unstructured":"Ritirc D, Biere A, Kauers M (2017) Column-wise verification of multipliers using computer algebra. In: Int\u2019l Conf. on Formal Methods in CAD. IEEE, pp 23\u201330","DOI":"10.23919\/FMCAD.2017.8102237"},{"key":"452_CR34","doi-asserted-by":"crossref","unstructured":"Ritirc D, Biere A, Kauers M (2018) Improving and extending the algebraic approach for verifying gate-level multipliers. In: Design, automation and test in Europe. IEEE, pp 1556\u20131561","DOI":"10.23919\/DATE.2018.8342263"},{"issue":"3","key":"452_CR35","doi-asserted-by":"publisher","first-page":"218","DOI":"10.1109\/TEC.1958.5222579","volume":"7","author":"JE Robertson","year":"1958","unstructured":"Robertson JE (1958) A new class of digital division methods. IRE Trans Electron Comput 7(3):218\u2013222","journal-title":"IRE Trans Electron Comput"},{"key":"452_CR36","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1112\/S1461157000000176","volume":"1","author":"DM Russinoff","year":"1998","unstructured":"Russinoff DM (1998) A mechanically checked proof of IEEE compliance of the floating point multiplication, division and square root algorithms of the AMD-K7 processor. LMS J Comput Math 1:148\u2013200","journal-title":"LMS J Comput Math"},{"key":"452_CR37","doi-asserted-by":"crossref","unstructured":"Savoj H, Brayton RK, Touati HJ (1991) Extracting local don\u2019t cares for network optimization. In: International conference on computer-aided design. IEEE computer society, pp 514\u2013517","DOI":"10.1109\/ICCAD.1991.185319"},{"key":"452_CR38","doi-asserted-by":"crossref","unstructured":"Sayed-Ahmed A, Gro\u00dfe D, K\u00fchne U et\u00a0al (2016) Formal verification of integer multipliers by combining Gr\u00f6bner basis with logic reduction. In: Design, automation and test in Europe. IEEE, pp 1048\u20131053","DOI":"10.3850\/9783981537079_0248"},{"key":"452_CR39","doi-asserted-by":"crossref","unstructured":"Scholl C, Konrad A (2020) Symbolic computer algebra and SAT based information forwarding for fully automatic divider verification. In: Design automation conf. IEEE, pp 1\u20136","DOI":"10.1109\/DAC18072.2020.9218721"},{"key":"452_CR40","doi-asserted-by":"crossref","unstructured":"Scholl C, Konrad A, Mahzoon A et\u00a0al (2021) Verifying dividers using symbolic computer algebra and don\u2019t care optimization. In: Design, automation and test in Europe. IEEE, pp 1110\u20131115","DOI":"10.23919\/DATE51398.2021.9474019"},{"key":"452_CR41","unstructured":"Silva JPM, Glass T (1999) Combinational equivalence checking using satisfiability and recursive learning. In: Design, automation and test in Europe. IEEE Computer Society\/ACM, pp 145\u2013149"},{"issue":"2","key":"452_CR42","first-page":"171","volume":"3","author":"F Somenzi","year":"2001","unstructured":"Somenzi F (2001) Efficient manipulation of decision diagrams. Softw Tools Technol Transf 3(2):171\u2013181","journal-title":"Softw Tools Technol Transf"},{"key":"452_CR43","unstructured":"Temel M, Hunt WA (2021) Sound and automated verification of real-world RTL multipliers. In: Int\u2019l conf on formal methods in CAD. IEEE, pp 53\u201362"},{"key":"452_CR44","doi-asserted-by":"crossref","unstructured":"Temel M, Slobodov\u00e1 A, Hunt WA (2020) Automated and scalable verification of integer multipliers. In: Computer aided verification. Springer, pp 485\u2013507","DOI":"10.1007\/978-3-030-53288-8_23"},{"key":"452_CR45","doi-asserted-by":"publisher","first-page":"466","DOI":"10.1007\/978-3-642-81955-1_28","volume-title":"Automation of Reasoning: 2: classical papers on computational logic 1967\u20131970","author":"GS Tseitin","year":"1983","unstructured":"Tseitin GS (1983) On the complexity of derivation in propositional calculus. In: Siekmann JH, Wrightson G (eds) Automation of Reasoning: 2: classical papers on computational logic 1967\u20131970. Springer, Berlin Heidelberg, pp 466\u2013483"},{"key":"452_CR46","doi-asserted-by":"crossref","unstructured":"Wienand O, Wedler M, Stoffel D et\u00a0al (2008) An algebraic approach for proving data correctness in arithmetic data paths. In: Computer aided verification. Springer, pp 473\u2013486","DOI":"10.1007\/978-3-540-70545-1_45"},{"key":"452_CR47","doi-asserted-by":"crossref","unstructured":"Yasin A, Su T, Pillement S et\u00a0al (2019a) Formal verification of integer dividers: division by a constant. In: IEEE annual symposium on VLSI. IEEE, pp 76\u201381","DOI":"10.1109\/ISVLSI.2019.00022"},{"key":"452_CR48","doi-asserted-by":"crossref","unstructured":"Yasin A, Su T, Pillement S et\u00a0al (2019b) Functional verification of hardware dividers using algebraic model. In: VLSI of System-on-Chip. IEEE, pp 257\u2013262","DOI":"10.1109\/VLSI-SoC.2019.8920335"},{"issue":"12","key":"452_CR49","doi-asserted-by":"publisher","first-page":"2131","DOI":"10.1109\/TCAD.2016.2547898","volume":"35","author":"C Yu","year":"2016","unstructured":"Yu C, Brown W, Liu D et al (2016) Formal verification of arithmetic circuits by function extraction. IEEE Trans Comput Aided Design Circuits Syst 35(12):2131\u20132142","journal-title":"IEEE Trans Comput Aided Design Circuits Syst"},{"issue":"9","key":"452_CR50","doi-asserted-by":"publisher","first-page":"1907","DOI":"10.1109\/TCAD.2017.2772854","volume":"37","author":"C Yu","year":"2018","unstructured":"Yu C, Ciesielski M, Mishchenko A (2018) Fast algebraic rewriting based on And-Inverter graphs. IEEE Trans Comput Aided Design Circuits Syst 37(9):1907\u20131911","journal-title":"IEEE Trans Comput Aided Design Circuits Syst"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-024-00452-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10703-024-00452-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-024-00452-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,16]],"date-time":"2025-10-16T10:33:30Z","timestamp":1760610810000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10703-024-00452-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,5,24]]},"references-count":50,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2025,10]]}},"alternative-id":["452"],"URL":"https:\/\/doi.org\/10.1007\/s10703-024-00452-3","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,5,24]]},"assertion":[{"value":"15 December 2023","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"14 April 2024","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"24 May 2024","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors declare no competing interests.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflict of interest"}}]}}