FormalRTL: Verified RTL Synthesis at Scale

Ce papier présente FormalRTL, un cadre multi-agents novateur qui intègre des modèles de référence logiciels comme spécifications formelles pour générer et vérifier de manière fiable et évolutive du code RTL à l'échelle industrielle.

L'essentiel

Imaginez que vous devez construire un pont immense et complexe, comme le Golden Gate, mais au lieu de dessiner des plans sur du papier, vous demandez à un assistant très intelligent (une intelligence artificielle) de le construire directement avec des briques.

Le problème, c'est que si vous dites simplement à l'IA : « Construis-moi un pont qui résiste aux tremblements de terre », elle risque de faire des erreurs graves : un pilier trop faible, un câble mal attaché. Dans le monde des puces électroniques (les cerveaux de nos ordinateurs et téléphones), ces erreurs coûtent des millions de dollars et peuvent rendre le produit inutilisable.

Voici comment FormalRTL, présenté dans cet article, change la donne, expliqué simplement :

1. Le Problème : L'IA qui rêve sans boussole

Jusqu'à présent, les chercheurs demandaient aux IA de créer du code pour des puces électroniques en se basant uniquement sur une description en langage naturel (comme une phrase). C'est comme demander à un architecte de construire une maison en lui disant juste « Je veux une maison confortable ». L'IA va essayer, mais elle risque de se tromper sur la taille des fenêtres ou la solidité des murs, car elle n'a pas de référence précise.

2. La Solution : Le « Double de Sécurité » (Le Modèle de Référence)

L'équipe de FormalRTL a eu une idée brillante : au lieu de donner juste une description à l'IA, ils lui donnent deux choses :

