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) 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.

Memristor-Aided Logic (MAGIC)-based In-Memory Computing (IMC) executes Boolean operations directly within crossbar arrays, addressing the von Neumann bottleneck. However, the efficiency of MAGIC-based arithmetic circuits strongly depends on mapping strategies. This work presents a unified, parallel row-wise, multi-scheduling-aware framework for efficient crossbar mapping of MAGIC-based adders, multipliers, and dividers. The proposed design flow integrates automated Register-Transfer Level (RTL) generation, NOT/NOR-constrained logic synthesis, and multiple scheduling strategies, namely As Soon As Possible (ASAP), As Late As Possible (ALAP), and Resource-Constrained (RC), to systematically extract micro-operations and evaluate latency, memristor counts, crossbar size, and energy. Comprehensive benchmarking across multiple arithmetic architectures (8–64-bit adders/multipliers and up to 128/64-bit division) demonstrates that RC scheduling consistently reduces crossbar size without increasing logic depth. Among the evaluated designs, Brent–Kung (BK) adders and Dadda Tree (DT) multipliers provide the best scalability, while Restoring Array Dividers offer high efficiency. The proposed mapping framework achieves reduced latency and improved area–latency trade-offs compared to prior MAGIC designs, and comparative evaluation shows competitive performance for adders and substantially lower latency with improved scalability for multiplier architectures compared with representative MAC-, MAJ-, and AIG-based IMC implementations.

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.

The growing demand for high-performance, realtime computation in data-intensive applications is increasingly constrained by the Von Neumann bottleneck. In-memory computing (IMC), particularly through memristor-based technologies such as Memristor-Aided loGIC (MAGIC), offers a promising solution by enabling logic operations directly within memory arrays. While prior research has demonstrated basic Boolean logic with memristors, arithmetic operations such as multiplication remain latency-bound due to sequential logic execution and inefficient crossbar utilization. This work introduces a scalable and efficient MAGIC-based Wallace Tree multiplier architecture tailored for in-memory computing. By integrating an optimized 3:2 compressor and leveraging a state-of-the-art synthesis-tomicro-operation mapping tool, our approach significantly reduces latency and improves parallelism within memristor crossbars. Experimental evaluations across 4- to 64-bit unsigned Wallace Tree multipliers show consistent improvements in speed and scalability. The proposed architecture presents a practical and fully scalable design for next-generation in-memory arithmetic systems.

Resistive Random-Access Memory (RRAM) crossbar arrays provide a high-density, low-power platform for neuromorphic computing. In this work, we implement an RRAM-based architecture for alphabet recognition using the EMNIST dataset, where all 26 English letters are represented as $28 \times 28$ binary images. Beyond ideal conditions, we study the impact of hardware imperfections, including stuck-at faults, random bit flips, and process variations, on recognition performance. To improve resilience, we evaluate two fault tolerance strategies: Triple Modular Redundancy (TMR) and Algorithm-Based Fault Tolerance (ABFT). TMR delivers strong reliability by masking faults through replication, while ABFT efficiently detects and corrects at a lower storage overhead, but at a higher computational cost. Our results demonstrate that RRAM crossbars combined with lightweight fault tolerance provide accurate, energy-efficient, and resilient neuromorphic computing, highlighting their promise for robust and efficient edge AI deployment.

In-memory computing (IMC) with Resistive Random Access Memory (ReRAM) crossbars has emerged as a promising solution to overcome the von Neumann bottleneck by enabling computation inside memory arrays. This paper presents a unified benchmarking of multi-bit arithmetic circuits in the MAGIC logic style, encompassing seven adder and three multiplier architectures with operand sizes from 8 to 64 bits. Through a proposed parallel mapping methodology, we achieve latency reductions of up to $26.3 \times$ for adders and $361 \times$ for multipliers relative to state-of-the-art designs, realized through efficient crossbar-level utilization with modest hardware overhead. Our evaluation shows that Brent-Kung (BK) adders are most latencyefficient for larger sizes, while Serial Prefix (SE) adders excel for smaller ones and also offer superior hardware efficiency. In addition, Dadda multipliers achieve the lowest total latency, whereas array multipliers provide the best hardware efficiency among multipliers. By systematically quantifying the trade-offs between latency and memristor count, this work offers a detailed design-space exploration of arithmetic units for ReRAM-based IMC, yielding practical insights for future high-performance, memory-centric architectures.

