An HDL-centric synthesis and verification approach for RRAM-based neuromorphic systems

Resistive RAM (RRAM) enables in-memory computing by combining storage and computation, with several intrinsic operations, including Multiply and Accumulate (MAC) operations naturally supported by crossbar architectures. While MAC has been widely exploited in neuromorphic systems, its use for general Boolean logic remains underexplored. This paper presents a comprehensive synthesis and verification methodology for Logic-in-Memory (LiM) systems on RRAM crossbars, realized at a higher level of abstraction. We introduce a MAC-oriented LiM-HDL compilation flow that translates conventional Boolean descriptions into executable MAC operations. To ensure functional correctness, a formal verification framework based on SAT-based equivalence checking is employed. Experimental results on standard benchmark suites demonstrate significant reductions in computation cycles compared to existing RRAM-based logic synthesis approaches, highlighting the practicality of MAC-based logic for emerging in-memory computing systems.