La conception de circuits synchrones et multi-horloges en Esterel v7

Mon équipe s’est engagée dans plusieurs années de développement du langage, du compilateur et de son environnement de développement Esterel Studio, accompagné d’expérimentations en recherche ou applications préindustrielles chez Intel, Texas Instruments (TI), ST microelectronics et NXP (ex Philips). Esterel Studio est ensuite entré en production chez TI et ST : contrôles de mémoires variés, dont les difficiles DMAs (Direct Memory Access) pour les applications voraces en données, gestion de bus, de réseaux sur puce et de communications, contrôle de systèmes vidéo, etc.

Le langage a été cédé en 2007 à l’IEEE [1], en vue de sa standardisation, conduite par un groupe de chercheurs et d’industriels. Sa rigueur formelle a permis que les circuits soient développés plus rapidement, avec moins d’ingénieurs, et surtout de vérifieurs, tout en conservant une excellente efficacité. Ce langage a permis aux architectes et micro-architectes de tester et de modifier rapidement leurs idées en utilisant nos simulateurs graphiques et outils de vérification formelle, tout en étant confiants dans la qualité de la synthèse finale. Je montrerai en 2014 à quel point l’industrie nous a posé des problèmes scientifiques plus difficiles que ceux que nous connaissions en recherche, et je présenterai ensuite les méthodes de vérification formelle pour Esterel v7.

L’aventure s’est terminée en mars 2009 à la suite de la crise de 2008, comme pour beaucoup de produits innovants à cette époque. La standardisation IEEE du langage, presque terminée, a été suspendue. Esterel Studio a été racheté par Synfora, lui-même racheté par Synopsys, leader du domaine. Synopsys a décidé de mettre Esterel Studio au congélateur, ce qui fait que même ses auteurs ne peuvent plus l’utiliser, alors que tout l’outillage était auparavant accessible gratuitement pour l’enseignement et la recherche.

Esterel v7, le design du langage                                                       

Les instructions temporelles d’Esterel v7 sont issues de celles d’Esterel v5, mais simplifient l’émission simultanée ou conditionnelle de signaux ; la structure modulaire a été améliorée et rendue plus générique. Les signaux d’Esterel v5 ont également été étendus pour répondre aux besoins des circuits ; leurs valeurs et bits de présence sont tous deux optionnels, et les valeurs peuvent êtres temporaires, mémorisées, ou retardées. Mais la nouveauté principale est le traitement des données et des tableaux. Esterel v7 introduit des types numériques bien plus précis que ceux des langages habituels, comme le type unsigned qui dénote l’ensemble des M entiers naturels i tels que 0 ≤ i < M et le type signed qui dénote l’ensemble des 2M entiers signés i tels que -M ≤ i < M. Il y a plusieurs raisons pour introduire ces types. D’abord, en circuits, le raisonnement sur la taille en nombre de bits de l’écriture binaire est insuffisant : par exemple, on a les typages 4 : unsigned<5>, 5 : unsigned<6> et 4*5 = 20 : unsigned<21>. Si 4 et 5 s’écrivent avec 3 bits en binaire, leur produit 20 s’écrit avec 5 bits, et non les 6 qu’on obtient en additionnant leurs tailles individuelles ; ceci devient évident grâce au type unsigned<21>. Ensuite, le binaire n’est pas le seul codage utile en matériel, où l’on travaille aussi en code Gray, un seul bit changeant à chaque incrémentation, ou en code onehot, avec un seul bit à 1 dans l’écriture du nombre. Les types signed et unsigned sont abstraits et indépendants de leurs représentations, qui peuvent être de nombre de bits variable. Enfin, les unsigned servent à indexer les tableaux et notre typage rend facile de tester les débordements d’index à la compilation par analyse de types ou vérification formelle.

En Esterel v7, les tableaux sont de types et de dimensions quelconques, qui peuvent être paramétriques. Ils s’appliquent aux signaux et aux valeurs. Une instruction de réplication statique permet de construire des tableaux de processus pour manipuler les tableaux de données et de signaux. Enfin, Esterel v7 permet deux types de manipulations d’horloge : le masquage de cycle (clock-gating), qui possède une vraie sémantique mathématique, au contraire des langages classiques Verilog/VHDL, et l’utilisation modulaire d’horloges multiples. Ces aspects seront détaillés en 2014.

Le cours s’est terminé par la présentation d’un mini-filtre vidéo qui illustre les différents aspects du langage, ainsi que la façon de l’utiliser pour « pipeliner » facilement les circuits et donc diminuer leur temps de cycle.