Thèse de doctorat: Génération assistée par LLM de modèles matériels fonctionnels et formels H/F

Thèse de doctorat: Génération assistée par LLM de modèles matériels fonctionnels et formels H/F

Nous cherchons à pourvoir une offre de thèse. Ce poste est basé sur le site Nano-Innov de Paris-Saclay, Essonne (91). Ce poste est à pourvoir pour septembre 2026.

Description de l'offre

Les systèmes matériels modernes, tels que les processeurs RISC‑V, les accélérateurs et les systèmes sur puce hétérogènes, reposent fortement sur des simulateurs fonctionnels et des modèles de vérification formelle afin de garantir la correction, la fiabilité et la sécurité. Toutefois, la construction et la maintenance manuelles de ces modèles à partir des spécifications de conception sont lentes et deviennent plus complexes à mesure que les architectures se complexifient.

L’objectif de cette thèse est de développer une méthodologie unifiée, pilotée par l’IA, pour la co‑génération automatique de modèles matériels fonctionnels et formels directement à partir des spécifications de conception. Les travaux porteront sur la génération de modèles fonctionnels exécutables, tels que des simulateurs au niveau jeu d’instructions, ainsi que de modèles de vérification formelle capturant précisément la sémantique architecturale.

La thèse développera des chaînes de génération basées sur les LLMs, combinant l’apprentissage par renforcement avec des boucles de retour pilotées par les outils, afin d’affiner itérativement une représentation intermédiaire inspirée des prompts et de guider la génération des modèles vers la correction, la cohérence et le succès de la vérification formelle. L’objectif à long terme est de proposer un environnement de co‑génération correcte par construction permettant de réduire significativement l’effort de modélisation manuelle tout en assurant un fort alignement entre les vues fonctionnelles et formelles de l’architecture.

La méthodologie développée sera évaluée sur des cas d’étude matériels réalistes et open‑source, avec un accent particulier sur les architectures RISC‑V, leurs extensions et les accélérateurs matériels. Les résultats expérimentaux permettront d’évaluer la précision des modèles générés, leur cohérence mutuelle, leur capacité à passer à l’échelle, ainsi que les gains de productivité obtenus par rapport aux approches de modélisation manuelle.

Profil du candidat

• Master en architecture des ordinateurs, génie informatique, systèmes embarqués ou informatique
• Solides compétences en programmation en Python et en C et/ou C++
• Intérêt marqué pour l’architecture matérielle, l’EDA ou la vérification
• Une bonne base en apprentissage automatique est attendue
• Une expérience ou une familiarité avec les méthodes formelles est un plus

Conformément aux engagements pris par le CEA en faveur de l'intégration des personnes handicapées, cet emploi est ouvert à toutes et à tous. Le CEA propose des aménagements et/ou des possibilités d'organisation pour l'inclusion des travailleurs handicapés.

Site de référence :

Référence :