Le bug à 10 millions de dollars écrit par l'IA — et pourquoi j'ai fondé une entreprise pour l'éradiquer

Je me souviens du moment exact où j'ai décidé de fonder Veriprajna.

Ce ne fut pas un éclair d'inspiration. Ce fut un appel téléphonique. Le genre d'appel où personne ne parle pendant les cinq premières secondes, parce que la personne à l'autre bout essaie de trouver comment dire ce qu'elle a à dire. Une équipe de conception — des gens que je respectais, des gens réellement compétents dans leur métier — venait de recevoir de la fonderie le premier silicium d'un accélérateur RISC-V sur mesure. La puce était morte. Pas morte au sens « il faut une solution de contournement ». Pas morte au sens « on peut la corriger dans le firmware ». Briquée. Sous un alignement précis et rare de limitation thermique et de trafic mémoire à haute bande passante, le module d'arbitrage entrait dans un état indéfini et l'ensemble se bloquait en interblocage.

La cause racine était une situation de compétition (race condition). Une seule et subtile discordance entre affectations bloquantes et non bloquantes dans le RTL — le genre de chose qui se simule parfaitement, passe le lint sans le moindre murmure, réussit tous les tests de régression que vous lui lancez, puis vous trahit dans le silicium, là où il n'y a pas de seconde chance.

Le jeu de masques de cette puce en 5 nm coûtait environ 10 millions de dollars. Perdu. Mais le vrai préjudice, ce n'étaient pas les masques. C'étaient les six mois nécessaires pour diagnostiquer, corriger, revérifier et refabriquer. Sur le marché des accélérateurs d'IA, où les générations de produits durent environ 18 mois, un glissement de six mois peut éroder 50 % du bénéfice brut total qu'un produit dégage sur toute sa durée de vie. Pour une entreprise visant 100 millions de dollars de chiffre d'affaires, cette situation de compétition n'a pas coûté 10 millions de dollars. Elle en a coûté 50 millions.

Et voici la partie qui m'empêchait de dormir la nuit : le code qui l'avait provoquée avait été généré par un LLM.

La ruée vers l'or que personne ne remet en question

En ce moment même, l'industrie des semi-conducteurs est en pleine ruée vers l'or. Tout le monde — et je dis bien tout le monde — se précipite pour brancher des grands modèles de langage sur le flux de travail de l'automatisation de la conception électronique (EDA). L'argument est irrésistible : prendre des cycles de conception qui duraient des années et les comprimer à quelques mois. Démocratiser la conception de puces. Laisser l'IA gérer le fastidieux codage au niveau transfert de registres pour que les ingénieurs puissent se concentrer sur l'architecture.

Je comprends l'attrait. Je l'ai ressenti moi-même. La première fois que j'ai vu un LLM générer un module Verilog syntaxiquement correct à partir d'une invite en langage naturel, je me suis dit : cela change tout.

Mais j'ai ensuite commencé à examiner de plus près ce que « syntaxiquement correct » signifie réellement quand on écrit du matériel plutôt que du logiciel. Et j'ai réalisé que l'industrie construisait sur des fondations de sable.

Les outils qui inondent le marché en ce moment sont ce que j'appelle des « wrappers ». Ils prennent un LLM généraliste — GPT-4, Claude, Llama — l'enveloppent dans une interface de discussion avec quelques invites système à saveur Verilog, et le vendent comme un « copilote de conception de puces ». Certains sont de démonstrations réellement impressionnantes. Le code a l'air propre. Il compile. Il se simule même.

Mais voici ce que sont fondamentalement ces outils : des prédicteurs stochastiques de jetons habillés d'un vernis matériel. Ils ne comprennent pas la topologie des circuits. Ils ne comprennent pas la fermeture temporelle. Ils ne comprennent pas la métastabilité. Ils prédisent le prochain jeton probable en fonction de motifs statistiques présents dans leurs données d'entraînement.

