💬 NLP

CktFormalizer: Autoformalization of Natural Language into Circuit Representations

CktFormalizer est un cadre qui exploite le langage de description matérielle à types dépendants de Lean 4 pour guider les modèles de langage dans la génération de descriptions matérielles garanties syntaxiquement correctes, exemptes de défauts empêchant la synthèse et vérifiées fonctionnellement par des preuves vérifiées par machine, permettant ainsi une réalisabilité quasi parfaite en phase de backend et une optimisation sûre et automatisée du PPA.

Auteurs originaux : Jing Xiong, Qi Han, Chenchen Ding, He Xiao, Zunhai Su, Chaofan Tao, Ngai Wong

Publié 2026-05-11

📖 5 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Jing Xiong, Qi Han, Chenchen Ding, He Xiao, Zunhai Su, Chaofan Tao, Ngai Wong

Article original sous licence CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Ceci est une explication générée par l'IA de l'article ci-dessous. Elle n'a pas été rédigée ni approuvée par les auteurs. Pour une précision technique, consultez l'article original. Lire la clause de non-responsabilité complète

Imaginez que vous demandiez à un architecte très talentueux mais légèrement négligent de dessiner les plans d'une maison à partir d'une description verbale.

Dans le monde traditionnel de la conception de puces, vous demanderiez à l'architecte de rédiger les instructions en Verilog (un langage utilisé pour décrire les puces informatiques). L'architecte pourrait rédiger une description magnifique, mais parce que le Verilog est un peu comme un ensemble de règles lâches, l'architecte pourrait accidentellement dire : « Reliez un tuyau de 4 pouces à un tuyau de 8 pouces », ou « Créez un couloir qui boucle sur lui-même ».

L'ordinateur vérifie la grammaire et dit : « Ça a l'air bon ! » Mais lorsque la maison est réellement construite (la puce est fabriquée), ces erreurs provoquent l'éclatement des tuyaux ou le piégeage des gens dans le couloir. Ce sont des défaillances coûteuses et silencieuses qui ne se manifestent que des semaines plus tard.

CKTFORMALIZER est un nouveau cadre qui change la donne. Au lieu de laisser l'architecte écrire directement dans le langage lâche du Verilog, il l'oblige à écrire dans un langage mathématique strict appelé Lean.

Voici comment cela fonctionne, en utilisant une analogie simple :

1. L'Éditeur Strict (Le Compilateur)

Considérez Lean comme un éditeur super strict qui sait exactement comment une maison doit être construite.

L'Ancienne Façon : L'architecte écrit « Reliez le tuyau A au tuyau B ». L'éditeur ne vérifie pas les tailles. Plus tard, l'équipe de construction découvre que le tuyau A est trop petit.
La Façon CKTFORMALIZER : L'architecte tente d'écrire « Reliez le tuyau A (taille 4) au tuyau B (taille 8) ». L'éditeur claque immédiatement la porte et dit : « Erreur ! Vous ne pouvez pas relier ceux-ci. Corrigez-le maintenant. »
Le Résultat : L'architecte (une IA) reçoit un retour immédiat. Il ne peut pas avancer tant que les tailles ne correspondent pas parfaitement. Cela détecte les « incohérences de largeur » et les « boucles » avant même qu'une seule brique ne soit posée.

2. Le Filet de Sécurité (Sécurité de Type)

Dans l'ancien système, vous pourriez accidentellement laisser une porte ouverte dans une pièce, et la maison serait construite avec une pièce courante et défectueuse. Dans le système Lean, les règles sont si strictes qu'il est physiquement impossible de rédiger un plan avec une pièce défectueuse.

Si l'architecte oublie de décrire ce qui se passe lorsqu'un interrupteur est actionné, l'éditeur dit : « Vous avez oublié un cas ! Vous devez décrire chaque possibilité. »
Cela garantit que la conception est « correcte par construction ». Si elle est compilée (passe la vérification de l'éditeur), elle est garantie structurellement solide.

3. La Preuve de Vérité (Vérification Formelle)

Habituellement, pour vérifier si un plan de maison fonctionne, vous construisez un petit modèle et vous le testez. Parfois, le modèle fonctionne, mais la vraie maison ne fonctionne pas.
CKTFORMALIZER utilise des preuves mathématiques. L'IA ne se contente pas de deviner ; elle rédige une preuve mathématique affirmant : « Ce nouveau design, moins cher, fait exactement la même chose que le design original parfait. »

C'est comme avoir un mathématicien prouver que votre nouveau plan, moins cher, est fonctionnellement identique à l'original à 100 %, jusqu'au dernier atome, pour chaque scénario possible, et pas seulement pour ceux que vous avez testés.

4. La Boucle d'Optimisation (Le Rénovateur Intelligent)

Une fois que l'IA a un design qui fonctionne, le système ne s'arrête pas. Il agit comme un rénovateur intelligent qui examine le plan et dit : « Nous pouvons rendre cette maison 35 % plus petite et utiliser 30 % d'énergie en moins. »

L'IA tente de réorganiser les pièces (la logique du circuit).
Elle construit une nouvelle version.
Elle exécute immédiatement à nouveau l'« Éditeur Strict » pour s'assurer que la nouvelle version fonctionne toujours parfaitement.
Elle exécute ensuite une simulation physique pour voir combien d'espace et d'énergie elle économise.
Si la nouvelle version est meilleure et toujours prouvée mathématiquement correcte, elle la conserve. Sinon, elle revient en arrière.

Les Résultats

L'article a testé cela sur des centaines de problèmes de conception (comme la construction de compteurs, d'unités de mémoire et de contrôleurs de feux de circulation).

