A Comprehensive Synthesis and Verification Approach for RRAM-Based Neuromorphic Computing

Resistive RAM (RRAM) has emerged as a promising technology for in-memory computing by enabling storage and computation within the same physical substrate. While its analog computation capability, particularly the multiply-accumulate (MAC) operation, has been effectively used in neuromorphic systems, its potential for logic synthesis remains underexplored. Logic synthesis using MAC not only unlocks new efficiency gains but also aligns with hardware already present in neuromorphic accelerators. In this work, we present the first automated framework for evaluating arbitrary Boolean functions on standard RRAM crossbars using highly parallel MAC operations. The proposed method introduces a logic computation core for RRAM-based neuromorphic architectures without requiring additional hardware, leveraging existing peripheral circuitry. To ensure functional correctness, we further integrate a formal verification approach based on equivalence checking via SAT solvers. Experimental results on standard benchmarks demonstrate substantial reductions in computation cycles and improved efficiency compared to existing RRAM-based logic synthesis methods, highlighting the practical potential of MAC-based logic in emerging computing systems.