Approximate computing improves performance and energy efficiency for error-tolerant applications such as machine learning. Prior work has proposed approximate adder libraries for memristive crossbars using IMPLY and MAGIC stateful logic, primarily focusing on area optimization or fixed crossbar mappings. However, the impact of functional approximation under fully parallel crossbar execution remains largely unexplored. This work presents a framework for generating, mapping, and evaluating approximate Ripple Carry Adders (RCAs) implemented using MAGIC logic in memristive ReRAM crossbars under fully parallel crossbar execution. We explore a large design space by generating 458,752 approximate 8-bit RCA variants. Each design is synthesized into NOR/NOT logic and mapped onto a MAGIC crossbar at the micro-operation level. The resulting implementations are evaluated in terms of latency, memristor count, and functional accuracy using Mean Squared Error (MSE) and Mean Absolute Error (MAE). Pareto-optimal designs reveal key trade-offs between latency, area, and approximation error, highlighting the potential of MAGIC-based in-memory arithmetic for low-latency and energy-efficient computing.

Resistive RAM (RRAM) has emerged as a promising technology for in-memory computing, allowing both storage and computation within the same physical substrate. Although its ability to perform analog computations, especially multiplyaccumulate (MAC) operations, has been effectively utilized in neuromorphic systems, there has been limited research on its applicability to Boolean logic synthesis. Existing approaches typically rely on graph-based representations of Boolean functions that are mapped to column-wise MAC operations on standard RRAM crossbars. However, these representations largely inherit binary fan-in constraints from conventional logic synthesis flows, resulting in limited exploitation of MAC-level parallelism and underutilization of available crossbar resources. In this work, we address this limitation by introducing the concept of multi-input OR-Inverter Graphs (m-OIGs), which allow OR nodes with fanin greater than two to better match the accumulation semantics of MAC operations. Experimental results on standard benchmark suites demonstrate that increasing OR fan-in consistently reduces both crossbar area and total evaluation cycles, leading to improved performance and more efficient use of RRAM crossbar resources, highlighting the importance of fan-in-aware logic representations.

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.

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.

Recent advancements in the fabrication of Resistive Random Access Memory (ReRAM) devices have led to the development of large-scale crossbar structures. In-memory computing architectures relying on ReRAM crossbars aim to mitigate the processor-memory bottleneck that exists with current complementary metal-oxide semiconductor technology. With this motivation, several synthesis and mapping approaches focusing on the realizations of Boolean functions in the ReRAM crossbars have been proposed earlier. Thus far, the verification of the designs realized on ReRAM crossbars is done either through manual inspection or using simulation-based approaches. Since manual inspections and simulation-based approaches are limited to smaller designs, they cannot be applied to the verification of complex designs on large-scale ReRAM crossbars. Motivated by this, we propose, for the first time, an automatic equivalence checking flow that determines the equivalence between the original function specification (e.g., Majority-inverter Graph ) and the crossbar micro-operations file formats. We consider two crossbar structures, zero-transistor, one-memristor (0T1R) and one-transistor, one-memristor (1T1R) to implement the micro-operations. While the micro-operations file format exists for 0T1R crossbar structures, no representations for micro-operations to be executed in 1T1R crossbars exist yet. In this work, we introduce the micro-operation file format for 1T1R crossbar structures to efficiently represent the micro-operations as ReRAM crossbar netlists. Afterwards, we introduce two intermediate data structures, ReRAM Sequence Graph for 0T1R crossbars (ReSG-0T1R) and for 1T1R crossbars (ReSG-1T1R) , that are derived from the 0T1R and 1T1R crossbar micro-operations file formats, respectively. These ReSGs are then translated into Boolean Satisfiability (SAT) formula, and then the verification is done by checking the generated SAT formulae against the golden functional specification (represented in Verilog) using Z3 Satisfiability solver. Experimental evaluations confirm the effectiveness of the proposed verification methodology on MCNC and ISCAS benchmarks.