La Référence (Ancienne Façon) : Lorsqu'ils ont tenté de fabriquer les puces, environ 20 % des designs qui semblaient corrects sur papier ont échoué lorsqu'ils ont essayé de les fabriquer.
CKTFORMALIZER (Nouvelle Façon) : 100 % des designs qui ont passé l'éditeur strict ont réussi à traverser l'ensemble du processus de fabrication (synthèse, placement et routage) sans échec.
Efficacité : Le système a également réussi à réduire la taille des designs et à économiser de l'énergie de manière significative (jusqu'à 35 % de surface en moins) tout en prouvant qu'ils étaient toujours parfaits.

En Résumé

CKTFORMALIZER revient à donner à un architecte IA un livre de règles magique qui l'empêche de faire des erreurs avant même qu'il ne commence à dessiner. Au lieu de construire une maison et d'espérer qu'elle ne s'effondre pas, il force l'architecte à prouver que la maison est solide avant que la première brique ne soit commandée. Cela transforme la conception de puces d'un jeu de « deviner et vérifier » en un processus de « prouver et construire », aboutissant à des puces plus petites, plus efficaces et garanties de fonctionner.

Résumé Technique : CktFormalizer

Énoncé du Problème

La conception matérielle reste une discipline sujette aux erreurs, où des défauts subtils, tels que des incohérences de largeur de bits, des boucles combinatoires ou une logique de cas incomplète dans les Machines à États Finis (FSM), peuvent passer les vérifications de syntaxe mais échouer silencieusement lors de la synthèse ou se manifester sous forme de bugs coûteux sur le silicium plus tard. Bien que les Grands Modèles de Langage (LLM) aient démontré leur capacité à générer du Verilog à partir de spécifications en langage naturel, le code résultant hérite souvent des pièges inhérents au Verilog et au VHDL : un manque de garanties statiques comme les types dépendants, la correspondance de motifs exhaustive et les preuves vérifiées par machine. Par conséquent, le matériel généré par les LLM nécessite fréquemment un débogage manuel approfondi et échoue souvent à atteindre l'implémentation physique (Placement et Routage, DRC, LVS), même lorsqu'il est fonctionnellement correct en simulation.

Méthodologie

L'article présente CktFormalizer, un cadre qui unifie la génération de code pilotée par les LLM avec la vérification formelle en ciblant un Langage de Description Matérielle (HDL) à types dépendants intégré dans Lean 4. Au lieu de générer directement du Verilog, le système redirige l'agent LLM pour qu'il génère du code Lean, qui sert de cible de compilation principale.

Architecture Principale

Le cadre fonctionne via un pipeline en boucle fermée impliquant trois rôles distincts pour Lean :

Vérificateur de Types (Vérificateur au Moment de la Compilation) : Le système de types dépendants de Lean encode les contraintes de largeur de bits, la couverture des cas et l'acyclicité. Les défauts matériels (par exemple, les incohérences de largeur ou les boucles combinatoires) sont détectés comme des erreurs de type au moment de la compilation plutôt que comme des échecs silencieux en aval. Cela fournit à l'agent LLM un retour d'information immédiat et exploitable pour réparer itérativement la conception.
Pare-feu de Correction : Les conceptions qui se compilent avec succès dans Lean sont structurellement garanties exemptes de classes spécifiques de défauts (incohérences de largeur, boucles combinatoires, verrous non intentionnels). Cela garantit que les conceptions compilées survivent au flux de synthèse et de Placement et Routage (P&R) en aval sans le taux de perte de 20 % observé dans la génération de Verilog de base.
Assistant de Preuve : L'agent construit des preuves de théorèmes automatisées pour vérifier l'équivalence fonctionnelle entre la spécification en langage naturel et l'implémentation générée (ou optimisée). Ces preuves couvrent des séquences d'entrées arbitraires et des largeurs paramétrables, dépassant les limites des vérifications basées sur les SMT bornés.

Flux de Travail

