Méthodologie de vérification pour les logiciels de systèmes synchrones

Le greffon Synchrone de Frama-C est dédié à l'analyse de programmes Lustre. Il combine les capacités des greffons WP et Eva et communique avec le solveur GaTeL pour prouver diverses propriétés à propos des programmes sous analyse. Les travaux de ce postdoc visent à améliorer l'usage global de Synchrone à travers cet ensemble de challenges scientifiques:
- développer une méthodologie de vérification qui tire parti de la combinaison de techniques disponibles au sein de l'outil, notamment en l'appliquant à des cas représentatifs de l'usage réel de Synchrone,
- pour supporter cette méthodologie, améliorer l'outillage disponible au sein de synchrone, notamment en ce qui concerne la génération des obligations de preuves, et leur optimisation pour les solveurs automatiques, comme le solveur Colibri2 développés au sein du laboratoire,
- améliorer le lien entre ce qui est vérifié et le modèle mathématique qui spécifie le système, par l'extension du langage LustreSpec et le développement de l'outillage associé, cela comprend notamment les aspects liés à la gestion des filtres numériques,
- développement de l'outillage pour la visualisation et le déboggage des obligations de preuve.

Ce postdoc est donc plutôt orienté vers un travail d'ensemble visant des publications orientées méthodologie de vérification dans un contexte industiel.

Co-Optimisations de Conceptions et Technologies (DTCO) pour les applications RF millimétriques: utilisation de l'intégration homogène et hétérogène puce à plaque par collage hybride

Ces dernières années ont été l'objet de nombreuses avancées technologiques dans les semi-conducteurs à base de silicium; néanmoins les limites en termes de performances fréquentielles et de puissance semblent atteintes et imposent le développement de nouveaux composants type III-V (telles que InP et GaN) plus rapides et plus puissants pour les applications RF millimétriques. Pour des raisons de flexibilité, de performances et de coûts, il est primordial de co-intégrer ces nouveaux composants hautes-performances III-V avec les filières plus classiques silicium : c'est un des objectifs majeurs du sujet proposé. Les deux années de formation par la recherche proposées seront principalement l'objet de conceptions et d’optimisations de circuits RF millimétriques tirant partie de la technologie d'assemblage 3D hétérogène puce à plaque collage hybride. De nombreux véhicules de tests ont été réalisés et caractérisés ces dernières années et ont permis de montrer les avantages et inconvénients de l'assemblage puce à plaque collage hybride pour les applications RF millimétriques. Il s'agit donc de prolonger ces travaux et de focaliser les études et recherches sur des systèmes RF réels de type amplificateur de puissance millimétrique. L'approche DTCO (Design and Technology Co-Optimisations) permettra non seulement de concevoir des circuits 3D-RF efficaces, mais aussi des réaliser des ajustements des différentes règles de conception 3D, et ainsi de rendre la technologie d'assemblage 3D par collage hybride pertinente pour la réalisation de systèmes intégrés 3D RF millimétriques.

Caractérisation électrique de matériaux 2D pour la microélectronique

Les composants de microélectroniques du futur seront de plus en plus petit et de moins en moins gourmands en énergie. Pour relever ce défi, les matériaux 2D sont d’excellents candidats du fait de leurs dimensions. De nouveaux matériaux 2D avec des propriétés nouvelles sont créés tous les jours. Mais leur intégration et la mesure de leurs performances dans des circuits est un défi. En effet, ils présentent des surfaces sans liaison pendantes ce qui leur permet de conserver leurs propriétés même à très petites dimensions mais il faut aussi réussir à préserver cette structure pendant l’intégration. Les étapes de dépôt, de transfert et de photolithographie sont susceptibles d’endommager ces surfaces fragiles.
L’objectif de ce post-doc est de développer des composants de caractérisation électrique et magnétique pour des matériaux 2D en configuration horizontale sur silicium. Le laboratoire a déjà mis au point un système de mesure verticale, mais les matériaux 2D étant très anisotropes, la mesure horizontale est nécessaire pour totalement qualifier ces matériaux. En s’appuyant sur les développements du procédé de réalisation vertical, le candidat mettra au point ce système de mesure et caractérisera différents matériaux réalisés en MBE par une autre équipe du CEA.

