QiMeng-CodeV-SVA: Training Specialized LLMs for Hardware Assertion Generation via RTL-Grounded Bidirectional Data Synthesis

L'article présente QiMeng-CodeV-SVA, un cadre d'entraînement utilisant une synthèse de données bidirectionnelle ancrée dans le RTL pour pallier le manque de corpus SVA réels et générer des modèles spécialisés performants pour la création d'assertions SystemVerilog à partir de descriptions naturelles.

L'essentiel

🛠️ Le Problème : Construire des murs de sécurité invisibles

Imaginez que vous êtes un architecte qui construit un château fort très complexe (c'est le circuit électronique ou le matériel). Pour que ce château ne s'effondre pas, vous devez écrire des règles strictes : "Si le pont-levis est levé, personne ne doit pouvoir entrer", ou "Si la porte est ouverte, l'alarme doit sonner".

Dans le monde des puces électroniques, ces règles s'appellent des Assertions (SVA). Elles servent à vérifier que le circuit fonctionne comme prévu.

Le problème ? Écrire ces règles à la main est :

1. Très difficile : Il faut être un expert en logique temporelle.
2. Très long : Les ingénieurs passent des mois à écrire ces règles.
3. Toujours imparfait : On oublie souvent des cas bizarres.

Les chercheurs ont pensé : "Pourquoi ne pas demander à une Intelligence Artificielle (IA) de le faire ?"
Mais les IA actuelles (comme les grands modèles de langage) sont comme des étudiants brillants en littérature, mais nuls en ingénierie. Elles comprennent bien le français, mais quand on leur demande de traduire une idée en "code de sécurité électronique", elles font des erreurs subtiles qui peuvent faire planter tout le système. De plus, il n'y a pas assez de "livres d'exercices" (données) pour les entraîner correctement.

💡 La Solution : Le "Double Jeu" et l'Atelier de Construction

L'équipe derrière QiMeng-CodeV-SVA a inventé une méthode géniale pour créer une IA spécialisée, sans avoir besoin de milliers d'ingénieurs humains pour écrire les données d'entraînement.

Voici comment ils ont fait, en trois étapes simples :

1. L'Atelier de Construction (Synthèse de données)

Au lieu de chercher des règles déjà écrites (qui sont rares), ils ont pris des plans de maisons existants (des codes électroniques open-source appelés RTL).

• Ils ont demandé à une IA générale de regarder ces plans et de dire : "Voici ce que cette machine devrait faire".
• Ensuite, ils ont demandé à l'IA de traduire cette phrase en "code de sécurité" (SVA).
• Le filtre magique : Ils ont passé ces règles dans un "trempeur" (un outil de vérification formelle). Si la règle ne tenait pas la route techniquement, elle était jetée.
• Résultat : Une énorme bibliothèque de règles validées, créées à partir de vrais plans.

2. Le Jeu du "Double Jeu" (La sélection bidirectionnelle)

C'est l'idée la plus ingénieuse de l'article. Comment savoir si une règle générée par l'IA est vraiment bonne et correspond à l'idée de départ ?
Imaginez un jeu de téléphone arabe :

1. Vous partez d'une idée (ex: "La porte s'ouvre si le bouton est vert").
2. L'IA la transforme en code (SVA).
3. Le test : On prend ce code et on demande à l'IA de le re-traduire en français.
4. Le verdict : Si le français de départ et le français de retour sont identiques, c'est que l'IA n'a rien perdu en cours de route. La règle est bonne !
5. Si le sens a changé (ex: "La porte s'ouvre si le bouton est rouge"), c'est que l'IA a fait une erreur subtile. On jette la règle.

C'est comme vérifier qu'un traducteur n'a pas inventé d'histoire en traduisant un livre dans une langue, puis en le retraduisant dans la langue originale.

3. L'Entraînement du Spécialiste

Une fois qu'ils ont nettoyé et sélectionné les meilleures règles grâce à ce "double jeu", ils ont entraîné un modèle d'IA spécifique (CodeV-SVA).

• Ils ont ajouté des étapes de "réflexion" : l'IA doit expliquer son raisonnement avant de donner la réponse (comme un élève qui montre ses calculs).
• Résultat : Une IA qui n'est plus un généraliste, mais un expert en sécurité électronique.

🏆 Les Résultats : Le Petit Génie bat les Géants

Pour tester leur création, ils l'ont mise en compétition contre des géants de l'IA comme GPT-5 ou DeepSeek-R1.

• Le résultat : Leur modèle, bien que plus petit et moins cher à faire tourner, a battu les géants.
• Il est plus précis, fait moins d'erreurs et comprend mieux les nuances du langage technique.
• Dans un test réel de vérification de circuits complexes, leur modèle a généré 2,5 à 3,5 fois plus de règles valides que les modèles grand public.

🚀 En Résumé

Les chercheurs ont résolu le problème du manque de données en créant leurs propres données à partir de plans réels, et ils ont inventé un système de contrôle qualité automatique (le double jeu de traduction) pour s'assurer que chaque donnée est parfaite.

Grâce à cela, ils ont créé un expert IA capable de rédiger des règles de sécurité pour les puces électroniques avec une précision que même les plus grandes IA du monde ne peuvent pas atteindre, le tout pour un coût de calcul bien plus faible. C'est une victoire de l'intelligence de la méthode sur la simple puissance brute.

Résumé technique

1. Problématique

La vérification formelle basée sur les assertions (SystemVerilog Assertions - SVA) est cruciale dans le flux de conception matérielle numérique. Cependant, la création manuelle de SVAs de haute qualité à partir de spécifications en langage naturel (NL) et de code RTL (Register Transfer Level) est coûteuse et nécessite une expertise pointue.

L'utilisation de grands modèles de langage (LLM) généralistes pour la tâche de traduction NL2SVA (Natural Language to SVA) se heurte à deux obstacles majeurs :

1. Pénurie de données d'entraînement : Les corpus de SVAs réels et de haute qualité sont rares. Les données publiques (manuels, dépôts open-source) sont limitées en volume et souvent déséquilibrées par rapport aux vastes quantités de code RTL disponibles.
2. Difficulté de validation sémantique : Il est difficile de vérifier automatiquement si une SVA générée correspond sémantiquement à la spécification en langage naturel. Les outils de vérification formelle peuvent valider des assertions triviales (ex: assert property (1'b1)) qui passent techniquement mais ne capturent aucune contrainte réelle. De plus, les LLMs utilisés comme juges ("LLM-as-a-judge") peinent à détecter des erreurs subtiles de syntaxe ou de priorité d'opérateurs.

2. Méthodologie

Les auteurs proposent un cadre de synthèse de données innovant pour entraîner des LLMs spécialisés, nommé CodeV-SVA. Ce processus se déroule en quatre étapes principales :

A. Synthèse de SVAs à partir de code RTL réel

Au lieu de dépendre de corpus existants, l'équipe utilise de vastes ensembles de code RTL open-source (issu de la base de données CodeV) comme "Designs Under Test" (DUT).

• Un LLM généraliste (DeepSeek-V3.1) analyse le code RTL et les spécifications associées pour générer des propriétés de vérification en langage naturel et leurs traductions en SVA.
• Un outil de vérification formelle (JasperGold) filtre ces SVAs pour ne conserver que celles qui sont formellement vérifiables et non triviales. Cela permet de créer un "seed dataset" de 159 000 instances.

B. Sélection Bidirectionnelle (Bidirectional Data Selection)

C'est le cœur de l'innovation pour garantir la qualité sémantique. Le processus suit une boucle de traduction :

1. SVA $\to$ NL : La SVA générée est re-traduite en langage naturel par un LLM.
2. NL $\to$ SVA : Ce nouveau texte en langage naturel est re-traduit en une nouvelle SVA.
3. Vérification d'équivalence : Les outils formels vérifient si la SVA originale et la SVA régénérée sont logiquement équivalentes.

• Principe : Si la traduction bidirectionnelle préserve l'équivalence logique, cela indique que la paire (NL, SVA) est cohérente et ne contient pas d'erreurs sémantiques subtiles (comme des erreurs de priorité d'opérateurs). Seules les paires validées sont conservées, réduisant le dataset à 105 000 paires de haute qualité.

C. Raffinement supplémentaire de la qualité

• LLM-as-a-judge avec expertise : Un LLM est entraîné à détecter des types d'erreurs spécifiques identifiés par des experts humains (désalignement logique, incohérence de signaux, etc.).
• Filtrage par difficulté : Un LLM plus faible (Qwen3-8B) tente de générer des SVAs pour chaque propriété. Si toutes les tentatives sont triviales ou équivalentes, l'échantillon est rejeté pour éviter d'entraîner le modèle sur des données trop simples.
• Augmentation par raisonnement (Reasoning Augmentation) : Un LLM de raisonnement avancé (DeepSeek-R1) génère des trajectoires de raisonnement détaillées pour chaque paire NL-SVA, enrichissant le dataset pour l'apprentissage supervisé.

D. Affinement par Supervision (SFT)

Les modèles de base (Qwen3-8B et Qwen3-14B) sont affinés (Fine-Tuning) sur ce dataset synthétisé de 83 000 instances, en intégrant les trajectoires de raisonnement dans le format d'entraînement.

3. Contributions Clés

1. Cadre de Synthèse de Données RTL-Grounded : Une méthode scalable pour générer des milliers de paires NL-SVA de haute qualité à partir de code RTL existant, résolvant le problème de la rareté des données.
2. Sélection Bidirectionnelle : Une technique novatrice utilisant la traduction aller-retour et la vérification formelle pour filtrer automatiquement les paires sémantiquement incohérentes, surpassant les méthodes de sélection traditionnelles.
3. Modèles Spécialisés CodeV-SVA : Développement de modèles open-source (8B et 14B paramètres) spécifiquement entraînés pour la génération de SVAs, surpassant les modèles généralistes massifs.
4. Ressources Open-Source : L'intention de publier le dataset, les modèles et le pipeline d'entraînement pour la communauté.

4. Résultats Expérimentaux

Les modèles CodeV-SVA ont été évalués sur les benchmarks FVEval-NL2SVA (Human et Machine).

• Performance de pointe :

  • CodeV-SVA-14B atteint 75,8% de précision (Func.@1) sur le benchmark NL2SVA-Human et 84,0% sur NL2SVA-Machine.
  • Ces résultats surpassent ou égalent des modèles généralistes de pointe comme GPT-5 et DeepSeek-R1 (671B), tout en étant beaucoup plus petits et moins coûteux à déployer.
  • Par rapport aux modèles de base (Qwen3-14B), l'amélioration est massive (+14,2% sur Human, +8,7% sur Machine en Func.@1).

• Efficacité en flux de travail complet :

  • Dans une évaluation de bout en bout sur le framework AssertionForge (5 designs matériels réels), CodeV-SVA-8B a généré significativement plus de SVAs syntaxiquement corrects et formellement prouvés que GPT-4o et DeepSeek-R1.
  • Sur le design complexe OPENMSP430, CodeV-SVA a généré 2,5x plus de SVAs prouvés que GPT-4o et 3,5x plus que DeepSeek-R1.

• Études d'ablation :

  • La sélection bidirectionnelle a été identifiée comme le composant ayant le plus grand impact sur la performance (gain de +12,3% en Func.@1).
  • L'utilisation de données synthétisées par LLM a prouvé être supérieure à l'utilisation de données collectées ou réécrites à partir de dépôts open-source existants.

5. Signification et Impact

Ce travail démontre que la création de modèles spécialisés pour l'EDA (Electronic Design Automation) ne nécessite pas nécessairement des modèles géants propriétaires, mais repose davantage sur la qualité des données d'entraînement.

• Réduction des coûts : Il offre une alternative open-source et économiquement viable aux solutions propriétaires coûteuses pour la vérification matérielle.
• Fiabilité accrue : En intégrant la vérification formelle directement dans le pipeline de sélection des données, le modèle apprend à éviter les pièges sémantiques courants, rendant l'automatisation de la vérification plus fiable.
• Avancée méthodologique : La méthode de "sélection bidirectionnelle" pourrait être appliquée à d'autres tâches de traduction technique où la validation automatique est complexe, ouvrant la voie à une meilleure utilisation des LLMs dans des domaines scientifiques et techniques rigoureux.