How We Learned to StopWorrying and Build a RISC-V VP with only one Microcode Instruction
Konferenz: MBMV 2023 – Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen - 26. Workshop
23.03.2023-24.03.2023 in Freiburg
Tagungsband: ITG-Fb. 309: MBMV 2023
Seiten: 3Sprache: EnglischTyp: PDF
Autoren:
Klemmer, Lucas; Gurtner, Sonja; Grosse, Daniel (Institute for Complex Systems, Johannes Kepler Universität Linz, Österreich)
Inhalt:
In this extended abstract we present Goldcrest-VP a Virtual Prototype (VP) which serves as an exploration platform for microcoded RISC-V cores leveraging the One Instruction Set Computer (OISC) principle. Furthermore, we introduce a formal verification framework for the microcode procedures. Using Goldcrest-VP, we developed SUBLEQ microcode that is fully RISC-V RV32I compliant. We were able to uncover several bugs in the microcode using our formal verification framework.