In-Memory SAT-Solver for Self-Verification of Programmable Memristive Architectures

Formal 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 overheads.