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.


Statcounter W3C Validator Last updated on 26 October 2016. Come back to main page.