Shirinzadeh, FatemehFatemehShirinzadehDeb, ArighnaArighnaDebShirinzadeh, SaeidehSaeidehShirinzadehKole, AbhoyAbhoyKoleDatta, KamalikaKamalikaDattaDrechsler, RolfRolfDrechsler2024-05-032024-09-052024-05-032024https://publica.fraunhofer.de/handle/publica/46715810.1109/VLSID60093.2024.00070Formal verification of programmable memristive architectures utilizing emerging nonvolatile memory technologies such as Resistive Random-Access Memory (RRAM) has only been recently addressed by a few works at the software level. In this paper we propose an in-memory SAT solver utilizing inherent analog features of RRAM that enables formal verification of arbitrary designs within resistive crossbars. More importantly, this allows self-verification of in-memory implementations as the correctness of designs can be dynamically checked. Additionally, the required architecture is presented, along with a complexity analysis for latency and hardware overheadsenconference paper