Microarchitectural timing side channels have been thoroughly investigated as a security threat in hardware designs featuring shared buffers (e.g., caches) and/or parallelism between attacker and victim task execution. However, contradicting common intuitions, recent activities demonstrate that this threat is real even in microcontroller SoCs without such features. In this paper, we describe SoC-wide timing side channels previously neglected by security analysis and present a new formal method to close this gap. In a case study on the RISC-V Pulpissimo SoC, our method detected a vulnerability to a previously unknown attack variant that allows an attacker to obtain information about a victim's memory access behavior. After implementing a conservative fix, we were able to verify that the SoC is now secure w.r.t. the considered class of timing side channels.

Hardware accelerators (HAs) underpin high-performance and energy-efficient digital systems. Correctness of these systems thus depends on the correctness of constituent HAs. Self-consistency-based pre-silicon verification techniques, like A-QED (Accelerator Quick Error Detection), provide a quick and provably thorough HA verification framework that does not require extensive design-specific properties or a full functional specification. However, A-QED is limited to verifying HAs which are non-interfering – i.e., they produce the same result for a given input independent of its context within a sequence of inputs. We present a new technique called G-QED (Generalized QED) which goes beyond non-interfering HAs while retaining A-QED’s benefits. Our extensive results as well as a detailed industrial case study show that: G-QED is highly thorough in detecting critical bugs in well-verified designs that otherwise escape traditional verification flows while simultaneously improving verification productivity 18-fold (from 370 person days to 21 person days). These results are backed by theoretical guarantees of soundness and completeness.

While semiconductors are becoming more efficient generation after generation, the continuous technology scaling leads to numerous reliability issues due, amongst others, to variations in transistors characteristics, manufacturing defects, component wear-out, or interference from external and internal sources. Induced bit flips and stuck-at-faults can lead to a system failure. Security-critical systems often use Physical Memory Protection (PMP) modules to enforce memory isolation. The standard loosely-coupled approach eases the implementation but creates overhead in area and performance, limiting the number of protected areas and their size. While delivering great support against malicious software and induced faults, better performance would benefit safety tasks by preventing the program from jumping into an undesired region and giving wrong outputs.We propose a novel model-driven approach to resolve these limitations by generating a tightly-coupled RISC-V PMP, which reduces the impact of run-time reconfiguration. We also discuss guidelines on configuring a PMP to minimize the overhead on performance and memory, and provide an area estimation for each possible PMP design instance. We formally verified a RISC-V Core with a PMP and evaluated its performance with the Dhrystone Benchmark. The presented architecture shows a performance gain of about 3 times against the standard implementation. Furthermore, we observed that adding the PMP feature to a RISC-V SoC led to a negligible performance loss of less than 0.1% per thousand PMP reconfigurations.

Safety-critical designs need to ensure reliable operations even under a hostile working environment with a certain degree of confidence. Continuous technology scaling has resulted in designs being more susceptible to the risk of failure. As a result, the safety requirements are constantly evolving and becoming more stringent. For validating and measuring the robustness of safety-critical designs, fault injection methods are employed within the design flows. To ensure safety requirements’ compliance, and at the same time to cope with the ever-increasing complexity of modern SoCs, the existing design flows become inadequate as the process is repetitive, time-tedious, and requires high manual efforts. In this paper, a fully automated, fast and accurate, fault emulation framework based on the FPGA platform is proposed that enables a high level of controllability and observability for fault injection. The approach uses model-driven engineering concepts and automates various fault injection campaigns, namely, statistical fault injection (SFI), direct fault injection (DFI), and exhaustive fault injection (EFI). A novel design architecture tailored for the FPGA platform is also proposed to improve the overall productivity of performing fault emulation. The proposed approach scales to a wide variety of RISC-V based CPU subsystems with varying complexity in size and features. The experimental results demonstrate a significant gain in the fault emulation performance by a factor of 2.75x to 47.57x when compared to the standard simulation-based fault injection methods.