Comparaison du Diamant et GaN vertical au SiC et Si sur des applications de puissance

L’électrification croissante des systèmes impose des dispositifs de puissance toujours plus performants. Si le carbure de silicium (SiC) est aujourd’hui une technologie mature et industrialisée, d’autres matériaux émergent pour repousser encore les limites. Le diamant, grâce à ses propriétés physiques exceptionnelles, et le nitrure de gallium (GaN) en architecture verticale, offrent un fort potentiel d’amélioration des performances. Cependant, leurs bénéfices réels face aux solutions existantes en silicium (Si) et en SiC restent à démontrer en fonction des applications et des contraintes d’industrialisation.

L’objectif de ce postdoctorat est d’identifier les domaines d’application où ces nouvelles technologies pourraient offrir des gains significatifs en considérant les tendances actuelles et futures du marché. Une approche combinant simulation et expérimentation permettra d’évaluer leur pertinence. À partir de simulations TCAD et SPICE, les performances des composants diamant et GaN vertical seront analysées et comparées aux solutions existantes. Ces simulations seront complétées par des mesures expérimentales réalisées sur des dispositifs de test, afin de confronter les résultats théoriques à des données réelles et d’affiner les modèles.

Le projet inclut l’analyse des besoins industriels, l’optimisation des architectures de composants, ainsi que la validation expérimentale des performances. Ce travail s’inscrit dans un cadre de recherche appliquée, avec des collaborations académiques et industrielles de premier plan. Il offre une opportunité unique de contribuer au développement des futurs dispositifs de puissance tout en travaillant sur des technologies de rupture.

Substrats RF disruptifs à base de matériaux polycristallins

Contexte et Objectifs
L’optimisation des performances des circuits haute fréquence repose sur l’utilisation de substrats de haute résistivité. Aujourd’hui, les substrats SOI (Silicon On Insulator) à haute résistivité avec une couche de pièges électroniques (« trap-rich ») sous l’oxyde enterré (BOX) sont la référence en matière de performances RF dans les technologies CMOS. Cependant, ces substrats présentent deux défis majeurs : 1) Leur coût relativement élevé. 2) Une dégradation des performances RF à des températures de fonctionnement supérieures à 100 °C.

Ce projet postdoctoral propose une approche innovante pour surmonter ces limitations en explorant les performances RF d’un substrat polycristallin de haute résistivité sur toute son épaisseur (plusieurs centaines de microns). Grâce à sa forte densité de pièges électroniques répartis dans tout son volume, ce substrat pourrait garantir une stabilité des performances RF, y compris à haute température.

Missions et Contributions
En rejoignant ce projet, vous travaillerez en collaboration avec le CEA-Leti et l’Université Catholique de Louvain (UCL), deux institutions de renommée internationale en microélectronique et en caractérisation RF. Vous serez impliqué(e) dans toutes les étapes de l’étude, depuis la modélisation jusqu’aux tests expérimentaux :
- Simulation et sélection des matériaux : Réalisation de simulations TCAD pour identifier les substrats polycristallins les plus prometteurs (ex. : poly-Si, poly-SiC, …).
- Intégration des substrats dans un procédé avancé : Développement et intégration des substrats polycristallins dans un process flow SOI au CEA-Leti.
- Caractérisation RF en conditions extrêmes : Mesures des performances RF en fréquence et en température à l’UCL, avec un focus particulier sur la compréhension des mécanismes physiques sous-jacents grâce au croisement des données expérimentales et des simulations.

Analyse in situ des dislocations en Dynamique Moléculaire

