FPGA-based acceleration has been explored to address performance challenges in architectures incorporating federated learning (FL) and homomorphic encryption (HE). However, model updates, which involve HE, are infrequent in FL applications; thus, static allocation of FPGA resources for HE can lead to inefficiency. In response, this paper presents a work-in-progress FPGA-based FL accelerator that leverages dynamic partial reconfiguration to accelerate HE operations flexibly.
The increasing complexity of multiprocessor embedded systems demands automated design flows that bridge the gap between high-level specifications and efficient parallel implementations. Automatic parallelization via rule-based model transformations has proven promising, but navigating the vast transformation space remains challenging. We present an automated strategy that systematically guides transformation application, enabling performance-aware parallelization through scalable and targeted space exploration.Our approach employs attributed graphs as a formal and expressive intermediate representation for evaluating and applying model transformations. These graphs enrich nodes and edges with semantic properties (such as process types, execution costs, and communication dependencies), capturing both application structure and platform characteristics in a unified model.We evaluate our strategy on an image processing application using a prototype implementation. The tool autonomously reduces the number of transformations from 203 to 74 and shortens the exploration time from over 17 hours to under 12, while improving performance by filtering out non-beneficial transformations.
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 68x compared to the baseline CPU of the VP, demonstrating its effectiveness in accelerating MVM-dominated applications.
While existing hardware runtime monitors for processors are limited in scope and reconfigurability, this paper addresses the need for a flexible and comprehensive monitoring solution. We introduce the Time Contract Co-Processor (TCCP), a reconfigurable open-source co-processor for RISC-V systems. The TCCP uses a formal contract-based notation as input to specify the system’s timing and behavioral requirements. A dedicated toolchain enables the translation of contract micro-programs executed in the TCCP to monitor complex applications.
We introduce a symbolic execution-based framework to generate the environment constraints needed to formally verify a hardware design. The core of the approach is a new search strategy that leverages piecewise composition, a divide-and-conquer algorithm introduced in prior work, to guide symbolic execution toward paths more likely to generate needed environment constraints. In our preliminary evaluation using the decoder module of the OpenTitan SoC, the framework finds the needed constraints without overconstraining the environment.
The push to support artificial intelligence in embedded systems introduces new challenges regarding software support of specialized hardware. The RISC-V instruction set architecture offers a promising platform for accelerators for said AI applications through custom instructions. Integrating these instructions into existing software codebases poses significant challenges, including manual adaptations and limited compiler support. This paper introduces a novel approach that generates hardware-optimized code utilizing custom instructions defined by a platform model. This method enhances the reusability of code and leverages design artifacts from the hardware design process to optimize the generated software in both C and Rust by generating intrinsic support for custom instructions through inline assembly. If the underlying platform does not allow the utilization of the specified custom instruction, an alternative implementation with optional global side effects is generated instead of the intrinsic. Thus, it expedites development by minimizing manual coding efforts and facilitates the seamless integration of hardware accelerators. An exemplary implementation of a matrix multiplication utilizing a custom multiply-accumulate instruction presented in this paper highlights the efficiency provided by this approach. Measurements based on this implementation show a reduction of the executed instructions by up to 75% while also achieving a 5-fold theoretical reduction in manual effort.
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.
Hardware design weaknesses, when overlooked, can lead to security vulnerabilities. Their cost of fixing is higher the later they are found in the development life cycle. The challenges of detecting these issues in the early stages of hardware design, compared to software design, can be attributed to limited research or poorly defined design guidelines. Using the existing hardware design weakness classification by the MITRE Corporation, we evaluated how Information Flow Tracking (IFT) can be utilized to identify security weaknesses in hardware designs. First, we provide a classification of design weaknesses tailored to detection using IFT. Second, we present a case study to identify one of such weaknesses using an open-source IFT tool. Additionally, we discuss the challenges of using IFT to detect information-flow-based hardware design weaknesses.
The hardware complexity in electronic devices has increased significantly in recent decades due to technological advancements. To ensure correct behavior of such devices and meet time-to-market constraints, modern circuit verification and testing tools rely on formal proof techniques. The two most popular methods in this context are Binary Decision Diagrams (BDDs) and Boolean Satisfiability (SAT) solvers. Even though these methods share some similarities, they are fundamentally different. Whereas BDDs usually require a large amount of memory to represent all solutions, SAT solvers are memory-efficient but they typically compute only a single solution. To tackle these issues, a hybrid approach called Binary Hybrid Diagram (BHD) is proposed for efficient generation of multiple solutions. BHDs combine the major advantages of BDDs and SAT solvers, and generate distinct solutions heuristically via algorithms. Experiments demonstrate that feasible solutions are generated rapidly by using BHDs while the memory requirement remains small compared to state-of-the-art methods.
Modern applications increasingly rely on embedded systems that incorporate visual interfaces developed utilizing so-called embedded graphics libraries. Verifying these embedded graphics libraries is challenging due to hardware dependencies and the lack of reference outputs. The lack of reference outputs is tackled in Metamorphic Testing (MT) by constructing two Firmware (FW) versions with distinct implementations that maintain the same input-output relationships. These relations are known as Metamorphic Relations (MRs). However, the development of these MRs remains a tedious and challenging task.In this paper, we present a novel approach for generating MRs for MT of embedded graphics libraries using Large Language Models (LLMs). Because directly creating MRs with simple prompts is too complex for the LLM, we employ proven prompting strategies to develop our LLM-assisted MR pipeline. Strategies include role prompting, least-to-most prompting, zero-shot prompting, constraint-based prompting, and style prompting. In our experiments, we verify a widely used embedded graphics library. We compare our results with an existing manual approach and demonstrate that LLM-assisted MRs nearly doubles coverage and identifies additional bugs.
System security requires a solid foundation in both development and operation. During development, performance trade-offs result in security infrastructures that are more or less effective, but usually imperfect. Hence, during operation, runtime monitoring and anomaly detection continuously check for security issues.In this paper, we show how development and operation can be linked. We demonstrate how information and data from development and operation can be aggregated in a digital twin and/or digital thread which is used as the basis for runtime monitoring and anomaly detection. In particular, we address the trade-off between system security and performance in a concrete smart grid system.
Transaction-level debugging in Virtual Prototypes (VPs) remains challenging due to the sheer number and intricate nature of interactions between software and hardware components. This paper presents ProtoLens, the first open-source tool for dynamic visualization of Transaction Level Modeling (TLM) transactions in SystemC-based VPs. Integrated with the open-source RISC-V VP++, ProtoLens provides an interactive web front-end that displays architecture-aware transaction flows in real-time. It captures transaction data via a lightweight extension of the TLM bus and enriches it with peripheral-specific views through user-defined modules, so-called Transaction View Modules (TVMs). Additionally, ProtoLens supports integration with software debuggers, allowing synchronized transaction inspection and control of the simulation flow. This enables developers to efficiently analyze issues such as incorrect memory mappings, unexpected peripheral behavior, and to better understand the overall system architecture.Two case studies highlight the capabilities of ProtoLens: one demonstrates how it complements classical debugging in a bare-metal software example, and the other showcases its ability to reconstruct real-time graphics output from a Linux-based game.
Modern cyber-physical systems (CPS) consist of multiple components including sensors, controllers, machine learning (ML) components, real-time schedulers, among others. Each component is usually designed separately with the aim of working perfectly. For example, task schedulers aim to ensure that all deadlines are met and ML components aim to always make perfect inferences. The correctness or "perfection" of the overall CPS is inferred from the correctness of its components. However, none of the CPS components are perfect in reality. Schedulers or tasks sometimes miss deadlines, ML components sometimes make inaccurate inferences, and sensors are occasionally noisy. These imperfections are assumed to be small enough to be ignored. In particular, it is assumed - without guarantees - that these imperfections do not compromise system safety or the correctness of the CPS. We propose to reverse this approach and argue that there is usually sufficient tolerance at the system level. This tolerance should be explicitly modeled, and its impact on the correctness or perfection of system components should be determined. This enables the design of more cost-effective, robust systems. Furthermore, appropriately designing the other components to compensate for the imperfection of individual components ensures that system-level safety remains within the specified margins.
Even when following a well-structured top-down design methodology, system designers regularly face obstacles and pitfalls posed by speed/accuracy tradeoffs in modeling and simulation of complex hardware and software systems. Across the abstraction levels, modeling details grow exponentially, while simulation speed decreases by multiple orders of magnitude. To quantify these effects, we systematically generate, simulate, and evaluate grid-based systems-on-chip in a top-down open-source based tool flow. We map two parallel software applications onto a scalable grid of RISC-V processors and successively refine and validate the models at lower abstraction levels, namely TLM, ISS, RTL, and FPGA. Our comprehensive experimental evaluation over five abstraction levels quantifies the speed-accuracy tradeoffs in simulator build and run times. In addition to its educational value, our work can guide the system designer on an efficient path to a cycle-accurate software simulation on fully constructed hardware.
The 32-bit Unix time, which is commonly used in computer systems, will overflow on 2038-01-19. Extending the format to 64 bit would allow to count seconds for 584 billion years but misses the opportunity to add features, such as sub-second precision or relative time encoding, which are useful for a universal datetime encoding.We propose and implement Flexpoch, a versatile 64-bit time encoding that is compatible with Unix time, has a high range of 21 thousand years, supports leap seconds and timezone offsets, and offers multiple precisions from 119 ns to millennia while being highly resource-efficient.
We study the problem where an autonomous system is in a critical situation and is faced with multiple options among which it has to choose to safely evade the criticality. Each of these options is also associated with some uncertainty. Traditional approaches from formal methods require a reachability analysis to evaluate which of the options is safe. While the computational cost of reachability analysis is well known, the presence of uncertainty adds an additional layer of complexity. As a result, performing reachability analysis for all the options before choosing one will not be feasible due to time constraints. This is a practical problem that arises is various scenarios, such as an autonomous vehicle in a potential accident that it has to evade to minimize damage. While models and algorithms for reachability analysis have been widely studied, reachability analysis in the presence of uncertainties have been less so. Despite its many applications, to the best of our knowledge, the problem of choosing in real-time, one of the many options for criticality evasion has not been studied in the past. We address this problem by proposing a new real-time reachable set computation technique for uncertain linear systems using techniques from perturbation theory.
Deep Neural Networks (DNNs) are increasingly used in safety-critical Cyber-Physical Systems (CPS), requiring rigorous verification. Existing methods struggle with scalability and over-approximation. We introduce Affine Arithmetic Decision Diagrams (AADDs) for DNN reachability analysis, leveraging affine arithmetic to preserve variable correlations and improve precision. Our approach provides a structured symbolic representation of network decisions, enabling efficient and accurate verification. Additionally, AADDs unify verification for DNNs and Analog-Mixed-Signal (AMS) systems, supporting holistic safety analysis.
A safety-critical domain-specific language is presented, EXS (ETCS eXecutable Specification). The language is designed to facilitate the implementation of on-board signalling applications responsible for the safe movement of trains, more specifically according to the European Train Control System (ETCS). The implementation of this language on a safety critical platform is presented, and is illustrated with various examples of applications developed, tested, and deployed on a fleet of freight locomotives running on the Belgium network. Lessons learned are presented, and future possible developments are discussed.
In exposed data path architectures, registers are replaced by an on-chip network that connects their processing units (PUs) directly. This allows the compiler to determine PU allocation, instruction scheduling, and data transport between the PUs. To prevent unnecessary synchronization of the PUs, their network ports are typically buffered. Although many performance models are available for traditional RISC architectures, there are no specific performance models for buffered exposed datapath (BED) architectures.In this paper, we investigate the impact of the relevant design parameters of BED architectures, consider their dependencies, and determine reasonable parameter values for designing cost-effective efficient BED processors. In particular, we examine the number of PUs, the instruction issue width (superscalarity), the size of network buffers, and the latency of instructions, and relate these parameters with the processor performance. We develop a performance model to estimate the runtime in terms of the mentioned parameters and validate our performance model with experimental results.
