SimSoC-Cert: a certified simulator for systems on chip. F. Blanqui, C. Helmstetter, V. Joloboff, J.-F. Monin and X. Shi. Draft. 2010.

The design and debugging of Systems-on-Chip using a hardware implementation is difficult and requires heavy material. Simulation is an interesting alternative approach, which is both more flexible and less expensive. SimSoC is a fast instruction set simulator for various ARM, PowerPC, and RISC-based architectures. However, speed involves tricky shortcomings and design decisions, resulting in a complex software product. This makes the accuracy of the simulator a non-trivial question: there is a strong need to strengthen the confidence that simulations results match the expected accuracy. We therefore decided to certify SimSoC, that is, to formally prove in Coq the correctness of a significant part of this software. The present paper reports our first efforts in this direction, targeting the ARMv6 architecture.