Title: Adopts ISA-Formal On High-End Out-Of-Order Execute RISC-V Cores

Speaker: Yu-Tse Huang, Andes

This session will be presented in Mandarin

This paper presents a formal verification approach: utilizing ISA-Formal techniques to verify a commercial RISC-V out-of-order (OOO) CPU pipeline.
We reveal three major steps to provide convincing results.
1. A reusable ISA model generated from Sail RISC-V.
2. A pipeline follower to collect information from design.
3. An universal assertion to make sure the RTL produces the same result as predicted.
First, we demostrate the steps of using Sail RISC-V formal model with custom codes (e.g., RAM read and write functions) to create reusable instruction models. Secondly, we leverage the reorder buffer (ROB) structure to create a CPU pipeline follower to extract essential information, such as general purpose registers (GPRs) states, and system control state registers (CSRs). Finally, we describe the implementation of the one-cycle assertion model to setup the ISA formal check. We adopt the ISA formal approach proposed by Alastair Reid and etc. [1], on a high-end OOO CPU design. The result not only shows the capability of formal verification but also highlights the importance of a strong formal model for RISC-V ecosystem. In this paper, we demonstrate a design bug, which was found immediately by adding new CSRs to the Sail model, proves the power and effectiveness of this solution.