Quand un LLM hallucine dans le logiciel, on obtient une erreur d'exécution que l'on peut corriger à distance. Quand un LLM hallucine dans le matériel, on obtient un presse-papiers à 10 millions de dollars.

Cette asymétrie est la raison même de l'existence de Veriprajna.

Pourquoi l'IA écrit-elle du mauvais code matériel ?

C'est la question qu'on me pose le plus souvent, généralement par des ingénieurs logiciels qui ont vu des LLM écrire du Python parfaitement fonctionnel et ne comprennent pas pourquoi le Verilog est différent. La réponse va plus loin que « le matériel est plus difficile ». C'est une incompatibilité fondamentale entre la façon dont les LLM pensent et la façon dont le matériel fonctionne.

Les LLM sont entraînés massivement sur du logiciel — Python, Java, C++, JavaScript. Ce sont des langages impératifs, séquentiels. La ligne A s'exécute, puis la ligne B. L'état du système est défini par l'ordre des opérations. Les LLM ont intériorisé ce paradigme si profondément qu'il est en gros leur langue maternelle.

Verilog et VHDL sont déclaratifs et concurrents. Dans un module matériel, chaque bloc always, chaque instruction assign, chaque instanciation de module s'exécute simultanément et en continu. L'ordre des lignes dans le code source n'a souvent aucune incidence sur l'ordre d'exécution dans le silicium.

J'ai vu cela se dérouler en temps réel lors d'une de nos premières expériences. Nous avons demandé à trois LLM de pointe différents d'implémenter un simple registre de pipeline à trois étages. Les trois ont utilisé des affectations bloquantes (=) au lieu d'affectations non bloquantes (<=). Le code semblait parfaitement raisonnable si on le lisait en plissant les yeux comme du code C. Mais dans le matériel, des affectations bloquantes dans un bloc synchronisé signifient que stage2 est mis à jour avec la valeur de stage1 immédiatement, puis stage3 reçoit la nouvelle valeur de stage2 — réduisant de fait un pipeline de deux cycles à un seul cycle.

Une de mes ingénieures, Priya, a fixé la sortie pendant une minute puis a dit : « Il écrit du C avec les points-virgules aux mauvais endroits. » Elle avait parfaitement raison. Le LLM avait un biais séquentiel — il traitait le Verilog comme un langage de programmation alors qu'il s'agit en réalité d'un langage de description. La distinction est subtile sur le plan syntaxique et catastrophique sur le plan physique.

Et cela empire. La conception matérielle repose sur des protocoles d'interface stricts — AXI, AHB, PCIe, TileLink — assortis de règles temporelles complexes. « Ready ne doit pas attendre Valid. » « Grant doit être asserté dans les 5 cycles. » Les LLM peuvent générer du code qui respecte ces règles 90 % du temps, ce qui semble formidable jusqu'à ce que vous réalisiez que les 10 % qu'ils se trompent sont précisément les cas limites qui tuent les puces. Un maître AXI qui asserte WVALID avant AWREADY dans une violation de sous-clause précise ne déclenchera pas d'erreur de syntaxe. Il compilera, se simulera, puis se figera une fois connecté à un contrôleur mémoire conforme dans le silicium.

Le problème des données d'entraînement aggrave tout. Le volume de Verilog de haute qualité, de qualité production, disponible pour l'entraînement est de plusieurs ordres de grandeur plus petit que celui de Python ou de JavaScript. Une grande partie du Verilog open source sur GitHub, ce sont des projets étudiants, des prototypes abandonnés, des implémentations jouets qui ne survivraient jamais à une revue de tape-out. Quand on s'entraîne sur des données médiocres, on obtient des sorties médiocres — des sorties qui ont l'air professionnelles mais qui contiennent l'ADN d'erreurs d'amateur.

La règle qui hante tout concepteur de puces

Il existe en conception de semi-conducteurs une heuristique appelée la « Règle des Dix », et une fois qu'on la comprend, on comprend pourquoi je suis à ce point obsédé par la détection précoce des bugs.

