{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,11]],"date-time":"2025-11-11T14:03:09Z","timestamp":1762869789743,"version":"build-2065373602"},"reference-count":33,"publisher":"Association for Computing Machinery (ACM)","issue":"1","funder":[{"name":"Strategic Priority Research Program of the Chinese Academy of Sciences","award":["XDA0320000 and XDA0320300"],"award-info":[{"award-number":["XDA0320000 and XDA0320300"]}]}],"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                    Synthesizing circuits to achieve better PPA is crucial, particularly in datapath netlists with various arithmetic operators. The verification relies on the Combinational Equivalence Checking (CEC) techniques, checking the equivalence of two combinational circuits. Contemporary CEC tools commonly utilize SAT as the principal reasoning engine, employing a SAT-sweeping algorithm, which sequentially confirms the equivalence of internal pairs in topological order, merging verified equivalents to reduce the netlist\u2019s scale. Nonetheless, datapath circuits frequently comprise pairs of nodes characterized by relatively limited transitive fan-in cones, yet these nodes display a pronounced density of XOR chains. This particular arrangement presents considerable obstacles for SAT solvers. To address this, exact probability-based simulation (EPS) provides an effective solution, but its high memory requirements limit its applicability. This article proposes a hybrid CEC prover,\n                    <jats:sc>hybridCEC<\/jats:sc>\n                    , and its parallel version,\n                    <jats:sc>paraHCEC<\/jats:sc>\n                    . Firstly, we decrease the memory requirements of the EPS method and integrate it into the SAT-sweeping framework. Secondly, we propose a dynamic engine selection heuristic for SAT and EPS, based on XOR chain density. Thirdly, we improve efficiency by identifying and reducing redundant engine calls by detecting regularity in the circuits. Finally, we parallelize the internal SAT and EPS engines, resulting in a highly efficient parallel CEC prover. Extensive experiments on industrial datapath circuit benchmarks demonstrate that our method significantly outperforms the state-of-the-art prover ABC \u201c&amp;cec\u201d, achieving up to 100\u00d7 speedups on 40% of instances and over 1000\u00d7 speedups on 14%. Moreover, our 64-thread parallel version achieved an impressive 70\u00d7 speedup, highlighting its scalability and effectiveness.\n                  <\/jats:p>","DOI":"10.1145\/3773040","type":"journal-article","created":{"date-parts":[[2025,10,24]],"date-time":"2025-10-24T11:20:43Z","timestamp":1761304843000},"page":"1-27","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Datapath Combinational Equivalence Checking With Hybrid Sweeping Engines and Parallelization"],"prefix":"10.1145","volume":"31","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5702-2508","authenticated-orcid":false,"given":"Zhihan","family":"Chen","sequence":"first","affiliation":[{"name":"Key Laboratory of System Software (Chinese Academy of Sciences) and State Key Laboratory of Computer Science, Institute of Software Chinese Academy of Sciences","place":["Beijing, China"]},{"name":"University of the Chinese Academy of Sciences School of Computer Science and Technology","place":["Beijing, China"]}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5541-7194","authenticated-orcid":false,"given":"Xindi","family":"Zhang","sequence":"additional","affiliation":[{"name":"Key Laboratory of System Software (Chinese Academy of Sciences) and State Key Laboratory of Computer Science, Institute of Software Chinese Academy of Sciences","place":["Beijing, China"]},{"name":"University of the Chinese Academy of Sciences School of Computer Science and Technology","place":["Beijing, China"]}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-9704-8534","authenticated-orcid":false,"given":"Yuhang","family":"Qian","sequence":"additional","affiliation":[{"name":"Key Laboratory of System Software (Chinese Academy of Sciences) and State Key Laboratory of Computer Science, Institute of Software Chinese Academy of Sciences","place":["Beijing, China"]},{"name":"University of the Chinese Academy of Sciences School of Computer Science and Technology","place":["Beijing, China"]}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1730-6922","authenticated-orcid":false,"given":"Shaowei","family":"Cai","sequence":"additional","affiliation":[{"name":"Key Laboratory of System Software (Chinese Academy of Sciences) and State Key Laboratory of Computer Science, Institute of Software Chinese Academy of Sciences","place":["Beijing, China"]},{"name":"University of the Chinese Academy of Sciences School of Computer Science and Technology","place":["Beijing, China"]}]}],"member":"320","published-online":{"date-parts":[[2025,11,11]]},"reference":[{"key":"e_1_3_2_2_2","first-page":"341","volume-title":"Proceedings of the 9th International Conference on VLSI Design","author":"Agrawal Vishwani D.","year":"1996","unstructured":"Vishwani D. Agrawal and David Lee. 1996. Characteristic polynomial method for verification and test of combinational circuits. In Proceedings of the 9th International Conference on VLSI Design. IEEE, 341\u2013342."},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.1109\/DAC18072.2020.9218691"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.2004.1382541"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.1993.580110"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICCD.2010.5647645"},{"key":"e_1_3_2_7_2","first-page":"39","article-title":"PRS: A new parallel\/distributed framework for SAT","author":"Chen Zhihan","year":"2023","unstructured":"Zhihan Chen, Xindi Zhang, Yuhang Qian, and Shaowei Cai. 2023. PRS: A new parallel\/distributed framework for SAT. SAT COMPETITION 2023 (2023), 39.","journal-title":"SAT COMPETITION 2023 (2023)"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD57390.2023.10323876"},{"key":"e_1_3_2_9_2","first-page":"15","article-title":"Kissat mab: Combining vsids and chb through multi-armed bandit","volume":"2021","author":"Cherif Mohamed Sami","year":"2021","unstructured":"Mohamed Sami Cherif, Djamal Habet, and Cyril Terrioux. 2021. Kissat mab: Combining vsids and chb through multi-armed bandit. SAT COMPETITION 2021 (2021), 15.","journal-title":"SAT COMPETITION"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1109\/43.784120"},{"key":"e_1_3_2_11_2","doi-asserted-by":"crossref","unstructured":"Jeffrey M. Dudek Kuldeep S. Meel and Moshe Y. Vardi. 2017. The hard problems are almost everywhere for random CNF-XOR formulas. arXiv:1710.06378. Retrieved from https:\/\/arxiv.org\/abs\/1710.06378","DOI":"10.24963\/ijcai.2017\/84"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)82542-3"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24605-3_37"},{"key":"e_1_3_2_14_2","first-page":"50","article-title":"CaDiCaL, kissat, paracooba, plingeling and treengeling entering the SAT competition 2020","volume":"2020","author":"Fleury ABKFM","year":"2020","unstructured":"ABKFM Fleury and Maximilian Heisinger. 2020. CaDiCaL, kissat, paracooba, plingeling and treengeling entering the SAT competition 2020. SAT COMPETITION 2020 (2020), 50.","journal-title":"SAT COMPETITION"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-04921-2_33"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00163-010-0097-y"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.2004.1382542"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2002.804386"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.1609\/aaai.v35i5.16503"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2021.3083682"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1109\/12.769433"},{"key":"e_1_3_2_22_2","unstructured":"Alan Mishchenko et\u00a0al. 2007. ABC: A system for sequential synthesis and verification. Retrieved October 31 2025 from http:\/\/www.eecs.berkeley.edu\/alanmi\/abc"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.5555\/1509456.1509516"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1145\/1233501.1233679"},{"key":"e_1_3_2_25_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 K. Brayton. 2005. FRAIGs: A Unifying Representation for Logic Synthesis and Verification. Technical Report. ERL Technical Report."},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICCD.1998.727017"},{"issue":"10","key":"e_1_3_2_27_2","doi-asserted-by":"crossref","first-page":"3081","DOI":"10.1109\/TCAD.2019.2946254","article-title":"Parallel combinational equivalence checking","volume":"39","author":"Possani Vinicius N.","year":"2019","unstructured":"Vinicius N. Possani, Alan Mishchenko, Renato P. Ribas, and Andre I. Reis. 2019. Parallel combinational equivalence checking. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 39, 10 (2019), 3081\u20133092.","journal-title":"IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1109\/DAC63849.2025.11132604"},{"key":"e_1_3_2_29_2","first-page":"169","volume-title":"Proceedings of the 2016 Formal Methods in Computer-Aided Design","author":"Sayed-Ahmed Amr","year":"2016","unstructured":"Amr Sayed-Ahmed, Daniel Gro\u00dfe, Mathias Soeken, and Rolf Drechsler. 2016. Equivalence checking using Gr\u00f6bner bases. In Proceedings of the 2016 Formal Methods in Computer-Aided Design. IEEE, 169\u2013176."},{"key":"e_1_3_2_30_2","article-title":"CUDD: CU decision diagram package release 2.3. 0","volume":"621","author":"Somenzi Fabio","year":"1998","unstructured":"Fabio Somenzi. 1998. CUDD: CU decision diagram package release 2.3. 0. University of Colorado at Boulder 621.","journal-title":"University of Colorado at Boulder"},{"key":"e_1_3_2_31_2","first-page":"2 (1983), 466\u20134","article-title":"On the complexity of derivation in propositional calculus","author":"Tseitin Grigori S.","year":"1983","unstructured":"Grigori S. Tseitin. 1983. On the complexity of derivation in propositional calculus. Automation of Reasoning: 2: Classical Papers on Computational Logic 1967\u201319702 (1983), 466\u2013483.","journal-title":"Automation of Reasoning: 2: Classical Papers on Computational Logic 1967\u20131970"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.1109\/ATS.2006.261000"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","DOI":"10.1145\/1146909.1147044"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","DOI":"10.1145\/1146909.1146970"}],"container-title":["ACM Transactions on Design Automation of Electronic Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3773040","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,11]],"date-time":"2025-11-11T13:50:52Z","timestamp":1762869052000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3773040"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,11,11]]},"references-count":33,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2026,1,31]]}},"alternative-id":["10.1145\/3773040"],"URL":"https:\/\/doi.org\/10.1145\/3773040","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-05-24","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-10-17","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"}}]}}