Formally verifying divider circuits is complex, and multiple effective methods have been developed. However, none of these methods provides an upper bound on the verification time, which limits their scalability for large divider circuits. Recently, Polynomial Formal Verification (PFV) based approaches have been investigated to ensure circuit correctness in polynomial time and space. However, there is no PFV based approach for the formal verification of dividers. In this paper, we introduce for the first time a two-level partitioning strategy and present PolyRAD, a novel PFV approach for verifying Restoring Array Divider (RAD). Finally, we prove that verification of RAD can be achieved in polynomial time, and conduct experimental evaluation on RAD of different sizes to validate our theoretical findings.

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.

Advancements in emerging technologies have recently increased the traction of non-von Neumann design styles. One of the most popular design styles in this domain involves using memristors to perform logic operations in memory, known as Logic-in-Memory (LiM). Memristor Aided Logic (MAGIC) is one of such LiM based design style that is widely used given its benefits in latency and energy. Several prior works have focused on the generation of logic operations, also called microoperations, for LiM based on the MAGIC design style. Recently, the generation of SPICE netlists for MAGIC design style has been achieved by the MemSPICE tool. While this represents a significant step forward, verifying the correctness of the generated netlists still depends on SPICE-level simulations. These simulations become particularly impractical for medium-to-large designs presenting a bottleneck in the validation process. To address this limitation, in this paper, we introduce veriSiM, an automated formal verification methodology for MAGIC-based LiM. More concretely, it ensures the correctness of the generated LiM SPICE netlists against the golden reference Verilog design. Our methodology involves generating clauses from the SPICE netlists and verifying them against clauses generated from the golden reference Verilog design, using the high-performance Z3 solver to perform the equivalence checking. The clause generation process from the SPICE netlists needs to be based on several conditions, which have been identified and discussed in detail. We have used several benchmarks from ISCAS’85, ISCAS’89, and ITC’99 to demonstrate the efficacy of the veri

Formal Verification (FV) is a widely used technique for verifying whether a gate-level design is functionally equivalent to its specification. However, when verification fails due to the presence of faults, Debugging and Fault Correction (DFC) becomes essential to localize bugs and correct them. Despite the success of various automatic DFC approaches, existing methods often lack theoretical guarantees on the computational resources required, making them unpredictable in terms of time and space complexity. Therefore, it is essential to establish upper bounds on the time and space complexity of the DFC process to ensure its practical feasibility. In this paper, we rely on the CutWidth (CW) property to introduce Polynomial Debugging and Fault Correction (PDFC) as a subclass of DFC for combinational circuits, where the time and space complexities of DFC are characterized by CW. Specifically, we show that for circuits with bounded CW, the entire DFC process can be polynomially bounded, unlike Yosys SAT, which has exponential complexity. Moreover, we prove that for circuits with constant CW, the entire DFC process can be carried out in linear time and space. Finally, we evaluate several architectures of adders with small constant cutwidth, considering various numbers and locations of faulty gates in terms of time and space required for the DFC process to confirm our theoretical findings and also compare it with Yosys SAT. To demonstrate that our PDFC approach is not limited to adders and can be applied to any design with bounded cutwidth, we also evaluate benchmark circuits fromITC’99andIWLS’93in terms of time and space of the DFC process.

Ensuring the functional correctness of a digital system is achievable through formal verification. Despite the increased complexity of modern systems, formal verification still needs to be done in a reasonable time. Hence, Polynomial Formal Verification (PFV) techniques are being explored, as they provide guaranteed polynomial upper bounds on the time and space required for the verification process. Recently, it was shown that circuits characterized by a constant cutwidth can be verified in linear time using Answer Set Programming (ASP) . However, these results are limited to combinational circuits, whereas most designs used in digital systems are sequential. In this article, we introduce Linear Formal Verification (LFV) as a subclass of PFV for sequential circuits with constant cutwidth, which are verifiable in linear time and space using ASP. We achieve this by proposing a new data structure called Weighted And-Inverter Graph (W-AIG) . Unlike existing formal verification methods, we prove that our approach can verify any sequential circuit with a constant cutwidth in linear time and space. Finally, we implement our approach and experimentally show that a variety of sequential circuits, such as pipelined adders, serial adders, and shift registers, can be verified in linear time and space, while ring counters can be verified in polynomial time and space, confirming our theoretical findings.

