We propose to leverage state-of-the-art symbolic execution techniques from the Software (SW) domain for processor verification at the Register-Transfer Level (RTL). In particular, we utilize an Instruction Set Simulator (ISS) as a reference model and integrate it with the RTL processor under test in a co-simulation setting. We then leverage the symbolic execution engine KLEE to perform a symbolic exploration that searches for functional mismatches between the ISS and RTL processor. To ensure a comprehensive verification process, symbolic values are used to represent the instructions and also to initialize the register values of the ISS and processor. As a case study, we present results on the verification of the open source RISC-V based MicroRV32 processor, using the ISS of the open source RISC-V VP as a reference model. Our results demonstrate that modern symbolic execution techniques are applicable to a full scale processor cosimulation in the embedded domain and are very effective in finding bugs in the RTL core.

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.

IoT devices offer insufficient protections against exploitation of critical programming errors (such as buffer overflows) it is therefore paramount to sufficiently test IoT software before deployment. A central source of these errors is the implementations of stateful network protocols used in the IoT (e.g., MQTT-SN). Unfortunately, comprehensive automated testing of such protocol implementations is challenging due to their large state space. Furthermore, prior work on automated testing of protocol implementations focuses on conventional desktop systems and does thus not address challenges specific to the IoT domain (e.g., handling of peripheral interactions). In this publication, we leverage symbolic execution (an automated software testing technique) for testing stateful network protocol implementation in the IoT domain. To mitigate issues regarding the state-space explosion, we propose a novel symbolic execution approach which is based on created protocol state and message format specifications and specifically tailored to the IoT domain. We employ our specification-based symbolic execution approach to test protocol implementations provided by two popular IoT operating systems. Our experiments indicate that a significant increase in code coverage can be achieved using our automated software testing approach. We were further able to discover three critical and previously unknown bugs in network protocol implementations provided by the RIOT operating system.

Software written for constrained devices, commonly used in the Internet of Things (IoT), is primarily written in C and thus subject to vulnerabilities caused by the lack of memory safety (e.g. buffer overflows). To prevent these vulnerabilities, we present a systematic approach for finding spatial memory safety violations in low-level code for constrained embedded devices. We propose implementing this approach using SystemC-based Virtual Prototypes (VPs) and illustrate an architecture for a non-intrusive integration into an existing VP. To the best of our knowledge, this approach is novel as it is the first for finding spatial memory safety violations which addresses challenges spe-cific to constrained devices. Namely, limited computing resources and utilization of custom hardware peripherals. We evaluate our approach by applying it to the IoT operating system RIOT where we discovered seven previously unknown spatial memory safety violations in the network stack of the operating system.

In this paper we propose an effective approach for verification of real-world SystemC TLM peripherals using modern C++ symbolic execution tools. We designed a lightweight SystemC peripheral kernel that enables an efficient integration with the modern symbolic execution engine KLEE and acts as a drop-in replacement for the normal SystemC kernel on pre-processed TLM peripherals. The pre-processing step essentially replaces context switches in SystemC threads with normal function calls which can be handled by KLEE. Our experiments, using a publicly available RISC-V specific interrupt controller, demonstrate the scalability and bug hunting effectiveness of our approach.

We propose a novel cross-level verification approach for processor verification at the Register-Transfer Level (RTL). The foundation is a randomized coverage-guided instruction stream generator that produces one endless and unrestricted instruction stream that evolves dynamically at runtime. We lever-age an Instruction Set Simulator (ISS) as a reference model in a tight co-simulation setting. Coverage information is continuously updated based on the execution state of the ISS and we employ Coverage-guided Aging to smooth out the coverage distribution of the randomized instruction stream over the time. In combination, this enables a broad and deep coverage to find intricate corner-case bugs in the RTL processor. Our case study with an industrial pipelined 32 bit RISC- V processor demonstrate the effectiveness of our approach.

This paper introduces the project Scale4Edge. The project is focused on enabling an effective RISC-V ecosystem for optimization of edge applications. We describe the basic components of this ecosystem and introduce the envisioned demonstrators, which will be used in their evaluation.

