
The Fiduccia-Mattheyses-Sanchis (FMS) algorithm is a widely used local search method for K-way circuit partitioning, but it's prone to getting stuck in local minima. Traditionally, this has been addressed by running FMS multiple times with different random initial solutions, hoping for a better result. Building on our previous work with an RL-based local search method that helps FMS avoid these traps, this research explores a new approach: using constructive methods to generate superior initial solutions. We explored two such methods: NDE (node growing algorithm), a commonly used node-based method that maximizes node absorption, and NET (net growing algorithm), an edge-based approach that maximizes net absorption. By integrating NDE and NET with our RL-based local search, we've achieved significant improvements. Experiments on ISPD98/IBM benchmarks demonstrate that an edge-based approach provides higher-quality solutions for larger circuits and larger numbers of partitions. Combining these initial solutions with our RL-based approach further reduces the cutsize generate by the RL-based approach by up to 79.5%.
In the domain of formal verification, translating natural language (NL) requirements into Computation Tree Logic (CTL) specifications presents a notable challenge due to the disparity between human-readable documents and formal specifications. This paper introduces a novel approach that leverages Large Language Models (LLMs) to automate this translation process, thereby enhancing the accuracy and efficiency of formal verification practices. We fine-tune three state-of-the-art LLMs—LLAMA3, Mistral, and Qwen2—with a particular focus on optimizing the Mistral model due to its superior performance. Our methodology is supported by the Natural2CTL dataset, consisting of 2,095 NL requirements and their corresponding CTL specifications. We employ evaluation metrics such as validation loss, accuracy, semantic similarity, and Structural Operator Jaccard Similarity (SOJS) for a comprehensive assessment of model performance. Additionally, a comparative analysis with human translators, trained in CTL logic, underscores the LLMs’ potential to match or even surpass human accuracy in translating NL requirements into formal specifications. Our findings reveal that the fine-tuned Mistral model significantly outperforms the other LLMs and human participants, demonstrating superior accuracy in generating CTL specifications. This study advances the field of formal verification by proposing a scalable solution to the NL-to-CTL translation challenge, setting a new benchmark for the integration of AI tools in complex specification tasks.
The diversity of Instruction Set Architectures (ISAs), each with its unique constraints and optimization strategies, presents significant opportunities and challenges in processor design. Modern processor vendors exploit these ISAs to enhance security, reliability, and performance. Recent security vulnerabilities, notably Spectre and Meltdown, have highlighted the critical need for robust hardware security measures. In this paper, we employ gem5, a state-of-the-art cycle-accurate simulation tool, to simulate the Spectre attack. We developed and modified scripts for both x86 and ARM architectures to ensure compatibility with gem5 version 23.1. Our simulation setup involved running attack scenarios under various configurations to gather comprehensive data on cache misses, cache hits, mispredicted branches, and level 2 cache hits and misses. In the simulation, we analyzed the trace files generated by gem5, utilizing a range of debug flags such as Exec for disassembly (dasm) insights. By detailed analysis of cache and branch prediction using detailed debug data revealed by gem5 traces, we identify some specific attack patterns that are useful for automating the detection of the attacks. Our future work aims to expand this analysis to include additional attack vectors and find more attack patterns, thereby strengthening our attack pattern recognition capabilities.
This study optimizes the Verilog-to-Routing (VTR) flow, an open-source Computer-Aided Design (CAD) tool. It utilizes ODIN II and Parmys for synthesis, ABC for technology mapping, and Versatile Place and Route for packing, placement, and routing. The ABC9 optimizations, integrated as a pass within the Yosys Open Synthesis Suite, enhance technology mapping and optimization stages and outperform the traditional ABC tool for large, complex designs. These optimizations improve timing behavior in multi-clock designs and include a delay model for Field Programmable Gate Array (FPGA) hard blocks. Various benchmarks assess the effectiveness of the workflow across different design complexities and FPGA architectures, including the utilization of hard blocks.
There is a conceptual divide between the ways cryptographic algorithms are defined (i.e., informal imperative pseudocode) and commodity hardware design languages (e.g., Verilog). How does one even begin to compare a pseudocode to an HDL design that purports to implement it in hardware? Bridging this divide requires substantial manual intervention and, consequently, “shrinking the divide” can drastically reduce the cost of high-assurance cryptographic hardware by reducing the cost of formal verification. We present a correct-by-construction methodology for the functional hardware design language, ReWire, in which a reference cryptographic algorithm is transformed into a provably correct hardware design with a program transformation called temporal staging. We illustrate this methodology with case studies including one for the BLAKE2b cryptographic hash function. Because the reference algorithm, the temporal staging transformation, and the resulting implementation are all expressed in ReWire, formal verification can proceed immediately via a published ReWire semantics.
The page size used for virtual to physical address translation has globally not changed since the late 1960’s: the IBM 360, circa 1964, already had 4 KiB pages. This 4 KiB page size has proven to be incredibly robust given the changes in processor architectures, workloads behavior, memory size, and access patterns. However, with 64-bit registers, 57-bit virtual addresses, and increasingly bigger physical memories, we have to ask ourselves whether 4 KiB is still an adequate page size for modern workloads on modern machines. Inherently, the page size has an influence on (a) the miss rate of the translation lookaside buffer, the cache that contains the recently used virtual to physical translations, and (b) the memory allocated by the system versus the memory actually used by a process. The page size also constraints some microarchitectural choices, such as cache design, which impacts the overall performance and energy efficiency. We focus more particularly on High Performance Computing (HPC) applications because they are extremely demanding in terms of memory, and are indicative of future general-purpose needs.In this paper, we empirically study the evolution of the miss rate and memory occupancy with respect to the page size, and conclude that a page size of 32 KiB is better suited for current HPC systems. We also propose a page table scheme for RISC-V-based HPC systems based on our observations and discuss its benefits.
We demonstrate how dynamic verification (e.g. simulation) can be replaced by deductive formal verification and how to benefit from the advantages of symbolic verification and the reuse of verification proofs. To do this, we swap the well-known module-hierarchy based concept with a transaction-level (TL) based alternative, which still allows us to describe the design as precisely as on RTL. We enhance the aspect-oriented and TL oriented language PDVL to support the definition of functional coverage (FC) and assertions at all levels of a TL-hierarchy.We then show how to use a deductive formal verification (DFV) flow which compiles PDVL code into Gallina code to be used by the Coq theorem prover. It can be argued that FC can be converted into proof obligations and that proving them is equivalent to 100% coverage. We also demonstrate how lower-level proofs can be reused when verifying aspects at higher-levels of a TL-hierarchy. We argue that the traditional assertion-based verification (ABV) methodology is still supported and SVA can be proven using DFV.
With increasing aging problems of advanced technologies, in-field testing becomes an inevitable challenge, on top of the already demanding requirements, such as the ISO26262 for automotive safety. SOCs used in space, automotive or military applications in particular are worst affected as the in-field failures in these applications could even be life threatening. We focus on on-line and in-field testing for Single Event Upsets (SEU, caused by a single ionizing particle) and aging defects (such as delay variation and stuck-at faults) which may appear during normal operation of the device. Interrupting normal operations for aging defects testing is a major challenge for the OS. Additionally, checkpointing with rollback-recovery can be costly and mission critical data can be lost in case of an SEU event. We eliminate many of these problems with our non-interfering in-field testing and recovery solution.We apply a hardware performance improvement technique called System Hyper Pipelining (SHP), which combines well-known context switching (Barrel CPU) and C-slow retiming techniques. The SoC is enhanced with an SEU detection and ultra-fast recovery mechanism. We also use an RTL ATPG framework that enables the generation of software-based self-tests to achieve 100% coverage of all testable stuck-at-faults. The paper finishes with very promising performance-per-area and test-cycles-per-net results. We argue that our robust system architecture and EDA solution, designed and developed primarily for in-field testing of SoCs, can also be used for production and on-line testing as well as other applications.
In precision agriculture, integrating advanced technologies is crucial for optimizing plant growth and health monitoring. Cyber-physical system (CPS) platforms tailored to specific agricultural environments have emerged, but the diversity of these environments poses challenges in developing adaptive CPS platforms. This paper explores rapid prototyping methods to address these challenges, focusing on non-destructive techniques for estimating plant growth. We present a CPS prototype that combines sensors, microcontrollers, digital image processing, and predictive modeling to measure leaf area and biomass accumulation in hydroponic environments. Our results show that the prototype effectively monitors and predicts plant growth, highlighting the potential of rapid CPS prototyping in promoting sustainability and improving crop yields at a moderate cost of hardware.
Circuit optimization, in any application, is of high importance since it not only improves the efficiency of the intended purpose but also enhances the quality of the final product. It enables the circuit designer to cater to the specific needs of the customer. For circuit optimization to occur, we need to elaborate these circuits on a primary level and perform synthesis operations. Previous research shows that the investigation of improvements to different Hardware Description Language (HDL) elaboration phases, was completely closed source. Verilog To Routing (VTR) is an open-source Electronic Design Automation (EDA) tool. ODIN II is the VTR synthesizer that parses the input Verilog, elaborates its Abstract Syntax Tree (AST), performs the partial mapping according to the architecture file, and performs optimizations such as unused logic removal. To that end, the hard versus soft logic trade-off aims to optimize the performance of the circuit. This project focuses on using machine learning approaches to make synthesis tools intelligent enough to decide this ratio on their own, without the need for human intervention, and based on some predefined criteria. This paper discusses the criteria for having less latency or less critical path delay in the circuit. Also, it aims at providing this level of intelligence at an earlier stage in the VTR pipeline to make better use of this information.
The Compact Muon Solenoid (CMS) high-granularity calorimeter (HGCAL) upgrade for CERN's Large Hadron Collider (LHC) high-luminosity phase is a detector with more than 6 million channels that will provide precise sensing and measurement of position, timing, and energy of the particles produced in the collisions of the beams. The HGCAL electronics are a large and complex set of processing systems split into front-end and back-end. The front-end, located in the experimental cavern, consists of $\boldsymbol{\approx 150}$ thousand radiation tolerant ASICs. The high-density FPGA-based back-end is housed away from the radiation area in a set of Advanced Telecommunications Computing Architecture (ATCA) boards and crates hosting $\boldsymbol{\approx 100}$ FPGAs. Each ATCA back-end board will comprise one (or two) FPGAs, managing up to $\boldsymbol{\approx 120}$ optical links, each providing a transmission rate of 10.24 Gb/s between the back-end and the front-end electronics. Each back-end FPGA is responsible for configuring and monitoring up to $\boldsymbol{\approx 3500}$ front-end ASICs and will be controlled by software running on a back-end MPSoC that provides the entry point for the whole control procedure. This paper presents the design and implementation of the prototyping infrastructure deployed to test and validate the slow-control block of the HGCAL back-end electronics, together with the related interfaces with the controller MPSoC and the front-end transceiver ASICs. The required functionalities have been validated with a ZCU102 Xilinx Ultrascale+ development board, which emulated the back-end elements that are still under development and not yet available for this comprehensive test. This development board was connected to other custom ASIC development boards via optical links, emulating the front-end side of the system, also still under development. Besides providing reliable testing and validation of the operation of the whole infrastructure, the prototyping platform also allowed to attain the required software/hardware portability that ensures easy integration/replacement of all the (still) emulated components with their final implementations.
Implementing nontrivial HDL designs can take a lot of time. Particularly for FPGAs, vendor tools tend to become slower, since the devices grow and thus, also the designs grow. It is therefore desirable to create mechanisms that speed up the implementation. Combining pre-implemented blocks to build the final design can be one such mechanism. It can help to reduce the time required for incremental builds, or it can reduce the time required to build families of designs. Yet, typical HDL code is not structured for this purpose. Many modules do not have the right size to be used as pre-implemented blocks. In this paper, we present a methodology to automatically analyze and modify existing HDL code such that the resulting module structure fits the purpose of pre-implementing the modules. To this end, we try to isolate parameters of the HDL code such that we have to reimplement only a small number of modules after a parameter change. The resulting tool is available as opensource software. We have tested our methodology using multiple different benchmark sets, which in total contain thousands of modules. On average, we can extract around 10% of the parameters into smaller modules.
We present a framework that enables systematic analysis of mixed-signal application on FPGA and show its application during architecture validation of a power controller. The open source synthesizable model generator for mixed-signal blocks (msdsl) is used to create a synthesizable prototype of the analog power control application. A library of instrumentation elements enables control from a host computer, time control, analog event capture, analog stimulus and noise generation, as well as trace, read and write of arbitrary signals. This keeps the effort of building the FPGA application prototype low and provides good debugging and analysis capabilities. The end-result is a unique analysis framework for mixed-signal applications that offers almost real time analog simulation speed - thus considering software as well as analog and digital hardware - no risk of damaging equipment and simulator alike analysis and debugging capabilities at a low overhead through an instrumentation library.
The demand for optimized and efficient embedded software is increasing in many applications such as the Internet of Things (IoT) or other Cyber-Physical Systems (CPS). Hence, early performance analysis of embedded software is essential to perform Design Space Exploration (DSE), ensure efficiency, and meet time-to-market constraints. Designers usually use real hardware, simulators, or static analyzers to obtain the performance. However, these methods suffer from serious drawbacks as real hardware is not available in the early stage of the design process, simulators either do not support any timing accuracy or require large execution time, and static analyzers need details of the hardware microarchitecture. In this paper, we present a novel Artificial Neural Network (ANN)-based approach that allows a fast and accurate performance estimation of embedded software for RISC-V processors in the early design phases. This can significantly reduce the burden on designers to perform DSE. The proposed approach takes advantage of the dynamic analysis technique and analytical models and does not require any microarchitecture-related parameters such as cache misses, cache hits, and memory-level parallelism. We compare our proposed microarchitecture-independent approach with state-of-the-art in terms of speed and accuracy. Our experiments on various benchmarks demonstrate that the proposed approach achieves a speed-up of $4.41\times$ compared to a RISC-V Virtual Prototype (VP) at the Electronic System Level (ESL), while the estimation results have only a Mean Absolute Percentage Error (MAPE) of 2%.
Object detection based on convolutional neural network (CNN) is widely used in multitude emergent applications. Yet, the deployment of CNNs on embedded devices at the edge with reduced resources and power budget poses a real challenge. In this paper, we address this issue by enhancing the detection performance without impacting the inference speed. We investigate the use of multi-view for the same scene to achieve better detection performance. A novel system of distributed smart cameras is proposed where each camera integrates a CNN for detection. Implementation results show that using light networks on the distributed cameras can lead to better detection performance and a reduction in the overall consumed power.
Photo-realistic neural rendering, represented by neural radiance field (NeRF), is considered to be a key technology for AR/VR applications and has been actively studied in recent years. In order to enable widespread adoptions of AR/VR, it is critical to enable low-cost and high-quality rendering on mobile and server systems. In our work, we investigate the feasibility of low-precision representation on the two state-of-the-art NeRF models, InstantNeRF and TensoRF. Our proposed quantization is based on our observation on the characteristics of trained NeRF models. In order to reduce the model size while limiting the loss of rendering quality due to model compression, we propose quantizing the portion of model which dominates the total model size while being robust to aggressive quantization. In our experiments, we demonstrate our proposed ternary quantization can reduce by $7 \times \sim 15\times$ the model sizes of state-of-the-art NeRF models at a negligible loss of rendering quality, which, we consider, will contribute to the AR/VR adoptions on mobile and server systems.
Artificial Intelligence techniques based on convolution neural networks (CNNs) are now dominant in the field of object detection and classification. The deployment of CNNs on embedded edge devices targeting real-time inference sets a challenge due to the limited computing resources and power budgets. Several optimization techniques such as pruning, quantization and use of light neural networks enable the realtime inference but at the cost of precision degradation. However, using efficient approaches to apply the optimization techniques at training and inference stages enable high inference speed with limited degradation of detection performance. In this paper, we revisit the problem of detecting and classifying maritime objects. We investigate different versions of the You Only Look Once (YOLO), a state-of-the-art deep neural network, for real-time object detection and compare their performance for the specific application of detecting maritime objects. The trained YOLO networks are efficiently optimized targeting three recent edge devices: Nvidia Jetson Xavier AGX, AMD-Xilinx Kria KV260 Vision AI Kit, and Movidius Myriad X VPU. The proposed deployments demonstrate promising results with an inference speed of 90 FPS and a limited degradation of 2.4% in mean average precision.
Cache and cache-coherence are major aspects of today's high performance computing. A cache stores data as cachelines of fixed size, and coherence between caches is guaranteed by the cache-coherence protocol which operates on fixed size coherency-blocks. In such systems cache-lines and coherencyblocks are usually the same size and are relatively small, typically 64 bytes. This size choice is a trade-off selected for generalpurpose computing: it minimizes false-sharing while keeping cache-maintenance traffic low. False-sharing is considered an unnecessary cache-coherence traffic and it decreases performances. However, for dedicated accelerator this trade-off may not be appropriate: hardware in charge of cache-coherence is expensive and not well exploited by most accelerator applications as by construction these applications minimize false-sharing. This paper investigates the possibility of an alternative tradeoff of cache-coherency and cache-maintenance block size for many-core accelerators, by decoupling coherency-block and cache-lines sizes. Interests, advantages and difficulties are presented and discussed in this paper. Then we also discuss needs of software and hardware modifications in prototypes and the capability of such prototypes to evaluate different coherenceblock sizes.
In-Memory Computing (IMC) is a promising paradigm to mitigate the von Neumann bottleneck. However its evaluation on complete applications in the context of full-scale systems is limited by the complexity of simulation frameworks as well is the disjunction between hardware exploration and compiler support. This paper proposes a global exploration flow in the scale of Instruction Set Architectures (ISA) to perform both modeling and the generation of compiler support to perform ISA-level exploration. Our emulation methodology is based on QEMU, implements a performance model based on hardware characterizations from the State-of-the-Art, and allows the modeling of cache hierarchies, while our compiler support is automatically generated and based on a specialized compiler. We evaluate three applications in the domains of image processing and linear algebra on a reference IMC architecture, and analyze the obtained results to validate our methodology.
EFPGAs give designers the flexibility to make changes at any point in the chip’s life span, even in the customers’ systems. Though, eFPGA are not efficient from an integration perspective, making proper dimensionning and tailoring mandatory. Unfortunately, designing an eFPGA is a complex and error-prone task. Even though automatic generation from high level models can produce correct-by-construction layouts, integration remains complex due to process variation. A key point is then to reduce the technology dependency.This paper presents the ELNATH project in which three implementations of the same architecture have been addressed: overlay, eFPGA, and 55 nm FPGA thanks to an open-source integrated tool flow that supports defining, implementing and programming reconfigurable architectures.