{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,17]],"date-time":"2026-07-17T15:06:18Z","timestamp":1784300778093,"version":"3.55.0"},"publisher-location":"New York, NY, USA","reference-count":31,"publisher":"ACM","license":[{"start":{"date-parts":[[2026,7,5]],"date-time":"2026-07-05T00:00:00Z","timestamp":1783209600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2026,7,5]]},"DOI":"10.1145\/3803437.3806400","type":"proceedings-article","created":{"date-parts":[[2026,7,17]],"date-time":"2026-07-17T14:27:39Z","timestamp":1784298459000},"page":"102-106","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["EquivFusion: Unifying Hardware Equivalence Checking from Algorithms to Netlists via MLIR"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0000-2023-2157","authenticated-orcid":false,"given":"Jiaying","family":"Zhu","sequence":"first","affiliation":[{"name":"The Chinese University of Hong Kong, Hong Kong, Hong Kong, Hong Kong"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-9879-2056","authenticated-orcid":false,"given":"Baoqi","family":"Zhang","sequence":"additional","affiliation":[{"name":"National Center of Technology Innovation for EDA, Nanjing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0002-0344-0282","authenticated-orcid":false,"given":"Mengxia","family":"Tao","sequence":"additional","affiliation":[{"name":"National Center of Technology Innovation for EDA, Nanjing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-2722-4983","authenticated-orcid":false,"given":"Kezhi","family":"Li","sequence":"additional","affiliation":[{"name":"The Chinese University of Hong Kong, Hong Kong, Hong Kong"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5312-4483","authenticated-orcid":false,"given":"Hao","family":"Yan","sequence":"additional","affiliation":[{"name":"Southeast University, Nanjing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6747-126X","authenticated-orcid":false,"given":"Qiang","family":"Xu","sequence":"additional","affiliation":[{"name":"The Chinese University of Hong Kong, Hong Kong, Hong Kong"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5486-2947","authenticated-orcid":false,"given":"Min","family":"Li","sequence":"additional","affiliation":[{"name":"Southeast University, Nanjing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2026,7,17]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"2025. CIRCT: Circuit IR Compilers and Tools. https:\/\/circt.llvm.org\/."},{"key":"e_1_3_2_1_2_1","unstructured":"2025. MLIR: Multi-Level Intermediate Representation. https:\/\/mlir.llvm.org\/."},{"key":"e_1_3_2_1_3_1","unstructured":"2025. torch-mlir. https:\/\/github.com\/llvm\/torch-mlir."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2228360.2228584"},{"key":"e_1_3_2_1_5_1","volume-title":"Proceedings of the 8th international workshop on satisfiability modulo theories","volume":"13","author":"Barrett Clark","year":"2010","unstructured":"Clark Barrett, Aaron Stump, Cesare Tinelli, et al. 2010. The smt-lib standard: Version 2.0. In Proceedings of the 8th international workshop on satisfiability modulo theories (Edinburgh, UK), Vol. 13. 14."},{"key":"e_1_3_2_1_6_1","unstructured":"Armin Biere. 2007. The AIGER and-inverter graph (AIG) format version 20071012. (2007)."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/12.494097"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/EWDTS.2008.5580149"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_5"},{"key":"e_1_3_2_1_10_1","unstructured":"Cadence Design Systems. 2025. Conformal Equivalence Checker Datasheet. https:\/\/www.cadence.com\/en_US\/home\/resources\/datasheets\/conformal-equivalence-checker-ds.html."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4020-8588-8"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/DATE.2006.243776"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_3_2_1_14_1","unstructured":"Amelia Dobis. 2024. Formal Verification of Hardware using MLIR. Master's thesis. ETH Zurich."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3508352.3561104"},{"key":"e_1_3_2_1_16_1","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_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2015.2481869"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1973009.1973054"},{"key":"e_1_3_2_1_19_1","volume-title":"Kolla Bhanu Prakash, and GR Kanagachidambaresan","author":"Imambi Sagar","year":"2021","unstructured":"Sagar Imambi, Kolla Bhanu Prakash, and GR Kanagachidambaresan. 2021. Py-Torch. In Programming with TensorFlow: solution for edge computing applications. Springer, 87\u2013104."},{"key":"e_1_3_2_1_20_1","volume-title":"van Eijk","author":"Kuehlmann Andreas","year":"2002","unstructured":"Andreas Kuehlmann and Cornelis A. J. van Eijk. 2002. Combinational and Sequential Equivalence Checking. Springer US, Boston, MA, 343\u2013372."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/CGO51591.2021.9370308"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/337292.337611"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/PACT52795.2021.00011"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","unstructured":"Rajdeep Mukherjee Mitra Purandare Raphael Polig and Daniel Kroening. 2017. Formal Techniques for Effective Co-verification of Hardware\/Software Co-designs. 10.1145\/3061639.3062253","DOI":"10.1145\/3061639.3062253"},{"key":"e_1_3_2_1_25_1","volume-title":"Bitwuzla. In International Conference on Computer Aided Verification. Springer, 3\u201317","author":"Niemetz Aina","year":"2023","unstructured":"Aina Niemetz and Mathias Preiner. 2023. Bitwuzla. In International Conference on Computer Aided Verification. Springer, 3\u201317."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96145-3_32"},{"key":"e_1_3_2_1_27_1","unstructured":"Synopsys. 2025. VC Formal Datapath Validation. https:\/\/www.synopsys.com\/verification\/static-and-formal-verification\/vc-formal\/vc-formal-datapath-validation.html."},{"key":"e_1_3_2_1_28_1","volume-title":"Formality: RTL-to-Gate Equivalence Checking. https:\/\/www.synopsys.com\/implementation-and-signoff\/signoff\/formality-equivalence-checking.html. Accessed: 2026-01-04.","year":"2026","unstructured":"Synopsys. 2026. Formality: RTL-to-Gate Equivalence Checking. https:\/\/www.synopsys.com\/implementation-and-signoff\/signoff\/formality-equivalence-checking.html. Accessed: 2026-01-04."},{"key":"e_1_3_2_1_29_1","unstructured":"Cadence Design Systems. 2025. Jasper C Formal Verification. https:\/\/www.cadence.com\/en_US\/home\/tools\/system-design-and-verification\/formal-and-static-verification\/jasper-c-formal-verification.html."},{"key":"e_1_3_2_1_30_1","unstructured":"Clifford Wolf Johann Glaser and Johannes Kepler. 2013. Yosys-A Free Verilog Synthesis Suite. https:\/\/api.semanticscholar.org\/CorpusID:202611483"},{"key":"e_1_3_2_1_31_1","volume-title":"EQY: Equivalence Checking with Yosys. https:\/\/github.com\/YosysHQ\/eqy.","author":"HQ.","year":"2023","unstructured":"YosysHQ. 2023. EQY: Equivalence Checking with Yosys. https:\/\/github.com\/YosysHQ\/eqy."}],"event":{"name":"FSE Companion '26: 34th ACM International Conference on the Foundations of Software Engineering","location":"Concordia University Montreal QC Canada","acronym":"FSE Companion '26","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering"]},"container-title":["Proceedings of the 34th ACM International Conference on the Foundations of Software Engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3803437.3806400","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,17]],"date-time":"2026-07-17T14:34:03Z","timestamp":1784298843000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3803437.3806400"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,7,5]]},"references-count":31,"alternative-id":["10.1145\/3803437.3806400","10.1145\/3803437"],"URL":"https:\/\/doi.org\/10.1145\/3803437.3806400","relation":{},"subject":[],"published":{"date-parts":[[2026,7,5]]},"assertion":[{"value":"2026-07-17","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}