Synthèse matérielle et compilation logicielle d'Esterel v7

La compilation d’Esterel v7 (cours 7)

La compilation d’Esterel v7 est délicate. Pour la compilation en circuits, le principe de base est resté celui d’Esterel v5, mais la technique a été compliquée par quatre facteurs : le traitement des tableaux, la compilation modulaire de gros programmes, la gestion des horloges, et, hélas, la mauvaise qualité sémantique des langages cibles VHDL et Verilog. La clef du succès final est l’optimisation du contrôle, qui s’appuie sur des algorithmes développés originellement pour Esterel v5 et améliorés pour Esterel v7. L’idée est de calculer symboliquement l’espace des états mémoire de contrôle atteignables pour les entrées légales, puis de simplifier la logique et de réallouer la mémoire de contrôle en fonction de ces états atteignables. Cette optimisation utilise le logiciel TiGeR, mentionné plus haut pour la vérification formelle d’Esterel v5[1]. Les résultats en taille et vitesse de circuits sont comparables à ceux des designs manuels, et souvent meilleurs.

La compilation en logiciel C ou C++ est devenue indispensable pour deux raisons. D’abord, c’est le moyen le plus rapide de tester le circuit en simulation ; ensuite, les ingénieurs logiciels doivent développer les applications avant même que le circuit n’existe physiquement, pour respecter le time-to-market. Esterel v7 a repris des techniques développées ailleurs pour Esterel v5, en particulier par S. Edwards à l’université Columbia (États-Unis) et D. Potop à l’Ecole des mines[2]. Ces techniques sont complexes et le cours n’en a présenté que le principe. Le cours s’est terminé par la démonstration de l’animation des sources lors de la simulation, fondée sur des techniques de traçabilité du code source dans le code généré.

 

[1]Esterel Studio utilise un autre système plus général de vérification, Prover SL de Prover Technologies.

[2]Voir D. Potop, S. Edwards et G. Berry, Compiling Esterel, Springer, 2007.