The popularity of Neural Processing Units (NPUs) is enabled by the growth of Artificial Intelligence. One of the main components of these processors are Multiply and Accumulate (MAC) operations. As these processors are becoming extremely important in the AI era, the design of efficient verification strategies is of utmost importance. In this context, formal verification methods ensure 100

The execution of large-scale quantum algorithms remains constrained by the limited number of available qubits, restricted qubit connectivity, and the intrinsic noise in current quantum processors. To address these challenges, Dynamic Quantum Circuits (DQC) have emerged as a promising design paradigm that leverages non-unitary operations–such as active reset, mid-circuit measurement, and classically controlled gates–to reduce qubit requirements during circuit realization. While DQC offers significant resource savings, it often incurs a trade-off in the form of increased circuit depth, making the assessment of circuit reliability a critical concern for near-term quantum hardware. In this work, we analyze the structure of oracle functions and observe that transforming their global mappings into vector-valued forms provides key benefits, including reduced circuit depth, improved parallelism, and minimal additional gate overhead. These properties make the proposed approach particularly effective for architectures with limited qubit connectivity and distributed quantum systems with communication constraints. Furthermore, we introduce a DQC-based transformation scheme and demonstrate its application to the Bernstein-Vazirani (BV) and Quantum Phase Estimation (QPE) algorithms across varying circuit sizes. Empirical results confirm that the proposed design methodology improves execution efficiency and reliability as a function of qubit count and circuit depth, paving the way for scalable DQC-based implementations in resource-constrained quantum architectures.

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.

Modern hardware verification of complex circuits relies heavily on the efficiency of formal methods. For complex arithmetic circuits in particular Symbolic Computer Algebra (SCA) engines which represent pseudo-boolean functions using polynomials are crucial. As circuit complexity grows in the age of AI, verification of arithmetic primitives, including Multiplication, Addition, Multiply-Accumulate (MAC), becomes a computational bottleneck. To address this, we introduce TRACE (Traversal and Reasoning Algebraic Computing Engine), a highly efficient framework designed to investigate the intersection of traversal strategies and proof efficiency. Unlike existing SCA tools which are mainly limited to multipliers, TRACE offers a flexible framework for researchers to analyze memory usage and verification time across a wide range of arithmetic circuits (adder, multiplier and MAC). To overcome the state-explosion problem inherent in polynomial expansion, the engine incorporates advanced reduction techniques, including optimized traversal strategies, conflict removal, and polarity-based optimization for compact symbolic representations. Our experimental results show that for optimized MAC, for the first time, TRACE was able to verify previously unverifiable circuits

The demand for compute-intensive applications such as AI/ML has led to the development of processors with complex functionalities. The Multiply Accumulate (MAC) unit is a vital component in these processors, but its verification is very challenging due to the highly optimized designs used to implement the MAC operation. In this paper, we show some interesting results for optimized MAC design verification using a formal proof engine, Symbolic Computer Algebra (SCA). For the first time, we exploit the combined benefit of phase and dynamic ordering in verifying MAC circuits, a capability not possible using state-of-the-art SCA proof engines.

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.

Memristors offer a solution to the processor-memory bottleneck in traditional computer systems, particularly in storage systems with in-memory computing (IMC) capabilities. However, challenges such as stability and parameter variations hinder their widespread use. The MAGIC NOR gate has shown promise in memristive-based digital IMC architectures, but the presence of sneak paths in 0-Transistor 1-Memristor (0T1M) crossbars limits their effectiveness. The 1-Transistor 1-Memristor (1T1M) structure emerges as a practical solution to this issue. This paper evaluates the feasibility of using the MAGIC NOR gate in a 1T1M crossbar array for IMC and discusses the constraints of such a setup. Our analysis suggests that only row-wise or column-wise MAGIC NOR gate evaluation is practical for a 1T1M crossbar array, as opposed to a 0T1M array where both row-wise and column-wise gate evaluations are possible. We propose a scalable sneak-path-free 1T1M crossbar array with the MAGIC design style for IMC architecture, operating in resistive memory mode for data storage and IMC mode for logic operations. We also propose a novel heuristic mapping method that exploits parallelism across the crossbar array. Using the Cadence Spectre environment, simulation results on adder circuits and ISCAS-85 benchmark functions show that, on average, our proposed method achieves a 32.41% improvement in computation steps and saves more than 52.48% of memristor cells compared to other 0T1M MAGIC families.

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.

In this paper, we propose a novel method for locating and diagnosing bugs in quantum circuits. Debugging in the quantum domain is especially challenging due to the inherent inability of assessing the quantum state of a program. Moreover, explaining the root cause behind unexpected outcomes is hard due to the limited information gain provided by measurements. Our approach aims to address both of these issue: Firstly, the bug site is identified using a standard circuit slicing technique combined with an associated measurement strategy. Secondly, we provide information about the nature of the bug, generated through repeated measurements. To minimize the number of measurements, we introduce a notion of equivalence classes based on unitary operations. This allows us to partition the gate library into classes that produce indistinguishable results under certain measurements. Finally, We assess the effectiveness and measurement complexity of our method by applying it to relevant primitive gate components and well-known quantum algorithms. Our empirical results shows that in 95.79% of all cases, our approach reveals the correct location of the bug along with a valid set of fault candidates. Furthermore, we demonstrate that the required number of circuit executions scales logarithmically with the circuit depth or linearly with the number of qubits.