RISC-V is a modern open source Instruction Set Architecture (ISA) and designed in a very extendable manner, which allows for highly application specific solutions. However, the identification of suitable instruction set extensions usually requires a significant manual effort and therefore is a very challenging process. In this paper we propose a lightweight alternative methodology to find suitable application-specific RISC-V extensions, using a Virtual Prototype (VP). This is done, purely by observing the used instructions during the execution of the targeted application on the VP. Therefore, no further information about the application itself are needed. In this context the advantages and the flexibility of a VP and the straightforward extendability of the RISC-V ISA are demonstrated.

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.

Coverage-guided Fuzzing (CGF) has been shown to be a very effective verification technique in the Software (SW) domain. However, the application of CGF in the embedded system domain is much more limited so far. Beside the necessary integration effort of the fuzzing engine, a main limiting factor is the employed coverage metric to guide the CGF process. Since embedded systems integrate Hardware (HW) and SW parts, the coverage metric should reflect both parts instead of reasoning exclusively about the SW execution in the CGF process.Therefore, in this paper, we propose a novel unified HW/SW coverage metric to boost state-of-the-art CGF for HW/SW co-verification. Following the modern design flow for embedded systems, we leverage a Virtual Prototype (VP) to represent the HW part. We designed effective representations of the unified HW/SW coverage to capture all relevant coverage information at run time in the VP and tailored it for integration with a modern CGF process. Our RISC-V experiments demonstrate the practical applicability of our proposed approach. Our proposed unified HW/SW coverage can be effectively managed at runtime and enables to reach deeper bugs compared to existing state-of-the-art CGF.

The demand for AI and specifically machine learning functionality on edge devices (TinyML) is growing. TinyML faces several unique challenges, one of them being the requirement of having a lower memory footprint for storage and inference of neural networks.In this paper, we propose and evaluate an approach to make Convolutional Neural Networks (CNNs) with higher memory footprint executable on edge devices. The idea is to combine flash memory with a cached access for the inference of CNNs. In order to evaluate the effectiveness of our proposed memory architecture by measuring the cache hitrate at the system level, we build a Virtual Prototype (VP) with a dedicated flash device and an exclusive cache. We are using Tensorflow Lite Micro (TFLM) for the network inference and mapping all model data and runtime buffers into the cache enhanced flash memory. Multiple experiments with several cache configurations show that a small cache of around 1 KB is able to achieve very high hitrates over 99%. Additionally, the experimental results show that the memory planning of TFLM supports the usage of caching because most memory accesses are adjacent.

Symbolic execution is a powerful software testing technique for finding bugs in complex software. Unfortunately, following the symbolic execution and understanding its results is challenging. However, since symbolic execution is commonly not complete (i.e. due to path explosion) it is important to understand the limitations of the performed analysis. Otherwise, insufficiently tested code parts may not be identified and bugs remain unnoticed. Prior work attempts to address this problem via 2D visualizations which communicate properties of the performed analysis to the verification engineer. Since symbolic execution requires a visualization of several properties, such 2D visualizations often lack important information or end up being dense and difficult to understand.In order to overcome this limitation, we propose a novel 3D visualization of symbolic execution which allows visualizing additional properties via the third dimension. For this purpose, we have implemented a 3D visualization for the symbolic execution of RISC-V machine code and evaluate this implementation by comparing it to an existing 2D visualization. Our results demonstrate that the third dimension allows us to include additional information which is not captured by the existing 2D visualization. In order to stimulate further research on 3D visualization of symbolic execution, we have released our implementation as open source software.

In this paper, we propose a novel simulation-based cross-level approach for processor verification at the Register-Transfer Level (RTL). We leverage state-of-the-art coverage-guided fuzzing techniques from the software domain to generate processor-level input stimuli. An Instruction Set Simulator (ISS) is utilized as a reference model for the RTL processor under test in an efficient co-simulation setting. To further boost the fuzzing effectiveness, we devised custom mutation procedures tailored for the processor verification domain. Our experiments using the popular open-source RISC-V based VexRiscv processor demonstrate the effectiveness of our approach in finding intricate bugs at the processor level.

RISC-V is a modern Instruction Set Architecture (ISA) that by its open nature in combination with a clean and modular design has enormous potential to become a game changer in the Internet of Things (IoT) era. Recently, SystemC-based Virtual Prototypes (VPs) have been introduced into the RISC-V ecosystem to lay the foundation for advanced industry-proven system-level use-cases. However, a VP-driven environment modeling and interaction has been mostly neglected in the RISC-V context.

