Formal Verification of SUBLEQ Microcode implementing the RV32I ISA

The open and royalty free nature as well as the extendable design of the RISC-V Instruction Set Architecture (ISA) has lead to a sprawling ecosystem of RISC-V software and hardware. One of the domains explored by the RISC-V community are processors with minimal area footprints. To reduce the area footprint to the minimum, typically performance is traded for a much more compact design. A promising approach to realizing very small RISC-V processors is to base them on a single instruction, such as SUBLEQ, and using a microcode layer. However, the minimalism of SUBLEQ makes writing correct microcode procedures challenging. In this paper, we target the formal verification of SUBLEQ microcode procedures. We present our verification framework and show that we can handle complex SUBLEQ procedures in practical times. In our experiments we consider a set of SUBLEQ procedures which implements the RV32I ISA and passes all official RISC-V compliance tests. However, based on our approach we found 9 intricate bugs in the SUBLEQ procedures.