Verification plays a major role in ensuring the functional correctness of any design. In recent years with growing complexity of processor designs, verification has assumed utmost importance. Simulation-based techniques cannot ensure completeness in verification, and in this regard formal methods prove crucial. Although formal methods guarantee completeness it is hard to quantify the exact time and space complexities. Recently some works have demonstrated that it is possible to achieve polynomial space and time complexities for various arithmetic circuits as well as for processors. In this paper we propose a Binary Decision Diagram (BDD) based Polynomial Formal Verification (PFV) approach for verifying processors. As a case study, we discuss the PFV for a multi-cycle processor (viz., MicroRV32) with support for combinational and sequential sub-systems. New data structures and code base are utilized to verify all the functional components. Experimental results reveal that the verification can indeed be performed in polynomial time.

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.

With the increasing popularity of compute intensive applications like AI, processors with complex functionalities are designed. Multiply and Accumulate (MAC) is one of the essential operations in modern Neural Processor Units (NPUs), but no sound formal verification technique exists that can efficiently ensure correctness. In this paper we analyze almost 200 configurations of MAC instances for various bit-widths starting from 8 up to several hundred bits. On top of the classical area-delay trade-off, we study verifiability as an additional parameter. It is shown that surprisingly the fastest and smallest instances are not the ones that are the hardest to verify. Exploiting Symbolic Computer Algebra (SCA) we provide a technique that allows scalable verification for large bit-width and classifies the set of MAC units.

The execution of large-scale quantum algorithms is currently constrained by the limited number of available qubits, qubit connectivity restrictions, and the inherent noise in quantum processors. To address these limitations, a design methodology known as Dynamic Quantum Circuits (DQC) has emerged. DQC leverages non-unitary operations-such as active reset, midcircuit measurement, and classically controlled gate operationsto reduce qubit requirements during circuit design. Recently, DQC-based implementations have been explored for various algorithms, including Shor’s Prime Factorization, Quantum Phase Estimation (QPE), and Bernstein-Vazirani (BV), as well as for key operations like state preparation, Toffoli networks, and nonlocal gates. While DQC offers a significant reduction in qubit usage, it introduces a trade-off in the form of increased circuit depth. Therefore, assessing the reliability of such circuits becomes crucial in the context of current quantum hardware architectures. In this paper, we analyze the reliability of DQC-based quantum circuit realizations as a function of qubit count and circuit depth. We present empirical results for two algorithms and evaluate how architectural parameters impact their reliability.

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.

The popularity of compute intensive applications, like AI/ML, has driven the design of processors with complex functionality. The Dot Product (DP) is one of the most essential operations in modern neural processors, although no complete formal verification technique exists that can ensure its 100% correctness. In this paper we show the first step towards formally verifying DP using Symbolic Computer Algebra (SCA). The verification process is performed without the need of a reference model generation which is a key factor in verification. Experimental results show the efficiency and scalability of SCA-based verification for DP architectures.

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.

Recent advancements in memristor technology and Resistive Random Access Memory (RRAM) have made in-memory computing an alternative to tackle the limitations of traditional von Neumann architecture. Although significant progress has been achieved in the synthesis and mapping of Boolean functions within crossbar arrays using styles like IMPLY, MAGIC and Majority, verification processes have been relatively less explored. In this paper, a comprehensive method is presented for the synthesis, mapping and verification of multi-input NOR-based MAGIC in-memory design on RRAM crossbars. Our contributions are twofold: firstly, we extend crossbar micro-operations tailored for multi-input NOR logic enabling precise mapping. Secondly, a verification tool processes the modified representation and compares it against the golden reference design using Boolean Satisfiability (SAT) formula and Satisfiability Modulo Theory (SMT) solver. Experiments were conducted on the ISCAS’85 benchmark suite which shows the efficiency of multi-input MAGIC NOR compared to the existing 2-input NOR-based MAGIC design.

Over the last two decades there has been immense progress in the field of quantum computing. Although today we have demonstrable quantum computers with more than 1000 qubits, researchers are still trying to show how these machines can be utilized to get substantial benefit for certain applications. We are also in the Noisy Intermediate Scale Quantum (NISQ) era that imposes certain restrictions in utilizing the entire physical qubit space. Implementation of various large-scale quantum algorithms suffers from limited number of available qubits and also the qubit coupling restrictions of the target quantum processor. To this end an advanced class of quantum circuits called Dynamic Quantum Circuits (DQC) has been proposed, which can work with very few additional qubits using various non-unitary operations (viz., active reset, mid-circuit measurement and classically controlled gate operations). This paper particularly presents various design automation challenges that exists in the current NISQ era and shows how DQC can be exploited to overcome some of the challenges.