In the field of Electronic Design Automation (EDA), managing circuit complexity is a crucial task for efficient circuit verification, testing, and optimization. Increasing design complexity presents challenges for tasks such as formal verification, fault detection, and circuit optimization. Therefore, reducing circuit complexity becomes crucial in improving the efficiency and scalability of these tasks. These circuits are typically represented as graphs. In the field of parameterized complexity, CutWidth (CW) and TreeWidth (TW) are well-studied decomposition techniques that have been used in analyzing graph algorithms. In this paper, we introduce the TW decomposition technique to the field of EDA for the first time and demonstrate its impact on reducing the circuit complexity of circuits. Additionally, we present a new decomposition technique that combines both decompositions, resulting in a further reduction in circuit complexity. Furthermore, we present experimental results comparing complexity upper bounds from various decompositions to highlight the efficacy of our approach on the ISCAS’85 and EPFL benchmark circuits. Our results show that our decomposition technique outperforms the complexity upper bounds of CW by 90.16× and the complexity upper bounds of TW by 9.34× for the ISCAS’85 benchmarks. Additionally, it outperforms the complexity upper bounds of CW by 1986.37× and the complexity upper bounds of TW by 94.13× for the EPFL benchmarks. Finally, to demonstrate the applicability of the decomposition techniques in solving various EDA problems, we propose a new Formal Verification (FV) approach that leverages these techniques to provide an upper bound for the verification process. We also conduct an experimental evaluation on the ITC’99 , MCNC’91 , and VHDL Library of Arithmetic Units ( ELAU ) benchmark circuits, adder circuits of various sizes (up to 3072-bit width), and Genmul multipliers of different sizes (up to 10×10), to demonstrate the scalability of our approach.

Ensuring the functional correctness of a digital system is achievable through formal verification. Despite the increased complexity of modern systems, formal verification still needs to be done in a reasonable time. Hence, Polynomial Formal Verification (PFV) techniques are being explored as they provide a guaranteed upper bound on the run time for verification. Recently, it was shown that combinational circuits characterized by a constant cutwidth can be verified in linear time using Answer Set Programming (ASP). However, most of the designs used in digital systems are sequential. Hence, in this paper, we propose a linear time formal verification approach using ASP for sequential circuits with constant cutwidth. We achieve this by proposing a new data structure called Weighted-And Inverter Graph (W-AIG). Unlike existing formal verification methods, we prove that our approach can verify any sequential circuit with a constant cutwidth in a linear time. Finally, we also implement our approach and experimentally show the results on a variety of sequential circuits like pipelined adders, serial adders, and shift registers to confirm our theoretical findings.

In-memory Computing (IMC) using emerging devices has shown immense potential. Among these devices, memristors have emerged as one of the most popular for performing digital IMC. While several methods exist for digital IMC using memristors, most require expensive write operations in terms of energy, latency, and endurance. Hence, READ-based IMC techniques have been proposed to reduce the number of writes to the memristor crossbar. However, existing techniques rely on simple gates that can be mapped to the memristive crossbar, making them non-optimal, and they suffer from unwanted sneak paths causing undesired behavior. In this work, we alleviate these limitations and propose an optimized synthesis methodology for 1T1M crossbars called RIVER. RIVER supports more complex gates and is sneak-path aware. When comparing RIVER with the state-of-the-art using ISCAS’ 85 and EPFL benchmarks, we achieve 33% less gate utilization on average while reducing the average staircase length by 37%. Moreover, these enhancements result in a 58% reduction in the required crossbar area. After eliminating sneak paths, RIVER still shows 38% less area usage on average as compared to the state-of-the-art.