Le coût de correction d'un défaut augmente d'un facteur 10x à chaque étape suivante du cycle de vie de la conception. Un bug détecté pendant la conception RTL coûte environ 100 $ à corriger — quelqu'un modifie un fichier et relance une vérification. Le même bug détecté pendant la vérification de bloc coûte 1 000 $. À la vérification système, 10 000 $. S'il s'échappe jusqu'à la validation post-silicium — quand vous déboguez de vraies puces en laboratoire — vous êtes face à 10 millions de dollars ou plus pour un respin. Et s'il atteint les clients sur le terrain ? On est dans le territoire des 100 millions de dollars. Rappels, procès, destruction de la marque. Demandez à Intel à propos du bug FDIV du Pentium.

Les outils d'IA « wrapper » opèrent presque exclusivement à l'étape de conception RTL. Ils aident les ingénieurs à écrire du code plus vite. Mais parce qu'ils ne disposent d'aucune capacité de vérification au-delà de « est-ce que ça compile », ils injectent des bugs qui traversent sans encombre la vérification de bloc et système, pour ne détoner que dans le silicium.

Voici l'ironie cruelle : en augmentant la vélocité de génération de code sans augmenter la rigueur de la vérification, ces outils accélèrent l'injection de défauts à coût élevé dans le pipeline. Vous ne faites pas que « aller vite et casser des choses ». Vous allez vite et vous cuisez des bugs dans des jeux de masques à 10 millions de dollars.

Les données de l'industrie le confirment. Seuls 32 % des designs atteignent le succès au premier silicium. Les 68 % restants nécessitent au moins un respin, et la cause principale, ce sont les défauts logiques et fonctionnels — exactement le type d'erreurs que génèrent les LLM lorsqu'ils hallucinent des protocoles ou comprennent mal la concurrence.

J'ai expliqué cela un jour à un investisseur, au début de notre levée de fonds. Il a écouté patiemment, puis a dit : « Vous ne pouvez pas simplement utiliser GPT-4 avec de meilleures invites ? »

J'ai affiché l'exemple du registre de pipeline. Je lui ai montré le bug d'affectation bloquante. Je lui ai montré qu'il passait le lint, passait la simulation, passait toutes les vérifications automatisées qu'offraient les outils wrapper. Puis je lui ai montré ce qu'il ferait dans le silicium.

Il n'a plus reparlé de meilleures invites.

Et si vous pouviez prouver qu'un code est correct au lieu de simplement le tester ?

C'est ici que l'histoire bascule. Parce que la réponse au problème de l'hallucination des LLM, ce ne sont pas de meilleures invites, des modèles plus grands, ni davantage de données d'entraînement. C'est une approche fondamentalement différente de la vérification.

La vérification traditionnelle repose sur la simulation — on écrit des bancs de test, on exécute des millions de cycles, et on vérifie si le design fait ce qu'on attend. C'est comme tester les freins d'une voiture en faisant mille fois le tour du pâté de maisons. Si les freins ne lâchent pas, on suppose qu'ils sont sûrs. Mais que se passe-t-il s'ils ne lâchent que sous la pluie, quand vous roulez exactement à 100 km/h et que la radio est réglée sur une fréquence précise ? La simulation ne peut vérifier que les scénarios qu'elle teste explicitement. Tout le reste relève de la prière.

La vérification formelle n'exécute pas du tout le design. Elle convertit l'ensemble du design en une formule mathématique et utilise des solveurs de Satisfiabilité Modulo Théories (SMT) — des outils comme Z3 de Microsoft — pour prouver de façon exhaustive qu'une propriété tient sous toutes les combinaisons d'entrées et tous les états internes possibles. Absolument tous. Pas un échantillon. Pas une approximation statistique. Une preuve mathématique.

