Towards Formal Verification for MAC-based In-Memory Computing

Resistive RAM (RRAM) is a non-volatile memory technology with an abrupt switching property that enables it to perform basic logic operations. RRAM also possesses analog computational features by means of the so-called Multiply and Accumulate (MAC) operation that can be performed in all memory columns simultaneously. The MAC operation is particularly interesting for neuromorphic computing as it enables highly parallelized calculation of complex matrix-vector multiplications on standard RRAM crossbars.So far, several forms of universal logic are executed within RRAM devices, which have been the basis for a variety of logic-in-memory synthesis approaches. Recent research has addressed the mapping of logical functions to RRAM crossbars using the MAC operation, which allows for the facilitation of RRAM-based neuromorphic architectures with a basic logical core. Recently, a few formal verification methods have been introduced, which are tailored for synthesis approaches using certain RRAM logic primitives, such as in-memory styles based on the three-input majority operation and NOR gates. This paper analyzes these methods and, for the first time, proposes a verification method customized for MAC-based in-memory computing. A case study has been conducted to compare the proposed method with the existing methods, which reveals the superior performance of our method.