This paper presents a comparative evaluation of seven adder architectures mapped to RRAM crossbars using a MAC-based logic style. By analyzing designs across 8- to 64-bit widths, we assess trade-offs in total evaluation cycles, crossbar area, and logical depth. The results highlight Ladner-Fischer and Kogge-Stone adders as the most efficient for high-bit-width applications, offering superior parallelism and scalability in MAC-based in-memory computing systems. Hence, these adder designs can be used as a reference for future works related to the optimization of adders for MAC-based logic style.

Formal verification of programmable memristive architectures utilizing emerging nonvolatile memory technologies such as Resistive Random-Access Memory (RRAM) has only been recently addressed by a few works at the software level. In this paper we propose an in-memory SAT solver utilizing inherent analog features of RRAM that enables formal verification of arbitrary designs within resistive crossbars. More importantly, this allows self-verification of in-memory implementations as the correctness of designs can be dynamically checked. Additionally, the required architecture is presented, along with a complexity analysis for latency and hardware overheads.

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 CMOS 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 (MIG)) 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 till date. 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.

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.

Resistive Random Access Memory (ReRAM) technologies enable the development of innovative architectures for inmemory computing. Many logic design styles, like Imply, Magic or Majority, have been explored for mapping Boolean functions to ReRAM crossbars. However, little attention has been given to the verification of the mapping process. Simulation based approaches can be used to check the functional correctness of smaller designs, but only formal verification techniques can ensure completeness for larger designs. Some initial works in this area have been proposed, which specifically focus on the verification of micro-operations using majority-based logic design. However, these techniques cannot be directly applied to other logic design styles, like Imply or Magic. This necessitates the design and exploration of more general verification techniques for logic-in-memory using ReRAM crossbars, and opens up the scope for further investigation. In this paper, we provide an overview of existing verification techniques for logic-in-memory designs, and also discuss directions for future work.

Recent progress in the fabrication of Resistive Random Access Mem-ory (ReRAM) devices has paved the way for large scale crossbar structures. In particular, in-memory computing on ReRAM cross-bars 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 sim-ulation 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. In this paper for the first time as per our knowledge we pro-pose an automated equivalence checking methodology for majority based in-memory designs on ReRAM crossbars. Our contributions are twofold: first, we introduce an intermediate data structure called ReRAM Sequence Graph (ReSG) to represent the logic-in-memory design. This in turn is translated into Boolean Satifiability (SAT) formulas. These SAT formulas are verified against the golden functional specification using Z3 Satifiability Modulo Theory (SMT) solver. We validate the proposed method by running widely avail-able benchmarks.

Data science driven applications (e.g., big data and artificial intelligence) can support the transition to a green economy. However, this requires overcoming existing barriers and providing appropriate framework conditions. Based on an analysis of 295 German and US start-ups using data science to create positive environmental impacts, we identify six main obstacles to a greater use of data science for sustainable transformation, and propose six measures that can be used to formulate policy recommendations.This paper examines the intersections between the hoped-for shift toward a green economy and data science (various forms of big data analytics and artificial intelligence). It does so through an analysis of data science applications with environmental relevance developed or deployed by German and US start-ups. The majority of the data science applications identified seek to improve the efficiency of existing products and processes, or to provide information. Applications that support more fundamental transformations of existing production and consumption patterns are fewer in number. To increase the sustainability-related impact of data science, it seems necessary to adjust policy framework conditions. Based on our findings, recommendations for action are presented regarding sustainability-related changes of the legal and regulatory framework conditions.

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.

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.