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.

Continuous demands for improved performance within constrained resource budgets are driving a move from homogeneous to heterogeneous processing platforms for the implementation of today’s Real-Time (RT) embedded systems. The applications executing on such systems are typically represented as a Precedence Task Graph (PTG), where a node represents a task or algorithm for one functionality and edges represent the complex interactions between multiple functionalities. Due to RT constraints, the task graph needs to be executed within a specified deadline. Although some existing studies have looked into solving this challenge, comprehensive studies that combine the theoretical features of RT task-graph mapping and scheduling with practical runtime architectural characteristics have mostly been ignored to date. Hence, in this article, we consider the challenge of scheduling an RT application modeled as a single PTG, with the objective of minimizing the overall execution time under Hardware (HW) resource and deadline constraints for heterogeneous Central Processing Unit (CPU) + Field Programmable Gate Array (FPGA) architectures. First, we introduce an optimal solution using Integer Linear Programming (ILP). However, this ILP-based optimal solution suffers from computational complexity and does not scale well even for moderately large problem sizes. Hence, we additionally propose heuristic algorithms for task mapping and scheduling. The efficiency of the proposed scheme, named MESSI, has been evaluated through experiments using PTG on a practical CPU+FPGA system regarding current technology restrictions. Our experiments demonstrate that performance gains of 55.6% and area usage reductions of 46.3% are possible compared to full Software (SW) and HW execution, respectively.

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.

Among various arithmetic circuits, dividers are one of the costliest in terms of area, energy, and delay. Hence, approximate divider designs have been implemented to reduce their cost for error-resilient applications. However, approximate dividers based on memristors for in-memory computing (IMC) have not received any attention. In this work, we propose a library of 16 by 8 approximate restoring array dividers suitable for memristor-based IMC that can be used as benchmark circuits. We developed these benchmark circuits by performing an exhaustive design space exploration based on functional approximation. We used the state-of-the-art mapping tool, SIMPLER, to perform the mapping of the divider design to the memristor crossbar. We identified the pareto optimal approximate divider designs based on the MAGIC design style with varying output qualities. We compare our pareto optimal designs with the existing state-of-the-art CMOS-based approximate divider designs when mapped to IMCs. We also performed a case study on two image processing applications. Overall we propose MARADIV, a library of MAGIC design style-based approximate restoring array divider benchmark circuits tailored for memristor-based IMC. We believe that MARADIV’s benchmark designs can be used for future research in this direction. Hence, all pareto optimal approximate restoring array divider designs will be made available at https://github.com/agra-uni-bremen/tcasii2022-maradiv-lib.

In this paper, we propose a Virtual Prototype (VP) driven verification methodology for Hardware (HW) peripherals. In particular, we combine two approaches that complement each other and use the VP as a readily available reference model: We use (A) Coverage-Guided Fuzzing (CGF) which enables comprehensive verification at the unit-level of the Register-Transfer Level (RTL) HW peripheral with a Transaction Level Modeling (TLM) reference, and (B) an application-driven co-simulation-based approach that enables verification of the HW peripheral at the system-level. As a case-study, we utilize a RISC-V Platform Level Interrupt Controller (PLIC) as HW peripheral and use an abstract TLM PLIC implementation from the open source RISC-V VP as the reference model. In our experiments we find three behavioral mismatches and discuss the observation of these, as well as non-functional timing behavior mismatches, that were found through the proposed synergistic approach. Furthermore, we provide a discussion and considerations on the RTL/TLM Transactors, as they embody one keystone in cross-level methods. As the different approaches uncover different mismatches in our case-study (e.g., behavioral mismatches and timing mismatches), we conclude a synergy between the methods to aid in verification efforts.

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.