Data-intensive Neural Network (NN) applications place high demands on data movement and computation, making the traditional von Neumann architecture inefficient. Compute-in-Memory (CIM) technology offers a promising alternative by accelerating Matrix-Vector Multiplication (MVM), the core operation in NN inference. However, the broad design space makes it challenging to identify an optimal CIM configuration. Virtual Prototypes (VPs) enable fast Design Space Exploration (DSE) across various configurations. In this work, we perform a system-level DSE by modeling a configurable CIM unit in SystemC and integrating it into a RISC-V-based VP. The CIM timing model reflects characteristics of various in-memory devices. We evaluate performance across multiple workloads, including a standalone MVM operation, a lightweight fully connected NN model, and a Convolution Neural Network (CNN) model inference. Experimental results show that the CIM unit achieves a speedup of up to 68× compared to the baseline CPU of the VP, demonstrating its effectiveness in accelerating MVM-dominated applications.

Approximate adders have received significant attention as they give benefits in power, performance, and area for error-resilient applications. Due to their ubiquitous use, formal verification of approximate adders has also gained traction. However, prior works on formal verification of approximate adders are limited to relaxed equivalence checking, i.e., checking whether the approximate adder designs have an error less than a specified threshold. This method has limitations, as multiple approximate adder designs can satisfy the relaxed equivalence checking criterion, which can cause more than expected deterioration in the output quality. The deterioration in output quality is larger in approximate adder designs that produce exact results for some regions of the input space but have the freedom to produce approximate results in other regions of the input space. In this paper, we propose a methodology called Correct and Verify (CAV), which exploits Binary Decision Diagrams (BDDs) to guarantee that the approximate adder with correct carry bits exactly matches its functional specification. Our idea takes advantage of the BDD structure in extracting the internal signals, particularly the carry signal from the golden reference exact adder. Afterward, a corrector circuit is generated from the functional specification and the extracted carry signal is used as input in the corrector circuit. The corrector circuit is used to generate the corrected adder from the approximate adder. The generated corrected adder can be compared against a formally verified golden reference exact adder. We show the efficacy of CAV over approximate Ripple Carry Adders (RCA) as well as approximate Parallel Prefix Adders (PPA). Lastly, we perform a qualitative analysis by introducing mutations in the designs to show the fault detection quality of the CAV methodology.

Ensuring functional correctness is achieved through formal verification. As circuit complexity increases, limiting the upper bounds for time and space required for verification becomes crucial. Polynomial Formal Verification (PFV) has been introduced to tackle this problem. In modern digital system designs, approximate circuits are widely employed in error resilient applications. Therefore, ensuring the functional correctness of these circuits becomes essential. In prior works, it has been proven that approximate circuits with constant cutwidth can be verified in linear time. However, extending binary logic verification to Multi-Valued Logic (MVL) introduces challenges, particularly regarding the encoding of MVL operators. It has been shown that MVL circuits with constant cutwidth can be verified in linear time using Answer Set Programming (ASP), due to the ASP encoding capabilities of MVL operators. In this paper, we present a PFV approach of MVL approximate circuits with constant cutwidth using ASP. We then demonstrate that the verification of MVL approximate circuits with constant cutwidth can be achieved in linear time. Finally, we evaluate various MVL approximate circuits with constant cutwidth across different logic levels to show the efficacy of our approach.

Approximate circuits have become ubiquitous in error-resilient applications. These circuits provide large reductions in area, power, and delay at the cost of erroneous computations. The error-resilient applications produce acceptable output quality, even after the introduction of erroneous computations. However, we observed that the error resilience of an application varies widely with respect to the applied inputs. Since prior works have mostly focused on using samples from a uniform distribution while designing the approximate circuits, they are unable to exploit input aware properties to design optimal circuits. Hence, in this work, we bridge this gap and propose Formally Verified Library of Input Data Aware Approximate Circuits (FV-LIDAC). FV-LIDAC is the first formally verified library of input distribution aware approximate arithmetic circuits. We use three of the most widely occurring distributions, namely uniform, normal, and exponential distributions, to show that optimal design sets are heavily dependent on the input data. FV-LIDAC chooses the best designs among millions of functional approximated adder and multiplier circuits, depending upon the inputs. Since there are no existing input-aware approximate circuit libraries, we compared FV-LIDAC against state-of-the-art input-unaware EvoApproxLib, to further highlight the need for FV-LIDAC. Additionally, we perform case studies on real-world applications to further highlight the improvement over state-of-the-art. We aim to make the Pareto-optimal designs available as open source to stimulate further research.

