Chaos Communication Congress

End-to-end formal ISA verification of RISC-V processors with riscv-formal (34x8)

Data di messa in onda: Dic 27, 2017

Speaker: Clifford Wolf 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.