La simulation demande : « Est-ce que cela fonctionne dans les cas que j'ai testés ? » La vérification formelle demande : « Existe-t-il un cas possible où cela échoue ? » Cette différence, c'est la différence entre l'espoir et la preuve.

Quand le solveur renvoie « UNSAT » — insatisfiable — cela signifie qu'aucun contre-exemple n'existe. La propriété est mathématiquement garantie. Quand il renvoie « SAT », il vous remet une séquence précise d'entrées qui casse votre design, jusqu'au cycle d'horloge exact.

La vérification formelle existe depuis des décennies. La raison pour laquelle elle n'a pas conquis l'industrie, c'est que l'écriture des propriétés formelles — les assertions SystemVerilog, ou SVA — est notoirement difficile. Elle exige un ensemble de compétences spécialisées dont la plupart des équipes de conception ne disposent pas. Les assertions sont le « contrat » du matériel : « Si request passe au niveau haut, grant doit suivre dans un délai de N cycles. » « La donnée lue à l'adresse X doit correspondre à la dernière donnée écrite à l'adresse X. » « Le pipeline ne doit jamais s'interbloquer. » Les écrire correctement est un art, et il n'y a pas assez de praticiens pour répondre à la demande.

C'est précisément là que l'IA devient utile — non pas pour écrire le code matériel, mais pour écrire la preuve.

Le « sandwich formel » — comment nous l'avons réellement construit

J'ai passé des mois à débattre avec mon équipe de la bonne architecture. Le débat était acharné et, rétrospectivement, éclairant. Un camp voulait affiner un LLM jusqu'à ce qu'il génère par défaut du Verilog correct. L'autre camp — celui auquel je me suis finalement rallié — soutenait que la correction par entraînement était un fantasme. On ne peut pas entraîner l'hallucination pour qu'elle disparaisse. On ne peut que l'attraper.

Nous avons abouti à ce que nous appelons le « sandwich formel » — une architecture neuro-symbolique où le LLM est le moteur créatif et un solveur de vérification formelle est le critique intransigeant. Ni l'un ni l'autre ne fonctionne seul. Ensemble, ils accomplissent quelque chose qu'aucun des deux ne peut faire indépendamment.

Voici comment cela fonctionne en pratique. Un concepteur fournit une spécification — « Concevez un pont APB vers AXI » ou même une capture d'écran de chronogramme. Notre agent analyseur de spécifications décompose cela en exigences fonctionnelles. Vient ensuite l'innovation clé : au lieu de générer uniquement du code, le LLM génère deux artefacts simultanément.

L'artefact A est l'implémentation RTL — le code Verilog lui-même. L'artefact B est la spécification formelle — un ensemble de propriétés SVA dérivées des mêmes exigences. Si la spécification dit « Grant doit suivre Request », le LLM génère la machine à états et l'assertion qui prouve que la machine à états fait ce qu'elle prétend faire.

Puis nous déchaînons le solveur. Il prend l'artefact A et tente de le casser à l'aide de l'artefact B. D'abord, une vérification de vacuité — pour s'assurer que les assertions ne sont pas trivialement vraies (une génération « paresseuse » où la condition de déclenchement ne se produit jamais). Ensuite, la vérification bornée de modèle, en explorant des espaces d'états profonds — 50, 100 cycles de profondeur — à la chasse aux interblocages, aux situations de compétition, aux violations de protocole.

Si le solveur trouve un bug, il ne se contente pas de le signaler. Il produit une trace de contre-exemple — une forme d'onde précise montrant exactement comment le bug se manifeste. Et c'est ici que la boucle se referme : nous réinjectons cette trace dans le LLM sous forme d'invite. « Votre design a échoué. Voici la trace : cycle 1, Reset se désasserte. Cycle 2, Request passe au niveau haut. Cycle 10, Grant est toujours au niveau bas. Le grant n'est jamais arrivé. Corrigez la machine à états. »

