Formal hardware verification (hardware model checking) can prove that a design has a specified property. Historically only very simple properties in simple designs have been provable this way, but improvements in model checkers over the last decade enable us to prove very complex design properties nowadays. riscv-formal is a framework for formally verifying RISC-V processors directly against a formal ISA specification. In this presentation I will discuss how the complex task of verifying a processor against the ISA specification is broken down into smaller verification problems, and other techniques that I employed to successfully implement riscv-formal.
Formal hardware verification (hardware model checking) can prove that a design has a specified property. This is different from simulation, which can only demonstrate that a property holds for some concrete traces (sets of inputs). Historically only very simple properties in simple designs have been provable this way, but improvements in model checkers over the last decade enable us to prove very complex design properties nowadays. riscv-formal is a framework for formally verifying RISC-V processors directly against a formal ISA specification. (The ISA specification used in riscv-formal is itself formally verified against Spike , the official RISC-V simulator and "golden reference" implementation.) riscv-formal can be made to work with any existing processor design, all that is needed is to add an additional RVFI (RISC-V formal interface) trace port to the core. riscv-formal by default uses the open source SymbiYosys toolchain to perform the formal proofs, but it should be compatible with all major HDL formal verification flows. In this presentation I will discuss how the complex task of verifying a processor against the ISA specification is broken down into smaller verification problems in riscv-formal, how to implement RVFI, how integrate a core with riscv-formal, and what kind of bugs can be detected using our method. Most of the proofs performed by riscv-formal are bounded proofs, i.e. it is only proven that the properties hold for the first N cycles after reset. But with a sufficiently large N we can create high confidence that in fact all relevant states can be reached within the bound of the proof and that therefore the bounded case is a sufficient proxy for the more general unbounded case. Abstractions, cut-points, and blackboxing can further help extend the effective bound of the proof. The presentation also touches on those techniques.
Speakers: Claire Wolf