{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,11]],"date-time":"2025-11-11T14:04:13Z","timestamp":1762869853022,"version":"build-2065373602"},"reference-count":51,"publisher":"Association for Computing Machinery (ACM)","issue":"1","funder":[{"DOI":"10.13039\/501100001659","name":"German Research Foundation","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"crossref"}]},{"name":"Polynomial Verification of Electronic Circuits","award":["DR 287\/36-1"],"award-info":[{"award-number":["DR 287\/36-1"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Des. Autom. Electron. Syst."],"published-print":{"date-parts":[[2026,1,31]]},"abstract":"<jats:p>\n                    In the field of Electronic Design Automation (EDA), managing circuit complexity is a crucial task for efficient circuit verification, testing, and optimization. Increasing design complexity presents challenges for tasks such as formal verification, fault detection, and circuit optimization. Therefore, reducing circuit complexity becomes crucial in improving the efficiency and scalability of these tasks. These circuits are typically represented as graphs. In the field of parameterized complexity, CutWidth (CW) and TreeWidth (TW) are well-studied decomposition techniques that have been used in analyzing graph algorithms. In this paper, we introduce the TW decomposition technique to the field of EDA for the first time and demonstrate its impact on reducing the circuit complexity of circuits. Additionally, we present a new decomposition technique that combines both decompositions, resulting in a further reduction in circuit complexity. Furthermore, we present experimental results comparing complexity upper bounds from various decompositions to highlight the efficacy of our approach on the\n                    <jats:italic toggle=\"yes\">ISCAS\u201985<\/jats:italic>\n                    and\n                    <jats:italic toggle=\"yes\">EPFL<\/jats:italic>\n                    benchmark circuits. Our results show that our decomposition technique outperforms the complexity upper bounds of CW by 90.16\u00d7 and the complexity upper bounds of TW by 9.34\u00d7 for the ISCAS\u201985 benchmarks. Additionally, it outperforms the complexity upper bounds of CW by 1986.37\u00d7 and the complexity upper bounds of TW by 94.13\u00d7 for the EPFL benchmarks.\n                  <\/jats:p>\n                  <jats:p\/>\n                  <jats:p>\n                    Finally, to demonstrate the applicability of the decomposition techniques in solving various EDA problems, we propose a new Formal Verification (FV) approach that leverages these techniques to provide an upper bound for the verification process. We also conduct an experimental evaluation on the\n                    <jats:italic toggle=\"yes\">ITC\u201999<\/jats:italic>\n                    ,\n                    <jats:italic toggle=\"yes\">MCNC\u201991<\/jats:italic>\n                    , and\n                    <jats:italic toggle=\"yes\">VHDL Library of Arithmetic Units<\/jats:italic>\n                    (\n                    <jats:italic toggle=\"yes\">ELAU<\/jats:italic>\n                    ) benchmark circuits, adder circuits of various sizes (up to 3072-bit width), and\n                    <jats:italic toggle=\"yes\">Genmul<\/jats:italic>\n                    multipliers of different sizes (up to 10\u00d710), to demonstrate the scalability of our approach.\n                  <\/jats:p>","DOI":"10.1145\/3771280","type":"journal-article","created":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T11:30:11Z","timestamp":1760095811000},"page":"1-27","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Advanced And-Inverter Graph Decomposition Technique for Reducing Circuit Complexity"],"prefix":"10.1145","volume":"31","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0835-1070","authenticated-orcid":false,"given":"Mohamed","family":"Nadeem","sequence":"first","affiliation":[{"name":"Faculty 03 Mathematics and Computer Science, University of Bremen","place":["Bremen, Germany"]}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-5001-5241","authenticated-orcid":false,"given":"Luca","family":"M\u00fcller","sequence":"additional","affiliation":[{"name":"Faculty 03 Mathematics and Computer Science, University of Bremen","place":["Bremen, Germany"]},{"name":"Department of Cyber-Physical Systems, DFKI GmbH","place":["Bremen, Germany"]}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7237-5878","authenticated-orcid":false,"given":"Chandan Kumar","family":"Jha","sequence":"additional","affiliation":[{"name":"Faculty 03 Mathematics and Computer Science, University of Bremen","place":["Bremen, Germany"]}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9872-1740","authenticated-orcid":false,"given":"Rolf","family":"Drechsler","sequence":"additional","affiliation":[{"name":"Faculty 03 Mathematics and Computer Science, University of Bremen","place":["Bremen, Germany"]},{"name":"Department of Cyber-Physical Systems, DFKI GmbH","place":["Bremen, Germany"]}]}],"member":"320","published-online":{"date-parts":[[2025,11,11]]},"reference":[{"key":"e_1_3_2_2_2","unstructured":"2018. ABC: A System for Sequential Synthesis and Verification. Available at https:\/\/people.eecs.berkeley.edu\/alanmi\/abc\/ (Accessed on October 20 2025)."},{"key":"e_1_3_2_3_2","doi-asserted-by":"crossref","unstructured":"Michael Abseher Nysret Musliu and Stefan Woltran. 2017. htd A free open-source framework for (customized) tree decompositions and beyond. In Integration of AI and OR Techniques in Constraint Programming Domenico Salvagnin and Michele Lombardi (Eds.). Springer International Publishing Cham 376\u2013386.","DOI":"10.1007\/978-3-319-59776-8_30"},{"key":"e_1_3_2_4_2","unstructured":"Luca Amaru Pierre-Emmanuel Gaillardon and Giovanni De Micheli. 2015. The EPFL combinational benchmark suite. In International Workshop on Logic and Synthesis."},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1137\/0608024"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1016\/0166-218X(89)90031-0"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1073\/pnas.38.8.716"},{"key":"e_1_3_2_8_2","first-page":"133","volume-title":"Proceedings of the 36th International Conference on Computer Aided Verification, CAV 2024","volume":"14681","author":"Biere Armin","year":"2024","unstructured":"Armin Biere, Tobias Faller, Katalin Fazekas, Mathias Fleury, Nils Froleyks, and Florian Pollitt. 2024. CaDiCaL 2.0. In Proceedings of the 36th International Conference on Computer Aided Verification, CAV 2024. Lecture Notes in Computer Science, Vol. 14681, Arie Gurfinkel and Vijay Ganesh (Eds.), Springer, 133\u2013152."},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-19488-6_110"},{"key":"e_1_3_2_10_2","volume-title":"Proceedings of the 25th Annual ACM Symposium on Theory of Computing","author":"Bodlaender Hans L.","year":"1993","unstructured":"Hans L. Bodlaender. 1993. A linear time algorithm for finding tree-decompositions of small treewidth. In Proceedings of the 25th Annual ACM Symposium on Theory of Computing."},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2009.03.008"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1145\/2043174.2043195"},{"key":"e_1_3_2_13_2","volume-title":"Proceedings of IEEE International Symposium on Circuits and Systems (ISCAS 85)","author":"Brglez F.","year":"1985","unstructured":"F. Brglez and H. Fujiwara. 1985. A neutral netlist of 10 combinational benchmark circuits and a target translator in Fortran. In Proceedings of IEEE International Symposium on Circuits and Systems (ISCAS 85)."},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676819"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1109\/12.73590"},{"key":"e_1_3_2_16_2","doi-asserted-by":"crossref","first-page":"408","DOI":"10.1145\/127601.127703","volume-title":"Proceedings of the ACM\/IEEE Design Automation Conference","author":"Burch J. R.","year":"1991","unstructured":"J. R. Burch. 1991. Using BDDs to verify multipliers. In Proceedings of the ACM\/IEEE Design Automation Conference. 408\u2013412."},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.1137\/0606026"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","unstructured":"Bruno Courcelle and Stephan Olariu. 2000. Upper bounds to the clique width of graphs. Discrete Applied Mathematics 101 1 (2000) 77\u2013114. 10.1016\/S0166-218X(99)00184-5","DOI":"10.1016\/S0166-218X(99)00184-5"},{"key":"e_1_3_2_19_2","doi-asserted-by":"crossref","unstructured":"Marek Cygan F. Fomin Lukasz Kowalik Daniel Lokshtanov D\u00e1niel Marx Marcin Pilipczuk Michal Pilipczuk and Saket Saurabh. 2015. Parameterized algorithms. Springer.","DOI":"10.1007\/978-3-319-21275-3"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1109\/TEST.1999.805857"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14279-6"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.5555\/2464827"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1007\/b105236"},{"key":"e_1_3_2_24_2","first-page":"70:1\u201370:9","volume-title":"Proceedings of the IEEE\/ACM International Conference on Computer-Aided Design","author":"Drechsler Rolf","year":"2022","unstructured":"Rolf Drechsler and Alireza Mahzoon. 2022. Polynomial formal verification: Ensuring correctness under resource constraints. In Proceedings of the IEEE\/ACM International Conference on Computer-Aided Design. 70:1\u201370:9."},{"key":"e_1_3_2_25_2","first-page":"54","volume-title":"Proceedings of the Workshop on Synthesis and System Integration of Mixed Information Technologies","author":"Fey G.","year":"2003","unstructured":"G. Fey and R. Drechsler. 2003. A hybrid approach combining symbolic and structural techniques for disjoint SOP minimization. In Proceedings of the Workshop on Synthesis and System Integration of Mixed Information Technologies. 54\u201360."},{"key":"e_1_3_2_26_2","volume-title":"The Design and Implementation of the Postgres Query Optimizer: Research Project","author":"Fong Z.","year":"1986","unstructured":"Z. Fong, Berkeley. 1986. Department of Electrical Engineering University of California, and Computer Sciences. The Design and Implementation of the Postgres Query Optimizer: Research Project. Retrieved from https:\/\/books.google.de\/books?id=dx2AGwAACAAJ"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1982.1676041"},{"key":"e_1_3_2_28_2","article-title":"Computers and intractability: A guide to the theory of np-completeness, freeman","author":"Garey Michael R.","year":"1997","unstructured":"Michael R. Garey. 1997. Computers and intractability: A guide to the theory of np-completeness, freeman. Fundamental (1997).","journal-title":"Fundamental"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.5555\/574848"},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","unstructured":"Ivo H\u00e1le\u010dek Petr Fi\u0161er and Jan Schmidt. 2018. Towards AND\/XOR balanced synthesis: Logic circuits rewriting with XOR. Microelectronics Reliability 81 (2018) 274\u2013286. 10.1016\/j.microrel.2017.12.031","DOI":"10.1016\/j.microrel.2017.12.031"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1002\/j.1538-7305.1970.tb01770.x"},{"key":"e_1_3_2_32_2","first-page":"44","volume-title":"Proceedings of the 2022 International Symposium on Design and Diagnostics of Electronic Circuits and Systems","author":"Klhufek Jan","year":"2022","unstructured":"Jan Klhufek and Vojtech Mrazek. 2022. ArithsGen: Arithmetic circuit generator for hardware accelerators. In Proceedings of the 2022 International Symposium on Design and Diagnostics of Electronic Circuits and Systems. 44\u201347."},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(88)90039-6"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","DOI":"10.1145\/275107.275122"},{"key":"e_1_3_2_35_2","doi-asserted-by":"crossref","unstructured":"Alireza Mahzoon Daniel Gro\u00dfe and Rolf Drechsler. 2021. GenMul: Generating architecturally complex multipliers to challenge formal verification tools. In Recent Findings in Boolean Techniques Rolf Drechsler and Daniel Gro\u00dfe (Eds.). Springer 177\u2013191.","DOI":"10.1007\/978-3-030-68071-8_9"},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","unstructured":"Klaus Meer and Dieter Rautenbach. 2009. On the OBDD size for graphs of bounded tree- and clique-width. Discrete Math. 309 4 (March 2009) 843\u2013851. 10.1016\/j.disc.2008.01.022","DOI":"10.1016\/j.disc.2008.01.022"},{"key":"e_1_3_2_37_2","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1145\/1508128.1508152","volume-title":"Proceedings of the ACM\/SIGDA International Symposium on Field Programmable Gate Arrays (FPGA \u201909)","author":"Mishchenko Alan","year":"2009","unstructured":"Alan Mishchenko, Robert Brayton, Jie-Hong Roland Jiang, and Stephen Jang. 2009. Scalable don\u2019t-care-based logic optimization and resynthesis. In Proceedings of the ACM\/SIGDA International Symposium on Field Programmable Gate Arrays (FPGA \u201909). ACM, 151\u2013160."},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","DOI":"10.1145\/1233501.1233679"},{"key":"e_1_3_2_39_2","volume-title":"Proceedings of the Annual Design Automation Conference","author":"Mishchenko Alan","year":"2006","unstructured":"Alan Mishchenko, Satrajit Chatterjee, and Robert K. Brayton. 2006. DAG-aware AIG rewriting: A fresh look at combinational logic synthesis. In Proceedings of the Annual Design Automation Conference."},{"key":"e_1_3_2_40_2","volume-title":"FRAIGs: A Unifying Representation for Logic Synthesis and Verification","author":"Mishchenko Alan","year":"2005","unstructured":"Alan Mishchenko, Satrajit Chatterjee, Roland Jiang, and Robert Brayton. 2005. FRAIGs: A Unifying Representation for Logic Synthesis and Verification. Technical Report. Department of Electrical Engineering and Computer Sciences, University of California, Berkeley. Retrieved from https:\/\/people.eecs.berkeley.edu\/alanmi\/publications\/2005\/tech05_fraigs.pdf"},{"key":"e_1_3_2_41_2","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1109\/DSD64264.2024.00017","volume-title":"Proceedings of the 2024 27th Euromicro Conference on Digital System Design (DSD)","author":"M\u00fcller Luca","year":"2024","unstructured":"Luca M\u00fcller and Rolf Drechsler. 2024. SAT can ensure polynomial bounds for the verification of circuits with limited cutwidth. In Proceedings of the 2024 27th Euromicro Conference on Digital System Design (DSD). 57\u201364."},{"key":"e_1_3_2_42_2","first-page":"1","volume-title":"Proceedings of the 2024 IEEE European Test Symposium (ETS)","author":"Nadeem Mohamed","year":"2024","unstructured":"Mohamed Nadeem, Chandan Kumar Jha, and Rolf Drechsler. 2024. Polynomial formal verification of approximate adders with constant cutwidth. In Proceedings of the 2024 IEEE European Test Symposium (ETS). 1\u20136."},{"key":"e_1_3_2_43_2","volume-title":"Proceedings of the 2025 Design, Automation & Test in Europe Conference & Exhibition (DATE)","author":"Nadeem Mohamed","year":"2025","unstructured":"Mohamed Nadeem, Chandan Kumar Jha, and Rolf Drechsler. 2025. Polynomial formal verification of sequential circuits using weighted-AIGs. In Proceedings of the 2025 Design, Automation & Test in Europe Conference & Exhibition (DATE)."},{"key":"e_1_3_2_44_2","volume-title":"Proceedings of the 34th International Workshop on Rapid System Prototyping (RSP \u201923)","author":"Nadeem Mohamed","year":"2024","unstructured":"Mohamed Nadeem, Jan Kleinekathofer, and Rolf Drechsler. 2024. Polynomial formal verification exploiting constant cutwidth. In Proceedings of the 34th International Workshop on Rapid System Prototyping (RSP \u201923). ACM."},{"key":"e_1_3_2_45_2","doi-asserted-by":"publisher","DOI":"10.1023\/A:1012820722053"},{"key":"e_1_3_2_46_2","volume-title":"Proceedings of the 1st International ASP\u201901 Workshop","author":"Provetti Alessandro","year":"2001","unstructured":"Alessandro Provetti and Tran Cao Son. 2001. Answer set programming: Towards efficient and scalable knowledge representation and reasoning. In Proceedings of the 1st International ASP\u201901 Workshop."},{"key":"e_1_3_2_47_2","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2005.852031"},{"key":"e_1_3_2_48_2","doi-asserted-by":"crossref","first-page":"1326","DOI":"10.1109\/DATE.2009.5090870","volume-title":"Proceedings of the 2009 Design, Automation & Test in Europe Conference & Exhibition","author":"Sulflow Andre","year":"2009","unstructured":"Andre Sulflow, Gorschwin Fey, Cecile Braunstein, Ulrich Kuhne, and Rolf Drechsler. 2009. Increasing the accuracy of SAT-based debugging. In Proceedings of the 2009 Design, Automation & Test in Europe Conference & Exhibition. 1326\u20131331."},{"key":"e_1_3_2_49_2","doi-asserted-by":"publisher","unstructured":"G. S. Tseitin. 1983. On the Complexity of Derivation in Propositional Calculus. Springer Berlin Heidelberg Berlin Heidelberg 466\u2013483. 10.1007\/978-3-642-81955-1_28","DOI":"10.1007\/978-3-642-81955-1_28"},{"key":"e_1_3_2_50_2","unstructured":"ClaireWolf. 2016. Yosys Open SYnthesis Suite. Available at https:\/\/yosyshq.net\/yosys\/ (Accessed on October 20 2025)."},{"key":"e_1_3_2_51_2","unstructured":"S. Yang. 1991. Logic Synthesis and Optimization Benchmarks User Guide: Version 3.0. Microelectronics Center of North Carolina (MCNC)."},{"key":"e_1_3_2_52_2","first-page":"267","volume-title":"Proceedings of the 1st International Forum on Design Languages (FDL\u201998)","author":"Zimmermann Reto","year":"1998","unstructured":"Reto Zimmermann. 1998. VHDL library of arithmetic units. In Proceedings of the 1st International Forum on Design Languages (FDL\u201998). Citeseer, 267\u2013272."}],"container-title":["ACM Transactions on Design Automation of Electronic Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3771280","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,11]],"date-time":"2025-11-11T13:51:04Z","timestamp":1762869064000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3771280"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,11,11]]},"references-count":51,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2026,1,31]]}},"alternative-id":["10.1145\/3771280"],"URL":"https:\/\/doi.org\/10.1145\/3771280","relation":{},"ISSN":["1084-4309","1557-7309"],"issn-type":[{"type":"print","value":"1084-4309"},{"type":"electronic","value":"1557-7309"}],"subject":[],"published":{"date-parts":[[2025,11,11]]},"assertion":[{"value":"2025-03-28","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-10-05","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-11-11","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}