Doctorant f/h conception rigoureuse de circuits basée sur les méthodes formelles

Contexte et atouts du poste

Les projets du

Mission confiée

Dans un premier temps, le travail consistera à étudier HPDcache [Fug23], un cache de données L1 hautes performances compatible avec les processeurs RISC-V. HPDcache est utilisé dans l'implémentation CVA6 [ZB19] du RISC-V utilisé par plusieurs industriels (Bosch, Thales, ...). Il s'agit d'un cache hautement configurable, avec exécution dans le désordre (out-of-order) et reexécution (replay), muni d'interfaces compatibles avec AMBA AXI5 et RISC-V.

L'étude du HPDcache sera faite en construisant un modèle formel de son architecture, qui comporte un pipeline à trois étages, permettant de traiter environ 10 transactions simultanées. Plusieurs configurations seront considérées, en fonction des différentes fonctionnalités activées du HPDcache. Ce modèle formel servira de base pour vérifier des propriétés de correction (absence de livelocks et de deadlocks, respect du modèle de cohérence du processeur, etc.), pour générer des tests de conformité et pour estimer les performances du cache.

Dans un deuxième temps, le travail consistera à proposer des extensions de la méthodologie de conception des circuits avec des méthodes formelles (modélisation, vérification, test de conformité), notamment en considérant les architectures à composants communicants (chiplets). Une partie intéressante de cette méthodologie pourrait être des passerelles entre les langages de description de ces circuits et de leurs protocoles de communication sous-jacents et les langages formels utilisés pour la vérification.

Références

[Fug23] César Fuguet Tortolero. HPDcache: Open-Source High-Performance L1 Data Cache for RISC-V Cores. Proc. of the 20th ACM International Conference on Computing Frontiers (CF'2023), Bologna, Italy, pp. 377-378, ACM Press, 2023. Florian Zaruba and Luca Benini. The Cost of Application-Class Processing: Energy and Performance Analysis of a Linux-Ready 1.7-GHz 64-Bit RISC-V Core in 22-nm FDSOI Technology. IEEE Transactions on Very Large Scale Integration (VLSI) Systems 27:2629-2640, 2019. Hubert Garavel, Frédéric Lang, Radu Mateescu, and Wendelin Serwe. CADP 2011: A Toolbox for the Construction and Analysis of Distributed Processes. Springer International Journal on Software Tools for Technology Transfer (STTT) 15:89-107, 2013.

Principales activités

1. Modéliser les systèmes à étudier en utilisant les langages formels développés par CONVECS
2. Etudier différentes configurations et les analyser formellement (vérification, génération de tests, évaluation de performances)
3. Participer aux réunions de projet et à la rédaction des livrables

Compétences

Compétences techniques : connaissance des langages de spécification pour systèmes concurrents asynchrones

Langues : français requis ; bon niveau d'anglais

Relationnel : travail en équipe

Avantages

4. Restauration subventionnée
5. Transports publics remboursés partiellement
6. Congés: 7 semaines de congés annuels + 10 jours de RTT (base temps plein) + possibilité d'autorisations d'absence exceptionnelle (ex : enfants malades, déménagement)
7. Possibilité de télétravail et aménagement du temps de travail
8. Équipements professionnels à disposition (visioconférence, prêts de matériels informatiques, etc.)
9. Prestations sociales, culturelles et sportives (Association de gestion des œuvres sociales d'Inria)
10. Accès à la formation professionnelle
11. Sécurité sociale

Rémunération

12. Salaire brut : 1ère année : 2082 euros mensuel2e et 3e année : 2190 euros mensuel