Formal that "Floats" High: Formal Verification of Floating Point Arithmetic

Cet article présente une méthode évolutive de vérification formelle de l'arithmétique à virgule flottante au niveau RTL, qui combine une stratégie de vérification directe RTL-à-RTL, un raffinement guidé par les contre-exemples et la génération automatisée de propriétés par intelligence artificielle pour améliorer l'efficacité et la couverture.

L'essentiel

🌊 Le Grand Défi des Nombres à Virgule : Comment s'assurer que le calcul est parfait ?

Imaginez que vous construisez une usine géante (c'est votre puce électronique) qui doit faire des calculs mathématiques complexes, comme additionner des nombres avec des virgules (ex: 3,14 + 2,71). C'est ce qu'on appelle l'arithmétique à virgule flottante.

Le problème ? Dans le monde réel, une petite erreur de calcul peut être catastrophique. Si votre calculateur de fusée se trompe d'un millimètre, la fusée rate sa cible. Si votre carte bancaire se trompe d'un centime, c'est le chaos.

Les chercheurs de ce papier (Hansa, Vaisakh et Deepak) ont développé une nouvelle méthode pour s'assurer que cette usine de calcul ne fait aucune erreur, même dans les cas les plus bizarres.

Voici comment ils ont fait, expliqué avec des analogies du quotidien :

1. Le Problème : "Traduire" le langage des humains vs celui des machines

Avant, pour vérifier si l'usine fonctionnait bien, les ingénieurs utilisaient une méthode un peu lourde :

• Ils prenaient le plan de l'usine (le code informatique complexe, appelé RTL).
• Ils le traduisaient dans un langage plus simple, comme du C (un langage que les humains comprennent mieux).
• Ils comparaient ensuite les deux.

L'analogie : C'est comme si vous vouliez vérifier si un chef cuisinier a bien suivi une recette. Au lieu de regarder directement ce qu'il fait dans la cuisine, vous lui demandez d'écrire ce qu'il fait sur un papier, vous traduisez ce papier en une autre langue, et vous comparez avec la recette originale.
Le souci : La traduction perd des détails. Parfois, ce qui semble correct sur le papier ne l'est pas dans la vraie cuisine. De plus, c'est lent et compliqué pour les recettes très complexes.

2. La Solution : La Comparaison Directe (RTL-to-RTL)

Cette équipe a dit : "Oubliez la traduction ! Regardons directement le chef cuisinier et le chef cuisinier de référence, côte à côte."

• La méthode : Ils ont créé un "jumeau numérique" parfait de l'usine (le modèle de référence) et l'ont comparé directement à l'usine réelle, étape par étape, sans passer par un langage intermédiaire.
• L'analogie : C'est comme avoir deux chefs cuisiniers dans la même cuisine. L'un suit la recette parfaite (le modèle d'or), l'autre est celui qu'on teste. On regarde leurs assiettes à chaque seconde. Si l'assiette du testeur a un grain de sel en trop, on le voit tout de suite.

3. La Stratégie : "Diviser pour régner" (Le Puzzle)

Vérifier toute l'usine d'un coup est trop difficile, comme essayer de résoudre un puzzle de 10 000 pièces en une seconde.

• La méthode : Ils ont découpé l'addition en deux grandes étapes :
  1. L'alignement : Mettre les nombres sur la même échelle (comme aligner deux règles).
  2. L'addition et l'arrondi : Faire la somme et arrondir le résultat.
• L'analogie : Au lieu de vérifier tout le gâteau d'un coup, on vérifie d'abord si la pâte est bien mélangée, puis si la crème est bien étalée, et enfin si le glaçage est lisse. Si une étape échoue, on sait exactement où chercher le problème.

