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
A Two-level Auction for Resource Allocation in Mul
Réseaux sans fil et mobiles
Friday 09 March 2018 - 14h30
Salle : 445 - PCRI-N
Mira Morcos .............................................

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

Approximate Bayesian Computation and Random Forest
Thursday 08 February 2018 - 00h00
Salle : 455 - PCRI-N
Valentin Thouzeau .............................................

A concurrent lock-free algorithm for computing a f
Combinatoire
Friday 12 January 2018 - 14h30
Salle : 445 - PCRI-N
James Mitchell .............................................

Acyclic Partitioning of Large Directed Acyclic Gra
Calcul à haute performance
Tuesday 09 January 2018 - 10h30
Salle : 465 - PCRI-N
Julien Herrmann .............................................