LV-RM 3 : Logic Synthesis and Verification of Computing-in-Memory Systems Using 3-Input Resistive Majority Gates

Resistive random-access memory (ReRAM) is a promising non-volatile technology that enables both data storage and in-memory Boolean computation, with 3-input resistive majority (RM \({}_{3}\) ) logic as a native computational primitive. Efficiently synthesizing, mapping, and verifying RM \({}_{3}\) -based logic under device constraints remains a critical challenge for ReRAM-based computing-in-memory (CiM) architectures. This paper presents an end-to-end framework for logic synthesis, mapping, and verification tailored to RM \({}_{3}\) -based ReRAM systems. The proposed approach employs an RM \({}_{3}\) -based logic representation and integrates exact synthesis, algebraic rewriting, and inversion-aware optimization to reduce logic complexity and hardware cost. A dynamic mapping and instruction-generation strategy is further developed to optimize execution efficiency and resource utilization on crossbar arrays. To ensure correctness, a dedicated intermediate representation, ReRAM micro-operation intermediate representation (ReMOIR), is introduced to model stateful execution and enable SAT-based equivalence checking between logic specifications and generated micro-operation sequences. Experimental results on the EPFL benchmark suite demonstrate that the proposed method reduces logic network size and depth by 14% and 17.7%, respectively, compared to majority-inverter graph (MIG)-based approaches. In addition, it outperforms the SIMPLER MAGIC architecture, reducing execution cycles by 10.16% and ReRAM usage by 41.11%. The proposed framework is implemented in the open-source logic synthesis tool ALSO .