The project “Hardening the value chain through open-source, trustworthy EDA tools and processors (HEP)” uses open-source, free components and tools for the production of a prototypical security chip. A design flow using only free and open tools from the abstract description in SpinalHDL via OpenROAD down to the GDS-file for tape-out has been established, and first ASICs produced at IHP. The prototypical hardware security module (HSM) produced in this way provides, among other things, a processor based on VexRiscv, a cryptographic accelerator and masking of cryptographic keys. The open development tools used in the process were integrated into a common environment and expanded to include missing functionality. Subsequently, the whole tool chain and its peripherals are wrapped into a new Nyx container. The easy accessibility of the used process significantly reduces the learning curve for chip design. Additionally, we provide tools for formal verification and masking against side-channel attacks in our design flow. Interest in the results of project HEP has been shown in publications in which industrial partners participated, such as Elektrobit, Hensoldt Cyber, IAV, Secure-IC and Swissbit Germany.

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.

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.