Identification of ISA-Level Mutation-Classes for Qualification of RISC-V Formal Verification

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.