{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,5]],"date-time":"2026-06-05T15:48:03Z","timestamp":1780674483859,"version":"3.54.1"},"publisher-location":"New York, NY, USA","reference-count":25,"publisher":"ACM","license":[{"start":{"date-parts":[[2023,9,21]],"date-time":"2023-09-21T00:00:00Z","timestamp":1695254400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2023,9,21]]},"DOI":"10.1145\/3625223.3649274","type":"proceedings-article","created":{"date-parts":[[2024,6,21]],"date-time":"2024-06-21T15:03:43Z","timestamp":1718982223000},"page":"1-7","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":9,"title":["Polynomial Formal Verification exploiting Constant Cutwidth"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0835-1070","authenticated-orcid":false,"given":"Mohamed","family":"Nadeem","sequence":"first","affiliation":[{"name":"University of Bremen, Bremen, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6357-0914","authenticated-orcid":false,"given":"Jan","family":"Kleinekathofer","sequence":"additional","affiliation":[{"name":"University of Bremen, Bremen, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9872-1740","authenticated-orcid":false,"given":"Rolf","family":"Drechsler","sequence":"additional","affiliation":[{"name":"University of Bremen, Bremen, Germany"},{"name":"DFKI GmbH, Bremen, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,6,21]]},"reference":[{"key":"e_1_3_2_1_2_1","doi-asserted-by":"crossref","first-page":"92","DOI":"10.1145\/2043174.2043195","article-title":"Answer Set Programming at a Glance","volume":"54","author":"Brewka Gerhard","year":"2011","unstructured":"Gerhard Brewka, Thomas Eiter, and Miros\u0142aw Truszczy\u0144ski. 2011. Answer Set Programming at a Glance. ACM 54, 12 (2011), 92--103.","journal-title":"ACM"},{"key":"e_1_3_2_1_3_1","first-page":"268","article-title":"On the Cutwidth and the Topological Bandwidth of a Tree","volume":"6","author":"Chung Fan R. K.","year":"1985","unstructured":"Fan R. K. Chung. 1985. On the Cutwidth and the Topological Bandwidth of a Tree. SIDMA 6, 2 (1985), 268--277.","journal-title":"SIDMA"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"crossref","unstructured":"W. F. Clocksin and C. S. Mellish. 1987. Programming in Prolog.","DOI":"10.1007\/978-3-642-97005-4"},{"key":"e_1_3_2_1_5_1","volume-title":"Graph Theory","author":"Diestel Reinhard","unstructured":"Reinhard Diestel. 2010. Graph Theory (fourth ed.). Vol. 173. Springer."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"crossref","unstructured":"Rolf Drechsler. 2021. PolyAdd: Polynomial Formal Verification of Adder Circuits. In DDECS. 99--104.","DOI":"10.1109\/DDECS52668.2021.9417052"},{"key":"e_1_3_2_1_7_1","first-page":"1","article-title":"Polynomial Formal Verification: Ensuring Correctness under Resource Constraints","volume":"70","author":"Drechsler Rolf","year":"2022","unstructured":"Rolf Drechsler and Alireza Mahzoon. 2022. Polynomial Formal Verification: Ensuring Correctness under Resource Constraints. In ICCAD. 70:1--70:9.","journal-title":"ICCAD."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"crossref","first-page":"112","DOI":"10.1007\/s100090100056","article-title":"Binary Decision Diagrams in Theory and Practice","volume":"3","author":"Drechsler R.","year":"2001","unstructured":"R. Drechsler and D. Sieling. 2001. Binary Decision Diagrams in Theory and Practice. STTT 3 (2001), 112--136.","journal-title":"STTT"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"crossref","first-page":"762","DOI":"10.1109\/12.53597","article-title":"Computational Complexity of Controllability\/Observability Problems for Combinational Circuits","volume":"39","author":"Fujiwara Hideo","year":"1990","unstructured":"Hideo Fujiwara. 1990. Computational Complexity of Controllability\/Observability Problems for Combinational Circuits. IEEE Trans. Computers 39, 6 (1990), 762--767.","journal-title":"IEEE Trans. Computers"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"crossref","unstructured":"Martin Gebser Roland Kaminski Benjamin Kaufmann and Torsten Schaub. 2012. Answer Set Solving in Practice.","DOI":"10.1007\/978-3-031-01561-8"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"crossref","unstructured":"Martin Gebser Roland Kaminski Arne K\u00f6nig and Torsten Schaub. 2011. Advances in gringo Series 3. In LPNMR. 345--351.","DOI":"10.1007\/978-3-642-20895-9_39"},{"key":"e_1_3_2_1_12_1","volume-title":"The Stable Model Semantics For Logic Programming. Logic Programming 2","author":"Gelfond Michael","year":"2000","unstructured":"Michael Gelfond and Vladimir Lifschitz. 2000. The Stable Model Semantics For Logic Programming. Logic Programming 2 (2000)."},{"key":"e_1_3_2_1_13_1","first-page":"557","article-title":"Cutwidth","volume":"81","author":"Giannopoulou Archontia C.","year":"2019","unstructured":"Archontia C. Giannopoulou, Michal Pilipczuk, Jean-Florent Raymond, Dimitrios M. Thilikos, and Marcin Wrochna. 2019. Cutwidth: Obstructions and Algorithmic Aspects. Algorithmica 81, 2 (2019), 557--588.","journal-title":"Obstructions and Algorithmic Aspects. Algorithmica"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"crossref","unstructured":"Aarti Gupta Malay K. Ganai and Chao Wang. 2006. SAT-Based Verification Methods and Applications in Hardware Verification. In Formal Methods for Hardware Verification. 108--143.","DOI":"10.1007\/11757283_5"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"crossref","unstructured":"John Harrison. 2008. Theorem Proving for Verification (Invited Tutorial). In CAV. 11--18.","DOI":"10.1007\/978-3-540-70545-1_4"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"crossref","unstructured":"Jan Klhufek and Vojtech Mrazek. 2022. ArithsGen: Arithmetic Circuit Generator for Hardware Accelerators. In DDECS. 44--47.","DOI":"10.1109\/DDECS54261.2022.9770152"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"crossref","unstructured":"Alireza Mahzoon and Rolf Drechsler. 2021. Late Breaking Results: Polynomial Formal Verification of Fast Adders. In DAC. 1376--1377.","DOI":"10.1109\/DAC18074.2021.9586107"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"crossref","unstructured":"Alireza Mahzoon and Rolf Drechsler. 2021. Polynomial Formal Verification of Prefix Adders. In ATS. 85--90.","DOI":"10.1109\/ATS52891.2021.00027"},{"key":"e_1_3_2_1_19_1","first-page":"1","article-title":"PolyCleaner: Clean your Polynomials before Backward Rewriting to Verify Million-gate Multipliers","volume":"129","author":"Mahzoon Alireza","year":"2018","unstructured":"Alireza Mahzoon, Daniel Gro\u00dfe, and Rolf Drechsler. 2018. PolyCleaner: Clean your Polynomials before Backward Rewriting to Verify Million-gate Multipliers. In ICCAD. 129:1--129:8.","journal-title":"ICCAD."},{"key":"e_1_3_2_1_20_1","volume-title":"Marek and Miroslaw Truszczynski","author":"Victor","year":"1998","unstructured":"Victor W. Marek and Miroslaw Truszczynski. 1998. Stable models and an alternative logic programming paradigm. A Computing Research Repository (1998)."},{"key":"e_1_3_2_1_21_1","volume-title":"Brayton","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 DAC. 532--535."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1018930122475"},{"key":"e_1_3_2_1_23_1","first-page":"509","article-title":"Why is Combinational ATPG Efficiently Solvable for Practical VLSI Circuits","volume":"17","author":"Prasad Mukul R.","year":"2001","unstructured":"Mukul R. Prasad, Philip Chong, and Kurt Keutzer. 2001. Why is Combinational ATPG Efficiently Solvable for Practical VLSI Circuits? JETTA 17 (2001), 509--527.","journal-title":"JETTA"},{"key":"e_1_3_2_1_24_1","volume-title":"Proceedings of the 1st Intl. ASP'01 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 Intl. ASP'01 Workshop."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/j.jalgor.2004.12.001","article-title":"Cutwidth I: A linear time fixed parameter algorithm","volume":"56","author":"Thilikos Dimitrios M.","year":"2005","unstructured":"Dimitrios M. Thilikos, Maria Serna, and Hans L. Bodlaender. 2005. Cutwidth I: A linear time fixed parameter algorithm. Journal of Algorithms 56, 1 (2005), 1--24.","journal-title":"Journal of Algorithms"},{"key":"e_1_3_2_1_26_1","unstructured":"Clifford Wolf. 2022. Yosys open synthesis suit. available at https:\/\/github.com\/YosysHQ\/yosys."}],"event":{"name":"RSP '23: 34th International Workshop on Rapid System Prototyping","location":"Hamburg Germany","acronym":"RSP '23","sponsor":["SIGBED ACM Special Interest Group on Embedded Systems","SIGDA ACM Special Interest Group on Design Automation","SIGMICRO ACM Special Interest Group on Microarchitectural Research and Processing","CEDA","IEEE CAS"]},"container-title":["Proceedings of the 34th International Workshop on Rapid System Prototyping"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3625223.3649274","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3625223.3649274","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T22:50:03Z","timestamp":1750287003000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3625223.3649274"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,9,21]]},"references-count":25,"alternative-id":["10.1145\/3625223.3649274","10.1145\/3625223"],"URL":"https:\/\/doi.org\/10.1145\/3625223.3649274","relation":{},"subject":[],"published":{"date-parts":[[2023,9,21]]},"assertion":[{"value":"2024-06-21","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}