1. La description du projet (ce qu'on veut faire).
2. Un modèle de référence en logiciel (un programme informatique simple, écrit en C ou C++, qui simule exactement comment la puce doit fonctionner).

L'analogie du Chef et du Sous-chef :
Imaginez que vous êtes le Chef (l'ingénieur humain). Vous avez un Sous-chef très talentueux mais parfois étourdi (l'IA).

• Avant : Vous disiez au Sous-chef : « Fais-moi un gâteau au chocolat ». Il essaie, mais il met trop de sel.
• Avec FormalRTL : Vous donnez au Sous-chef la recette écrite (le modèle de référence) ET l'ordre de faire le gâteau. Le Sous-chef prépare le gâteau, puis il le compare immédiatement à la recette. Si le goût ne correspond pas, il corrige tout de suite.

3. Comment ça marche ? (L'Équipe de 3 Agents)

FormalRTL ne laisse pas une seule IA faire tout le travail. C'est une équipe de trois « agents » (des programmes IA spécialisés) qui travaillent ensemble :

• L'Architecte (Agent de Planification) :
  Au lieu de demander à l'IA de construire tout le pont d'un coup, l'Architecte regarde le modèle de référence et dit : « On va diviser ce travail en petites pièces. D'abord les fondations, puis les piliers, puis le tablier ». Il découpe le gros problème en petits morceaux gérables, un peu comme on assemble un Lego complexe pièce par pièce.

• Le Constructeur (Agent d'Initialisation) :
  Il prend chaque petit morceau et écrit le code électronique (RTL) pour le construire. Il s'assure que ce qu'il construit correspond exactement à la petite pièce du modèle de référence.

• L'Inspecteur de Contrôle (Agent de Débogage) :
  C'est la partie la plus géniale. Au lieu de juste dire « Ça marche » ou « Ça ne marche pas », l'Inspecteur utilise un outil mathématique puissant pour comparer le pont construit avec le modèle de référence.

  • S'il y a une erreur, l'Inspecteur ne dit pas juste « Erreur ! ». Il dit : « Regarde, au niveau du pilier 3, quand il pleut, l'eau coule à l'intérieur au lieu de dehors. Voici exactement où c'est cassé ».
  • L'IA reçoit ce message précis, répare le problème, et recommence. Elle ne s'arrête pas tant que le pont n'est pas parfait.

4. Pourquoi c'est révolutionnaire ?

• Fiabilité totale : Dans l'industrie, on ne peut pas se permettre d'avoir des bugs. FormalRTL utilise des mathématiques pour prouver que le code est correct, pas juste pour espérer qu'il fonctionne. C'est comme avoir un ingénieur qui vérifie chaque vis avec un microscope avant de livrer le pont.
• Évolutivité : Cela permet de construire des puces très complexes (comme celles utilisées dans les puces d'intelligence artificielle) qui seraient trop difficiles à faire à la main ou avec les anciennes méthodes.
• Gain de temps : Au lieu que des ingénieurs passent des semaines à chercher pourquoi une puce ne fonctionne pas, l'IA trouve et répare les erreurs en quelques minutes.

En résumé

FormalRTL, c'est comme donner à une IA un manuel d'instructions parfait (le modèle de référence) et un inspecteur de contrôle infatigable qui vérifie chaque étape. Cela permet de transformer des idées complexes en puces électroniques réelles, sûres et prouvées mathématiquement, en évitant les erreurs coûteuses qui bloquaient l'industrie jusqu'à présent.

C'est un pas de géant pour rendre la fabrication de puces aussi rapide et fiable que la construction de logiciels, mais avec la rigueur nécessaire pour le monde matériel.

Résumé technique

Voici un résumé technique détaillé de l'article "FormalRTL: Verified RTL Synthesis at Scale", rédigé en français.

1. Problématique

La conception de puces intensives en calcul (GPU, NPU, TPU) est devenue un goulot d'étranglement majeur en ingénierie, principalement en raison de la complexité des logiques de calcul et de la poursuite incessante d'objectifs stricts en matière de puissance, de performance et de surface (PPA). Bien que les grands modèles de langage (LLM) aient montré des capacités prometteuses pour générer du code matériel (RTL), leur application à l'échelle industrielle se heurte à deux obstacles fondamentaux :

• Complexité des conceptions à grande échelle : Les spécifications en langage naturel sont souvent ambiguës et insuffisantes pour guider les LLM dans la prise de décisions architecturales complexes pour des IP (Propriété Intellectuelle) industrielles nécessitant des milliers de lignes de code.
• Absence de garanties de correction formelle : Contrairement aux benchmarks open-source simples, les designs industriels comportent des datapaths profonds et des types de données personnalisés. La vérification basée sur la simulation échoue souvent à couvrir les cas limites (corner cases). Les approches existantes ne peuvent pas garantir formellement que le code RTL généré est fonctionnellement équivalent aux spécifications.

2. Méthodologie : FormalRTL

Les auteurs proposent FormalRTL, un cadre de travail multi-agents de bout en bout qui intègre systématiquement des modèles de référence logiciels (écrits en C/C++) comme spécifications formelles exécutables pour guider la génération et la vérification du code RTL.

Le flux de travail repose sur trois agents principaux orchestrés par une analyse statique :

• Agent de Planification (Planning Agent) :

  • Il effectue une analyse statique du modèle de référence C (via un compilateur comme Clang) pour décomposer le design complexe en sous-tâches modulaires basées sur les dépendances de fonctions (AST - Abstract Syntax Tree).
  • Cette décomposition permet de générer des spécifications ciblées pour chaque sous-module, évitant ainsi les ambiguïtés des spécifications purement textuelles.
  • La génération suit un ordre topologique strict : les modules dépendants sont générés et vérifiés avant les modules de niveau supérieur.

• Agent d'Initialisation (Initializing Agent) :

  • Pour chaque sous-module, il génère le code RTL initial et un "harness" de vérification.
  • Ce harness établit un environnement de vérification où les entrées du modèle C et du RTL sont identiques, et où l'équivalence des sorties est affirmée.
  • Il détermine également la fenêtre temporelle (nombre de cycles d'horloge) nécessaire pour les logiques séquentielles, alignant ainsi la vérification transactionnelle sur les exigences de latence.

• Agent de Débogage (Debugging Agent) :

  • Il utilise un outil de vérification d'équivalence formelle (hw-cbmc) pour comparer le modèle logiciel (C) et le modèle matériel (RTL).
  • En cas d'échec, l'outil fournit deux types de retours exploitables :
    1. Erreurs de syntaxe : Un localisateur de bugs identifie la ligne exacte.
    2. Contre-exemples (Counterexamples) : Un simplificateur de contre-exemples réduit les rapports complexes pour ne montrer que les signaux et fonctions en conflit.
  • Le LLM utilise ces informations pour générer des correctifs (patches) automatiques, créant une boucle de rétroaction efficace bien supérieure aux simples tests "pass/fail".

3. Contributions Clés

• Méthodologie pilotée par le modèle de référence : Première approche utilisant systématiquement un modèle C comme "spécification dorée" exécutable pour ancrer le processus de synthèse LLM, assurant ainsi l'alignement fonctionnel.
• Moteur multi-agents automatisé : Un pipeline complet couvrant la planification, la synthèse, le débogage et la vérification formelle, capable de gérer des designs complexes de manière itérative.
• Nouvelle suite de benchmarks industriels : Création et publication d'un ensemble de benchmarks de niveau industriel (incluant des opérateurs FP16 et le type de données Hifloat8 utilisé dans les puces Ascend d'Huawei), accompagnés de spécifications et de modèles de référence C, comblant ainsi le vide entre la recherche académique et les besoins industriels.

4. Résultats Expérimentaux

Les évaluations ont été menées sur des benchmarks académiques (Softfloat) et industriels (Hifloat8), avec des designs allant jusqu'à plus de 1000 lignes de code RTL.

• Taux de réussite initial (ISR) : Bien que le taux de réussite au premier essai soit variable (souvent faible pour les modules complexes), il démontre la difficulté inhérente de la génération directe.
• Efficacité du débogage : Grâce à l'agent de débogage guidé par les contre-exemples, le Taux de Réussite Final (FSR) atteint des niveaux très élevés (souvent 95-100% pour les modules combinatoires, 70-80% pour les séquentiels complexes).
• Étude d'ablation (Planification) : La comparaison avec une approche de base (génération monolithique sans analyse C) montre que la méthode de FormalRTL maintient une haute réussite même avec la complexité croissante, là où l'approche de base échoue complètement (0% de réussite sur les gros designs). La décomposition modulaire est cruciale pour l'évolutivité.
• Étude d'ablation (Outils de débogage) : L'absence de localisateur de bugs ou de simplificateur de contre-exemples entraîne une dégradation significative du nombre d'itérations nécessaires et du taux de réussite final.
• Qualité du résultat (QoR) : Les designs générés sont fonctionnellement corrects mais présentent une surface et un délai légèrement supérieurs à ceux des designs manuels optimisés par des ingénieurs. Cependant, ils offrent une base exécutable fiable pour des itérations PPA ultérieures.

5. Signification et Impact

FormalRTL représente une avancée majeure vers l'automatisation industrielle de la conception matérielle. En comblant le fossé entre les prototypes de recherche LLM et les besoins réels de l'industrie, il démontre que :

1. L'utilisation de modèles de référence logiciels comme spécifications formelles est essentielle pour garantir la correction des designs complexes.
2. L'intégration de la vérification formelle (Equivalence Checking) dans la boucle de génération LLM permet de surmonter les limites de la simulation et d'assurer une fiabilité industrielle.
3. Cette approche ouvre la voie à un développement matériel plus agile, où les ingénieurs peuvent se concentrer sur l'optimisation PPA à partir d'une base fonctionnelle vérifiée, plutôt que sur la correction d'erreurs fonctionnelles de base.

Le code source de FormalRTL et la suite de benchmarks sont prévus pour être open-sourcés, facilitant ainsi les recherches futures dans ce domaine.