Btor2MLIR: A Format and Toolchain for Hardware Verification

Imaginez que vous soyez un détective essayant de résoudre un mystère, mais que les indices soient écrits dans un code secret que seuls quelques spécialistes peuvent lire. Dans le monde de l'informatique, ce « code secret » est le langage utilisé pour décrire la manière dont les puces informatiques (le matériel) sont censées se comporter. Les ingénieurs construisent ces puces pour faire fonctionner tout, de votre téléphone aux satellites dans l'espace, mais s'il y a ne serait-ce qu'une minuscule erreur dans la conception, tout le système peut planter ou agir de manière étrange. Pour prévenir cela, les chercheurs utilisent les « méthodes formelles » — des outils mathématiques qui agissent comme des correcteurs orthographiques surpuissants pour prouver qu'une conception est parfaite avant même qu'elle ne soit construite.

Pendant longtemps, ces correcteurs orthographiques parlaient des langues différentes. Certains parlaient « BTOR2 », un format populaire dans les compétitions de matériel, tandis que d'autres parlaient « LLVM-IR », un langage utilisé par les compilateurs de logiciels pour vérifier le code. C'était comme avoir un traducteur qui ne savait traduire du français vers l'anglais, et un autre qui parlait de l'espagnol vers l'anglais. Si vous vouliez utiliser un traducteur français pour vérifier un livre espagnol, vous étiez mal partis. Vous deviez construire un tout nouveau traducteur à partir de zéro à chaque fois. Ce document présente un nouveau traducteur magique appelé BTOR2MLIR. Il se situe au milieu, agissant comme un pont universel qui permet aux conceptions matérielles de parler aux outils logiciels sans avoir à réinventer la roue à chaque fois.

Le Problème : Trop de Dialectes, Pas Assez de Ponts

Dans le monde de la vérification matérielle, le format BTOR2 est devenu la norme pour décrire les circuits lors de compétitions comme la Hardware Model Checking Competition (HWMCC). Considérez BTOR2 comme un dialecte très spécifique et efficace pour décrire comment un circuit numérique compte, additionne des nombres ou vérifie des erreurs. Des outils comme BTORMC sont construits spécifiquement pour lire ce dialecte et vérifier si le circuit est sûr.

Cependant, le monde de la vérification logicielle est immense et puissant. Des outils comme SEAHORN sont des experts pour vérifier le code logiciel écrit dans le langage LLVM-IR. Ces outils sont incroyablement matures, ayant été affinés au fil des décennies par des projets massifs comme l'infrastructure de compilateur LLVM. Ils possèdent des fonctionnalités intégrées pour optimiser le code, trouver des bugs et exécuter des simulations.

Le problème est que ces deux mondes communiquent rarement entre eux. Pour utiliser un outil logiciel puissant afin de vérifier une conception matérielle, les chercheurs devaient écrire des traducteurs personnalisés et ponctuels. C'était comme essayer de faire entrer une pièce carrée dans un trou rond à chaque fois. Ces traducteurs devaient souvent réimplémenter des fonctionnalités de base (comme la gestion des nombres ou des boucles) qui existaient déjà dans les outils logiciels, ce qui entraînait un gaspillage d'efforts et des erreurs potentielles.

La Solution : L'Adaptateur Universel (BTOR2MLIR)

Les auteurs de ce document, Joseph Tafese, Isabel Garcia-Contreras et Arie Gurfinkel de l'Université de Waterloo, ont décidé de construire un meilleur pont. Ils ont créé BTOR2MLIR, un nouveau format et une chaîne d'outils basés sur MLIR (Multi-Level Intermediate Representation).

Pour comprendre MLIR, imaginez un jeu de Lego géant et modulaire. Au lieu de construire un château entier à partir de zéro chaque fois que vous voulez construire un type de maison différent, MLIR vous donne un ensemble de briques de base (des dialectes) que vous pouvez assembler. Vous pouvez définir une nouvelle brique « matérielle » qui ressemble et agit exactement comme BTOR2, mais qui s'emboîte directement dans la structure Lego « logicielle » existante.

Voici comment fonctionne leur nouvel outil :

