• core
• formal verification
• JasperGold
• processor
• RISC-V
• RVFI
• verification
• Yosyshq

The RISC-V instruction set architecture has gained significant attention in recent years due to its open-source nature and potential to revolutionize the processor industry. RISC-V is designed to be simple, modular, and extensible, allowing for flexibility in implementation and customization for specific applications.
However, the verification of RISC-V processors remains a critical challenge
due to the complexity of the ISA and the need for rigorous testing to ensure correctness and reliability.
Formal verification is a promising approach to address the challenge of RISC-V cores verification, as it provides rigorous mathematical proof of correctness that can guarantee the absence of bugs and errors in the design.
Within the many initiatives of the RISC-V ecosystem, the RISC-V Formal framework by YosysHQ allows to apply formal verification to a RISC-V core.
RISC-V Formal contains a set of checkers and models for the various instructions of the base ISA and some extensions, as well as the specification of the RISC-V Formal Interface (RVFI) which must be implemented by a core to interface with RISC-V Formal.
In this thesis work, the RVFI was implemented on the STRiVe2.4 core designed by STMicroelectronics, to enable formal verification of this RISC-V processor.
The implementation phase was followed by the integration in the verification flow, using JasperGold - the Cadence formal verification tool - to apply the formal checks to the core, and providing some scripts to make formal analysis easy to use and available for every member of the team.
The results obtained in this work demonstrate the potential of formal verification in bug hunting and trace the path for several possible developments.