Abstract Virtual prototypes (VPs) are crucial in today’s design flow. VPs are predominantly created in SystemC transaction-level modeling (TLM) and are leveraged for early software development and other system-level use cases. Recently, virtual prototyping has been introduced for the emerging RISC-V instruction set architecture (ISA) and become an important piece of the growing RISC-V ecosystem. In this paper, we present enhanced virtual prototyping solutions tailored for RISC-V. The foundation is an advanced open source RISC-V VP implemented in SystemC TLM and designed as a configurable and extensible platform. It scales from small bare-metal systems to large multi-core systems that run applications on top of the Linux operating system. Based on the RISC-V VP, this paper also discusses advanced VP-based verification approaches and open challenges. In combination, we provide for the first time an integrated and unified overview and perspective on advanced virtual prototyping for RISC-V.

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.

Constrained Internet of Things (IoT) devices with limited computing resource are increasingly employed in security critical areas. Therefore, it is important for the firmware of these devices to be tested sufficiently. On non-constrained conventional devices, dynamic testing techniques (e.g. fuzzing, symbolic execution, or concolic testing) are successfully utilized to discover critical bugs in tested software. Unfortunately, the diverse ecosystem and the dependence on low-level details of a wide range of peripherals makes it difficult to use these techniques in the IoT context. In order to address these challenges, we present SymEx-VP an open source emulation-based approach for concolic testing of IoT firmware. SymEx-VP is a virtual prototype for RISC-V hardware platforms and allows concolic testing of RISC-V machine code. To support a wide range of different peripherals, SymEx-VP utilizes SystemC, a hardware modeling language for C++. By employing a SystemC extension mechanism, SymEx-VP can inject concolic inputs into the emulated firmware through the memory-mapped I/O peripheral interface of existing SystemC peripheral models. This allows us to support different operating systems and libraries used in the IoT with minimal integration effort. We provide an extensive description of SymEx-VP, illustrate peripheral modeling and firmware testing using it by example, and perform tests with four operating systems to demonstrate the advantages of our OS-agnostic firmware testing method.

Compliance testing for RISC-V is very important. Essentially, it ensures that compatibility is maintained between RISC-V implementations and the ever growing RISC-V ecosystem. Therefore, an official Compliance Test-suite (CT) is being actively developed. However, it is very difficult to achieve that all relevant functional behavior is comprehensively tested.

In this paper we propose to combine the safe C dialect Checked C with concolic testing to obtain an effective methodology for attaining safer C code. Checked C is a modern and backward compatible extension to the C programming language which provides facilities for writing memory-safe C code. We utilize incremental conversions of unsafe C software to Checked C. After each increment, we leverage concolic testing, an effective test generation technique, to support the conversion process by searching for newly introduced and existing bugs.Our RISC-V experiments using the RIOT Operating System (OS) demonstrate the effectiveness of our approach. We uncovered 4 previously unknown bugs and 3 bugs accidentally introduced through our conversion process.

With the advent of 5G and IoT applications, there is a greater thrust in terms of hardware security due to imminent risks caused by high amount of intercommunication between various subsystems. Security gaps in integrated circuits, thus represent high risks for both-the manufacturers and the users of electronic systems. Particularly in the domain of Intellectual Property (IP) protection, there is an urgent need to devise security measures at all levels of abstraction so that we can be one step ahead of any kind of adversarial attacks. This work presents IP protection measures from multiple perspectives-from system-level down to device-level security measures, from discussing various attack methods such as reverse engineering and hardware Trojan insertions to proposing new-age protection measures such as multi-valued logic locking and secure information flow tracking. This special session will give a holistic overview at the current state-of-the-art measures and how well we are prepared for the next generation circuits and systems.

We propose an effective methodology for integrating Concolic Testing (CT) with SystemC-based Virtual Prototypes (VPs) for verification of embedded SW binaries. Our methodology involves three steps: 1) integrating CT support with the Instruction Set Simulator (ISS) of the VP, 2) utilizing the standard TLM-2.0 extension mechanism for transporting concolic values alongside generic TLM transactions, and 3) providing lightweight concolic overlays for SystemC-based peripherals that enable non-intrusive CT support for peripherals and thus significantly reduce the CT integration effort. Our RISC-V experiments using the RIOT operating system demonstrate the effectiveness of our approach.

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.

