Vérification formelle d'une implémentation d'un processeur RISC-V

Description de l'offre

CE QUE NOUS POUVONS ACCOMPLIR ENSEMBLE :Dans le cadre de ce stage, nous allons nous intéresser à vérifier formellement une implémentation libre d'un processeur RISC-V.Etat de l'art sur les techniques et outils de vérification formelle de code HDL. Identifier une implémentation libre de RISC-V, identifier des propriétés d'intérêts à vérifier sur cette implémentation. Appliquer l'une de ces techniques et outil sur une implémentation libre d'un processeur RISC-V.Proposer des évolutions de l'implémentation étudiée pour une meilleure sureté de fonctionnement, meilleure sécurité ou une vérification facilitéeInnovation, passion, ambition : rejoignez Thales et créez le monde de demain, dès aujourd'hui.

Profil recherché

QUI ETES-VOUS ?De niveau BAC+5 en Master de Recherche ou Professionnel, ou en dernière année d'école d'Ingénieur Logiciel, Ingénieur Méthodes Formelles, Ingénieur Mathématicien.Vous possédez des connaissances indispensables en VHDL ou Verilog, C, Notions sur les architectures processeurs.Connaissances souhaitables : Méthodes formelles, Spécifications RISC-V.
Vous maîtrisez l'anglais à un niveau technique.}

À propos de Thales

QUI SOMMES-NOUS ?

Situé sur le campus de l'École polytechnique, au cœur du pôle scientifique et technologique d'envergure mondiale de Paris-Saclay, le site de Palaiseau regroupe les activités de Thales Research & Technology (TRT), le centre de recherche du Groupe, et de ThereSIS (THALES European REsearch center for Security & Information Systems) au service des activités mondiales du Groupe. Grâce à une politique de partenariat proactive avec le monde académique et un réseau international d'entreprises innovantes, nos équipes de recherche de TRT développent des technologies de rupture et celles de ThereSIS sont dédiées à la sécurisation des systèmes d'information, à l'ingénierie des systèmes complexes et aux technologies innovantes de la transformation numérique afin d'obtenir rapidement des résultats répondant à des demandes opérationnelles concrètes.Le Groupe de Recherche Logiciel de TRT-Fr se compose de plusieurs laboratoires dont un est spécialisé dans la conception des systèmes temps-réel embarqué critiques (LSEC).THALES conçoit et développe des systèmes temps-réel de plus en complexes et critiques. De ce fait, la difficulté de vérification de ces systèmes n'est que croissante. En conséquence, les coûts associés à la vérification par tests constituent une part majeure du coût de développement d'un système. De plus, dans le cadre du développement de circuits numériques, cette problématique est encore exacerbée.Une piste envisagée pour réduire ces coûts est la vérification formelle de la description matérielle. La vérification formelle est une technique mathématique afin de prouver (et non plus tester) que le code HDL répond à sa spécification.Un enjeu majeur pour les futurs systèmes embarqués est la maîtrise fine de l'exécution du logiciel et à ce titre, la spécification de processeur RISC-V ouvre l'opportunité d'observer et d'optimiser le matériel pour les besoins spécifiques des applications critiques.Les activités de ce stage seront de :
* Réaliser un état de l'art des techniques de vérification formelle de code HDL ;
* Analyser une implémentation libre RISC-V et identifier les propriétés d'intérêt pour la sureté de fonctionnement, ou la sécurité.
* Appliquer l'une de ces techniques de vérification formelle sur l'implémentation choisie d'un processeur RISC-V ;

Proposer des évolutions de l'implémentation étudiée pour une meilleure sûreté de fonctionnement, une meilleure sécurité ou une meilleure observabilité pour la vérification.