As technology continues to advance, it becomes increasingly integrated into daily life facilitating complex tasks across a range of environments. While some applications such as smartphones and smartwatches are less critical, others like healthcare devices and autonomous vehicles demand bug-free performance to prevent financial loss or harm. Traditionally, simulation-based testing and formal verification played a major role in ensuring a bug-free device. However, the simulation of bigger systems is limited to a definite number of scenarios on the Design under Verification (DUV). Hence, it is unable to explore all possible inputs that can occur. Formal verification, on the other hand, offers a higher level of assurance through mathematical proofs but is both time-consuming and suffers from scalability issues, especially as designs grow in complexity. Recently, Large Language Models (LLMs) have shown promise in tasks previously limited to human expertise. Their natural language processing capabilities can assist in handling extensive specifications and source code, particularly in debugging hardware descriptions and analyzing security and functionality. The utilization of Retrieval Augmented Generation (RAG) has further enhanced LLMs by incorporating large specification or source code bases, thereby improving their bug-identification and correction capabilities. While recent advancements in LLMs, particularly with RAG, have yielded promising results in bug identification and correction for a small class of hardware bugs, significant gaps remain in their full potential for systematically addressing a wide range of hardware bugs. For instance, existing LLM methodologies struggle to detect bugs involving incorrect constant values, i.e., the use of wrong constants in source code. This limitation underscores the need for further exploration in utilizing LLMs to fully optimize the verification process. To bridge this gap, we propose a 3-phased 4-stage LLM-assisted systematic bug closure methodology that focuses on functional bugs in Verilog HDL rather than structural or syntactic issues. Our approach extracts functional properties of the DUV and systematically breaks down complex expressions into smaller sub-expressions to facilitate bug detection and correction. By employing RAG, the LLM is guided using the functional specifications and source code to identify and correct bugs. If the initial guidance through RAG is insufficient, our methodology initiates an iterative bug closure process. This includes incorporating more extensive information from the specifications, fetching additional lines of code for bug localization, and breaking down complex Verilog HDL expressions. In our comprehensive evaluation, we assess the LLM’s capabilities using 9 different categories of bugs. As benchmarks, we use 5 OpenTitan Intellectual Property (IP) cores to demonstrate the scalability and effectiveness of our bug closure methodology where ≈ 60% of the bugs were corrected. Specifically, we evaluate OpenAI’s GPT-4 in its ability to identify and correct functional bugs in Verilog HDL code.

Existing logic-in-memory (LiM) research is limited to generating mappings and micro-operations. In this paper, we present MemSPICE, a novel framework that addresses this gap by automatically generating both the netlist and testbench needed to evaluate the LiM on a memristive crossbar. MemSPICE goes beyond conventional approaches by providing energy estimation scripts to calculate the precise energy consumption of the testbench at the SPICE level. We propose an automated framework that utilizes the mapping obtained from the SIMPLER tool to perform accurate energy estimation through SPICE simulations. To the best of our knowledge, no existing framework is capable of generating a SPICE netlist from a hardware description language. By offering a comprehensive solution for SPICE-based netlist generation, testbench creation, and accurate energy estimation, MemSPICE empowers researchers and engineers working on memristor-based LiM to enhance their understanding and optimization of energy usage in these systems. Finally, we tested the circuits from the ISCAS’85 benchmark on MemSPICE and conducted a detailed energy analysis.

Large Language Models (LLMs) have gained immense popularity and are being explored for use in several domains. In this paper, we describe the LLMs for their use in the Electronic Design Automation (EDA) domain specifically for hardware verification. LLMs are being rapidly explored for hardware design generation and verification. However, given the inherent non-determinism and the limited capabilities of the current LLMs, the designs may contain bugs or the generated properties could be incorrect. The process of manually checking these bugs can be tedious and time-consuming. This highly limits the applicability of the LLMs. Researchers are looking to alleviate these limitations by incorporating verification strategies using the LLMs and enhancing the LLMs’ capabilities not only for bug-free design generation but also stand-alone for verification. The current pace of development in these can cause many areas to be overlooked. Therefore in this work, we discuss the state-of-the-art tools and frameworks available for utilizing LLMs for EDA. We will then discuss the hardware verification techniques being explored using LLMs. We then discuss the consistency of the natural language properties generated using LLMs. Lastly, we will discuss the future directions in which the LLMs can aid in the hardware verification process.

