Dans le monde complexe de la conception de puces, s'assurer que les « bits » se déplacent correctement d'un point à un autre ne suffit pas à garantir l'intégrité du système. Vidya Chandran Darbari et Ashish Darbari, de la société Axiomise, proposent une vision analytique suggérant d'emprunter la méthodologie scientifique utilisée en biologie moléculaire pour développer des méthodes plus précises de vérification des systèmes silicium (Silicon Systems Verification).
Contexte contre simple connectivité
La lacune majeure réside dans la croyance selon laquelle la simple présence d'une connexion entre les composants signifie que le système fonctionnera comme prévu. En biologie, il ne suffit pas de savoir qu'il existe une interaction entre deux protéines ; il faut comprendre la concentration, le lieu, l'affinité et le timing. De même, dans l'ingénierie des puces, un contrôleur (Controller) ou une interconnexion (Interconnect) peut fonctionner correctement dans certaines conditions, mais le système peut s'effondrer lorsque les conditions environnantes ou l'ordre des événements changent.
L'article souligne que les ingénieurs doivent faire du contexte (Context) une partie explicite du processus de vérification, en définissant les états adjacents, les ressources disponibles et l'ordre des événements sur lesquels repose toute garantie technique.
Le timing : quand l'interprétation échoue malgré l'intégrité des données
L'analyse pointe un problème technique critique : les données (bits) peuvent arriver parfaitement intactes sans aucune corruption, et pourtant l'interprétation du système peut être erronée en raison d'un défaut de timing. Par exemple, si un contrôleur fusionne des données provenant d'un capteur de caméra et d'un capteur de distance, et qu'il existe un décalage temporel non pris en compte entre les deux lectures, le résultat final sera la représentation d'un état qui n'a jamais existé en réalité.
Par conséquent, les exigences de conception doivent inclure des éléments tels que :
- L'association des horodatages (Timestamp association).
- La fraîcheur des données (Freshness).
- Le décalage admissible (Allowable skew).
Méthodologie d'investigation et vérification formelle (Formal Verification)
Au lieu de simplement tenter de reproduire l'erreur (Reproducing a trace), les auteurs suggèrent d'adopter une méthodologie d'« investigation expérimentale ». Plutôt que de chercher la cause du symptôme (Symptom), il faut poser des questions qui distinguent les différentes hypothèses, telles que : « Que se passe-t-il si l'horloge (Clock) continue de fonctionner ? » ou « L'échec persistera-t-il si le service en aval change ? ».
C'est ici que l'importance de l'approche axée sur le formel (Formal-first approach) apparaît, non pas comme un substitut à la simulation, mais comme un moyen de transformer les mécanismes techniques en obligations architecturales (Architectural Obligations). Cela signifie formuler des exigences précises qui garantissent la non-perte des crédits (Credits), le maintien de l'ordre et la garantie de la restauration de l'état correct lors de la réinitialisation (Reset).
Qu'est-ce qui change concrètement ?
Pour les ingénieurs de conception et de vérification, cette transition signifie passer de la question « Le composant fonctionne-t-il ? » à « Dans quelles conditions le composant garantit-il l'intégrité du système dans son ensemble ? ». Cela nécessite :
- Liaison entre les couches : Ne pas se contenter des données RTL, mais les lier aux données de charge de travail (Workload) et aux mesures physiques (Telemetry).
- Propriété des systèmes transversaux : Lorsqu'une défaillance chevauche la gestion de l'énergie et le contrôle du flux de données, il doit y avoir une responsabilité partagée garantissant l'absence de dépendances circulaires (Circular dependencies).
- Vérification des hypothèses : Ne pas accepter les résultats de simulation réussis sans vérifier si les hypothèses utilisées ont exclu des cas critiques de l'environnement.