Raimmy's blog

Goal of my internship at UC Berkeley

Mar 12, 20257 min read

Cet article est aussi disponible en français.

TODO : translate the French post (soz’)

In , quand une personne A apprend que je vais en stage à UC Berkeley (University of California, Berkeley), à côté de San Francisco donc, cela donne lieu à un échange comme ça :

Standard encounter

A : So, what are you doing here ? me : Je vais contribuer au développement d’un outil vérifié formellement pour la synthèse de circuits électroniques.
A, vaguely grasped some terms : Whoa, looks nice.

Bon, malheureusement, si vous êtes là c’est que ces termes ne doivent pas vous parler beaucoup - et c’est bien normal ! Tellement normal que plutôt que d’avoir à réinventer une explication à chaque fois, je vais l’écrire une fois (ce qui ne m’empêchera pas de tenter de ré-expliquer à l’oral mais de finir par rediriger vers ici dans tous les cas).

Pour ça, il va falloir expliquer deux choses distinctes :

  • les outils de synthèse dans l’industrie du semi-conducteur
  • les méthodes formelles informatiques

Petit avertissement pour les spécialistes

Cette page est destinée à un public le plus vaste possible, potentiellement non-scientifique - pas pour des spécialistes donc. Des approximations grossières sont donc faites par souci de pédagogie. Cependant, certaines notes de bas de page renvoient vers des références plus sérieuses pour creuser.

Zoom sur l’industrie du semi-conducteur

Créer des circuits électroniques, c’est sympa, mais c’est compliqué. À l’heure actuelle, les CPU (Central Processing Unit, qui sont les “cerveaux” des objets électroniques) comportent plusieurs milliards de transistors (le composant électronique élémentaire). Ça fait un paquet de transistors à agencer correctement pour qu’ils fassent ce qu’on veule. Heureusement, ce travail ne se fait pas à la main et des tas de logiciels ont été développés pour concevoir des circuits.1 Malheureusement, ces logiciels ont des bugs2, ce qui expliquera la démarche de méthodes formelles présentées après.

Les logiciels qui m’intéressent sont les outils de synthèse. Ce sont des logiciels qui prennent en entrée une représentation “logique” des circuits (c’est-à-dire des informations sur le comportement du circuit), dans un langage appelé Verilog3, et qui génèrent à partir de ça une netlist de transistors, c’est-à-dire une grande carte physique “prête à graver” des transistors du circuit électronique.

Ces opérations sont complexes et intensives et durent en général de plusieurs heures à plusieurs jours.

Comme évoqué précédemment, ces logiciels comportent des bugs. Cela entraîne que la sémantique du circuit n’est pas forcément préservée : le circuit décrit sous forme de Verilog peut ne pas avoir le même comportement que le circuit en sortie, sous forme de netlist. Un circuit bien conçu en Verilog peut donc, à la sortie de la synthèse, comporter des erreurs, introduites par le logiciel de synthèse utilisé.

Ce défaut est très gênant et a donc motivé l’apparition de méthodes de validation des netlists produites. L’idée est d’avoir un autre logiciel, qui va prendre la source Verilog ainsi que la netlist, et vérifier si elles ont bien toutes les deux le même comportement4. Le problème est qu’il faut alors effectuer cette étape de vérification à chaque nouvelle synthèse, étape qui est elle aussi intensive et dure elle aussi entre plusieurs heures à plusieurs jours. À noter que le logiciel de vérification non plus n’est pas complètement exempt de bugs.

Historiquement, le terme “méthodes formelles” est utilisé au sein de l’industrie du semi-conducteur pour désigner ce processus de vérification au cas par cas. Nous allons voir qu’il peut désigner une approche bien plus intéressante.

Les méthodes formelles informatiques

L’idée est simple : plutôt que de procéder à des vérifications au cas par cas sur chaque synthèse effectuée, nous allons plutôt prouver que le logiciel de synthèse lui-même est correct. Alors nécessairement, le comportement des circuits en entrée sera préservé jusqu’en sortie.

Comment ça, on peut prouver des logiciels ?
Oui ! De la même manière qu’en maths on peut prouver un théorème, il existe des méthodes (assez récentes) pour prouver des propriétés sur des logiciels. Malheureusement, on ne peut pas juste prendre les logiciels existants et prouver des choses dessus. Ça serait trop beau. Pour ça, il faut comprendre ce que ça veut dire que de prouver des propriétés sur un programme informatique5.

La grande difficulté c’est d’arriver à exprimer de manière formelle (mathématique) les propriétés que l’on veut prouver. Dire qu’un programme est correct, c’est une phrase en français, mais ce n’est pas une propriété très bien définie. L’enjeu, c’est d’arriver à formaliser la notion de comportement pour le Verilog, pour les netlists, et raisonner sur les algorithmes qui permettent de passer de l’un à l’autre.

De nombreux langages et assistants de preuves dédiés à ce but de formalisation et de preuve ont vu le jour6. Cependant, ils ne peuvent pas se greffer à des projets existants. Ce sont les projets qui doivent être développés dans l’optique d’être prouvé depuis le départ, et utiliser l’écosystème de l’assistant de preuves sur lequel ils vont se baser.

Et le stage dans tout ça ?

On peut enfin y venir !

L’objectif est donc de contribuer aux efforts de développement de logiciels de synthèse vérifiés formellement7. Bien que des initiatives existent à l’heure actuelle8, elles ne sont pas encore largement adoptées. Plusieurs raisons peuvent expliquer cette non-adoption :

  • le sous-ensemble du langage en entrée (Verilog) est trop restrictif, certaines fonctionnalités ne sont pas encore prises en compte
  • les netlists obtenues ne sont pas suffisamment bonnes selon des critères d’évaluation (problème de performance des sorties)
  • le logiciel est trop lent pour une utilisation sur des cas réels (problème de performance du logiciel lui-même)

Le but est donc de comprendre un peu mieux ce qui bloque, et essayer si possible de surmonter ces obstacles.

Footnotes

  1. C’est ce qu’on appelle la conception assistée par ordinateur (CAO) pour l’électronique. Plus sur la page wikipedia. On parle d’Electronic Design Automation (EDA) tools en anglais. ↩

  2. À l’heure actuelle, de nombreuses démarches de fuzzing ont trouvé un nombre significatif de bugs. Des références en vrac. ↩

  3. Il existe bien d’autres langages alternatifs de description matériel (Bluespec, VHDL, …), mais Verilog est celui sur lequel je me concentrerai. Il s’agit du langage le plus répandu. ↩

  4. Un logiciel auquel je pense est Formality de Synopsys, leader du marché des logiciels de conception pour la microélectronique. ↩

  5. La preuve formelle et la théorie des types nécessiterait un article entier (voire plusieurs). Pour creuser, vous pouvez consulter (par ordre d’investissement nécessaire) :

    ↩

  6. Comme Agda, Rocq, HOL4, … ↩

  7. De manière très pratico-pratique, cette contribution pourrait se faire via des contributions au logiciel open source Lutsig, qui semble être le plus prometteur des logiciels de synthèse pour Verilog vérifié formellement. ↩

  8. Autre que Lutsig mentionné précédemment, il existe aussi des alternatives pour des variantes de Bluespec comme Koika et un synthétiseur pour Fe-Si. ↩