Recent progress in the fabrication of Resistive Random Access Memory (ReRAM) devices has paved the way for large scale crossbar structures. In particular, in-memory computing on ReRAM crossbars helps in bridging the processor-memory speed gap for current CMOS technology. To this end, synthesis and mapping of Boolean functions to such crossbars have been investigated by researchers. However the verification of simple designs on crossbar is still done through manual inspection or sometimes complemented by simulation based techniques. Clearly this is an important problem as real world designs are complex and have higher number of inputs. As a result manual inspection and simulation based methods for these designs are not practical.

Memristors or Resistive Random Access Memory (RRAM) are emerging non-volatile memory devices that can be used for both storage and computing. In this type of memory the information is stored in memory cells in the form of resistance. One of the very important challenges in memristive crossbars is the existence of Sneak Paths, which result in erroneous reading of memory cells. Most of the logic in-memory techniques have emphasized on improving the logic design perspective, but have given minor importance to the sneak path issue. In this paper we show the effect of sneak paths on crossbars of various sizes, and then try to analyze the logic design approaches like MAGIC and MAJORITY with respect to their immunity to sneak paths. Experimental result shows that with some extra overhead we can eliminate the sneak path effect in various logic design methods.

Memristor-based crossbar architectures have been explored by researchers for neuromorphic computing, where analog vector-matrix multiplication can be carried out in a single time step. In this paper we explore such architectures for carrying out various arithmetic operations. Since the computations are carried out in analog domain, they are affected by fabrication and performance variability of the manufactured devices. As a result, there can be inherent errors during the computation. However, the architecture can be suitable for approximate computing applications where some errors can be tolerated. We have proposed a method for carrying out arithmetic operations with any multiple of k-bit resolution on the crossbar, for some limited values of k. The fault tolerant capability of the proposed architecture is evaluated through experimentation on benchmark datasets. We also perform case studies to analyze the performance of the approach with particular emphasis on approximate computing. The results of the case studies show that certain applications indeed exhibit fault tolerance in presence of faulty memristors.

Resistive Random Access Memory (ReRAM) is an emerging non-volatile memory technology. Besides its low power consumption and its high scalability, its inherent computation capabilities make ReRAM especially interesting for future computer architectures. Merging computations into the memory is a promising solution for overcoming the memory bottleneck. To perform computations in ReRAM, efficient synthesis strategies for Boolean functions have to be developed. In this article, we give a thorough presentation of how to employ parallel computing capabilities of ReRAM for the synthesis of functions given state-of-the-art graph-based representations AIGs or BDDs. Additionally, we introduce a new graph-based representation called m-And-Inverter Graph (m-AIGs), which allows us to fully exploit the computing capabilities of ReRAM. In the simulations, we show that our proposed approaches outperform state-of-the art synthesis strategies, and we show the superiority of m-AIGs over the standard AIG representation for ReRAM-based synthesis.

Resistive random access memory (RRAM) is a nonvolatile memory technology which allows to perform computations in both digital and analog circuits. Multiply-Accumulate (MAC) is an analog column-based operation enabled on RRAM crossbars providing high efficiency to perform complex matrix vector multiplications, which is attractive for neural network accelerators. However, the analog computational capability of RRAM devices has not been yet utilized for logic synthesis. In this paper, we show how a synthesis approach based on binary decision diagrams (BDD) can efficiently exploit efficient MAC computation enabled by RRAM. The proposed approach highly benefits from a symmetric structure of Boolean functions. Therefore, a design methodology is presented which optimizes and approximates BDDs under provided error thresholds to maximize efficiency of synthesized logic circuits under negligible loss of accuracy. In the experiments, we show that our proposed synthesis approach allows for an average reduction of up to 47% in the number of operations and up to 66% in the number of required devices compared to state-of-the art methods, even without approximation. Using approximation, we can further reduce the number of required devices.