4. Le Détective : L'IA et l'Humain (L'Équipe de Super-Héros)

C'est ici que ça devient moderne. Vérifier tout cela manuellement prendrait des années. Ils ont donc fait appel à l'Intelligence Artificielle (IA), mais pas n'importe comment.

• Le rôle de l'IA (Le Robot Junior) : Ils ont utilisé des IA (comme GPT-5) pour écrire automatiquement les règles de vérification. C'est comme donner un manuel d'instructions à un robot pour qu'il écrive la liste de contrôle.
• Le rôle de l'Humain (Le Chef d'Équipe) : L'IA fait parfois des bêtises ou des répétitions. C'est là qu'intervient l'humain (HITL - Human-in-the-Loop). L'humain lit ce que l'IA a écrit, corrige les erreurs, et dit : "Non, pour ce cas précis, il faut vérifier aussi la virgule décimale."
• L'analogie : Imaginez un stagiaire très rapide (l'IA) qui rédige un rapport. Il est rapide mais il se trompe parfois de chiffres. Le manager (l'humain) relit, corrige les erreurs et valide le rapport final. Ensemble, ils sont beaucoup plus efficaces que l'un ou l'autre seul.

5. Le Test de Résistance : "Casser pour mieux réparer"

Pour être sûrs que leur méthode est solide, ils ont fait quelque chose de contre-intuitif : ils ont cassé volontairement leur propre usine.

• Ils ont introduit des bugs (des erreurs) dans le code pour voir si leur système de détection les trouvait.
• Résultat : Le système a détecté tous les bugs, même les plus subtils (comme une virgule mal placée ou un arrondi incorrect). C'est comme tester un détecteur de fumée en allumant une bougie dans la cuisine : s'il sonne, il fonctionne !

🏆 Ce qu'il faut retenir (La Conclusion)

Ce papier nous dit trois choses importantes :

1. Direct est mieux : Comparer directement le code de la puce avec un modèle parfait est plus précis et plus rapide que de passer par des traductions compliquées.
2. L'IA est un super-assistant, mais pas un chef : L'IA peut écrire beaucoup de règles très vite, mais elle a besoin de l'œil expert d'un humain pour être précise et éviter les répétitions inutiles.
3. La sécurité avant tout : Avec cette méthode, on peut vérifier des puces électroniques complexes avec une confiance absolue, ce qui est crucial pour les voitures autonomes, les satellites et les systèmes bancaires.

En résumé, c'est une nouvelle façon de s'assurer que nos ordinateurs ne font pas d'erreurs de calcul, en utilisant une équipe combinant la rapidité des robots et la sagesse des humains, le tout sans jamais quitter le terrain de jeu réel (le code de la puce).

Résumé technique

Voici un résumé technique détaillé de l'article présenté à la 37e Conférence IEEE internationale sur la microélectronique (ICM) 2025.

Titre

Formal that "Floats" High : Vérification formelle de l'arithmétique à virgule flottante

1. Problématique

La vérification formelle de l'arithmétique à virgule flottante (FPU) reste un défi majeur en raison de la nature non linéaire des opérations arithmétiques et du couplage étroit entre la logique de contrôle et les chemins de données (datapath).

• Limites des approches existantes : La plupart des méthodes actuelles reposent sur des modèles de haut niveau (souvent en C) pour effectuer des vérifications d'équivalence contre la conception au niveau RTL (Register Transfer Level). Cela introduit des écarts d'abstraction, des surcharges de traduction et limite l'évolutivité.
• Complexité des FPU : Les unités de virgule flottante impliquent des opérations complexes (alignement d'exposant, normalisation, arrondi) soumises à la norme IEEE-754. La gestion des cas limites (opérandes dénormalisés, débordement, sous-débordement) rend l'exploration exhaustive de l'espace d'états au niveau RTL difficile.

2. Méthodologie Proposée

L'article présente une méthodologie scalable pour la vérification formelle directe RTL-vers-RTL, éliminant le besoin de modèles de référence logiciels (C/C++).

• Vérification Directe RTL-vers-RTL : L'implémentation RTL est comparée directement à un modèle de référence "golden" (également en RTL/SystemVerilog) qui respecte strictement la norme IEEE-754, garantissant une précision bit à bit.
• Stratégie "Diviser pour Régner" (Divide-and-Conquer) :
  • Le design est décomposé hiérarchiquement en étapes modulaires. Pour l'additionneur étudié, deux étapes principales sont identifiées :
    1. Alignement de la mantisse : Décalage de la mantisse plus petite selon la différence d'exposant.
    2. Addition et Arrondi : Addition, normalisation et arrondi du résultat.
  • Chaque étape est vérifiée via des lemmes intermédiaires et des assertions (théorèmes de correction) avant de prouver le théorème global d'équivalence.
• Raffinement Guidé par les Contre-Exemples (CEX) : Lorsqu'une propriété échoue, le contre-exemple généré par l'outil formel permet d'isoler et de corriger les défauts d'implémentation de manière itérative.
• Injection de Fautes : Des défauts contrôlés sont injectés dans le RTL pour valider la robustesse de la méthode et sa capacité à détecter des erreurs critiques de précision.
• Génération de Propriétés par IA Agente : Un système multi-agents (utilisant des LLM comme GPT-5 et Llama 3.3) génère automatiquement des assertions SystemVerilog (SVA) à partir de spécifications naturelles. Ce processus est supervisé par une boucle humaine (Human-in-the-Loop ou HITL) pour affiner les propriétés, corriger les ambiguïtés et éliminer les redondances.

3. Contributions Clés

1. Vérification RTL-vers-RTL sans abstraction C : Une approche qui évite les écarts sémantiques entre le logiciel et le matériel.
2. Preuve formelle hiérarchique : Utilisation de lemmes et d'assertions intermédiaires pour prouver l'équivalence fonctionnelle d'un additionneur à virgule flottante.
3. Détection et correction de bugs : Identification de défauts réels dans un design open-source (sélection d'opérandes incorrecte, logique d'inversion défectueuse, comportement d'exposant non contraint).
4. Intégration de l'IA Agente : Évaluation comparative de la génération de propriétés par des LLM (avec et sans supervision humaine) dans des contextes de vérification avec et sans modèle de référence.
5. Injection de fautes systématique : Validation de la capacité des propriétés formelles à détecter des erreurs subtiles dans les chemins de données.

4. Résultats Expérimentaux

Les expériences ont été menées sur la plateforme Cadence Jasper avec un additionneur à virgule flottante simple précision.

• Efficacité de la couverture (RTL-vers-RTL) :
  • Les assertions manuelles ont atteint 98,42 % de couverture formelle avec seulement 2 propriétés et un temps de preuve de 0,073 s.
  • Les propriétés générées par LLM (sans HITL) nécessitaient beaucoup plus d'assertions (7 à 15) et de temps, souvent avec des redondances.
  • Avec HITL, les LLM (notamment GPT-5) ont produit des ensembles d'assertions concis (3 à 6 assertions) atteignant une couverture équivalente aux assertions manuelles, avec des temps de preuve réduits (ex: 1,318 s pour GPT-5).
• Vérification RTL autonome (Sans modèle de référence) :
  • La couverture a chuté significativement (autour de 62-69 % sans HITL) en raison de l'incapacité des LLM à contraindre correctement l'espace d'états sans guide architectural.
  • Le raffinement HITL a été crucial pour augmenter la couverture (jusqu'à 92,30 % pour GPT-5), mais a nécessité un effort humain important pour ajouter des vérifications micro-architecturales spécifiques (propagation du bit sticky, profondeur de normalisation, etc.).
• Détection de fautes : Tous les défauts injectés (ex: erreur de décalage, inversion incorrecte, violation des règles d'arrondi) ont été détectés avec succès par les propriétés formelles.

5. Signification et Conclusion

Cette étude démontre que la vérification formelle directe RTL-vers-RTL, couplée à une génération de propriétés assistée par l'IA et supervisée par l'humain, constitue une stratégie supérieure pour les datapaths arithmétiques complexes par rapport aux méthodes traditionnelles basées sur des modèles C ou à la vérification autonome.

• Avantage principal : L'approche élimine les écarts d'abstraction, offrant une garantie mathématique rigoureuse de la conformité IEEE-754.
• Rôle de l'IA : Les LLM sont capables de générer des propriétés pertinentes, mais nécessitent une supervision humaine (HITL) pour éliminer les redondances, corriger les fausses hypothèses et atteindre une couverture optimale, en particulier dans des scénarios complexes sans modèle de référence.
• Perspectives : Bien que l'étude se limite actuellement à un additionneur, la méthodologie est conçue pour être extensible à des unités plus complexes (multiplicateurs, diviseurs), ouvrant la voie à une vérification formelle assistée par l'IA à grande échelle pour les processeurs modernes.