Le LLM analyse la trace, identifie la transition d'état manquante, réécrit le code. Le solveur vérifie à nouveau. Cette boucle se répète automatiquement jusqu'à ce que le design soit prouvé correct.

J'ai écrit sur cette architecture de façon bien plus approfondie dans la version interactive de nos recherches, mais l'idée centrale est simple : nous utilisons l'IA pour écrire la preuve, et les mathématiques pour contrôler l'IA. Ni l'un ni l'autre ne fait confiance à son homologue. Chacun rend l'autre meilleur.

Les bugs qui ont fait de moi un croyant

Je suis devenu un véritable croyant en cette approche non pas par la théorie, mais grâce à des bugs précis que nous avons attrapés et que rien d'autre n'aurait trouvés.

La communauté RISC-V open source a produit des cœurs de processeur réellement excellents — Ibex (utilisé dans la puce de sécurité OpenTitan de Google), la plateforme PULP de l'ETH Zurich. Ce sont des designs très scrutés, portés par un vrai talent d'ingénierie. Et ils contiennent tout de même des bugs que seule la vérification formelle peut trouver.

Axiomise, un cabinet de conseil en vérification formelle, a trouvé un bug dans le cœur Ibex où une requête de débogage arrivant à un cycle précis pendant une instruction de branchement pouvait faire s'interbloquer le cœur ou lui faire exécuter la mauvaise instruction. Songez-y — un cœur critique pour la sécurité, revu par des dizaines d'ingénieurs, et un outil formel a trouvé un bug que la simulation avait entièrement manqué.

Dans la plateforme PULP, un bug a été trouvé où l'interconnexion AXI pouvait affamer indéfiniment un maître de bus sous un motif « occupé » précis d'interactions entre AWVALID et AWREADY. Un classique échec de vivacité — le système ne plante pas, il cesse simplement de progresser. Jamais vous n'écririez un test dirigé pour ce motif d'interaction précis. Il y a trop de motifs possibles à énumérer.

Quand nous pointons Veriprajna vers une unité Load-Store RISC-V, il génère automatiquement des assertions de conformité d'interface (« si valid est asserté, il doit rester au niveau haut jusqu'à ready »), d'intégrité des données (« la donnée lue à l'adresse X correspond à la dernière écriture à l'adresse X ») et de progression (« l'unité doit finir par renvoyer une réponse »). Ce ne sont pas des ajouts après coup boulonnés sur le code. Elles sont générées en même temps que le code, à partir de la même spécification, et appliquées avant qu'une seule ligne de RTL ne quitte notre système.

Pour le décryptage technique complet de notre méthodologie et du moteur de vérification formelle, consultez notre article de recherche détaillé.

« Mais la vérification formelle ne passe pas à l'échelle »

Les gens contestent toujours ce point, et je comprends pourquoi. La vérification formelle a la réputation d'être computationnellement explosive — l'espace d'états d'un SoC moderne est astronomiquement grand, et les approches formelles naïves s'étranglent sur tout ce qui dépasse un design jouet.

Nous y avons consacré des efforts considérables. Notre système utilise des techniques d'abstraction automatisées pour rendre le formel traitable à grande échelle. Le black-boxing nous permet de vérifier la logique de liaison tout en traitant de grands sous-blocs comme les RAM ou les ALU complexes en tant qu'entités abstraites dotées d'interfaces définies. Les points de coupe (cut-points) rompent les chemins de handshake valid/ready afin que nous puissions vérifier le contrôle de flux indépendamment du traitement des données. La réduction par symétrie nous permet de prouver une propriété pour un canal d'un routeur multiport et d'en induire mathématiquement la validité pour les N canaux.

Est-ce entièrement résolu ? Non. La physique analogique présentera toujours des défis que les méthodes formelles ne peuvent pas toucher. Mais les bugs logiques — les situations de compétition, les interblocages, les violations de protocole — deviennent mathématiquement impossibles dans le code généré. Et ce sont ces bugs-là qui provoquent les respins.

