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
Resilient PDE solving approaches for exascale comp
Calcul à haute performance
Tuesday 29 May 2018 - 10h30
Salle : 465 - PCRI-N
Paul Mycek .............................................

Binary pattern of length greater than 14 are abeli
Combinatoire
Friday 25 May 2018 - 14h30
Salle : 445 - PCRI-N
Matthieu Rosenfeld .............................................

TBA
Algorithmique distribuée
Wednesday 02 May 2018 - 10h30
Salle : 465 - PCRI-N
Evangelos Bampas .............................................

Mariage stable auto-stabilisant et distribué
Théorie des graphes
Friday 13 April 2018 - 14h30
Salle : 445 - PCRI-N
Marie Laveau .............................................

Modélisation et implémentation du produit de matri
Calcul à haute performance
Wednesday 11 April 2018 - 10h30
Salle : 465 - PCRI-N
Thomas Lambert .............................................