Design of nonvolatile in-memory computing devices has attracted high attention to resistive random access memories (RRAMs). We present a comprehensive approach for the synthesis of resistive in-memory computing circuits using binary decision diagrams, and-inverter graphs, and the recently proposed majority-inverter graphs for logic representation and manipulation. The proposed approach allows to perform parallel computing on a multirow crossbar architecture for the logic representations of the given Boolean functions throughout a level-by-level implementation methodology. It also provides alternative implementations utilizing two different logic operations for each representation, and optimizes them with respect to the number of RRAM devices and operations, addressing area, and delay, respectively. Experiments show that upper bounds of the aforementioned cost metrics for the implementations obtained by our synthesis approach are considerably improved in comparison with the corresponding existing methods in both area and especially latency.

Resistive Random Access Memory (RRAM) is a promising non-volatile memory technology which enables modern in-memory computing architectures. Although RRAMs are known to be superior to conventional memories in many aspects, they suffer from a low write endurance. In this paper, we focus on balancing memory write traffic as a solution to extend the lifetime of resistive crossbar architectures. As a case study, we monitor the write traffic in a Programmable Logic-in-Memory (PLiM) architecture, and propose an endurance management scheme for it. The proposed endurance-aware compilation is capable of handling different trade-offs between write balance, latency, and area of the resulting PLiM implementations. Experimental evaluations on a set of benchmarks including large arithmetic and control functions show that the standard deviation of writes can be reduced by 86.65% on average compared to a naive compiler, while the average number of instructions and RRAM devices also decreases by 36.45% and 13.67%, respectively.

Approximate computing is an emerging methodology that allows to increase efficiency in a range of resilient applications for an affordable loss of precision or quality. In this paper, we exploit approximation in a multi-criteria optimization approach for the widely used data structure Binary Decision Diagram (BDD) to achieve higher efficiency besides lowering the inaccuracy. For this purpose, we utilize an ε-preferred evolutionary algorithm giving a higher priority to minimize BDD sizes as well as maintaining certain error constraints. In particular, we propose an adaptive ε-setting method which adds an automated factor to the algorithm based on the behavior of the function under approximation. This improves the performances of the algorithm by correcting the effect of the user set error constraints which can restrict the dimensions of the search and can lead to immature convergence.

Resistive memories have gained high research attention for enabling design of in-memory computing circuits and systems. We propose for the first time an automatic compilation methodology suited to a recently proposed computer architecture solely based on resistive memory arrays. Our approach uses Majority-Inverter Graphs (MIGs) to manage the computational operations. In order to obtain a performance and resource efficient program, we employ optimization techniques both to the underlying MIG as well as to the compilation procedure itself. In addition, our proposed approach optimizes the program with respect to memory endurance constraints which is of particular importance for in-memory computing architectures.

Resistive switching property enables various promising applications such as design of non-volatile in-memory computing devices which has attracted high attention to Resistive Random Access Memories (RRAMs). In this work, we present a multi-objective BDD optimization approach for RRAM based logic circuit design. Dissimilar to classical BDD optimization, evaluating the cost metrics of the circuits in this case does not only depend on the number of BDD nodes but is more advanced. We have utilized a non-dominated sorting genetic algorithm for bi-objective BDD optimization with respect to the number of required RRAMs and computational steps addressing the area and delay of the resulting circuits, respectively. The algorithm also allows preference to one of the objectives if it is of higher significance. Experimental results show that the proposed multi-objective genetic algorithm achieves considerable reduction in both aforementioned criteria in comparison with an existing approach.

Binary Decision Diagrams (BDDs) are widely used in electronic design automation and formal verification. BDDs are a canonical representation of Boolean functions with respect to a variable ordering. Finding a variable ordering resulting in a small number of nodes and paths is a primary goal in BDD optimization. There are several approaches minimizing the number of nodes or paths in BDDs, but yet no method has been proposed to minimize both objectives at the same time.