Constrained IoT devices with limited computing resources are on the rise. They utilize low-end multithreaded operating systems (e.g. RIOT) where each thread is assigned a fixed stack size during the development process. In this regard, it is important to choose an appropriate stack size which does not cause stack overflows and at the same time does not waste scarce memory resources by overestimating the required thread stack size. In this paper we propose an in-vivo technique for stack overflow detection and stack size estimation that leverages Virtual Prototypes (VPs) and is specifically tailored for low-end multithreaded IoT operating systems. We focus on SystemC-based VPs which operate on the TLM abstraction level. VPs are an industrial proven modeling standard to enable early software development and testing. We propose a non-intrusive extension for existing VPs which allows detecting stack overflows and provides a stack size estimation, which is beneficial to a VP-based development process. Our analysis works in-vivo, hence no modification of the executed software binary is required between testing and deployment. Our evaluation using the RIOT operating system revealed two previously unknown stack overflows in RIOT and identified potential stack size overestimation.

Metamorphic Testing (MT) has been shown to be a very effective technique in the Software (SW) domain. MT does not require a reference model to compare against for testing but instead relies on Metamorphic Relations (MR) to derive the expected result from relationships between several calls to the function under test. An example of an MR is the expectation that the sum of an arbitrary list of integers remain unchanged regardless of it being sorted or reversed. Thus, a key requirement for applying MT effectively is availability of MRs specific to the domain at hand. In this paper, we propose MT to the domain of processor verification. As a case study, we consider the RISC-V Instruction Set Architecture (ISA) and provide MRs tailored for RISC-V For evaluation purposes, we propose an efficient on-the-fly MT framework that integrates the MRs with an Instruction Set Simulator (ISS). We measure the quality of those MRs by the number of mutations they kill, also referred to as mutation analysis. Our experiments demonstrate the effectiveness of the MRs to kill all mutations, which confirms our research question that MT is also a suitable technique for the domain of processor verification.

Recently, Virtual Prototypes (VPs) were introduced for the emerging RISC-V Instruction Set Architecture (ISA) and become an important part of the growing RISC-V ecosystem. A central component of the VP is the Instruction Set Simulator (ISS). VPs should provide a high simulation performance and at the same time yield accurate results, which are two conflicting requirements. To tackle this problem, we present an efficient VP-based adaptive simulation that is tailored for the RISC-V ISA and allows to seamlessly switch the accuracy setting in the ISS at runtime. This enables to selectively simulate the application as fast as possible and as accurate as necessary. In this paper we focus on the performance impact of different accuracy settings and leave the evaluation of accuracy results for future work. Our RISC-V experiments, using bare-metal and operating system based benchmarks, demonstrate that up-to 543x speed-up is possible with a JIT-based setting in the ISS.

Compliance testing for RISC-V is very important. Therefore, an official hand-written compliance test-suite is being actively developed. However, besides requiring significant manual effort, it focuses on positive testing (the implemented instructions work as expected) only and neglects negative testing (consider illegal instructions to also ensure that no additional/unexpected behavior is accidentally added). This leaves a large gap in compliance testing. In this paper we propose a fuzzing-based test-suite generation approach to close this gap. We found new bugs in several RISC-V simulators including riscvOVPsim from Imperas which is the official reference simulator for compliance testing.

Avoiding security vulnerabilities is very important for embedded systems. Dynamic Information Flow Tracking (DIFT) is a powerful technique to analyze SW with respect to security policies in order to protect the system against a broad range of security related exploits. However, existing DIFT approaches either do not exist for Virtual Prototypes (VPs) or fail to model complex hardware/software interactions.In this paper, we present a novel approach that enables early and accurate DIFT of binaries targeting embedded systems with custom peripherals. Leveraging the SystemC framework, our DIFT engine tracks accurate data flow information alongside the program execution to detect violations of security policies at run-time. We demonstrate the effectiveness and applicability of our approach by extensive experiments.

