Les grands modèles de langage se rapprochent de l’exécution de l’une des tâches les plus fastidieuses de la vérification de la conception des puces : convertir des spécifications rédigées en langage naturel en un ensemble de propriétés formelles pouvant servir à évaluer la conformité d’une implémentation RTL. Des entretiens menés par Brian Bailey dans Semiconductor Engineering montrent que les outils actuels peuvent produire une première version utile, mais qu’ils sont encore loin de créer un ensemble complet pouvant être adopté sans une révision technique approfondie.
L’importance de cette évolution tient au fait que la rédaction des propriétés constitue depuis des années un goulot d’étranglement de la vérification formelle. Les propriétés SystemVerilog, connues sous le nom d’assertions lorsqu’elles sont intégrées à l’environnement de vérification, servent à décrire les relations logiques et temporelles entre les signaux, comme le comportement de la réinitialisation, les handshakes, les conditions one-hot et les contrôles de sécurité de base. Lorsque ces propriétés sont complètes et précises, elles peuvent servir à comparer le comportement d’une implémentation RTL à la spécification, indépendamment de la manière dont la conception a été construite.
Que peuvent faire les outils aujourd’hui ?
Un outil fondé sur un grand modèle de langage peut lire un document de spécification, une norme de protocole ou même des commentaires intégrés au RTL, puis proposer une première version de propriétés SVA. Ashish Darbari, directeur général d’Axiomise, affirme que cet usage est plus facilement applicable lorsque les spécifications reposent sur des normes stables qui évoluent peu. Dans ce cas, l’outil réduit la part répétitive de la rédaction du code initial, au lieu de prendre en charge l’ensemble du processus de vérification.
Certaines approches tentent d’améliorer la précision des modèles en créant un knowledge graph, c’est-à-dire un graphe de connaissances qui stocke les entités et les relations entre elles. Les nœuds peuvent inclure un signal, un module, une exigence ou un port, tandis que les arêtes décrivent des relations telles que « pilote », « réinitialise » et « répond à ». Au lieu de récupérer des extraits de texte qui semblent liés à la demande, le système peut se référer à des faits et à des liens précis, ce qui réduit le risque d’inventer le nom d’un signal ou de mal comprendre une relation entre des composants de la conception. La source mentionne dans ce contexte une étude intitulée RAG-SVA in the Landscape of LLM-Based Assertion Generation, réalisée par Cohen et Chibani.
Le problème commence avant l’intelligence artificielle
L’outil ne peut pas extraire ce qui n’a pas été écrit ou tranché au préalable. Ravindra Aneja, directeur de l’ingénierie des applications chez Synopsys, affirme que la spécification idéale n’a pas été disponible au cours des trois dernières décennies ; le développement commence souvent avant l’achèvement de la documentation, et certains projets, notamment les conceptions dérivées ou ceux dont les exigences évoluent en cours de travail, peuvent ne disposer d’aucune spécification complète.
Ce problème ne concerne pas uniquement la formulation, mais aussi la gestion des changements. L’équipe marketing peut ajouter une fonctionnalité ou modifier une exigence existante, et les équipes de conception et de vérification doivent déterminer l’impact de ce changement. Abhi Kolpekwa, vice-président senior et directeur général chez Siemens EDA, estime que la conversion de la spécification en propriétés nécessite une « intelligence contextuelle » capable de suivre l’historique et le contexte des changements, et non un agent qui génère à chaque fois un nouveau texte.
Le risque d’une fausse confiance
L’une des principales limites de l’approche actuelle est qu’une propriété peut être syntaxiquement correcte, être compilée et être prouvée par les outils de vérification, sans pour autant tester réellement le comportement visé. Darbari avertit qu’une propriété faible ou vacuous peut être facilement prouvée parce qu’elle autorise de nombreux comportements, parce qu’elle utilise le mauvais signal ou parce qu’elle contient une condition antérieure manquante ou excessivement restrictive. Ainsi, une « preuve verte » ne signifie pas que la conception est exempte d’erreurs ; la preuve n’est pas plus solide que la propriété qui a été prouvée.
La source ajoute que les modèles tendent à être plus performants en matière de couverture structurelle et de syntaxe que dans la compréhension de l’intention architecturale et de la raison d’être de la règle. Une lecture imprécise de la spécification par le modèle peut donc se transformer en un élément qui semble formel et rigoureux, tout en dissimulant une lacune dans les exigences. Si cette lacune se propage à des activités telles que la FMEDA, aux dossiers de sécurité ou aux éléments de preuve de certification associés à l’ISO 26262 et à l’ISO 21434, son impact peut dépasser largement le projet de vérification initial.
La question de la séparation entre la conception et la vérification se pose également. Kaye Mao, responsable de la conception des produits chez Normal Computing, souligne la nécessité de limiter les documents du projet auxquels les agents peuvent accéder, car autoriser l’agent à utiliser la conception elle-même pour générer des cas de test pourrait compromettre l’indépendance du processus de vérification.
Qu’est-ce qui change concrètement ?
L’intelligence artificielle peut réduire, selon Darbari, le temps de préparation des premières versions de plusieurs jours à quelques minutes, mais elle peut multiplier le travail ultérieur. Chaque propriété générée doit être vérifiée par rapport à la spécification, faire l’objet d’une analyse de couverture et d’un test de vacuity, puis être examinée au regard de sa relation avec les signaux de conception ; les échecs peuvent également nécessiter une analyse des chronogrammes. Si le nombre de propriétés est multiplié par dix tandis que le niveau de contrôle requis pour chacune reste le même, la charge de révision peut dépasser le gain obtenu grâce à la génération rapide.
Du point de vue de certi.news, le véritable changement ne consiste pas à remplacer l’ingénieur de vérification, mais à déplacer le centre de gravité de la rédaction des propriétés vers leur évaluation et le suivi de leur source. Darbari recommande de traiter les propriétés générées comme des brouillons et non comme des résultats approuvés, et de créer une étape de révision avant leur intégration dans la regression suite. Il convient également d’enregistrer la source de chaque propriété : le paragraphe de la spécification, l’exigence ou l’élément RTL qui l’a produite, afin que l’ingénieur puisse vérifier la conformité.
Cette approche peut abaisser le seuil d’accès à la formal verification pour les ingénieurs de vérification qui souhaitent l’utiliser, affirme Yaron Ilani, ingénieur en solutions de vérification chez Normal Computing. Elle ne tranche toutefois pas la question du retour sur investissement. Kaye Mao estime que le temps consacré à vérifier les résultats de l’agent doit être comptabilisé dans le coût, tandis qu’Arvind Srinivasan, responsable des ingénieurs solutions chez Normal Computing, souligne que le passage à l’échelle ne dépend pas uniquement du calcul, mais aussi de l’exhaustivité des données et du coût de la révision humaine.
En conclusion, les grands modèles de langage sont désormais capables d’accélérer la partie automatique et répétitive de la formulation des propriétés, mais ils n’ont pas encore résolu les problèmes de complétude de la spécification et de compréhension de l’intention de conception. La valeur de ces outils restera liée à la présence d’un ingénieur qui comprend la conception et à l’existence de mécanismes indépendants permettant de mesurer la couverture et de détecter les propriétés vacuous ou inappropriées, plutôt qu’au nombre de propriétés que le modèle peut produire.