Generating an efficient instruction set simulator from a complete property suite

Instruction set simulators can be used for the early development and testing of software for a processor before it is manufactured. While gate-level simulation offers cycleaccurate results, performance of the simulation is typically not sufficient for in-depth software testing. In addition, such a gate-level simulation cannot be carried out in the early phases of the design process when only the instruction set architecture (ISA) is present and the design is not yet complete. Therefore, more abstract simulators are based on the ISA; these simulators can achieve a performance of several million instructions per second. However, by introducing a simulator separate from the design, the ISA has to be re-implemented for the simulator. Therefore, there is a risk that the instruction set simulator is not in sync with the design or the ISA. We present an approach to automatically generate an instruction set simulator from a complete property suite, which can be used for the formal verification of the processor. In this way, we obtain a provably correct simulator with relatively small effort. We show the feasibility of the approach for an industrial design; the performance of the resulting simulator is shown to be comparable to custom state-of-the-art simulators.