In this paper, we propose a methodology for hardware verification assisted by Large Language Models (LLMs) in the incremental proof generation process. First, an LLM identifies the basic module of the Design Under Verification (DUV), followed by expanding the proof scope as more modules are added. LLMs assist in defining and verifying invariants for each module using the Z3 solver, and in formulating integration properties at module interfaces. Our case studies on a Ripple Carry Adder (RCA) and a Dadda Tree Multiplier (DTM) demonstrate that LLMs enhance the efficiency and accuracy of hardware verification.

The increasing complexity of modern hardware designs poses significant challenges for design verification, particularly defining and verifying properties and invariants manually. Recently, Large Language Models (LLMs) such has GPT-4 have been explored to generate these properties. However, assessing the quality of these LLM generated properties is still lacking. In this paper, we introduce a LLM-guided formal verification methodology combined with mutation testing for creating and assessing invariants for Design Under Verification (DUV). Utilizing OpenAI's GPT-4, we automate the generation of invariants and formal models from design specifications and Verilog behavioral models, respectively. We further enhance this approach with mutation testing to validate the quality of the invariants. We use a 27-channel interrupt controller (C432) from ISCAS-85 benchmarks as a complex case-study to showcase the methodology.

Reconfigurable Field Effect Transistors (RFETs) can be programmed on the fly to behave either as NMOS or PMOS. Digital circuit designs using RFETs have been shown to benefit both in design and security metrics compared to traditional FETs. In this paper, we highlight the problem associated with the cascading of RFET-based logic cells that have their Source(S)/Drain(D) terminals not connected to the supply Voltage(VDD)/Ground(GND). While these circuits occupy a lesser area, there is a drastic increase in the delay of these logic cells when they are cascaded as a result of the S/D being driven by inputs. We then discuss two methods to mitigate this issue using a) buffer insertion for delay minimization, and b) logic cells that have their S/D terminals driven by VDD/GND.

In the context of digital circuits, formal verification methods have been well-studied to ensure their functional correctness. However, several verification methods fail to provide an upper bound for the time and space complexity. Therefore, Polynomial Formal Verification (PFV) has been introduced to address this problem. Unlike prior works, which have shown that approximate circuits can be verified in polynomial time, we show that approximate circuits with a constant cutwidth can be verified even in linear time. Since approximate circuits have become ubiquitous in error-resilient applications, it becomes essential to guarantee their correctness. While prior works have been limited to formal error analysis, we use Answer Set Programming (ASP) based formal verification to guarantee that the approximate circuit matches its functional specification. In this paper, we first show that several approximate adder circuits exhibit a constant cutwidth. We then provide a PFV approach that relies on this cutwidth as a structural property of the circuits to guarantee a linear-time verification w.r.t. the bitwidth using ASP. Finally, we evaluate several approximate adders in terms of the upper bound of the cutwidth, and verification time.

In-memory computing (IMC) has gained signifi- cant attention recently as it attempts to reduce the impact of memory bottlenecks. Numerous schemes for digital IMC are presented in the literature, focusing on logic operations. Often, an application's description has data dependencies that must be resolved. Contemporary IMC architectures perform read followed by write operations for this purpose, which results in performance and energy penalties. To solve this fundamental problem, this paper presents in-memory mirroring (IMM). IMM eliminates the need for read and write-back steps, thus avoiding energy and performance penalties. Instead, we perform data movement within memory, involving row-wise and column-wise data transfers. Additionally, the IMM scheme enables parallel cloning of entire row (word) with a complexity of O(1). Moreover, we analyzed the energy consumption of the proposed technique on an RRAM crossbar with an experimentally validated JART VCM v1b model. The IMM increases energy efficiency and shows 2x performance improvement compared to conventional data movement methods.