RISC-V is gaining huge popularity in particular for embedded systems. Recently, a SystemC-based Virtual Prototype (VP) has been open sourced to lay the foundation for providing support for system-level use cases such as design space exploration, analysis of complex HW/SW interactions and power/timing/performance validation for RISC-V based systems.In this paper, we propose an efficient core timing model and integrate it into the VP core to enable fast and accurate performance evaluation for RISC-V based systems. As a case-study we provide a timing configuration matching the RISC-V HiFive1 board from SiFive. Our experiments demonstrate that our approach allows to obtain very accurate performance evaluation results while still retaining a high simulation performance.

Compliance testing for RISC-V is very important. Therefore, an official hand-written compliance test-suite is being actively developed. However, this requires significant manual effort in particular to achieve a high test coverage.In this paper we propose a test-suite specification mechanism in combination with a first set of instruction constraints and coverage requirements for the base RISC-V ISA. In addition, we present an automated method to generate a test-suite that satisfies the specification. Our evaluation demonstrates the effectiveness and potential of our method.

Extensive processor verification at the Register-Transfer Level (RTL) is crucial to avoid bugs. Therefore, simulation-based approaches are prevalent but they require efficient test generation methods to achieve a thorough verification. In this paper we propose an efficient cross-level testing approach for processor verification targeting the RISC- V Instruction Set Architecture (ISA). We generate an endless instruction stream without restrictions on the generated instructions by evolving the instruction stream on-the-fly during simulation. An Instruction Set Simulator (ISS) is leveraged as reference model for the RTL core under test in a tightly coupled cross-level co-simulation setting. This enables a very efficient and comprehensive testing process. As a case-study we present results on the verification of the 32 bit pipelined RISC- V core of MINRES The Good Folk (TGF) Series Our approach has been very effective in finding several serious bugs.

Extensive verification of embedded SW is very important to avoid errors and security vulnerabilities. Therefore, mainly simulation-based methods are employed that leverage Virtual Prototypes (VPs) for SW execution early in the design flow. VPs are essentially abstract models of the entire HW platform including peripherals. They are predominantly created in SystemC. However, a comprehensive simulation-based verification requires integration of sophisticated test generation techniques.

Recently, Virtual Prototypes (VPs) were introduced for the emerging RISC-V Instruction Set Architecture (ISA) and become an important part of the growing RISC-V ecosystem. A central component of the VP is the Instruction Set Simulator (ISS). VPs should provide a high performance and at the same time yield accurate results, which are conflicting requirements. To tackle this problem, we present an efficient VP-based adaptive simulation that is tailored for the RISC-VISA and allows to seamlessly switch the accuracy setting in the ISS at runtime. This enables to selectively simulate the application as fast as possible and as accurate as necessary. In this paper we focus on the performance impact of different accuracy settings and leave the evaluation of accuracy results for future work. Our RISC-V experiments demonstrate that up-to 543x speed-up is possible with a JIT-based setting in the ISS.

Virtual Prototypes (VPs) are becoming increasingly attractive for the early analysis of SoC power management, which is nowadays mostly implemented in firmware (FW). Power and timing constraints can be monitored and validated by executing a set of test-cases in a power-aware FW/VP co-simulation. In this context, cross coverage of power states is an effective but challenging quality metric. This paper proposes a novel coverage-driven approach to automatically generate test-cases maximizing this cross coverage. In particular, we integrate a coverage-loop that successively refines the generation process based on previous results. We demonstrate our approach on a LEON3-based VP.

Extensive testing of IoT SW is very important to prevent errors and security vulnerabilities. In the SW domain the automated concolic testing technique has been shown very effective.

Verification of Instruction Set Simulators (ISSs) is crucial. Predominantly simulation-based approaches are used. They require a comprehensive testset to ensure a thorough verification.We propose a novel coverage-guided fuzzing (CGF) approach to improve the testcase generation process. In addition to code coverage we integrate functional coverage and a custom mutation procedure tailored for ISS verification. As a case-study we apply our approach on a set of three publicly available RISC-V ISSs. We found several new errors, including one error in the official RISC-V reference simulator Spike.