1. Le Traducteur : Ils ont construit un « Dialecte BTOR » à l'intérieur de MLIR. Il s'agit d'une traduction directe et sans perte du format BTOR2. Si vous avez un fichier BTOR2, BTOR2MLIR peut le transformer instantanément en ce dialecte MLIR.
2. Le Pont : Parce que MLIR est conçu pour être extensible, ils ont créé une « passe de conversion » qui transforme leur Dialecte BTOR en le Dialecte LLVM standard. C'est l'étape magique. Elle prend la description matérielle et la transforme en un format que les outils logiciels comme SEAHORN peuvent comprendre nativement.
3. Le Résultat : Le résultat est le LLVM-IR, un langage que les moteurs de vérification logicielle peuvent absorber et analyser.

L'Expérience : Est-ce que cela fonctionne vraiment ?

L'équipe n'a pas seulement construit le pont ; elle a fait traverser un camion pour voir s'il tenait bon. Ils ont pris une collection de benchmarks matériels du monde réel issus de la compétition HWMCC (spécifiquement les ensembles 2020 et 2019) et les ont passés par leur nouvelle chaîne d'outils.

D'abord, ils ont vérifié la correction. Ils ont pris un fichier BTOR2, l'ont converti en leur format MLIR, puis l'ont reconverti en BTOR2. Ils ont comparé le fichier original et le fichier après l'aller-retour. Le résultat ? Ils étaient identiques. Les propriétés de sécurité (les règles que le circuit doit suivre) ont été parfaitement préservées. Même dans les cas délicats où les outils originaux avaient expiré ou manqué de mémoire, leurs versions après l'aller-retour ont parfois résolu le problème, suggérant que la traduction n'a introduit aucune erreur.

Ensuite, ils ont testé la performance. Ils ont connecté leur outil à SEAHORN, un célèbre vérificateur de modèles logiciels, et à BOOLECTOR, un solveur rapide. Ils ont comparé ce nouveau pipeline « hybride » contre BTORMC, l'outil de référence construit spécifiquement pour BTOR2.

Les résultats ont été surprenants et encourageants :

• Vitesse : Dans de nombreux cas, le pipeline hybride (BTOR2MLIR + SEAHORN + BOOLECTOR) était compétitif et parfois plus rapide que l'outil dédié BTORMC. Par exemple, dans la catégorie de benchmarks « 19/mann », l'approche hybride a résolu 44 instances en environ 3 190 secondes, alors que BTORMC a mis plus de temps ou a expiré sur plus d'instances.
• Flexibilité : L'outil a géré avec succès des opérations complexes comme la division et les vecteurs de bits, prouvant que les « briques Lego » de MLIR pouvaient supporter la charge lourde de la logique matérielle.
• Limites : Les auteurs ont été honnêtes sur ce que leur outil ne peut pas encore faire. Il prend actuellement en charge les vecteurs de bits et les tableaux, mais ne gère pas encore les contraintes de « fairness » (équité) et de « justice » (règles sur le comportement d'un système sur un temps infini). De plus, bien qu'il fonctionne bien, il n'a pas complètement écrasé les outils matériels dédiés dans chaque catégorie ; c'était un concurrent sérieux, pas un remplacement total.

Pourquoi cela importe

Le document ne prétend pas avoir résolu toute la vérification matérielle. Au contraire, il suggère une nouvelle façon de penser. En utilisant l'infrastructure mature et robuste du compilateur LLVM (qui alimente les outils pour tout, des jeux vidéo aux navigateurs Web), les chercheurs en matériel peuvent cesser de réinventer la roue.

Les auteurs montrent que vous pouvez prendre une conception matérielle, la traduire dans un langage universel, puis utiliser de puissants outils logiciels existants pour la vérifier. Cela ouvre la porte au prototypage rapide. Si un chercheur souhaite essayer une nouvelle technique de vérification, il n'a pas besoin de construire un tout nouvel moteur ; il lui suffit de brancher son idée dans le framework MLIR.

À l'avenir, l'équipe prévoit de connecter ce pont à encore plus d'outils, comme KLEE (un moteur d'exécution symbolique) et LIBFUZZER (un outil de fuzzing), qui sont actuellement utilisés pour les logiciels mais pourraient révolutionner la façon dont nous trouvons les bugs dans le matériel. Ils prévoient également de générer d'autres formats comme AIGER et SMT-LIB.

En fin de compte, BTOR2MLIR est une preuve de concept qui montre que les murs entre la vérification matérielle et logicielle sont en train de tomber. Cela suggère qu'en parlant un langage commun, nous pouvons rendre notre monde numérique plus sûr, plus rapide et plus facile à construire.