White-box Verification of a RISC-V Processor: NOEL-V

Abstract

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.