In this paper, we propose the first approach for verifying plans of cognition-enabled autonomous robots that perform everyday manipulation activities in human environments. Our methodology is based on the new Intermediate Plan Verification Language (IPVL) which is used to represent plans, environments, and robot belief states in one joint formal model. We devise a symbolic execution engine for IPVL and show the effectiveness of our overall verification methodology in a case study.

Small embedded devices are highly specialized plat forms that integrate several peripherals alongside the CPU core. Embedded devices extensively rely on Firmware (FW) to control and access the peripherals as well as other important functionality. This poses challenges to FW development since the FW must be adapted to each specific device configuration. Besides ensuring functional correctness to avoid errors and security vulnerabilities, an important design factor today is the control and adaptivity of a system with respect to non-functional properties, like for example application-specific timing budgets. Furthermore, optimizations of the FW and HW/SW interface play a very important role due to the tight resource constraints of small embedded devices. To satisfy these requirements new FW design methods are needed targeting FW generation, FW verification and FW optimization.This paper presents such new methods to enable an early, efficient and systematic FW design taking the underlying HW architecture into account. We use the RISC-V Instruction Set Architecture (ISA) as a case study to demonstrate our methods.

Formal verification of high-level SystemC designs is an important and challenging problem. One has to deal with the full complexity of C++ to extract a suitable formal model (front-end problem) and then, with large cyclic state spaces defined by symbolic inputs and concurrent processes. This paper describes a scalable and efficient stateful symbolic simulation approach for SystemC that combines state subsumption reduction (SSR) with partial order reduction (POR) and symbolic execution (SymEx) under the SystemC simulation semantics. While the SymEx+POR combination provides basic capabilities to efficiently explore the state space, SSR prevents revisiting symbolic states and therefore makes the verification complete. The approach has been implemented on top of an intermediate verification language for SystemC to address the front-end problem. The scalability and efficiency of the implemented verifier is demonstrated using an extensive set of experiments.

An ESL design flow starts with a TLM description, which is thoroughly verified and then refined to a RTL description in subsequent steps. The properties used for TLM verification are refined alongside the TLM description to serve as starting point for RTL property checking. However, a manual transformation of properties from TLM to RTL is error prone and time consuming. Therefore, in this paper we propose a fully automated TLM-to-RTL property refinement based on a symbolic analysis of transactors. We demonstrate the applicability of our property refinement approach using a case study.

There is a growing need for error-resilient software that can tolerate hardware faults as well as for new resilience evaluation techniques. For the latter, a promising direction is to apply formal techniques in fault injection-based evaluations to improve the coverage of evaluation results. Building on the recent development of Software-implemented Fault Injection (SWiFI) techniques on compiler's intermediate code, this paper proposes a novel resilience evaluation framework combining LLVM-based SWiFI and SMT-based symbolic execution. This novel combination offers significant advantages over state-of-the-art approaches with respect to accuracy and coverage.

Internet-of-Things (IoT) opens a new world of possibilities for both personal and industrial applications. At the heart of an IoT device, the processor is the core component. Hence, as an open and free instruction set architecture RISC-V is gaining huge popularity for IoT. A large ecosystem is available around RISC-V, including various RTL implementations at one end and high-speed instruction set simulators (ISSs) at the other end. These ISSs facilitate functional verification of RTL implementations as well as early SW development to some extent. However, being designed predominantly for speed, they can hardly be extended to support further system-level use cases such as design space exploration, power/timing/performance validation or analysis of complex HW/SW interactions. In this paper, we propose and implement the first RISC-V based Virtual Prototype (VP) with the goal of filling this gap. We provide a RISC-V RV321M core, a PLIC-based interrupt controller and an essential set of peripherals together with SW debug capabilities. The VP is designed as extensible and configurable platform with a generic bus system and implemented in standard-compliant SystemC and TLM-2.0. The latter point is very important, since it allows to leverage cutting-edge SystemC-based modeling techniques needed for the mentioned use cases. Our VP allows a significantly faster simulation compared to RTL, while being more accurate than existing ISSs. Finally, our RISC-V VP is fully open source to help expanding the RISC-V ecosystem and stimulating further research and development.

