Minimally Invasive Generation of RISC-V Instruction Set Simulators from Formal ISA Models

The development process for new embedded systems relies increasingly on simulation, e.g. to develop hardware and software components in parallel using virtual prototyping. The central component of a virtual prototype is the instruction set simulator (ISS) which implements instruction execution for a specific instruction set architecture (ISA). To avoid erroneous behavior during software simulation, it is paramount to ensure that the provided ISS implements the ISA exactly as specified, i.e. that there are no discrepancies between the hardware and the VP. In order to increase confidence in the correctness of the VP's ISS, it is advantageous to generate it automatically from a formal model of the ISA instead of implementing it manually. While a variety of formal ISA models have been proposed in prior work, they are presently not widely used in the VP domain. We attempt to ease employment of formal models for ISS generation in this domain. To this end, we reduce the integration effort through a simulator-agnostic ISS generation approach that integrates well with existing simulators and existing vendor-supplied VP components. Our approach leverages a formal RISC-V ISA model which exclusively describes instruction semantics and abstracts interactions with hardware components through an interface model, thus encapsulating interactions with simulator-specific code. As part of our experiments, we were able to generate an ISS for the popular RISC-V implementations Spike and RISC-V VP, thereby replacing their manually written implementations. Performed benchmarks indicate that the generated ISS offers the same simulation performance as a manually written one, while still passing the official RISC-V tests.