Doctorant F/H Conception rigoureuse de circuits basée sur les méthodes formelles

Le Centre Inria de l’Université Grenoble Alpes, regroupe un peu moins de 600 personnes réparties au sein de 22 équipes de recherche et 8 services support à la recherche.

Son effectif est distribué sur 3 campus à Grenoble, en lien étroit avec les laboratoires et les établissements de recherche et d'enseignement supérieur (Université Grenoble Alpes, CNRS, CEA, INRAE, …), mais aussi avec les acteurs économiques du territoire.

Présent dans les domaines du calcul et grands systèmes distribués, logiciels sûrs et systèmes embarqués, la modélisation de l’environnement à différentes échelles et la science des données et intelligence artificielle, le Centre Inria de l’Université Grenoble Alpes participe au meilleur niveau à la vie scientifique internationale par les résultats obtenus et les collaborations tant en Europe que dans le reste du monde.

Les projets du PEPR Cloud soutiennent la souveraineté européenne dans ce domaine, qui comprend également le matériel, notamment les processeurs et les accélérateurs de calcul. Dans un contexte technologique de ralentissement de la loi de Moore, l’amélioration des performances des processeurs nécessite des architectures matérielles avec plus de parallélisme (multi-cœurs), plus de spécialisation (accélérateurs), un rapprochement du calcul et de la mémoire, ainsi que de nouveaux types d’interconnexions entre les composants. En dissociant les ressources matérielles (calcul, mémoire, interconnexion) des ressources logiques, la virtualisation facilite le déploiement des architectures convergées qui regroupent l'infrastructure de calcul, de stockage et de réseau. Le cloud gagne ainsi en modularité, en vitesse et en agilité pour le déploiement de nouveaux services avec une utilisation optimale des ressources.

La désagrégation matérielle et la virtualisation des ressources rendent la couche d’adaptation intermédiaire de plus en plus complexe, difficile à valider et sujette aux pannes. Le projet Archi-CESAM du PEPR Cloud propose de repenser le matériel (calcul, mémoire et interconnexion) afin qu’il soit co-conçu avec l’applicatif dans une perspective d’architecture convergée et de confiance, en présence de données massives à traiter.

Les travaux de recherche de l'équipe CONVECS du centre Inria de l'UGA portent sur la modélisation et la vérification formelle de systèmes concurrents asynchrones, qui s'instancient dans de nombreux domaines (protocoles de communication, algorithmes distribués, systèmes embarqués, réseaux sur puce, etc.). A cette fin, CONVECS propose des langages formels de nouvelle génération pour spécifier le comportement et les propriétés des systèmes concurrents, ainsi que des algorithmes de vérification efficaces. Ces travaux sont instanciés dans des outils de l'environnement CADP [GLMS13], qui assiste les différentes phases du processus de conception (compilation et prototypage rapide, simulation interactive et guidée, vérification par logiques temporelles et par équivalences, génération de tests de conformité, co-simulation et évaluation de performances) et est largement utilisé en milieu académique et indutriel.

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. https://cea.hal.science/cea-04110679/en

[ZB19] 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(11):2629-2640, 2019. https://doi.org/10.1109/TVLSI.2019.2926114

[GLMS13] 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(2):89-107, 2013. http://hal.inria.fr/hal-00715056/en

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

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

• Restauration subventionnée
• Transports publics remboursés partiellement
• 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)
• Possibilité de télétravail  et aménagement du temps de travail
• Équipements professionnels à disposition (visioconférence, prêts de matériels informatiques, etc.)
• Prestations sociales, culturelles et sportives (Association de gestion des œuvres sociales d'Inria)
• Accès à la formation professionnelle
• Sécurité sociale

• Salaire brut :
  • 1ère année : 2082 euros mensuel
  • 2e et 3e année : 2190 euros mensuel