Résumé Technique : SpecAlign – Un Cadre d'Alignement Sémantique pour la Génération d'Assertions SystemVerilog

1. Énoncé du Problème

La complexité croissante des conceptions matérielles modernes a favorisé l'adoption de modèles de langage de grande taille (LLM) pour générer des assertions SystemVerilog (SVA) afin de soutenir la vérification basée sur les assertions (ABV). Cependant, les approches existantes de LLM se concentrent principalement sur la validité syntaxique et les résultats de la vérification formelle (FV) (par exemple, si une assertion est prouvée ou produit un contre-exemple sur un RTL donné). Ces métriques ne parviennent pas à traiter l'alignement sémantique : si l'assertion générée reflète fidèlement l'intention comportementale décrite dans la spécification en langage naturel.

Les LLM peuvent produire des assertions qui sont syntaxiquement correctes et formellement prouvables sur une implémentation RTL spécifique, mais qui sont sémantiquement inefficaces ou hallucinées. Par exemple, une assertion pourrait échantillonner une horloge sur le même front qui déclenche la propriété, la rendant vide (vacuous) malgré le passage de la FV. En l'absence d'un modèle RTL « golden » pour comparaison, l'inspection manuelle de telles assertions est chronophage et réduit la confiance. De plus, les moteurs de FV rencontrent des problèmes d'évolutivité (explosion de l'espace d'états) lors de l'évaluation de grands ensembles d'assertions générées pour des conceptions complexes. Il existe un besoin critique d'un cadre qui évalue la cohérence sémantique par rapport à la spécification elle-même, indépendamment des détails d'implémentation RTL.

2. Méthodologie : Le Cadre SpecAlign

SpecAlign est un cadre centré sur la spécification conçu pour évaluer et affiner itérativement les SVA générés par LLM sans dépendre d'un RTL golden. Il fonctionne via deux boucles itératives principales : une Boucle d'Alignement de Propriété et une Boucle d'Alignement SVA. Les deux boucles utilisent trois étapes fondamentales : Vérification d'Alignement, Analyse des Incohérences et Extraction de Preuves.

A. Aperçu Architectural

Le cadre normalise la comparaison entre différentes représentations de l'intention de conception. Bien que l'entrée consiste en des propriétés en langage naturel ($P$) et des SVA générés ($A$), le cadre convertit chaque SVA en un Résumé en Langage Naturel ($N$) via un processus d'extraction spécifique. Cette normalisation permet d'évaluer à la fois les propriétés et les assertions au même niveau sémantique par rapport à la spécification de conception ($S$).

B. Composants Principaux

1. Vérification d'Alignement :

   • Classification : Le cadre classe les descriptions en langage naturel ($X_i$) en trois catégories basées sur leur relation avec la spécification :
     • Implique (Entails) : Tous les éléments sont soutenus par la spécification.
     • Contredit (Contradicts) : Au moins un élément contredit la spécification.
     • Inconnu (Unknown) : Les éléments ne sont ni soutenus ni contredits (souvent en raison d'hypothèses spécifiques à l'implémentation absentes de la spécification).
   • Vote de Cohérence Interne : Pour améliorer la fiabilité, le système emploie une stratégie d'incitation de type Chaîne de Pensée (CoT). Il génère $k$ chemins de raisonnement pour une entrée donnée et agrège les sous-verdicts en utilisant un vote majoritaire. En cas d'égalité, une priorité conservatrice est appliquée : Contredit > Inconnu > Implique.
   • Sélection de Référence : La Boucle de Propriété utilise la spécification de conception ($S$) comme référence. La Boucle SVA utilise une « Banque de Propriétés Alignées » (si disponible) pour réduire le bruit provenant de documents de spécification dispersés ; sinon, elle revient à $S$.

2. Analyse des Incohérences et Affinement :

   • Lorsqu'un verdict est Contredit, le système effectue une Analyse des Incohérences. Il identifie les éléments conflictuels spécifiques dans la description, fait référence au comportement correct dans la spécification et génère un feedback structuré et actionnable ($F_i$).
   • Ce feedback guide le LLM pour régénérer la propriété ou l'assertion ($P'_i$ ou $A'_i$), définissant explicitement les conditions de déclenchement et évitant l'introduction de nouveaux signaux ou comportements absents de la spécification.
   • La sortie affinée est réévaluée dans la boucle d'alignement jusqu'à ce qu'un nombre fixe d'itérations soit atteint ou que la sortie soit alignée.

3. Extraction de Preuves :

   • Pour les cas Implique, le système extrait des preuves de soutien (citations et emplacements) de la spécification pour faciliter l'examen humain et renforcer la confiance.
   • Pour les cas Inconnu, le système catégorise quels éléments sont ambigus ou non définis, distinguant les véritables contradictions des comportements sous-spécifiés.

