Equivalence Checking of Majority-based Function Mapping on ReRAM Crossbars

Abstract:
Recent developments in Resistive Random Access Memory (ReRAM) technology have led to the fabrication of large-scale crossbar structures. The processor-memory speed gap in conventional computer architectures can be bridged using in-memory computing on ReRAM crossbars, with suitable mitigation of unwanted sneak path currents. Synthesis of Boolean functions and mapping them to such crossbars have been investigated by researchers. However, very little effort has been put in towards verification of such mapping approaches. For smaller designs, the verification of mapping is typically carried out through manual inspection and simulation. This is an important problem to address as real world designs are complex and require proper design verification. As such manual inspection and simulation based methods for larger designs are not practical. In this summary paper, we report an automated equivalence checking approach for majority-based in-memory designs on ReRAM crossbars, which was published recently. First, we introduce an intermediate data structure called ReRAM Sequence Graph (ReSG) to represent the logic-in-memory operations, which in turn is translated into Boolean Satisfiability (SAT) formulas. These formulas are verified against the original function specification using Z3 Satisfiability solver. The proposed approach has been validated by running on widely available benchmarks.