Français Anglais
Accueil Annuaire Plan du site
Accueil > Evenements > Séminaires
Séminaire d'équipe(s)
Generating the SH4 Model with CompCert
Frederic Tuong, IRT SystemX

16 May 2013, 15h30 - 16 May 2013, 18h30
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 :
Séminaires
Programming computing media (reporté)
Combinatoire
Friday 18 September 2020 - 14h30
Salle : 445 - PCRI-N
Frédéric Gruau .............................................

forum-dev Continuous Integration
Friday 05 June 2020 - 10h00
Salle : 0 - 650
Erik Bray .............................................

Large-scale Spectral Clustering for GPU-based Plat
Calcul à haute performance
Tuesday 24 March 2020 - 10h30
Salle : 465 - PCRI-N
Guanlin He .............................................

Recherche Opérationnelle à Google
Optimisation combinatoire et stochastique
Thursday 12 March 2020 - 14h30
Salle : 445 - PCRI-N
Laurent Perron .............................................

Forum dev-LRI
Wednesday 05 February 2020 - 14h00
Salle : 455 - PCRI-N
Erik Bray .............................................