Génération et Itération : Un agent LLM (instancié avec Claude) génère du code HDL Lean basé sur une spécification en langage naturel. Il entre dans une boucle itérative « générer-compiler-réparer » où les erreurs du compilateur Lean guident l'agent pour corriger les bogues sémantiques avant qu'ils ne se propagent.
Extraction : Après une compilation réussie, un métagénère (#synthesizeVerilog) extrait du SystemVerilog synthétisable à partir du graphe de combinaisons de signaux Lean.
Implémentation Physique : Le SystemVerilog extrait est simulé, synthétisé (en utilisant Yosys) et implémenté physiquement (en utilisant OpenROAD avec le PDK SkyWater 130nm) pour générer des mises en page GDSII et des métriques Performance-Puissance-Surface (PPA).
Boucle d'Optimisation PPA : Une étape d'optimisation en boucle fermée renvoie les métriques PPA à l'agent. L'agent propose des variantes architecturales (par exemple, des chemins de données parallèles par rapport à des chemins de données sériels) et doit fournir des preuves d'équivalence vérifiées par machine pour garantir que la variante optimisée reste fonctionnellement équivalente à la spécification originale.

Contributions Clés

Premier Cadre de Bout en Bout : CktFormalizer est le premier cadre à combiner la génération matérielle pilotée par les LLM avec un HDL intégré dans Lean, offrant un pipeline allant du langage naturel au silicium synthétisable avec une optimisation PPA en boucle fermée.
Génération Guidée par les Types : L'article démontre que le ciblage d'un HDL sûr par les types améliore considérablement les taux de réussite des LLM par rapport à la génération directe de Verilog. Les erreurs de type au moment de la compilation fournissent un retour d'information structuré qui guide l'agent vers des conceptions correctes, s'adaptant à la propriété intellectuelle (IP) pertinente pour l'industrie, comme les interfaces de bus d'accusation de réception multi-canaux.
Intégration de la Vérification Formelle : Le cadre comble le fossé entre le code généré par les LLM et le matériel prouvablement correct en permettant à l'agent de produire des preuves d'équivalence vérifiées par machine. Cela garantit que les optimisations architecturales ne compromettent pas la correction fonctionnelle.

Résultats Expérimentaux

Le cadre a été évalué sur trois benchmarks : VerilogEval (156 problèmes), RTLLM (50 problèmes) et ResBench (56 problèmes).

Réalisabilité en Aval : Une découverte cruciale est que CktFormalizer préserve la correction fonctionnelle en aval. Alors que la base de référence (génération directe de Verilog) perd environ 20 % des conceptions fonctionnellement correctes lors de la synthèse et du routage, CktFormalizer préserve 100 % de ses conceptions compilées tout au long du flux complet de synthèse, P&R, DRC et LVS.
Compilation et Simulation : Sur VerilogEval, CktFormalizer a atteint un taux de compilation Lean de 92,3 % et un taux de réussite de simulation RTL de 72,4 %, compétitifs par rapport aux bases de référence de génération directe de Verilog. Lorsque le retour d'information de synthèse est inclus dans la boucle de l'agent, le taux de compilation passe à 99,4 %.
Optimisation PPA : L'étape d'optimisation en boucle fermée a produit des améliorations significatives. Grâce à une exploration d'architecture validée, le cadre a permis une réduction de surface allant jusqu'à 35 % et une réduction de puissance de 30 %.
Clôture Temporelle : Toutes les conceptions fonctionnellement correctes ayant terminé le Placement et le Routage ont atteint la clôture temporelle (WNS $\ge$ 0 ns) sans intervention manuelle.
Génération de Preuves : Dans une étude pilote, la génération de preuves étape par étape (affinement itératif avec retour d'information sur les objectifs de preuve) a amélioré les taux de complétion des preuves de 53 % à 63 %, démontrant la viabilité des assistants de preuve pour la vérification matérielle.

Signification et Revendications

L'article revendique que les types dépendants et les agents LLM sont complémentaires. En utilisant un langage formel (Lean) à la fois comme cible de génération et comme substrat de vérification, le cadre transforme la boucle « générer-et-tester » du LLM d'une recherche stochastique sur des programmes syntaxiquement valides en un processus d'affinement guidé par les types.

Les auteurs soulignent que le compilateur agit comme le vérificateur, déplaçant la détection des erreurs de la fin du flux EDA (où les corrections sont coûteuses) vers le moment de la compilation. Cette approche permet au système de produire un matériel non seulement fonctionnellement correct, mais aussi structurellement robuste face aux transformations en aval, résolvant efficacement le problème de « l'échec silencieux » courant dans le matériel généré par les LLM. Ce travail suggère que les langages formels peuvent servir de fondation à une conception matérielle automatisée et digne de confiance, permettant aux LLM de naviguer dans les compromis complexes de l'optimisation matérielle tout en maintenant des garanties rigoureuses de correction.