Data flow testing (DFT) has been shown to be an effective testing strategy. DFT features a high fault detection rate while avoiding the intense scalability problems to achieve full path coverage. In this paper we propose to apply data flow testing for SystemC virtual prototypes (VPs). Our contribution is twofold: First, we develop a set of SystemC specific coverage criteria for data flow testing. This requires to consider the SystemC semantics of using non-preemptive thread scheduling with shared memory communication and event-based synchronization. Second, we explain how to automatically compute the data flow coverage result for a given VP using a combination of static and dynamic analysis techniques. The coverage result provides clear suggestions for the testing engineer to add new testcases in order to improve the coverage result. Our experimental results on real-world VPs demonstrate the applicability and efficacy of our analysis approach and the SystemC specific coverage criteria to improve the testsuite.

Efficient power management is very important for modern System-on-Chip to satisfy the conflicting demands on high performance and low power consumption. Nowadays, global power management is mostly implemented in firmware (FW) due to the relative ease of development and its flexibility. Recent advances in system-level power modeling and estimation open up opportunities for early validation of these FW-based power management strategies. In this paper, we propose a novel approach for this purpose using SystemC-based Virtual Prototypes (VPs) and constrained random (CR) techniques. The CR-generated representative system workloads are executed in a power-aware FW/VP co-simulation to validate that available performance and power budgets are satisfied. As a proof-of-concept, we demonstrate our power validation approach on the LEON3-based SoCRocket VP.

Security is one of the most burning issues in embedded system design nowadays. The majority of strategies to secure embedded systems are being implemented in software. However, a potential hardware backdoor that allows unprivileged software access to confidential data will render even the perfectly secure software useless. As the underlying SoC cannot be patched after deployment, it is very critical to detect and correct SoC hardware security issues in the design phase. To prevent costly fixes in later stages, security validation should start as early as possible. In this paper, we propose a novel approach to SoC security validation at the system level using Virtual Prototypes (VP). At the heart of the approach is a scalable static information flow analysis that can detect potential security breaches such as data leakage and untrusted access; confidentiality and integrity issues, respectively. We demonstrate the applicability of the approach on real-world VPs.

Electronic systems integrate an increasingly large number of components on a single chip. This leads to increased risk of faults, e.g. due to radiation, aging etc. Such a fault can lead to an observable error and failure of the system. Therefore, an error effect simulation is important to ensure the robustness and safety of these systems. Error effect simulation with Virtual Prototypes (VPs) is much faster than with RTL designs due to less modeling details at TLM. However, for the same reason, the simulation results with VP might be significantly less accurate compared to RTL. To improve the quality of a TLM error effect simulation, a fault correspondence analysis between both abstraction levels is required. This paper presents a case study on applying fault localization methods based on symbolic simulation to identify corresponding TLM errors for transient bit flips at RTL. First results for the interrupt controller of the SoCRocket VP, which is being used by the European Space Agency, demonstrate the applicability of our approach.

Ensuring the correctness of SystemC virtual prototypes is indispensable. For such models, existing symbolic simulation approaches are based on interpreting their behavior. In this paper we propose a major enhancement called Compiled Symbolic Simulation (CSS). For more scalable state space exploration, CSS augments the DUV to integrate the symbolic execution engine and the Partial Order Reduction based scheduler. Then, a standard C++ compiler is used to generate a native binary, whose execution performs exhaustive verification of the DUV. An extensive experimental evaluation demonstrates the potential of our approach.

Formal verification of high-level SystemC designs is an important and challenging problem. Recent works have proposed symbolic simulation in combination with Partial Order Reduction (POR) as a promising solution and experimentally demonstrated its potential. However, these symbolic simulation approaches have a fundamental limitation in handling cyclic state spaces. The reason is that they are based on stateless model checking and thus unable to avoid revisiting states in a cycle. In this paper, we propose a novel stateful symbolic simulation approach for SystemC. For the efficient detection of revisited symbolic states, we apply symbolic subsumption checking. Furthermore, our implementation integrates a cycle proviso to preserve the soundness of POR in the presence of cycles. We demonstrate the scalability and the efficiency of the proposed approach using an extensive set of experiments.

Formal verification of SystemC is challenging. Before dealing with symbolic inputs and the concurrency semantics, a front-end is required to translate the design to a formal model. The lack of such front-ends has hampered the development of efficient back-ends so far.