RVFC: RISC-V Formal in Chisel

With the increasing complexity of hardware design requirements and the development of open-source hardware ecosystems, Chisel and RISC-V are becoming increasingly popular. As a domain-specific language of Scala, Chisel is gradually becoming the choice of hardware design development with the help of the features of high-level languages. Especially in the RISC-V open-source instruction set ecosystem, many representative projects are implemented with Chisel. In hardware development, the correctness verification of the design is essential. A promising stream for verifying the correctness of RISC-V designs is RISC-V Formal, which is at the SystemVerilog level. In this paper, we propose RVFC, a framework for formal verification of RISC-V designs at the Chisel level. It is based on the ability of ChiselFV to define formal properties and verify them at the Chisel level. We also reimplemented a textbook RISC-V five-stage pipeline design and found an oversight in the design through RVFC verification.