{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,7]],"date-time":"2026-03-07T18:05:08Z","timestamp":1772906708293,"version":"3.50.1"},"reference-count":39,"publisher":"Association for Computing Machinery (ACM)","issue":"6","license":[{"start":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T00:00:00Z","timestamp":1726012800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"German Research Foundation (DFG) within the Project PLiM","award":["DR 287\/35-1, DR 287\/35-2, SH 1917\/1-2"],"award-info":[{"award-number":["DR 287\/35-1, DR 287\/35-2, SH 1917\/1-2"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Embed. Comput. Syst."],"published-print":{"date-parts":[[2024,11,30]]},"abstract":"<jats:p>\n            Recent advancements in the fabrication of\n            <jats:italic>Resistive Random Access Memory<\/jats:italic>\n            (ReRAM) devices have led to the development of large-scale crossbar structures. In-memory computing architectures relying on ReRAM crossbars aim to mitigate the processor-memory bottleneck that exists with current complementary metal-oxide semiconductor technology. With this motivation, several synthesis and mapping approaches focusing on the realizations of Boolean functions in the ReRAM crossbars have been proposed earlier. Thus far, the verification of the designs realized on ReRAM crossbars is done either through manual inspection or using simulation-based approaches. Since manual inspections and simulation-based approaches are limited to smaller designs, they cannot be applied to the verification of complex designs on large-scale ReRAM crossbars.\n          <\/jats:p>\n          <jats:p>\n            Motivated by this, we propose, for the first time, an automatic equivalence checking flow that determines the equivalence between the original function specification (e.g.,\n            <jats:italic>Majority-inverter Graph<\/jats:italic>\n            ) and the crossbar micro-operations file formats. We consider two crossbar structures,\n            <jats:italic>zero-transistor, one-memristor\u00a0(0T1R)<\/jats:italic>\n            and\n            <jats:italic>one-transistor, one-memristor\u00a0(1T1R)<\/jats:italic>\n            to implement the micro-operations. While the micro-operations file format exists for 0T1R crossbar structures, no representations for micro-operations to be executed in 1T1R crossbars exist yet. In this work, we introduce the micro-operation file format for 1T1R crossbar structures to efficiently represent the micro-operations as ReRAM crossbar netlists. Afterwards, we introduce two intermediate data structures,\n            <jats:italic>ReRAM Sequence Graph<\/jats:italic>\n            for 0T1R crossbars\u00a0\n            <jats:italic>(ReSG-0T1R)<\/jats:italic>\n            and for 1T1R crossbars\u00a0\n            <jats:italic>(ReSG-1T1R)<\/jats:italic>\n            , that are derived from the 0T1R and 1T1R crossbar micro-operations file formats, respectively. These ReSGs are then translated into\n            <jats:italic>Boolean Satisfiability<\/jats:italic>\n            (SAT) formula, and then the verification is done by checking the generated SAT formulae against the golden functional specification (represented in Verilog) using\n            <jats:italic>Z3 Satisfiability<\/jats:italic>\n            solver. Experimental evaluations confirm the effectiveness of the proposed verification methodology on MCNC and ISCAS benchmarks.\n          <\/jats:p>","DOI":"10.1145\/3615358","type":"journal-article","created":{"date-parts":[[2023,8,9]],"date-time":"2023-08-09T12:28:57Z","timestamp":1691584137000},"page":"1-24","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["ReSG: A Data Structure for Verification of Majority-based In-memory Computing on ReRAM Crossbars"],"prefix":"10.1145","volume":"23","author":[{"ORCID":"https:\/\/orcid.org\/0009-0009-1976-7619","authenticated-orcid":false,"given":"Kousik","family":"Bhunia","sequence":"first","affiliation":[{"name":"School of Electronics Engineering, KIIT DU, Bhubaneswar, India"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2993-3184","authenticated-orcid":false,"given":"Arighna","family":"Deb","sequence":"additional","affiliation":[{"name":"School of Electronics Engineering, KIIT DU, Bhubaneswar, India"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1191-998X","authenticated-orcid":false,"given":"Kamalika","family":"Datta","sequence":"additional","affiliation":[{"name":"German Research Centre for Artificial Intelligence (DFKI), Bremen, Germany, Group of Computer Architecture, University of Bremen, Bremen, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4217-3079","authenticated-orcid":false,"given":"Muhammad","family":"Hassan","sequence":"additional","affiliation":[{"name":"German Research Centre for Artificial Intelligence (DFKI), Bremen, Germany, Group of Computer Architecture, University of Bremen, Bremen, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8824-1428","authenticated-orcid":false,"given":"Saeideh","family":"Shirinzadeh","sequence":"additional","affiliation":[{"name":"German Research Centre for Artificial Intelligence (DFKI), Bremen, Germany, Fraunhofer Institute for Systems and Innovation Research (ISI), Karlsruhe, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9872-1740","authenticated-orcid":false,"given":"Rolf","family":"Drechsler","sequence":"additional","affiliation":[{"name":"German Research Centre for Artificial Intelligence (DFKI), Bremen, Germany Group of Computer Architecture, University of Bremen, Bremen, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,9,11]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.1145\/2593069.2593158"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.1109\/VLSID.2017.10"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.5555\/1550723"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1038\/nature08940"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1109\/IDT.2014.7038601"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICRC.2017.8123643"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1109\/TCT.1971.1083337"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1109\/PROC.1976.10092"},{"key":"e_1_3_2_10_2","unstructured":"C. F. Coors. 2022. Verification of Programs Generated from HDL for the Programmable Logic-In-Memory (PLiM) Architecture. Master Thesis Group of Computer Architecture University of Bremen Bremen Germany."},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1109\/DSD57027.2022.00111"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1145\/3566097.3567842"},{"key":"e_1_3_2_13_2","first-page":"502","volume-title":"Proceedings of the International Conference on Theory and Applications of Satisfiability Testing","author":"E\u00e9n N.","year":"2003","unstructured":"N. E\u00e9n and N. S\u00f6rensson. 2003. An extensible SAT-solver. In Proceedings of the International Conference on Theory and Applications of Satisfiability Testing. Springer, 502\u2013518."},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.1109\/DSD57027.2022.00114"},{"key":"e_1_3_2_15_2","first-page":"427","volume-title":"Proceedings of the Design, Automation and Test in Europe Conference and Exhibition (DATE\u201916)","author":"Gaillardon P.-E.","year":"2016","unstructured":"P.-E. Gaillardon, L. Amar\u00fa, A. Siemon, E. Linn, R. Waser, A. Chattopadhyay, and G. De Micheli. 2016. The programmable logic-in-memory (PLiM) computer. In Proceedings of the Design, Automation and Test in Europe Conference and Exhibition (DATE\u201916). 427\u2013432."},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1109\/TVLSI.2017.2763171"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.5555\/367072.367111"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1109\/54.785838"},{"issue":"10","key":"e_1_3_2_19_2","article-title":"SIMPLER MAGIC: Synthesis and mapping of in-memory logic executed in a single row to improve throughput","volume":"39","author":"Hur R. B.","year":"2020","unstructured":"R. B. Hur, R. Ronen, A. H. Ali, D. Bhattacharjee, A. Eliahu, N. Peled, and S. Kvatinsky. 2020. SIMPLER MAGIC: Synthesis and mapping of in-memory logic executed in a single row to improve throughput. IEEE Trans. Comput. Aided Des. Integr. Circ. Syst. 39, 10 (2020), 2434\u2013244.","journal-title":"IEEE Trans. Comput. Aided Des. Integr. Circ. Syst."},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1109\/IWCMC.2018.8450341"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1145\/266021.266090"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2002.804386"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1109\/TCSII.2014.2357292"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1142\/S0218126622500712"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1145\/240518.240637"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2017.2750064"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.3850\/9783981537079_0771"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-51724-7_17"},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","DOI":"10.1038\/nature06932"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1109\/TNANO.2016.2570248"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.3390\/electronics7100224"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","DOI":"10.1109\/TCSI.2018.2792474"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","DOI":"10.1109\/IDT.2016.7843030"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.vlsi.2019.11.014"},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","DOI":"10.1109\/ISSCC42613.2021.9365769"},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.vlsi.2018.10.001"},{"key":"e_1_3_2_38_2","volume-title":"Logic Synthesis and Optimization Benchmarks User Guide: Version 3.0","author":"Yang S.","year":"1991","unstructured":"S. Yang. 1991. Logic Synthesis and Optimization Benchmarks User Guide: Version 3.0. Citeseer."},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.mejo.2012.10.001"},{"key":"e_1_3_2_40_2","doi-asserted-by":"publisher","DOI":"10.1145\/3287624.3287672"}],"container-title":["ACM Transactions on Embedded Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3615358","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3615358","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:36:53Z","timestamp":1750178213000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3615358"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,9,11]]},"references-count":39,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2024,11,30]]}},"alternative-id":["10.1145\/3615358"],"URL":"https:\/\/doi.org\/10.1145\/3615358","relation":{},"ISSN":["1539-9087","1558-3465"],"issn-type":[{"value":"1539-9087","type":"print"},{"value":"1558-3465","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,9,11]]},"assertion":[{"value":"2023-01-29","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-07-31","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-09-11","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}