MBMV 2023 – Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen
All proceedings of this conference

How We Learned to StopWorrying and Build a RISC-V VP with only one Microcode Instruction

Conference: MBMV 2023 – Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen - 26. Workshop
03/23/2023 - 03/24/2023 at Freiburg

Proceedings: ITG-Fb. 309: MBMV 2023

Pages: 3Language: englishTyp: PDF

Authors:
Klemmer, Lucas; Gurtner, Sonja; Grosse, Daniel (Institute for Complex Systems, Johannes Kepler Universität Linz, Österreich)

Abstract:
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.