TensorEQC: Structure-Aware Equivalence Checking with GF(2) Algebra, Exact Tensor Networks, and Reset Analysis : a Multi-Algorithmic Study of Datapath Verification and Reset-State Dependence

Résumé Technique : TensorEQC – Vérification d'Équivalence Sensible à la Structure

Énoncé du Problème
La vérification d'équivalence (EC) est extrêmement sensible à la représentation d'un circuit. Les différentes structures de circuits — telles que les réseaux riches en XOR, les chaînes de retenue, les multiplicateurs sur corps finis et les multiplicateurs entiers — présentent des propriétés structurelles distinctes qui favorisent différentes approches de vérification. Aucune méthode unique (par exemple, l'algèbre booléenne, les diagrammes de décision ou les réseaux de tenseurs) ne domine universellement tous les types de circuits. De plus, la vérification des circuits séquentiels nécessite de distinguer la dépendance à l'état initial observable de l'incertitude qui se résout dans une limite d'observation spécifique, particulièrement concernant les états de réinitialisation (reset).

Méthodologie
Le document présente TensorEQC, un flux de travail de recherche exécutable conçu comme un portefeuille multi-algorithmique plutôt que comme un solveur monolithique unique. Sa philosophie centrale est qu'un moteur ne doit décharger une obligation de vérification que s'il peut le faire selon sa propre sémantique exacte ; sinon, l'obligation est transmise à un autre moteur.

Le flux de travail se compose de trois composants principaux :

1. Portefeuille Combinatoire : Un pipeline séquentiel de moteurs de vérification qui traite les sorties jusqu'à ce qu'elles soient déchargées ou qu'une limite de ressources soit atteinte. Le pipeline comprend :
   • Hachage Structurel : Établit l'identité des DAG d'expressions sous des primitives supportées (AND, OR, XOR, etc.) avec une normalisation commutative.
   • Simulation : Utilise une simulation compactée avec des motifs aléatoires, tous à zéro et tous à un pour trouver des témoins négatifs (contre-exemples).
   • Formes Normales Algébriques (ANF) : Représente les fonctions booléennes sous forme de polynômes multilinéaires sur GF(2). Il utilise un lemme spécifique pour générer des témoins négatifs exacts à partir de polynômes non nuls.
   • Élimination de Tenseur Relationnel : Représente les portes comme des tenseurs indicateurs booléens. Il effectue l'élimination de variables par disjonction sur le semi-anneau booléen (pour préserver l'existence d'assignations satisfaisantes) plutôt que par sommation GF(2) (qui calcule la parité).
   • ROBDD & Repli Exhaustif : Utilise des diagrammes de décision booléens ordonnés (OBDD) avec des plafonds de nœuds et une énumération exhaustive à faible support comme recourss de dernier ressort.
2. Analyses Tensor Train (TT) : Un module compagnon qui construit des représentations TT exactes à partir de tables de vérité pour mesurer le rang algébrique et tester les fonctions nulles. Il distingue les rangs sur GF(2) et sur les nombres réels, notant que les rangs GF(2) peuvent être nettement plus petits.
3. Analyse de Réinitialisation (Reset) : Un module synchrone utilisant l'auto-composition d'états explicites pour vérifier la dépendance à l'état initial. Il distingue les cas où la dépendance au reset est observable immédiatement des cas où elle disparaît après un nombre spécifique de cycles de « vidage » (flushing).

Principales Contributions

• Intégration de Moteurs Exacts : Le travail démontre une intégration pratique du hachage structurel, de l'algèbre GF(2), des réseaux de tenseurs relationnels et des ROBDD, tout en maintenant des contrats de preuve distincts pour chacun.
• Stratégie Sensible à la Structure : Il fournit des preuves empiriques que l'efficacité de la vérification dépend fortement de la structure du circuit et de l'ordonnancement des variables. Par exemple, les opérandes d'un additionneur entrelacés produisent de faibles rangs tensoriels (≤3), tandis que les opérandes séparés résultent en des rangs élevés (129), rendant ces derniers moins adaptés aux approches basées sur les tenseurs.
• Diagnostics de l'État de Réinitialisation : Il offre une méthode pour distinguer explicitement la véritable dépendance à l'état initial de l'incertitude transitoire dans les conceptions synchrones.
• Validation Reproductible : Le document inclut un nouveau supplément autonome qui valide la construction exacte des tenseurs train GF(2), les mesures de rang et les tests de fonctions nulles sur cinq fonctions à 16 entrées, confirmant la distinction entre l'annulation de parité et les fonctions réellement nulles.

Résultats Expérimentaux
L'étude rend compte de deux ensembles distincts de preuves :

1. Campagne de Portefeuille Historique (v1.0.0) : Ce jeu de données comprend 89 exécutions impliquant des additionneurs à propagation de retenue (ripple adders) de 2 048 bits, des multiplicateurs à base polynomiale de 128 bits et des réseaux affines.
   • Succès : Le flux complet a vérifié avec succès des additionneurs de 2 048 bits (2,87s) et des multiplicateurs GF de 128 bits (0,80s), surpassant les approches basées uniquement sur les BDD dans certains cas (par exemple, les additionneurs de 2 048 bits où les BDD n'ont pas pu résoudre).
   • Limitations : L'approche a atteint des limites de ressources (plafonds de nœuds, plafonds de largeur) sur des additionneurs de 1 024 bits et des réseaux affines de 1 024 entrées. Les résultats de la multiplication entière ont été limités à 10 bits en raison de la croissance de l'ANF et des plafonds de portée des tenseurs.
   • Observation : Le flux complet induit parfois un surcoût par rapport à la sélection directe du moteur optimal, soulignant le compromis entre automatisation et efficacité.
2. Nouveau Supplément Reproductible : Une expérience ciblée sur cinq fonctions de 16 entrées (incluant la parité et la multiplication GF) a confirmé que la construction de tenseurs train exacts et l'analyse de rang sont réalisables pour de petites fonctions. Elle a validé qu'une somme scalaire GF(2) nulle n'implique pas une fonction nulle (annulation de parité), une distinction correctement gérée par le test de zéro du TT.

Signification et Revendications
Le document cadre explicitement sa contribution comme une évaluation technique délimitée plutôt qu'une solution universelle.

• Absence de Supériorité Universelle : Les résultats ne soutiennent pas la thèse selon laquelle les réseaux de tenseurs sont supérieurs à toutes les autres méthodes. Au contraire, ils soutiennent une « stratégie sensible à la représentation » où différents moteurs sont sélectionnés en fonction du domaine mathématique (par exemple, l'algèbre GF pour les fonctions à bas degré sur corps finis, l'élimination relationnelle pour les chaînes de retenue).
• Intégration plutôt que Remplacement : Le résultat central est l'intégration réussie de l'algèbre exacte, de l'élimination relationnelle, des diagrammes de décision et du raisonnement temporel tout en maintenant des contrats de preuve distincts.
• Limites Explicites : L'auteur souligne que l'implémentation actuelle est limitée aux primitives booléennes combinatoires et aux petites machines synchrones. Elle ne prend pas encore en charge le SystemVerilog général, la sémantique sensible à la puissance, le timing asynchrone ou les réseaux de grande échelle industrielle. Le document distingue la « preuve » (satisfaction exacte de l'obligation booléenne encodée) de la « certification » (qui nécessite une chaîne de front-end et de vérificateur de preuve vérifiée, toutes deux notées comme travaux futurs).

En résumé, TensorEQC fournit un cadre pour combiner plusieurs méthodes de vérification exacte afin de gérer une logique hétérogène, démontrant que si aucun moteur n'est universellement optimal, un portefeuille structuré peut vérifier efficacement des classes de circuits spécifiques tout en identifiant clairement ses propres limites.