The scalable and extendable RISC-V ISA introduced a new level of flexibility in designing highly customizable processors. This flexibility in processor designs adds to the complexity of already complex functional verification process. Although formal methods are increasingly used to exhaustively verify the processors, the required manual effort and verification expertise become the major hurdles in industrial flows. Furthermore, efficient ISA modeling techniques are required that are scalable to multiple ISA extensions and to different architectural variants of a processor. This paper proposes a trace notation for ISA definition to capture the implicit execution behavior of a processor and specific characteristics. The proposed trace notation can be annotated with timing and hierarchy information to adapt the trace to any kind of processor architecture. From this trace notation, a complete set of properties are generated to detect all functional bugs in a processor implementation. The approach requires significantly less manual effort compared to the contemporary techniques. Its industry strength has been demonstrated by formally verifying a wide variety of RISC-V processor implementations with one or more ISA extensions (RV32I, C, Zicsr, M and custom extensions supporting AI acceleration and safety features).

Despite the high configurability of IPs and hardware generators, code modifications are still required to introduce aspect-oriented instrumentation to satisfy emerging design requirements such as on-chip debug and functional safety. These code modifications lead to escalated development, verification efforts and deteriorate the code reuse. This paper proposes a highly efficient aspect-oriented design automation approach that leverages graph-grammar-based model transformations. With the proposed approach, main design functionalities and aspect-oriented instrumentation are separately developed, automatically integrated and verified. To demonstrate the applicability, industrial SoCs were transformed to support on-chip debug. Experimental results confirm the efficiency of the approach. Further, reduced code is needed with the proposed automation approach, which also replaces the error-prone manual RTL coding. Finally, the transformation scripts are applicable to different SoCs, which promotes the overall code reuse.

The required manual effort and verification expertise are among the main hurdles for adopting formal verification in processor design flows. Developing a set of properties that fully covers all instruction behaviors is a laborious and challenging task. This paper proposes a highly automated and "complete" processor verification approach which requires considerably less manual effort and expertise compared to the state of the art.The proposed approach extends the S2QED approach to cover both single and multiple instruction bugs and ensures that a design is completely verified according to a well-defined criterion. This makes the approach robust against human errors. The properties are simple and can be automatically generated from an ISA model with small manual effort. Furthermore, unlike in conventional property checking, the verification engineer does not need to explicitly specify the processor's behavior in different special scenarios, such as stalling, exception, or speculation, since these scenarios are taken care of implicitly by the proposed computational model. The great promise of the approach is shown by an industrial case study with a 5-stage RISC-V processor.

The complexity of today's System on Chips (SoCs) forces designers to use higher levels of abstractions. Here, early design decisions are conducted on abstract models while different configurations describe how to actually realize the desired SoC. Since those decisions severely affect the final costs of the resulting SoC (in terms of utilized area, power consumption, etc.), a fast and accurate cost estimation is essential at this design stage. Additionally, the resulting costs heavily depend on the adopted logic synthesis algorithms, which optimize the design towards one or more cost objectives. But how to structure a cost estimation method that supports multiple configurations of an SoC, implemented by use of different synthesis strategies, remains an open question. In this work, we address this problem by providing a cost estimation method for a configurable SoC using Machine Learning (ML). A key element of the proposed method is a data representation which describes SoC configurations in a way that is suited for advanced ML algorithms. Experimental evaluations conducted within an industrial environment confirm the accuracy as well as the efficiency of the proposed method.

Hardware/software co-designs are usually defined at high levels of abstractions at the beginning of the design process in order to provide a variety of options on how to realize a system. This allows for design exploration which relies on knowing the costs of different design configurations (with respect to hardware usage and firmware metrics). To this end, methods for cost estimation are frequently applied in industrial practice. However, currently used methods oversimplify the problem and ignore important features, leading to estimates which are far off from real values. In this article, we address this problem for memory systems. To this end, we borrow and re-adapt solutions based on Machine Learning (ML) which have been found suitable for problems from the domain of Computer Vision (CV). Based on that, an approach is proposed which outperforms existing methods for cost estimation. Experimental evaluations within an industrial context show that, while the accuracy of the state-of-the-art approach is frequently off by more than 20 percent for area estimation and more than 15 percent for firmware estimation, the method proposed in this article comes rather close to the actual values (just 5-7 percent off for both area and firmware). Furthermore, our approach outperforms existing methods for scalability, generalization, and decrease in manual effort.