Grâce aux nouvelles architectures des supercalculateurs, les simulations de dynamique moléculaire classique (DM) entreront bientôt dans le domaine du millier de milliard d’atomes. Ces systèmes de simulation – de tailles inédites – seront ainsi capables de représenter la plasticité des métaux à l’échelle du micron. De telles simulations génèrent une quantité considérable de données et la difficulté réside désormais dans leur exploitation, afin d'en extraire les ingrédients statistiques pertinents pour l’échelle de la plasticité « mésoscopique » (échelle des modèles continus). L'évolution d'un matériau est complexe car elle dépend de lignes de défauts cristallins très étendues (les dislocations) dont l’évolution est régie par de nombreux mécanismes. Afin d'alimenter les modèles aux échelles supérieures, les grandeurs à extraire sont les vitesses et la longueur des dislocations, ainsi que leur évolution au cours du temps. L’extraction de ces données peut se faire par des techniques d'analyse spécifique a posteriori basées sur la caractérisation de l'environnement local ('distortion score' [goryaeva_2020], 'local deformation' [lafourcade_2018], ‘DXA’ [stukowski_2012], mais qui restent très couteuses et ne permettent pas de traitement in situ. Nous avons récemment développé une méthode robuste permettant d'identifier à la volée la structure cristalline [lafourcade_2023], qui sera bientôt étendue au cas de la classification des dislocations. L'objectif du stage post doctoral est le développement d'une chaîne d'analyse complète menant à l'identification in-situ des dislocations au sein des simulations atomistiques ainsi qu'à leur extraction sous forme nodale. La première étape de ce processus passe par la classification et l'identification des atomes voisins du coeur de la dislocation.

Calcul Haute performance exploitant la technologie CMOS Silicium à température cryogénique

Les avancées en matériaux, architectures de transistors et technologies de lithographie ont permis une croissance exponentielle des performances et de l’efficacité énergétique des circuits intégrés. De nouvelles voies, dont le fonctionnement à température cryogénique, pourraient permettre de nouvelles avancées. L’électronique cryogénique, nécessaire pour manipuler des Qubits à très basse température, est en plein essor. Des processeurs à 4.2 K utilisant 1.4 zJ par opération ont été proposés, basés sur l’électronique supraconductrice. Une autre approche consiste à réaliser des processeurs séquentiels très rapides en utilisant des technologies spécifiques et la basse température, réduisant la dissipation énergétique mais nécessitant un refroidissement. À basse température, les performances des transistors CMOS avancés augmentent, permettant de travailler à plus basse tension et d’augmenter les fréquences de fonctionnement. Cela pourrait améliorer l’efficacité séquentielle des calculateurs et simplifier la parallélisation des codes informatiques. Cependant, il faut repenser les matériaux et l’architecture des composants et circuits pour maximiser les avantages des basses températures. Le projet post-doctoral vise à déterminer si la température cryogénique offre un gain de performances suffisant pour le CMOS ou si elle doit être vue comme un catalyseur pour de nouvelles technologies de calcul haute performance. L’objectif est notamment d’évaluer l’augmentation de la vitesse de traitement avec des composants silicium conventionnels à basse température, en intégrant mesures et simulations.

Conception et mise en œuvre d’un réseau de neurones pour la simulation thermo-mécanique en fabrication additive

Le procédé WAAM (Wire Arc Additive Manufacturing) est une méthode de fabrication additive métallique permettant de fabriquer des pièces de grandes dimensions avec un taux de dépôt élevé. Cependant, ce procédé engendre des pièces fortement contraintes et déformées, rendant complexe la prédiction de leurs caractéristiques géométriques et mécaniques. La modélisation thermomécanique est essentielle pour prédire ces déformations, mais elle nécessite d'importantes ressources numériques et des temps de calcul élevés. Le projet NEUROWAAM vise à développer un modèle numérique thermomécanique précis et rapide en utilisant des réseaux de neurones pour prédire les phénomènes physiques du procédé WAAM. Un stage en 2025 fournira une base de données via des simulations thermomécaniques avec le logiciel CAST3M. L'objectif du post-doc est de développer une architecture de réseaux de neurones capable d'apprendre la relation entre la configuration de fabrication et les caractéristiques thermomécaniques des pièces. Des essais de fabrication sur la plateforme PRISMA du CEA seront réalisés pour valider le modèle et préparer une boucle de rétroaction. Le Laboratoire de Simulation Interactive du CEA List apportera son expertise en accélération de simulations par réseaux de neurones et en apprentissage actif pour réduire le temps d'entraînement.

Conception et déploiement de stratégies innovantes de pilotage pour les réseaux énergétiques intelligents

Les réseaux de chaleur (RdC) jouent un rôle crucial dans les stratégies de transition énergétique grâce à leur capacité à intégrer efficacement les énergies renouvelables et la chaleur de récupération. En France, la stratégie nationale bas-carbone met l’accent sur l’expansion et l’optimisation des RdC, y compris des réseaux de plus petite taille avec plusieurs sources de chaleur comme le solaire thermique et le stockage. Les systèmes de contrôle intelligents, tels que le contrôle prédictif basé sur des modèles (MPC), visent à remplacer les pratiques manuelles basées sur l’expertise humaine pour améliorer l’efficacité. Cependant, le déploiement de systèmes de contrôle avancés sur de petits réseaux reste difficile en raison des coûts et de la complexité liés au matériel et à la maintenance.

Les solutions industrielles actuelles pour les grands RdC utilisent la programmation linéaire en nombres entiers mixtes (MILP) pour l’optimisation en temps réel, tandis que les petits réseaux s’appuient souvent sur des systèmes à base de règles. Les travaux de recherche se concentrent sur la simplification des modèles MPC, l’utilisation de pré-calculs hors ligne ou l’intégration de l’apprentissage automatique pour réduire la complexité. Des études comparatives évaluent diverses stratégies de contrôle en termes d’adaptabilité, d’interprétabilité et de performance opérationnelle.

Ce projet postdoctoral vise à faire progresser les stratégies de contrôle des RdC en développant, testant et déployant des approches innovantes sur un site expérimental réel. Il s’agit de créer et de comparer des modèles de contrôle, de les implémenter dans un simulateur physique, et de déployer les solutions les plus prometteuses. Les objectifs incluent l’optimisation des coûts d’exploitation, l’amélioration de la robustesse des systèmes et la simplification du déploiement.

Correction numérique de l’état de santé d’un réseau électrique

Les défauts de câbles sont généralement détectés lorsque la communication est interrompue, ce qui entraîne des coûts et des temps de réparation non négligeables. De plus, l’intégrité des données devient un enjeu majeur en raison des menaces d’attaques et d’intrusions accrues sur les réseaux électriques, qui peuvent perturber la communication. Pouvoir distinguer une perturbation due à la dégradation de la couche physique d’un réseau électrique ou à une attaque en cours sur le réseau énergétique, permettra de guider la prise de décision concernant les opérations de correction, notamment la reconfiguration du réseau et la maintenance prédictive, afin de garantir la résilience du réseau. Le sujet propose d’étudier la relation entre les défauts naissants sur les câbles et leur impact sur l’intégrité des données dans le cadre d’une communication par lignes électriques ou PLC (Power Line Communication). Les travaux se baseront sur le déploiement d’une instrumentation utilisant la réflectométrie électrique, combinant des capteurs distribués et des algorithmes d’IA pour le diagnostic en ligne des défauts naissants sur les réseaux électriques. En présence de certains défauts, des méthodes avancées d’IA seront appliquées afin de corriger numériquement l’état de santé de la couche physique du réseau électrique et garantir ainsi sa fiabilité.

Top