Approximate circuits have become ubiquitous in error-resilient applications. Given their widespread use, formal verification of these approximate designs is essential. Recently, there have been attempts that use formal verification techniques based on Boolean Satisfiability (SAT) Methods and Binary Decisions Diagrams (BDDs) to perform formal error analysis. These methods guarantee that the designed approximate circuits satisfy the error metrics, e.g., Mean Square Error (MSE), etc. However, in certain approximate circuits tailored for a particular input data distribution, only performing error analysis is not enough. In addition to error metrics, the functional specifications in these approximate circuits should also be satisfied. Otherwise, it can lead to a larger-than-expected deterioration in the output quality. In this work, for the first time, we alleviate this issue by proposing an automated formal verification methodology, cecApprox, that guarantees the approximate circuit matches the functional specification. This is crucial for circuits that are tailored for a particular input distribution. We show that in the designs where the structure is preserved, the corrected circuit can be generated from the approximate circuit. This corrected circuit can then be formally verified by performing combinational equivalence checking with the exact circuit as the golden reference. If the corrected circuit is equivalent to the exact circuit, it guarantees that the approximate circuit matches the given functional specification in addition to error metrics. Hence, the cecApprox methodology complements the formal error analysis method. We show the efficacy of cecApprox by generating and formally verifying millions of different 8-bit and 16-bit structural preserved approximate adders and multipliers using combinational equivalence checking.

In-Memory Computing (IMC) using memristors has gained significant interest in recent years as it addresses the issue of memory bottleneck in the von Neumann architectures. One of the most popular design styles that have been developed to perform memristor-based IMC is Memristor-Aided loGIC (MAGIC). MAGIC design style based NOR and NOT operations can be used to perform IMC on memristor crossbars. The state-of-the-art SIMPLER MAGIC tool is used to generate a mapping of any arbitrary Boolean function to MAGIC operations that are suitable for high-throughput applications. The correctness of the mapping is examined by tedious manual inspections and functional simulations which may not account for all the edge cases which is not desirable. In this work, we alleviate this issue to the best of our knowledge for the first time by proposing veriSIMPLER. veriSIMPLER is an automated formal verification methodology to ensure the functional correctness of the mapping obtained using the SIMPLER MAGIC tool. The veriSIMPLER methodology generates Boolean Satisfiability Formulas (SAT) of the mapping obtained using the SIMPLER MAGIC tool and the golden reference Verilog designs. These SAT formulas are verified against each other using the Z3 solver. The veriSIMPLER methodology identified a critical bug in the mapping obtained from the SIMPLER MAGIC tool when buffers are connected between input and output. We also propose a methodology to patch this bug to generate the correct mapping, which in turn extends the capability of the SIMPLER MAGIC tool to handle buffers on top of providing a formal verification methodology. We have used a variety of benchmark circuits from the widely used ISCAS’85, ISCAS’89, ITC’99, and IWLS’93 to show the efficacy of the veriSIMPLER methodology. We aim to make the formally verified mapping obtained using the veriSIMPLER methodology open-source to promote further research in this direction.

Quantization techniques promise to significantly reduce the latency, energy, and area associated with multiplier hardware. This work, to the best of our knowledge, for the first time, shows the system-level impact of quantization on SOTA DNN accelerators from different digital accelerator paradigms. Based on the placement of data and compute site, we identify SOTA designs from Conventional Hardware Accelerators (CHA), Near Data Processors (NDP), and Processing-in-Memory (PIM) paradigms and show the impact of quantization when inferencing CNN and Fully Connected Layer (FCL) workloads. We show that the 32-bit implementation of SOTA from PIM consumes less energy than the 8-bit implementation of SOTA from CHA for FCL, while the trend reverses for CNN workloads. Further, PIM has stable latency while scaling the word size while CHA and NDP suffer 20% to$2\times$slow down for doubling word size.

