Publication
Identification of ISA-Level Mutation-Classes for Qualification of RISC-V Formal Verification
Milan Funck; Sallar Ahmadi-Pour; Vladimir Herdt; Rolf Drechsler
In: FDL. Forum on Specification & Design Languages (FDL-2023), September 12-15, Turin, Italy, IEEE, 2023.
Abstract
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-V ISA. 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 opensource
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.