White-box Verification of a RISC-V Processor: NOEL-V
Typ
Examensarbete för masterexamen
Master's Thesis
Master's Thesis
Program
Embedded electronic system design (MPEES), MSc
Publicerad
2022
Författare
Jonsson, Jonathan
Toselli, Matteo
Modellbyggare
Tidskriftstitel
ISSN
Volymtitel
Utgivare
Sammanfattning
The NOEL-V processor, based on the RISC-V ISA, targets space applications and safety-critical applications. The design has gone through verification since its early development stages. However, this verification has mostly consisted of broader software-level tests. Therefore, to extend the verification effort, Google’s RISCV-DV framework is applied. Furthermore, formal verification is performed on the physical memory protection (PMP) unit, which is used to divide user-level code and privileged code at the hardware level. RISCV-DV was able to expose one decode issue and one configuration issue. Formal verification found corner cases that could expose privileged regions to non-privileged accesses. While the bugs uncovered with RISCV-DV were non-critical, unintentional exposure of safety-critical memory regions to user-level code, containing for example encryption keys, can lead to severe consequences. In addition, since different bugs were found using different methods, this shows that RISCV-DV alone could not uncover all issues related to PMP. Hence, it is also likely that not all issues related to other units are uncovered. Therefore, multiple approaches and multiple engineers are necessary to reach a thorough verification effort.
Beskrivning
Ämne/nyckelord
RISC-V , NOEL-V , RISCV-DV , Formal Verification , RTL , ISA , ISS , JasperGold , Physical Memory Protection (PMP) , SystemVerilog Directives