Compilation modèle-vers-FPGA pour systèmes réactifs critiques

Les systèmes embarqués critiques du domaine aéronautique et spatial exigent simultanément temps réel garanti, prédictibilité et traçabilité du code exécuté. Les circuits FPGA constituent aujourd’hui une solution privilégiée pour ces applications, grâce à leur capacité à combiner hautes performances, faible latence et reconfigurabilité.

Toutefois, la synthèse matérielle certifiable à partir de modèles de contrôle reste un verrou technologique. La précédente thèse menée conjointement par l’ENAC, l’ISAE-SUPAERO et le CNES, intitulée Génération de circuits FPGA pour les systèmes critiques / Autocoding of FPGA for advanced GNC algorithm, a permis de franchir une première étape majeure en développant une chaîne de compilation complète depuis Lustre jusqu’à des netlists FPGA via Reticle.

Ce travail a démontré la faisabilité d’une synthèse prédictible, traçable et performante, ouvrant la voie à une automatisation partielle du flot matériel pour les systèmes critiques (présentée à IEEE SMC-IT 2024 [1]).

La thèse proposée vise à renforcer la fiabilité et la certification des systèmes embarqués critiques utilisés dans l’aéronautique et le spatial, en améliorant la compilation automatique de modèles de contrôle vers des circuits FPGA. Ces circuits, prisés pour leur performance et leur reconfigurabilité, exigent un flot de conception garantissant temps réel, traçabilité et prédictibilité.

Elle s’inscrit dans la continuité du prototype PYXIS [2], qui a démontré la faisabilité d’une génération automatique de circuits FPGA à partir du langage synchrone Lustre via le compilateur Reticle. L’objectif est désormais d’étendre cette chaîne pour la rendre plus complète, formelle et vérifiable.

Trois axes de recherche structurent le projet :

1. L’extension du front-end Lustre pour prendre en charge les automates et horloges logiques, assurant la traduction formelle et traçable des systèmes hiérarchiques et multi-taux.
2. L’intégration d’algorithmes d’optimisation embarqués (tels que les solveurs QP ou la commande prédictive MPC) directement synthétisables sur FPGA, afin de traiter des fonctions avancées de contrôle temps réel.
3. L’introduction d’un solveur logique (MiniSAT) au sein du compilateur, permettant la vérification automatique de propriétés structurelles du circuit généré et posant les bases d’une certification formelle.

La méthodologie prévoit quatre phases : formalisation du langage, intégration des optimisations, ajout de la vérification SAT, puis évaluation expérimentale sur plateformes FPGA Artix-7 et UltraScale+.

Les livrables incluent un outil de compilation open-source enrichi, un démonstrateur spatial validé par le CNES, et plusieurs publications internationales.

Ce travail collaboratif mené entre ISAE-SUPAERO et l’ENAC vise à consolider la France comme acteur de référence dans la conception sûre et certifiable de circuits FPGA pour les applications critiques.

[1] I. Winandy, A. Dion, P.-L. Garoche, and F. Manni, “A reactive system-specific compilation chain from synchronous dataflow models to fpga netlist,” in 2024 IEEE 10th International Conference on Space Mission Challenges for Information Technology (SMC-IT), 2024, pp. 11–21.

[2] I. Winandy, A. Dion, P.-L. Garoche, F. Manni, “PYXIS: A higly predictable toolchain for FPGA circuit production of advanced GNC algorithm”, in 2025 IEEE 10th International Conference on Space Mission Challenges for Information Technology (SMC-IT), 2025