4. Métrique Quantitative :

   • Le cadre définit un Score d'Alignement ($a_t$) calculé comme le rapport des assertions impliquées ($E$) sur le nombre total d'assertions ($n$) à une itération donnée ($a_t = E/n$). L'objectif du processus d'affinement est de maximiser ce score.

C. Extraction de Résumé en Langage Naturel

Une étape de prétraitement critique consiste à convertir les SVA formels en résumés structurés en langage naturel. Le LLM est incité à identifier des composants SVA spécifiques (Déclencheur, Antécédent, Opérateur d'Implication, Conséquent et Disable If) et à les mapper à des phrases équivalentes en langage naturel. Cela garantit que l'intention sémantique du code formel est préservée pour la comparaison.

3. Contributions Clés

L'article expose les contributions suivantes :

• Cadre d'Évaluation Sémantique : Une approche novatrice pour évaluer les SVA générés par LLM par rapport aux spécifications en langage naturel sans dépendre de la vérification formelle appliquée à un RTL golden.
• Pipeline d'Affinement Itératif : Un cadre structuré comprenant la Vérification d'Alignement, l'Analyse des Incohérences et l'Extraction de Résumé SVA, conçu pour l'intégration dans les flux de travail de génération basés sur LLM existants.
• Métrique d'Alignement Quantitative : Une métrique de score d'alignement basée sur la classification d'implication sémantique pour mesurer la cohérence avec la spécification, offrant une alternative évolutive à l'évaluation traditionnelle de la correction par FV.
• Mécanisme d'Analyse des Incohérences : Une méthode pour générer un feedback spécifique et actionnable pour les propriétés et assertions contradictoires, soutenant à la fois l'examen manuel et l'affinement automatisé.
• Validation Empirique : Résultats expérimentaux démontrant la réduction des assertions contradictoires dans les conceptions APB et UART grâce à l'affinement sémantique.

4. Résultats Expérimentaux

Les auteurs ont évalué SpecAlign sur deux conceptions matérielles : APB (Interface APB vers I2C) et UART (Interface UART vers Bus). Le cadre a été comparé à AssertionForge, une méthode de base utilisant un graphe de connaissances et incorporant le RTL dans la génération.

• Résultats APB :
  • Base (AssertionForge) : A généré 442 SVA avec un score d'alignement de 0,02. Seuls 8 étaient impliqués, tandis que 148 étaient contradictoires.
  • SpecAlign : A maintenu 442 SVA mais a augmenté le score d'alignement à 0,15. Crucialement, le nombre d'assertions contradictoires est tombé à 0, avec 66 assertions impliquées. Les 376 restants ont été classés comme Inconnus.
• Résultats UART :
  • Base : A généré 325 SVA avec un score d'alignement de 0,06 (21 impliqués, 142 contradictoires).
  • SpecAlign : A généré 319 SVA avec un score d'alignement de 0,28. Les assertions contradictoires ont été réduites à 6, tandis que les assertions impliquées sont passées à 92.

Analyse des Résultats :
Les expériences ont révélé que les méthodes de base génèrent souvent des assertions qui sont soit contradictoires avec la spécification, soit reposent fortement sur des détails spécifiques à l'implémentation (RTL) absents de la spécification en langage naturel. SpecAlign filtre efficacement ces contradictions. L'augmentation des classifications « Inconnu » dans SpecAlign (par exemple, 376 pour APB) est interprétée non pas comme un échec, mais comme une stratégie de classification plus conservatrice et précise qui sépare les hypothèses spécifiques à l'implémentation des comportements soutenus par la spécification. Cette distinction empêche l'étiquetage faux positif des comportements non soutenus comme « impliqués ».

5. Signification et Revendications

L'article revendique que SpecAlign fournit un complément évolutif à la vérification formelle traditionnelle. En séparant la correction sémantique des résultats de preuve RTL, il adresse la limitation selon laquelle la vérification formelle seule ne peut pas déterminer si une assertion capture le comportement intentionnel décrit dans la spécification.

Les auteurs soulignent que si la vérification formelle est nécessaire pour prouver que les assertions tiennent sur le RTL, elle est insuffisante pour évaluer la qualité de l'intention de l'assertion. SpecAlign améliore la confiance dans les assertions générées par LLM en :

1. Détectant les incohérences sémantiques que les outils formels pourraient manquer (par exemple, les vérités vides).
2. Réduisant les efforts de débogage en identifiant les contradictions avant la simulation RTL ou la preuve formelle.
3. Fournissant un mécanisme pour affiner les assertions de manière itérative sans nécessiter de modèle golden.

L'article conclut modestement, notant que si le cadre améliore l'alignement, des travaux futurs sont nécessaires pour affiner les méthodologies de classification, mieux capturer les erreurs syntaxiques et étendre l'approche à d'autres tâches d'automatisation de la conception matérielle comme la génération et le débogage RTL.