Computer Engineering Cider Seminars

Instruction set simulators can be used for the early development and testing of software for a processor before it is manufactured. While gatelevel simulation of the overall design offers cycle-accurate 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 comparable to custom state-of-the-art simulators.

Ulrich Kühne studied computer science at the University of Bremen, Germany, where he received his Diploma in 2006. Since then, he is with Rolf Drechsler in the Group for Computer Architecture in Bremen as a PhD student. His research interests include decision procedures, model checking and formal verification methodology. At this time, he is just about to graduate.