Developing software in a slightly different way can have a dramatic impact on soft error resilience. This observation can be transferred in a process of improving existing code by transformations. These transformations are of systematic nature and can be automated. In this paper, we present a framework for low level embedded software generation - commonly referred to as firmware -- and the inclusion of safety measures in the generated code. The generation approach follows a three stage process starting with formalized firmware specification using both platform dependent and independent firmware models. Finally, C-code is generated from the view model in a straight forward way. Safety measures are included either as part of the translation step between the models or as transformations of single models.

This paper presents an automated process for end-to-end embedded system design following OMG's model driven architecture (MDA) vision. It tackles a major challenge in automation: bridging the large semantic gap between the specification and the target code. The shown MDA adaption proposes an uniform and systematic way by splitting the translation process into multiple layers and introducing design platform independent and implementation independent views.In our adaption of MDA, we start with a formalized specification and we end with code (view) generation. The code is then compiled (software) or synthesized (hardware) and finally assembled to the embedded system design. We split the translation process in Model-of-Thing (MoT), Model-of-Design (MoD) and Model-of-View (MoV) layers. MoTs represent the formalized specification, MoDs contain the implementation architecture in a view independent way, and MoVs are implementation dependent and view dependent, i.e., specific details in target language.MoT is translated to MoD, MoD is translated to MoV and MoV is finally used to generate views. The translation between the Models is based on templates, that reflect design and coding blueprints. The final step of the view generation is itself part of generation. The Model MoV and the unparse method are generated from a view language description.The approach has been successfully adapted for generating digital hardware (RTL), properties for verification (SVA), and snippets of firmware that have been successfully synthesized to an FPGA.

Hardware/software co-designs are usually defined at high levels of abstractions at the beginning of the design process in order to allow plenty of options how to eventually realize a system. This allows for design exploration which in turn heavily relies on knowing the costs of different design configurations (with respect to hardware usage as well as firmware metrics). To this end, methods for cost estimation are frequently applied in industrial practice. However, currently used methods for cost estimation oversimplify the problem and ignore important features - leading to estimates which are far off from the real values. In this work, we address this problem for memory systems. To this end, we borrow and re-adapt solutions based on Machine Learning (ML) which have been found suitable for problems from the domain of Computer Vision (CV) - in particular age determination of persons depicted in images. We show that, for an ML approach, age determination from the CV domain is actually very similar to cost estimation of a memory system.

We present an industrial case study that demonstrates the practicality and effectiveness of Symbolic Quick Error Detection (Symbolic QED) in detecting logic design flaws (logic bugs) during pre-silicon verification. Our study focuses on several microcontroller core designs (~1,800 flip-flops, ~70,000 logic gates) that have been extensively verified using an industrial verification flow and used for various commercial automotive products. The results of our study are as follows: 1. Symbolic QED detected all logic bugs in the designs that were detected by the industrial verification flow (which includes various flavors of simulation-based verification and formal verification). 2. Symbolic QED detected additional logic bugs that were not recorded as detected by the industrial verification flow. (These additional bugs were also perhaps detected by the industrial verification flow.)3.Symbolic QED enables significant design productivity improvements: (a) 8X improved (i.e., reduced) verification effort for a new design (8 person-weeks for Symbolic QED vs. 17 person-months using the industrial verification flow). (b) 60X improved verification effort for subsequent designs (2 person-days for Symbolic QED vs. 4-7 person-months using the industrial verification flow). (c) Quick bug detection (runtime of 20 seconds or less), together with short counterexamples (10 or fewer instructions) for quick debug, using Symbolic QED.

This paper presents a practical methodology for applying formal verification on industrial designs. The methodology is developed considering the quality, efficiency and productivity required in an industrial verification setup. The flow proposes a systematic approach addressing various aspects of the formal verification. First, the design implementation (RTL) is analyzed for its formal friendliness based on several predefined criteria. Next, a property automation flow is adapted for an efficient property development. Later, a series of verification tasks, grouped into formal test plan and formal execution plan are carried out to reach the formal sign-off stage. To demonstrate the applicability and effectiveness of the methodology, the proposed flow has been successfully applied on several industrial designs. In this paper, we consider the formal verification of Error Correction Codes, generally implemented in program and data flash memory interfaces to benchmark the proposed flow. Automatic property generation flow is used to generate an optimal property set with varying abstraction levels. The property proof runtimes are drastically reduced and better coverage compared to the previous hand-written properties has been achieved. New RTL bugs and specification errors have been found that were previously missed during the simulation.

