The simulation of Systems-on-Chip (SoC) gains wider acceptance
in the area of embedded systems, allowing to test exhaustively the
hardware as soon as the prototyping step begins. SimSoC is a sim-
ulator firstly optimized on the CPU component (ISS), as this part is
a major bottleneck for the simulation speed. But a fast simulator is
especially profitable for the debugging activity, if beyond speed it sim-
ulates faithfully the ISS. So the SimSoC-Cert project has formalized
in Coq a model of a real CPU: the ARMv6 processor is automatically
generated from its reference manual.
However, to evaluate the scalability of this toolkit, we propose to
enhance modularly the process behind the generator so that ideally
a bundle of processors could be certified at the cost of one. In this
presentation, we generate a well typed version of the SH4 processor’s man-
ual, verified by the GCC and CompCert compilers, and we report our
experimentations of using CompCert as a generic platform for proofs
in Coq to deeply embed the resulting well typed simulator, both the
ARMv6 and SH4 ISS. As a side effect, CompCert being defined in Coq,
we develop in Coq a parsing/printing loop from Coq to Coq. Based
on a high level front-end as CompCert-C, the goal is to easily mimic the
correctness proof being established for one processor (e.g. ARMv6) to
others (e.g. SH4), and at long-term, extend the overall to prove the
correctness of a given CompCert-C program, that would moreover have
ARMv6 and SH4 as certified back-end.