The Capability Hardware Enhanced RISC Instructions (CHERI) architecture provides fine-grained memory protection for systems, but introduces additional hardware overheads that may negatively impact performance. Evaluating and optimizing such secure architectures require benchmarks that explicitly exercise their security mechanisms. Despite the abundance of benchmarks for unhardened systems, security-aware benchmarks for CHERI-based architectures remain scarce. We address this gap by proposing a framework for generating security-aware benchmarks for CHERI-based RISC-V systems, leveraging the TestRIG tool and applying CHERI-specific post-processing to ensure valid capability usage. As a demonstration use case, we apply the generated benchmarks to evaluate an In-Memory Computing (IMC)-based acceleration of the CHERI tagged memory. Our results show best-case speedups between 6% and 11%, while also identifying scenarios in which the acceleration proves no performance benefit.

Virtual Prototypes (VPs) are important tools in modern hardware development. At high abstractions, they are often implemented in SystemC and offer early analysis of increasingly complex designs. These complex designs often combine one or more processors, interconnects, and peripherals to perform tasks in hardware or interact with the environment. Verifying these subsystems is a well-suited task for VPs, as they allow reasoning across different abstraction levels. While modern verification techniques like symbolic execution can be seamlessly integrated into VP-based workflows, they require modifications in the SystemC kernel. Hence, existing approaches modify and replace the SystemC kernel, or ignore the opportunity of cross-level scenarios completely, and would not allow focussing on special challenges of particular subsystems like peripherals. We propose CrosSym and SEFOS, two opposing approaches for a versatile symbolic execution of peripherals. CrosSym modifies the SystemC kernel, while SEFOS instead modifies a modern symbolic execution engine. Our extensive evaluation applies our tools to various peripherals on different levels of abstractions. Both tools’ extensive sets of features are demonstrated for (1) different verification scenarios, and (2) identifying 300+ mutants. In comparison with each other, SEFOS convinces with the unmodified SystemC kernel and peripheral, while CrosSym offers slightly better runtime and memory usage. In comparison to the state-of-the-art, that is limited to Transaction Level Modelling (TLM), our tools offered comparable runtime, while enabling cross-level verification with symbolic execution.

Modern hardware design is challenged by the ever-increasing complexity of designs. An important step is hardware verification, where Virtual Prototypes (VPs) can be used for a cross-level verification throughout the refinements. Peripherals are relevant targets, because they characteristically implement a wide range of integral tasks. Symbolic execution is a popular verification method, but has been applied to SystemC peripherals only once, and never for a cross-level verification. We propose CrosSym, the first method to verify peripherals at both Register Transfer Level (RTL) and Transaction Level Modelling (TLM) abstraction with symbolic execution, explicitly supporting cross-level. Our extensive evaluation explores (1) the performance costs of two abstraction levels, (2) our approach’s suitability for a full verification, using three peripherals, (3) it’s bug finding capabilities by killing over 1500 mutants in under 15 min. In the latter, most scenarios found 97+% of the observable mutations.

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

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.

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.

In this paper, we introduce a novel set of security coverage metrics for information flow at the system level. The proposed security coverage metrics play a crucial role in assessing the qualification and quantification of various security properties, in addressing specific threat models, such as availability, and in identifying potential security vulnerabilities associated with information flow. To implement these metrics, we present SiMiT, a tool that leverages Virtual Prototypes (VP), and Static and Dynamic Information Flow Tracking (IFT) methodologies. We demonstrate the applicability of the proposed security coverage metrics through SiMiT on an open-source RISC-V VP architecture with its peripherals. By assessing the security properties using these metrics, we pave the way for a security-aware Completeness Driven Development (CDD) concept and the development of secure System-on-Chip (SoC) designs.

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.

RISC-V has generated a lot of interest in academia and industry alike due to the open source, modular, and royalty-free design of the Instruction Set Architecture (ISA). With its modular extensibility and the ability to customize the ISA to meet application-specific needs, new challenges arise in terms of verification. Various approaches have been proposed to overcome these challenges, including traditional simulation-based verification and formal verification. While formal verification is considered thorough, its quality heavily depends on the properties and assumptions of the proofs meeting the exact specification. In this paper, we propose a structured and mutation-based approach for qualifying formal verification techniques related to the RISC-VISA. Specifically, we identify rules and mutation classes that can be used to derive a set of mutations to test the capabilities of formal verification tools. We evaluate our approach through a case study, applying a set of mutations to an open-source RISC-V processor, which we verify using the riscv-formal formal verification framework. Our results identify verification gaps uncovered through the generated mutations. We discuss the impact of these identified gaps and how they can be assessed within the context of formal verification.

Heterogeneous platforms, that integrate CPU and FPGA-based processing units, are emerging as a promising solution for accelerating various applications in the embedded system domain. However, in this context, so far, comprehensive studies that combine theoretical features of real-time task scheduling with practical runtime architectural characteristics have mostly been ignored. To fill this gap, in this paper we propose a real-time scheduling algorithm with the objective of minimizing the overall execution time under hardware resource constraints for heterogeneous CPU+FPGA architectures. In particular, we propose an Integer Linear Programming (ILP) based technique for task allocation and scheduling. We then show how to implement a given scheduling on a practical CPU+FPGA system regarding current technology restrictions and validate our methodology using a practical RISC-V case-study. Our experiments demonstrate that performance gains of 40 % and area usage reductions of 67 % are possible compared to a full software and hardware execution, respectively.

In this paper we propose μ RV32 (MicroRV32) an open source RISC-V platform for education and research. μ RV32 integrates several peripherals alongside a configurable 32 bit RISC-V core interconnected with a generic bus system. It supports bare-metal applications as well as the FreeRTOS operating system. Beside an RTL implementation in the modern SpinalHDL language ( μ RV32 RTL) we also provide a corresponding binary compatible Virtual Prototype (VP) that is implemented in standard compliant SystemC TLM ( μ RV32 VP). In combination the VP and RTL descriptions pave the way for advanced cross-level methodologies in the RISC-V context. Moreover, based on a readily available open source tool flow, μ RV32 RTL can be exported into a Verilog description and simulated with the Verilator tool or synthesized onto an FPGA. The tool flow is very accessible and fully supported under Linux. As part of our experiments we provide a set of ready to use application benchmarks and report execution performance results of μ RV32 at the RTL, VP and FPGA level together with a proof-of-concept FPGA synthesis statistic for different processor configurations. We believe that our μ RV32 platform is a suitable foundation for further research and education purposes due to its open source nature, accessible toolchain working in Linux and support for small low-priced FPGAs in combination with a solid feature set.

Recently, Virtual Prototypes (VPs) implemented in SystemC TLM (Transaction-Level Modeling) have been introduced into the growing RISC-V ecosystem to facilitate early software development and testing. However, accurate environment modeling, which is crucial for Cyber-Physical Systems (CPS), has been mostly neglected to this point. Thus, in this paper, we propose the RISC-V AMS VP framework, that combines an existing open source RISC-V VP with the SystemC AMS (Analog/Mixed Signal) environment modeling style to obtain a RISC-V evaluation platform tailored for CPS. As a case study we created a temperature control system that integrates a sensor and heater component together with a control software. Moreover, we present results on an exemplary fault-injection evaluation that is enabled by bringing together software, hardware and environment models in our unified RISC-V AMS VP framework. Finally, we provide the RISC-V AMS VP framework together with the temperature control system as open source to stimulate further research and as foundation for educational purposes.