Various DNN accelerators based on Conventional compute Hardware Accelerator (CHA), Near-Data-Processing (NDP) and Processing-in-Memory (PIM) paradigms have been proposed to meet the challenges of inferencing Deep Neural Networks (DNNs). To the best of our knowledge, this work aims to perform the first quantitative as well as qualitative comparison among the state-of-the-art accelerators from each digital DNN accelerator paradigm. Our study provides insights into selecting the best architecture for a given DNN workload. We have used workloads of the MLPerf Inference benchmark. We observe that for Fully Connected Layer (FCL) DNNs, PIM-based accelerator is 21× and 3× faster than CHA and NDP-based accelerator respectively. However, NDP is 9× and 2.5× more energy efficient than CHA and PIM for FCL. For Convolutional Neural Network (CNN) workloads, CHA is 10% and 5× faster than NDP and PIM-based accelerator respectively. Further, CHA is 1.5× and 6× more energy efficient than NDP and PIM-based accelerators respectively.

In this article, we present the design of approximate adders which provide dynamic runtime configurability between exact and approximate modes at the circuit level. We propose the single exact single approximate (SESA) adders that allow for fine grain configurability between exact and approximate modes. We also propose the single exact dual approximate (SEDA) adder that allows for coarse grain configurability between exact and approximate modes. Unlike SESA adders, the SEDA adder allows for two approximate computations at a time. Both the SESA and SEDA adders have a maximum bounded error. We implemented SESA and SEDA adders using UMC 28-nm technology node and evaluated them using the Cadence virtuoso tool. On average, SESA and SEDA adders consume 40% and 51% lesser energy when compared with the exact mirror adder when used in approximate mode. We have evaluated our result on image addition and image enhancement using 16-bit SESA and SEDA adders. We also evaluated 32-bit SESA and SEDA adders on the Moby benchmarks to highlight their use in approximate processors.

Graph analytics is powering a wide variety of applications in the domains of cybersecurity, contact tracing, and social networking. It consists of various algorithms (or workloads) that investigate the relationships between entities involved in transactions, interactions, and organizations. CPU-based graph analytics is inefficient because their cache hierarchy performs poorly owing to highly irregular memory access patterns of graph workloads. Policies managing the cache hierarchy in such systems are ignorant to the locality demands of different data types within graph workloads, and therefore are suboptimal. In this paper, we conduct an in-depth data type aware characterization of graph workloads to better understand the cache utilization of various graph data types. We find that different levels of the cache hierarchy are more sensitive to the locality demands of certain graph data types than others. Hence, we propose GRACE, a graph data-aware cache management technique, to increase cache hierarchy utilization, thereby minimizing off-chip memory traffic and enhancing performance. Our thorough evaluations show that GRACE, when augmented with a vertex reordering algorithm, outperforms a recent cache management scheme by up to 1.4×, with up to 27% reduction in expensive off-chip memory accesses. Thus, our work demonstrates that awareness of different graph data types is critical for effective cache management in graph analytics.

In this paper, we propose the design of a power-efficient floating point configurable approximate multiplier (FPCAM) suitable for error resilient applications. FPCAM allows systematic approximation, and the amount of approximation can be configured at run-time, depending on the error-tolerance of the applications. We show that compared to the existing state of the art multipliers, FPCAM on average consumes 62% lesser power and has 69% less power delay product. FPCAM also has 66% less area as compared to state of the art approximate multipliers. We have analyzed FPCAM for three different multimedia applications and random inputs to show that we achieve similar output quality as compared to existing multipliers while benefiting in power, area, and power delay product.

Data transfer across DRAM channels accounts for nearly a quarter of the total energy consumption of DDR4 DRAMs. Modern applications with high bandwidth requirements further increase channel energy consumption. However, channel energy consumption is dependent on data being transferred. Pseudo Open Drain (POD) asymmetric termination, used in current DDR4 systems, consumes energy only when 1's are being transmitted over the channels. Many modern applications, including AI/ML ones are resilient to errors in data, and can work well with approximate data. This resilience can vary widely across and within applications, which provides a number of ways for exploiting these characteristics to save data transfer energy across the DRAM channel. However, all DRAM data encoding schemes have been targeted towards applications that require exact data and are not approximation resilient. In this paper, we propose Zero Aware Configurable Data Encoding by Skipping Transfer (ZAC-DEST), a data encoding scheme to reduce the energy consumption of DRAM channels, specifically targeted towards approximate computing and error resilient applications. ZAC-DEST exploits the similarity between recent data transfers across channels and information about error resilience behaviour of applications to reduce on-die termination and switching energy by reducing the number of 1's transmitted over the channels. ZAC-DEST also provides a number of knobs for trading off application's accuracy for energy savings, and vice versa, and can be applied to both training and inference. We apply ZAC-DEST to five machine learning applications. On average, across all applications and configurations, we observed a reduction of 40% in termination energy and 37% in switching energy as compared to the state of the art data encoding technique BD-Coder with an average output quality loss of 10%. We show that if both training and testing are done assuming the presence of ZAC-DEST, the output quality of the applications can be improved upto 9× as compared to when ZAC-DEST is only applied during testing leading to energy savings during training and inference with increased output quality.

