Coverage-Driven RTL Assertion Generation with Formal Exploration and Neuro-Symbolic Refinement

Dans le monde invisible des micropuces, où des milliards de transistors s'activent et se désactivent pour alimenter tout, des smartphones aux engins spatiaux, une seule erreur cachée peut provoquer la défaillance catastrophique d'un système. Les ingénieurs conçoivent ces puces en utilisant un langage appelé Register Transfer Level, ou RTL, qui décrit comment les données circulent entre les éléments de stockage au fil du temps. Pour garantir que ces conceptions fonctionnent correctement avant d'être fabriquées, les experts en vérification écrivent des « assertions ». Considérez une assertion comme une règle stricte inscrite dans la conception elle-même, une déclaration qui dit : « Si ceci arrive, alors cela doit suivre. » Si la puce viole un jour cette règle, le système déclenche une alarme, révélant un bug qui autrement pourrait passer inaperçu. Pendant des décennies, l'écriture de ces règles a été une tâche lente, manuelle et sujette à l'erreur, exigeant que les ingénieurs devinent quels comportements pourraient mal tourner et écrivent des contrôles spécifiques pour eux. Bien que les ordinateurs aient aidé en extrayant des modèles à partir des simulations de conception existantes, ces méthodes automatisées manquent souvent les scénarios les plus dangereux simplement parce que les tests aléatoires sur lesquels elles reposent ne tombent jamais dessus par hasard.

Une équipe de chercheurs de l'Université des sciences et technologies de Hong Kong (Guangzhou) a développé une nouvelle approche pour résoudre ce problème, baptisant leur système NeuroAssertion. Au lieu de compter sur le hasard pour trouver des bugs, leur méthode traque activement les comportements les plus difficiles à atteindre dans une conception de puce, puis utilise une combinaison d'intelligence artificielle et de logique formelle pour écrire les règles de sécurité nécessaires. Le processus commence par la transformation de la conception afin de faciliter la visualisation des parties testées. Les chercheurs insèrent des marqueurs spéciaux dans le code qui suivent si des conditions spécifiques et difficiles à déclencher sont déjà survenues. Ils utilisent ensuite un puissant moteur mathématique, appelé vérificateur de modèle (model checker), pour forcer la conception à exécuter ces conditions rares. Cela génère un ensemble de cas de test hautement spécifiques qui exposent des comportements que les simulations aléatoires ignoreraient probablement pour toujours. Ces nouvelles traces diversifiées fournissent une base bien plus riche pour l'étape suivante.

Une fois que le système possède ces comportements difficiles à trouver, il passe à la phase de génération. Il utilise une technique appelée synthèse guidée par la syntaxe pour créer des règles de sécurité initiales basées sur les données observées. Cependant, les chercheurs ont reconnu que ce premier passage est rarement parfait. Pour y remédier, ils ont introduit une boucle de raffinement qui agit comme un éditeur rigoureux. Le système mesure la capacité de l'ensemble actuel de règles à détecter des changements dans la conception en injectant des erreurs délibérées et de petite taille, appelées mutants, dans le code. Si les règles ne parviennent pas à attraper un mutant, le système sait exactement quel comportement reste non vérifié. Il fait alors appel à un grand modèle de langage pour proposer une nouvelle règle spécifiquement conçue pour combler cette lacune. Si la règle proposée est logiquement défectueuse, un second modèle de langage ne la rejette pas ; au lieu de cela, il analyse l'erreur et construit un ensemble spécialisé d'instructions, ou une grammaire, pour guider un solveur symbolique afin de réparer la règle. Cela crée un cycle où le système propose, vérifie et corrige les assertions jusqu'à ce qu'elles soient à la fois nombreuses et robustes.

Les résultats de cette approche ont été testés sur sept conceptions de puces différentes, allant de petits circuits d'arbitrage à des cœurs de processeurs complexes. Le nouveau cadre surpasse systématiquement la méthode de pointe précédente, connue sous le nom de SMART, qui repose sur un passage unique d'extraction sans ce raffinement actif. Dans ces expériences, NeuroAssertion a généré environ deux fois plus d'assertions que l'ancienne méthode. Plus important encore, la qualité de ces règles est nettement supérieure. Lorsqu'on mesure leur capacité à détecter des erreurs injectées, le nouveau système atteint environ deux fois la couverture de l'approche traditionnelle. Sur certains benchmarks spécifiques, l'amélioration est encore plus spectaculaire ; par exemple, sur un composant de processeur, la couverture par mutation est passée d'environ six pour cent à plus de trente-deux pour cent. Les chercheurs ont également comparé leur système à une approche directe où un grand modèle de langage est chargé d'écrire des règles sans aucune étape de vérification formelle ou de raffinement. Cette méthode directe a produit beaucoup moins de règles et n'a pas réussi à détecter la plupart des erreurs potentielles, démontant que la simple génération de langage est insuffisante pour cette tâche à enjeux élevés.

En traitant la génération d'assertions comme une boucle continue d'exploration et de raffinement plutôt que comme un événement ponctuel, les chercheurs ont montré qu'il est possible d'automatiser la création de règles de sécurité de haute qualité pour le matériel complexe. Le système ne se contente pas de deviner ; il cherche activement les angles morts d'une conception et utilise un partenariat entre réseaux neuronaux et logique formelle pour les combler. Ce travail suggère que l'avenir de la vérification matérielle réside dans la combinaison de la reconnaissance de formes de l'intelligence artificielle avec la certitude rigoureuse de la preuve mathématique, garantissant que les puces qui alimentent notre monde sont aussi fiables que les ingénieurs qui les conçoivent.