{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,26]],"date-time":"2025-11-26T16:49:48Z","timestamp":1764175788554,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":47,"publisher":"ACM","license":[{"start":{"date-parts":[[2024,10,27]],"date-time":"2024-10-27T00:00:00Z","timestamp":1729987200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["2319399","2404036"],"award-info":[{"award-number":["2319399","2404036"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2024,10,27]]},"DOI":"10.1145\/3676536.3676721","type":"proceedings-article","created":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T13:21:20Z","timestamp":1744204880000},"page":"1-9","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Equivalence Checking for Flow-Based Computing using Iterative SAT Solving"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8522-4617","authenticated-orcid":false,"given":"Sven","family":"Thijssen","sequence":"first","affiliation":[{"name":"Department of Electrical Engineering and Computer Science, Florida Atlantic University, Boca Raton, FL, United States"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0450-695X","authenticated-orcid":false,"given":"Muhammad Rashedul Haq","family":"Rashed","sequence":"additional","affiliation":[{"name":"Department of Computer Science and Engineering, University of Texas at Arlington, Arlington, TX, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0174-8822","authenticated-orcid":false,"given":"Muhammad Rubel","family":"Ahmed","sequence":"additional","affiliation":[{"name":"Department of Electrical and Computer Engineering, University of Central Florida, Orlando, FL, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9987-4848","authenticated-orcid":false,"given":"Suraj","family":"Singireddy","sequence":"additional","affiliation":[{"name":"Department of Electrical and Computer Engineering, University of Texas at San Antonio, San Antonio, TX, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0354-2940","authenticated-orcid":false,"given":"Sumit Kumar","family":"Jha","sequence":"additional","affiliation":[{"name":"Knight Foundation School of Computing and Information Sciences, Florida International University, Miami, FL, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4183-6926","authenticated-orcid":false,"given":"Rickard","family":"Ewetz","sequence":"additional","affiliation":[{"name":"Department of Electrical and Computer Engineering, University of Florida, Gainesville, FL, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,4,9]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"[n. d.]. Joint University Microelectronics Program. https:\/\/www.darpa.mil\/program\/joint-university-microelectronics-program."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/TED.2018.2856818"},{"key":"e_1_3_2_1_3_1","volume-title":"Proceedings of the 24th International Workshop on Logic & Synthesis (IWLS).","author":"Amar\u00fa Luca","year":"2015","unstructured":"Luca Amar\u00fa, Pierre-Emmanuel Gaillardon, and Giovanni De Micheli. 2015. The EPFL combinational benchmark suite. In Proceedings of the 24th International Workshop on Logic & Synthesis (IWLS)."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.5555\/1661445.1661509"},{"key":"e_1_3_2_1_5_1","volume-title":"Memristive' switches enable 'stateful' logic operations via material implication. Nature 464, 7290","author":"Borghetti Julien","year":"2010","unstructured":"Julien Borghetti, Gregory S Snider, Philip J Kuekes, J Joshua Yang, Duncan R Stewart, and R Stanley Williams. 2010. 'Memristive' switches enable 'stateful' logic operations via material implication. Nature 464, 7290 (2010), 873--876."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_5"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1116\/1.3301579"},{"key":"e_1_3_2_1_8_1","volume-title":"Automation & Test in Europe Conference & Exhibition (DATE)","author":"Chakraborty Dwaipayan","year":"2017","unstructured":"Dwaipayan Chakraborty and Sumit Kumar Jha. 2017. Automated synthesis of compact crossbars for sneak-path based in-memory computing. In Design, Automation & Test in Europe Conference & Exhibition (DATE), 2017. IEEE, 770--775."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISCAS.2017.8050965"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISCAS.2017.8050965"},{"key":"e_1_3_2_1_11_1","volume-title":"Sumit Kumar Jha, and Helmut Veith","author":"Clarke Edmund","year":"2005","unstructured":"Edmund Clarke, Ansgar Fehnker, Sumit Kumar Jha, and Helmut Veith. 2005. Temporal logic model checking. Handbook of Networked and Embedded Control Systems (2005), 539--558."},{"key":"e_1_3_2_1_12_1","volume-title":"Introduction to Algorithms","author":"Cormen Thomas H.","unstructured":"Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest, and Clifford Stein. 2009. Introduction to Algorithms, Third Edition (3rd ed.). The MIT Press.","edition":"3"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2000064.2000108"},{"key":"e_1_3_2_1_14_1","volume-title":"Automation & Test in Europe Conference & Exhibition (DATE). Ieee, 427--432","author":"Gaillardon Pierre-Emmanuel","year":"2016","unstructured":"Pierre-Emmanuel Gaillardon, Luca Amar\u00fa, Anne Siemon, Eike Linn, Rainer Waser, Anupam Chattopadhyay, and Giovanni De Micheli. 2016. The programmable logic-in-memory (PLiM) computer. In 2016 Design, Automation & Test in Europe Conference & Exhibition (DATE). Ieee, 427--432."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCSII.2018.2821678"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2897937.2898010"},{"key":"e_1_3_2_1_18_1","unstructured":"Yiming Huai et al. 2008. Spin-transfer torque MRAM (STT-MRAM): Challenges and prospects. AAPPS bulletin 18 6 (2008) 33--40."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3307650.3322237"},{"volume-title":"Towards automated system synthesis using sciduction","author":"Jha Susmit Kumar","key":"e_1_3_2_1_20_1","unstructured":"Susmit Kumar Jha. 2011. Towards automated system synthesis using sciduction. University of California, Berkeley."},{"key":"e_1_3_2_1_21_1","volume-title":"On the Design of Novel Attention Mechanism for Enhanced Efficiency of Transformers. In 61st ACM Design Automation Conference (DAC).","author":"Jha Sumit Kumar","year":"2024","unstructured":"Sumit Kumar Jha, Susmit Jha, Rickard Ewetz, and Alvaro Velasquez. 2024. On the Design of Novel Attention Mechanism for Enhanced Efficiency of Transformers. In 61st ACM Design Automation Conference (DAC)."},{"key":"e_1_3_2_1_22_1","volume-title":"NAECON 2024 - IEEE National Aerospace and Electronics Conference.","author":"Jha Sumit Kumar","year":"2024","unstructured":"Sumit Kumar Jha, Susmit Jha, Muhammad Rashedul Haq Rashed, Rickard Ewetz, and Alvaro Velasquez. 2024. Automated Synthesis of Hardware Designs using Symbolic Feedback and Grammar-Constrained Decoding in Large Language Models. In NAECON 2024 - IEEE National Aerospace and Electronics Conference."},{"key":"e_1_3_2_1_23_1","first-page":"319","article-title":"Computation of boolean formulas using sneak paths in crossbar computing","volume":"9","author":"Jha Sumit Kumar","year":"2016","unstructured":"Sumit Kumar Jha, Dilia E Rodriguez, Joseph E Van Nostrand, and Alvaro Velasquez. 2016. Computation of boolean formulas using sneak paths in crossbar computing. US Patent 9,319,047.","journal-title":"US Patent"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1137\/0204007"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICCD.1996.563581"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCSII.2014.2357292"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCSII.2015.2433536"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2897937.2898064"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/MCSE.2017.57"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1233501.1233679"},{"key":"e_1_3_2_1_31_1","first-page":"961","article-title":"Design and fabrication of flow-based edge detection memristor crossbar circuits","volume":"67","author":"Pannu Jodh Singh","year":"2020","unstructured":"Jodh Singh Pannu, Sunny Raj, Steven Lawrence Fernandes, Dwaipayan Chakraborty, Sarah Rafiq, Nathaniel Cady, and Sumit Kumar Jha. 2020. Design and fabrication of flow-based edge detection memristor crossbar circuits. IEEE Transactions on Circuits and Systems II: Express Briefs 67, 5 (2020), 961--965.","journal-title":"IEEE Transactions on Circuits and Systems II: Express Briefs"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD51958.2021.9643526"},{"key":"e_1_3_2_1_33_1","first-page":"48109","article-title":"Restoring circuit structure from SAT instances","volume":"1001","author":"Roy Jarrod A","year":"2004","unstructured":"Jarrod A Roy, Igor L Markov, and Valeria Bertacco. 2004. Restoring circuit structure from SAT instances. Ann Arbor 1001 (2004), 48109--2122.","journal-title":"Ann Arbor"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/AICAS54282.2022.9869979"},{"key":"e_1_3_2_1_35_1","volume-title":"SAT 2005","author":"Sorensson Niklas","year":"2005","unstructured":"Niklas Sorensson and Niklas Een. 2005. Minisat v1. 13-a sat solver with conflict-clause minimization. SAT 2005, 53 (2005), 1--2."},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2021.3138356"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICCD56317.2022.00101"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3489517.3530596"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3649329.3657340"},{"key":"e_1_3_2_1_40_1","volume-title":"Verification of Flow-Based Computing Systems Using Bounded Model Checking. In 2023 IEEE\/ACM International Conference on Computer Aided Design (ICCAD). IEEE, 1--9.","author":"Thijssen Sven","year":"2023","unstructured":"Sven Thijssen, Suraj Singireddy, Muhammad Rashedul Haq Rashed, Sumit Kumar Jha, and Rickard Ewetz. 2023. Verification of Flow-Based Computing Systems Using Bounded Model Checking. In 2023 IEEE\/ACM International Conference on Computer Aided Design (ICCAD). IEEE, 1--9."},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1109\/MCSE.2017.25"},{"key":"e_1_3_2_1_42_1","volume-title":"On the complexity of derivation in propositional calculus. Automation of reasoning: 2: Classical papers on computational logic 1967--1970","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--1970 (1983), 466--483."},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1109\/IDT.2014.7038603"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICCD.2015.7357090"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/216585.216588"},{"key":"e_1_3_2_1_46_1","unstructured":"Saeyang Yang. 1991. Logic synthesis and optimization benchmarks user guide: version 3.0. Citeseer."},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.2200\/S00736ED1V01Y201609EET008"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/2966986.2967069"}],"event":{"name":"ICCAD '24: 43rd IEEE\/ACM International Conference on Computer-Aided Design","sponsor":["SIGDA ACM Special Interest Group on Design Automation","IEEE CAS","IEEE CEDA","IEEE EDS"],"location":"Newark Liberty International Airport Marriott New York NY USA","acronym":"ICCAD '24"},"container-title":["Proceedings of the 43rd IEEE\/ACM International Conference on Computer-Aided Design"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3676536.3676721","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3676536.3676721","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3676536.3676721","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T23:43:57Z","timestamp":1750290237000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3676536.3676721"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,10,27]]},"references-count":47,"alternative-id":["10.1145\/3676536.3676721","10.1145\/3676536"],"URL":"https:\/\/doi.org\/10.1145\/3676536.3676721","relation":{},"subject":[],"published":{"date-parts":[[2024,10,27]]},"assertion":[{"value":"2025-04-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}