Approximate computing has emerged as a unique proposition for error-resilient applications such as image/video processing, neural networks, and the like, where both performance and power can be simultaneously reduced by trading off output quality. In this paper we propose a multistage approximation methodology for designing IEEE 754 floating point approximate dividers (FPADs). We propose a number of FPADs with varying upper bounds on error. For the same mean error, FPAD is 2.84× better in terms of power-delay product (PDP) as compared to state of the art approximate floating point divider. Further, when applied on applications, such as image enhancement, mean filtering and JPEG compression, FPAD outperforms the existing state-of-the-art approximate divider in terms of PDP by 25%. We also show that FPAD gives same PDP benefits in Alexnet convolutional neural network without noticeable drop in top-5 and top-1 accuracy.

Approximate circuits for ASICs have gained immense traction in recent years due to the benefits obtained in both energy and performance with little or no loss in output quality. Approximation in FPGAs remain a challenge due to the higher level of granularity at which logic is implemented on FPGAs. The smallest configurable blocks in FPGAs used for implementing logic consists of the look up tables (LUTs). In this paper, we exploit the inherent structures available in the FPGAs to implement SEDAAF. SEDAAF is a runtime configurable approximate adder that can perform a one-bit exact addition or two-bit approximate addition using the same hardware. SEDAAF also has a maximum bounded error, i.e. for an n-bit adder if m-bits are approximated the maximum error is 2m- 1. SEDAAF consumes 25% lesser power and has a 17% lesser power delay product as compared to existing designs. SEDAAF outperforms the existing state of the art designs in terms of output quality for Sobel edge detection application and can be used in approximate processors for performing both exact and approximate additions.

Approximate computing has gained a lot of popularity due to its energy benefits in a variety of error-tolerant applications. In this paper we are proposing an adder which can perform n-bit single exact addition or dual approximate addition (SEDA), and is suitable for processors. The conversion from exact to approximate addition can be dynamically done at runtime. The maximum error is bounded for SEDA adders as carry is not approximated. Our proposed design consumes 48% lesser energy, has 32% lesser delay, occupies 24% lesser area as compared to exact mirror adder.

Multimedia applications consume an immense amount of energy. These applications have division as one of the fundamental operations. Division is also one of the costliest operations in terms of energy consumption. Thus, various works have been done to address the issue of energy consumption in multimedia applications by using approximate dividers based on pass transistor logic (PTL). Since these applications have resilience towards erroneous computations huge energy benefits are obtained as a result of approximate computations with similar output quality. In this paper, we have shown that PTL based designs are not suitable for lower technology nodes. We performed an in-depth analysis using UMC 65nm and UMC 28nm to highlight the adverse effects of technology scaling on energy consumption and delay in PTL based design as compared to CMOS based designs. We also propose four different inexact CMOS subtractor (ICS) designs, as they are the basic repeated module in inexact restoring array dividers (IRADs). Our proposed ICS designs consume ~ 2× lesser dynamic energy, ~ 3× lesser static power and have ~ 2.5× lesser delay as compared to the existing PTL based designs in UMC 65nm. These benefits increase for UMC 28nm, which shows PTL based designs further worsens at lower technology nodes. IRADs also give about 50% reduction in energy consumption with only 3% degradation in Structural Similarity (SSIM) Index, an image quality metric in multimedia applications like change detection, background removal, and JPEG compression, as compared to exact restoring array divider (ERAD).