Verification of In-Memory Logic Design using ReRAM Crossbars

Resistive Random Access Memory (ReRAM) technologies enable the development of innovative architectures for inmemory computing. Many logic design styles, like Imply, Magic or Majority, have been explored for mapping Boolean functions to ReRAM crossbars. However, little attention has been given to the verification of the mapping process. Simulation based approaches can be used to check the functional correctness of smaller designs, but only formal verification techniques can ensure completeness for larger designs. Some initial works in this area have been proposed, which specifically focus on the verification of micro-operations using majority-based logic design. However, these techniques cannot be directly applied to other logic design styles, like Imply or Magic. This necessitates the design and exploration of more general verification techniques for logic-in-memory using ReRAM crossbars, and opens up the scope for further investigation. In this paper, we provide an overview of existing verification techniques for logic-in-memory designs, and also discuss directions for future work.