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.

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.

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.

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.

For IoT devices the demand in faster execution and at the same time lower energy consumption is a pressing problem. A very promising solution are Application-Specific Instruction-set Processors (ASIPs). They make use of custom instructions, which are added to the processor, forming the Instruction-Set Extension (ISE) of a given Instruction Set Architecture (ISA). While the selection process for the ISE is already challenging, an incorrect ISE specification leads to severe problems: errors and security vulnerabilities go undetected in the first formalization and in the worst case show up ultimately in the final implementation. In this paper, we propose an early verification approach for ISE specifications. Our novel approach is based on two ingredients: (i) Virtual Prototypes (VPs) to enable a rapid creation of an executable specification for the ISE; and (ii) Deep Reinforcement Learning (DRL) to search for ISE programs which violate the ISE specification intent. As case study we consider extensions of the RISC-V base ISA. We demonstrate the effectiveness of our approach for finding functional bugs in the executable specification of the ISE as well as specification gaps in the ISE leading to information leakage.

High-level Synthesis (HLS) is being increasingly adopted as a mean to raise design productivity. HLS designs, which can be automatically translated into RTL, are typically written in SystemC at a more abstract level. Hardware Trojan attacks and countermeasures, while well-known and well-researched for RTL and below, have been only recently considered for HLS. The paper makes a contribution to this emerging research area by proposing a novel detection approach for Hardware Trojans in SystemC HLS designs. The proposed approach is based on coverage-guided fuzzing, a new promising idea from software (security) testing research. The efficiency of the approach in identifying stealthy behavior is demonstrated on a set of open-source benchmarks.