Trimmed abstract: “This thesis introduces the work of certifying a part of a C/C++ program called SimSoC (Simulation of System on Chip), which simulates the behavior of architectures based on a processor such as ARM, PowerPC, MIPS or SH4… to shorten the development and test phases…offers a realistic simulation speed (about 100 Millions of instructions per second per individual core. SimSoC is a complex software, including about 60,000 lines of C++ code, many complex features from SystemC library, and optimizations to achieve high simulation speed. The subset of SimSoC dedicated to the ARM processor, one of the most popular processor design, somehow translates in C++ the contents of the ARM reference manual, which is 1138 pages long. Mistakes are then unavoidable for such a complex application.

…we aim at proving a significant part of the correctness of SimSoC in order to support the claim that the implementation of the simulator and the real system will exhibit the same behavior. We focused our efforts on a critical part of SimSoC : the instruction set simulator of the ARMv6 architecture… axiomatic semantics (typically, Hoare logic) are the most popular for proving the correctness of imperative programs. However, we prefered to try a less usual but more direct approach, based on operational semantics : this was made possible in theory since the development of an operational semantics for the C language formalized in Coq in the CompCert project… We provide a formalized representation of the ARM instruction set and addressing modes in Coq, using an automatic code generator from the instruction pseudo-code in the ARM reference manual. We also generate a Coq representation of a corresponding simulator in C, called Simlight, using the abstract syntax defined in CompCert.

From these two Coq representations, we can then state and prove the correctness of Simlight, using the operational semantics of C provided by CompCert. Currently, proofs are available for at least one instruction in each category of the ARM instruction set. During this work, we improved the technology available in Coq for performing inversions, a kind of proof steps which heavily occurs in our setting.”

Since it depends on SimSoC, here’s its paper and what looks like its code.