Lucas Klemmer, Sonja Gurtner, Daniel Große,
"How we learned to stop worrying and build a RISC-V VP with only one microcode instruction"
: ITG/GI/GMM-Workshop Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV), 2023
Original Titel:
How we learned to stop worrying and build a RISC-V VP with only one microcode instruction
Sprache des Titels:
Englisch
Original Buchtitel:
ITG/GI/GMM-Workshop Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV)
Original Kurzfassung:
In this extended abstract, summarizing[1]and[2], 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-VRV32I compliant. We were able to uncover several bugs in the microcode using our formal verification framework.
Forschungs-