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

Visa enkel post
dc.contributor.authorJonsson, Jonathan
dc.contributor.authorToselli, Matteo
dc.contributor.departmentChalmers tekniska högskola / Institutionen för data och informationstekniksv
dc.contributor.departmentChalmers University of Technology / Department of Computer Science and Engineeringen
dc.contributor.examinerPeterson, Lena
dc.contributor.supervisorLarsson-Edefors, Per
dc.date.accessioned2022-11-30T12:53:32Z
dc.date.available2022-11-30T12:53:32Z
dc.date.issued2022
dc.date.submitted2020
dc.description.abstractThe 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.
dc.identifier.coursecodeDATX05
dc.identifier.urihttps://odr.chalmers.se/handle/20.500.12380/305849
dc.language.isoeng
dc.setspec.uppsokTechnology
dc.subjectRISC-V
dc.subjectNOEL-V
dc.subjectRISCV-DV
dc.subjectFormal Verification
dc.subjectRTL
dc.subjectISA
dc.subjectISS
dc.subjectJasperGold
dc.subjectPhysical Memory Protection (PMP)
dc.subjectSystemVerilog Directives
dc.titleWhite-box Verification of a RISC-V Processor: NOEL-V
dc.type.degreeExamensarbete för masterexamensv
dc.type.degreeMaster's Thesisen
dc.type.uppsokH
local.programmeEmbedded electronic system design (MPEES), MSc
Ladda ner
Original bundle
Visar 1 - 1 av 1
Bild (thumbnail)
Namn:
CSE 22-78 Jonsson Toselli.pdf
Storlek:
1.52 MB
Format:
Adobe Portable Document Format
Beskrivning:
Ladda ner
License bundle
Visar 1 - 1 av 1
Bild (thumbnail)
Namn:
license.txt
Storlek:
1.64 KB
Format:
Item-specific license agreed upon to submission
Beskrivning:
Ladda ner
Samling
Examensarbeten för masterexamen