How we learned to stop worrying and build a RISC-V VP with only one microcode instruction
Sprache des Vortragstitels:
Englisch
Original Tagungtitel:
ITG/GI/GMM-Workshop Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV)
Sprache des Tagungstitel:
Englisch
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-