Advancements of Machine Learning (ML) in the field of computer vision have paved the way for its potential application in many other fields. Researchers and hardware domain experts are exploring possible applications of Machine Learning in optimizing many aspects of hardware development process. In this paper, we propose a novel approach for predicting the area of hardware components from specifications. The flow uses an existing RTL generation framework, for generating valid data samples that enable ML algorithms to train the learning models. The approach has been successfully employed to predict the area of real-life hardware components such as Control and Status Register (CSR) interfaces that are ubiquitous in embedded systems. With this approach we are able to predict the area with more than 98% accuracy and 600x faster than the existing methods. In addition, we are able to rank the features according to their importance in final area estimations.

In the last decade, several hardware generation languages (HGLs: chisel, metartl, spinalhdl, coreir and more) that focus on generation of RTL code have been proposed. These languages rise the level of abstraction from RTL description to RTL generation and utilize high-level languages such as Python or Scala for describing the generation intent. As a result, they are guiding the overall productivity and chip complexity on the rising trend. On the other front, pre -silicon verification is an equally important aspect of the design process and consumes more than 50% of the overall development time. As a consequence of increased chip complexity, the existing verification gap becomes wider. Therefore it neutralizes the productivity gain achieved from RTL generation or other productivity improvement techniques. In this paper, we describe a Python based generation language and framework for hardware properties in order to increase formal verification productivity. The described approach follows the model driven architecture (MDA) vision of OMG. The MDA approach includes transformations, that make the approach platform independent: Different property languages as well as different simulation and formal verification tools are supported. Applied to formal hardware verification, the approach empowers comparable productivity increase as HGLs in RTL designs. In addition, it is an ideal partner for HGLs, since it enables to generate a property set for each HGL generated RTL. The applicability of our approach for real -life industrial designs is demonstrated by generating properties for a RiscV CPU core and also for peripheral devices of a CPU system. The correctness of the generated properties are validated by verifying these designs with a formal verification tool.

Although Moore's law is slowing down, design productivity is still a big issue in semiconductor industry. Drivers are the trend to 3D integration, the addition of design goals such as ultra-low power and safety, and an increasing number of designs in IoT and automotive areas. EDA tools such as high-level synthesis cover a small design area only. Also, the impact of IP reuse is overestimated since IP integration often requires complex configuration and additional software to be developed. To continuously increase design productivity, Infineon heavily relies on an in-house automation framework that utilizes Python as language for automation and synthesis. It supports (and makes use of) classical HDSLs to describe specific design aspects. Mostly structured specification formalisms such as tables, requirements or diagrams (e.g. SysML subsets) are used. These formalisms can be seen as HDSLs with the additional benefit that they exist as a result of a specification process, i.e. need not be coded explicitly. To be able to deal with several formalisms, Infineon's automation framework follows OMG's MDA vision and utilizes meta-models e.g. for generation of infrastructure code. This work focuses on the aspect of combining DSLs, defining a formal semantic for HDSLs and using this definition to validate the correctness of the mapping of HDSLs to HDLs, an essential pillar to connect HDSLs to today's design flows.

This paper describes the Extendable Translating Instruction Set Simulator (ETISS). In addition to binary translation, ETISS features a plugin mechanism that allows to quickly include new functionality into the translation stage, the simulation loop, during accesses to the memory or whenever an interrupt is received. ETISS targets to become an advanced industrial-strength ISS with special focus on virtual prototypes (VPs) written in SystemC/TLM. In this paper, we will show examples of ETISS Plugins which include tracing tools, SystemC interfaces, closey-coupled peripherals or triggers for fault injection. A major drawback of developing a new binary translator such as ETISS is its lack of support for a variety of instruction set architectures (ISAs). At the moment ETISS supports the open-source OpenRISC orlk and partly RISC-V ISAs. Yet, in order to overcome this problem, we developed a toolchain to generate the binary translation stage for different ISAs following the MDA concept based on meta-modeling and code generation. It is planned to make ETISS available as an open-source tool to the research community.