**Generating the SH4 Model with CompCert**
Frederic Tuong, IRT SystemX

*16 May 2013, 15:30 - 16 May 2013, 18:30*
Salle/Bat : 465/PCRI-N

Contact :

**Activités de recherche : **
**Résumé :**
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.

*Pour en savoir plus : *