Description
Date depot: 2 septembre 2021
Titre: Programmation sûre, expressive et efficace de circuits reprogrammables de type FPGA
Directeur de thèse:
Emmanuel CHAILLOUX (LIP6)
Directeur de thèse:
Jocelyn SEROT (Institut Pascal)
Domaine scientifique: Sciences et technologies de l'information et de la communication
Thématique CNRS : Modèles de calcul, preuve, vérification
Resumé: Largement utilisées depuis un vingtaine d’années par la communauté des concepteurs de circuits numériques, les architectures reconfigurables de type FPGA (Field Programmable Gate Array) font l’objet d’un intérêt croissant de la part des programmeurs au sens large, en particulier pour les applications embarquées à performance ou sûreté critique. En permettant de « tailler sur mesure » le matériel aux besoins du logiciel, ce type d’architecture offre en effet un moyen inédit de contourner les limitations des processeurs classiques. Dans l’état de l’art, la programmation efficace de ce type de circuit passe toutefois par l’usage de langages dédiés à la description de matériel (Hardware Description Languages) comme VHDL ou Verilog. Ces langages, s’ils permettent un contrôle fin et une exploitation optimale des ressources matérielles disponibles sont néanmoins caractérisés par un faible niveau d’abstraction, ce qui rend leur usage délicat par un public non familier des architectures matérielles.
Pour répondre à ces difficultés, on propose propose une approche hybride. L’idée consiste d’une part à faire exécuter le programme principal, écrit dans un langage hôte de haut niveau (fonctionnel, impératif, …), par une machine virtuelle implémentée sur un processeur « softcore » – ce qui donne accès à toute la puissance expressive du langage hôte – et d’autre part à n’effectuer la traduction au niveau RT (Register Transfer) – traduction que l’on qualifiera ici d’ » inlining » matériel – que pour un certain nombre de fonctions spécifiques, dûment identifiées. L’identification de ces fonctions, dans ce cadre, est du ressort du programmeur, compte-tenu de son domaine d’application et des objectifs poursuivis. Celui-ci pourra ainsi choisir d’« inliner » certaines fonctions parce que leur exécution via la machine virtuelle sur le processeur « softcore » est trop lente – ce qui correspond à utiliser le matériel environnant comme un accélérateur matériel configurable dynamiquement – ou parce que, dans un contexte embarqué critique par exemple, il veut garantir certaines propriétés liées à l’exécution de ces fonctions (sûreté, vivacité, temps d’exécution borné, ...).
La formulation des fonctions à « inliner » se fera non pas directement dans le langage hôte mais via un langage dédié (DSL). Ce DSL sera, par construction, susceptible d’une traduction efficace et certifiable en une description au niveau RT (on entend par là que l’on peut prouver que ladite description produit un circuit dont le comportement est identique à celui déduit de la sémantique formelle du DSL). Il sera, par ailleurs, exécutable directement par le langage hôte (soit par interprétation soit par traduction directe dans ce langage). Enfin, il doit permettre d’exprimer les propriétés que l’on désire associer aux fonctions définies. La définition, et l’implémentation, de ce DSL constitue un point clé puisqu’il conditionne in fine d’une part la faisabilité de la traduction RTL et l’efficacité du code produit et d’autre part la nature des propriétés vérifiables associées aux fonctions ainsi décrites.
Doctorant.e: Sylvestre Loïc