Publikation
Automated Equivalence Checking Method for Majority based In-Memory Computing on ReRAM Crossbars
Arighna Deb; Kamalika Datta; Muhammad Hassan; Saeideh Shirinzadeh; Rolf Drechsler
In: Proceedings of the 28th Asia and South Pacific Design Automation Conference (ASP-DAC). Asia and South Pacific Design Automation Conference (ASP-DAC-2023), February 16-19, Tokyo, Japan, 2023.
Zusammenfassung
Recent progress in the fabrication of Resistive Random Access Memory (ReRAM) devices has paved the way for large scale crossbar structures. In particular, in-memory computing on ReRAM crossbars helps in bridging the processor-memory speed gap for current CMOS technology. To this end, synthesis and mapping of Boolean functions to such crossbars have been investigated by researchers. However the verification of simple designs on crossbar is still done through manual inspection or sometimes complemented by simulation based techniques. Clearly this is an important problem as real world designs are complex and have higher number of inputs.
As a result manual inspection and simulation based methods for these designs are not practical. In this paper for the first time as per our knowledge we propose an automated equivalence checking methodology for majority based in-memory designs on ReRAM crossbars. Our contributions are twofold: first, we introduce an intermediate data structure called ReRAM Sequence Graph (ReSG) to represent the logic-in-memory design. This in turn is translated into Boolean Satifiability (SAT) formulas. These SAT formulas are verified against the golden functional specification using Z3 Satifiability Modulo Theory (SMT) solver. We validate the proposed method by running widely available benchmarks