L'autre objection que j'entends porte sur la vitesse. « Faire tourner un solveur formel ne ralentit-il pas le processus de conception ? » Oui, cela ajoute un coût de calcul. Mais j'échangerai du temps de calcul contre de la certitude de calendrier chaque jour que Dieu fait. Un solveur formel qui tourne une heure de plus est infiniment moins cher qu'un respin de six mois.

La vérité inconfortable au sujet des « puces conçues par l'IA »

Un récit gagne du terrain dans l'industrie — celui selon lequel l'IA concevra bientôt les puces de bout en bout, celui selon lequel nous passons de la conception assistée par ordinateur à la conception automatisée par ordinateur. Je crois que ce récit est directionnellement juste mais dangereusement incomplet.

Nous construisons en direction de flux de travail agentiques où des agents d'IA autonomes collaborent — un agent Architecte pour le partitionnement de haut niveau, un Codeur RTL pour l'implémentation, un Ingénieur de vérification pour l'écriture des bancs de test et des assertions, un Manager pour orchestrer le flux au regard des contraintes de puissance, de performance et de surface. Nous utilisons la génération augmentée par récupération (RAG) non seulement pour le code, mais pour la connaissance — en tirant des règles de protocole précises, des contraintes de kit de conception de procédé et des standards de codage internes, afin que le LLM génère du code conforme sans halluciner.

Mais rien de tout cela ne fonctionne — absolument rien — sans une colonne vertébrale de vérification formelle. Plus l'IA devient autonome, plus il est critique que chaque sortie soit mathématiquement vérifiée avant de passer en aval. Un agent d'IA qui génère du code plus vite n'a de valeur que si ce code est correct. Un agent d'IA qui génère du code plus vite et en prouve la correction ? Voilà l'avenir.

Le problème de l'industrie des semi-conducteurs, ce n'est pas que l'IA soit trop lente à écrire du code matériel. C'est que l'IA est trop rapide à écrire du code matériel subtilement erroné.

Nous ne sommes pas un copilote. Nous ne sommes pas un chatbot. Nous sommes une fonderie de vérification formelle qui se trouve utiliser l'IA générative comme interface d'entrée. La distinction importe parce qu'elle détermine ce que vous optimisez. Les copilotes optimisent pour la vitesse. Nous optimisons pour la correction. Dans un monde où un seul bug échappé coûte 10 millions de dollars en masques et 50 millions de dollars en chiffre d'affaires perdu, je sais quelle optimisation je choisirais.

Le choix est déjà fait

L'industrie des semi-conducteurs ne peut plus se permettre l'approche « générer et prier ». La Règle des Dix n'est pas une suggestion — c'est la physique et l'économie qui conspirent pour punir quiconque expédie du silicium non vérifié. À 5 nm et en deçà, avec des jeux de masques approchant les 20 millions de dollars, la marge d'erreur s'est effondrée à zéro.

Chaque semaine, je parle à des équipes de conception enthousiasmées par ce que les LLM peuvent faire pour leur productivité et terrifiées par ce que les LLM pourraient faire à leur calendrier de tape-out. Elles ont raison de ressentir les deux choses en même temps. La technologie est réellement transformatrice. Elle est aussi réellement dangereuse sans filet de sécurité.

Veriprajna est ce filet de sécurité. Nous vous offrons la vitesse de l'IA avec la certitude des mathématiques. Pas « probablement correct ». Pas « a passé la régression ». Prouvé correct, pour chaque entrée possible, chaque état possible, chaque cas limite possible qu'une simulation n'aurait jamais l'idée de tester.

Le choix auquel est confronté tout concepteur de puces aujourd'hui n'est pas de savoir s'il faut utiliser l'IA. Ce navire a déjà quitté le port. Le choix est de savoir s'il faut utiliser une IA capable de prouver son propre travail, ou une IA qui se contente d'espérer que tout se passera bien.

Je sais sur laquelle des deux je miserais 10 millions de dollars.