A Formally Verified Reduction of the RV32I ISA

Some of the applications of processors, e.g. micro-controllers, require that processors can be built with an increasingly smaller area footprint. This is usually done by reducing the number of instructions in an Instruction Set Architecture (ISA), usually in a trade-off for performance. In this work, we explore whether redundancies exist within the RISC-V RV32I ISA and how they can be eliminated in order to reduce the number of instructions. Specifically, we replace many of the provided base instructions with sequences of the instruction SUB. Finally, since correct functionality is essential in processors, we formally verify the correctness of our replaced instructions. For this purpose, we develop an interpreter in the Rosette framework, and verify the equivalence of the original and replaced instructions using SMT solvers. We finish this work with a performance study to evaluate and compare different SMT solvers.