Knowledge Graphs, the Missing Link in Agentic AI-based Formal Verification

Résumé technique : Graphes de connaissances, maillon manquant dans la vérification formelle basée sur l'IA agentique

Énoncé du problème
Bien que les grands modèles de langage (LLM) aient démontré leur potentiel pour générer des assertions SystemVerilog (SVA) à partir de spécifications en langage naturel afin d'accélérer la vérification formelle (FV), des obstacles majeurs subsistent. Le défi principal est le problème de l'« ancrage » (grounding) : les spécifications sont souvent ambiguës ou incomplètes, tandis que les détails micro-architecturaux critiques résident dans le code au niveau de transfert de registre (RTL). Les approches existantes traitent généralement les spécifications et le RTL comme du texte faiblement structuré, ce qui entraîne un ancrage faible entre les spécifications et le RTL. Cela se traduit par des incohérences sémantiques, des échecs syntaxiques fréquents lors de l'analyse formelle, et des assertions nécessitant des corrections itératives étendues et un tri manuel. De plus, les méthodes antérieures échouent souvent à intégrer de manière persistante les retours des outils formels (tels que les contre-exemples ou CEX et les rapports de couverture) dans la boucle de génération, limitant ainsi le raffinement systématique.

Méthodologie
Les auteurs proposent une méthodologie centrée sur la vérification qui construit un graphe de connaissances (KG) à partir de représentations intermédiaires (IR) structurées pour combler le fossé entre l'intention et l'implémentation. Le flux de travail est organisé en quatre couches : Entrées, IR JSON typés, KGs d'exécution et Orchestration d'agents.

1. Représentations intermédiaires (IR) : Le système extrait et normalise les données en artefacts JSON typés, incluant spec_chunks.json (spécifications hiérarchiques), requirements.json, design_model.json (métadonnées RTL telles que les hiérarchies et les signaux), properties.json, et les résultats de vérification (formal_results.json, cex_cases.json, coverage_metrics.json).
2. Construction du graphe de connaissances : Ces IR sont exportés sous forme de nœuds et d'arêtes pour construire un KG d'exécution utilisant NetworkX. Le KG agit comme un registre d'artefacts, reliant les exigences, la hiérarchie de conception, les signaux, les hypothèses et les propriétés. Il permet une récupération de contexte borné ; par exemple, lors de la génération d'une propriété, le KG fournit l'exigence spécifique, son fragment de spécification parent, les signaux RTL pertinents et les livres de règles.
3. Orchestration multi-agents : Le processus de vérification est décomposé en agents spécialisés qui interrogent et mettent à jour le KG :
   • Génération de propriétés : Un agent principal coordonne un spec_analyst (décomposant les exigences), un sva_author (synthétisant la syntaxe SVA), un sva_reviewer (validant la conformité) et un sva_patcher (corrigeant sur la base des retours).
   • Correction syntaxique : Une boucle dédiée gère les erreurs de compilation. Les agents analysent les diagnostics, appliquent des réparations déterministes pour les motifs courants (par exemple, identifiants non déclarés) et utilisent un contexte complexe (déclarations RTL, texte d'exigence) pour les erreurs plus difficiles. Les propriétés sont autorisées un maximum de trois tentatives de correction.
   • Correction CEX : Lorsque les propriétés échouent, les agents analysent les formes d'onde VCD et les traces d'échec. Une classe spec_assertion_analyzer classe les causes racines (par exemple, bogues RTL vs sous-spécification), et un cex_fixer ajuste les contraintes ou renforce les assertions.
   • Amélioration de la couverture : Les agents analysent les métriques de couverture pour identifier le code inaccessible ou les propriétés vaines, générant des propriétés ciblées pour combler les lacunes.

Contributions clés
L'article revendique trois contributions principales :

1. Construction de KG centrée sur la vérification : Une approche novatrice construisant un KG à partir d'IR structurés qui intègre l'intention des spécifications, la structure RTL, les propriétés générées et les résultats des outils formels dans un seul artefact interrogeable.
2. Flux de travail multi-agents avec traçabilité : Un système où les agents utilisent un contexte ancré dans le KG pour générer et affiner les SVA, maintenant des liens de traçabilité explicites des exigences vers les éléments de conception, les propriétés et les résultats de vérification.
3. Évaluation empirique : Une évaluation sur sept conceptions de référence open source quantifiant l'impact du contexte ancré dans le KG sur l'efficacité de la génération de propriétés, la validité syntaxique et l'efficacité des boucles de raffinement CEX.

Résultats
La méthodologie a été évaluée sur sept conceptions (FIFO, Lemming, ALU, CICD, BST, Compteur TTC et CSR) utilisant le modèle GPT-5.2 et Cadence JasperGold.

• Syntaxe et compilation : L'approche a produit de manière cohérente des SVA compilables avec une faible surcharge de réparation syntaxique. Le contexte ancré dans le KG, en particulier la résolution déterministe des signaux et de la hiérarchie via l'IR design_model, a considérablement réduit les problèmes de front-end tels que les identifiants non déclarés.
• Couverture formelle : La couverture formelle de bout en bout variait de 78,5 % à 99,4 % sur les benchmarks.
• Efficacité du raffinement : Des conceptions comme le FIFO et le CIC Decimator ont montré une amélioration significative après les boucles CEX et de couverture, suggérant que de nombreux échecs initiaux étaient dus à des problèmes locaux (gardes manquantes, conditions limites) corrigibles via le contexte récupéré.
• Limites : La convergence dépendait de la conception. Des conceptions complexes comme l'arbre de recherche binaire (BST) et celles nécessitant des invariants globaux ou un raisonnement temporel profond (par exemple, Lemming, ALU) ont montré une amélioration limitée grâce à la correction automatisée. Les auteurs notent que les capacités actuelles des LLM peinent avec le raisonnement temporel et arithmétique complexe, et que le débogage sémantique reste le principal goulot d'étranglement pour les benchmarks plus difficiles.

Signification
L'article postule que l'approche centrée sur le KG proposée répond à la faiblesse critique des travaux antérieurs : l'absence de liens structurés et interrogeables entre les exigences, la sémantique RTL et les résultats de vérification. En traitant les retours des outils formels (CEX, lacunes de couverture) comme du contenu KG persistant et interrogeable plutôt que comme des sorties transitoires, le système permet un processus de raffinement en boucle fermée. Les auteurs concluent que si la correction sémantique pour le raisonnement complexe reste un défi, ce cadre fournit une base robuste pour une génération de propriétés traçable et ancrée dans la conception. À mesure que les capacités des LLM progresseront, ils seront mieux positionnés pour exploiter le contexte structuré et les traces fournis par ce KG, améliorant ainsi la fiabilité de la vérification formelle automatisée.