Couverture ElectroniqueS n°127

Les outils d'analyse hybride, qui combinent preuve formelle et simulation, améliorent significativement la productivité de la vérification. Dans le même temps, ils augmentent le degré de confiance du concepteur dans la bonne fonctionnalité de sa conception. Synopsys explique pourquoi en s'appuyant sur son outil Magellan. Au cours des dernières années, l'industrie du semiconducteur a vécu un déplacement significatif des ressources ingénieur d'une équipe de conception vers les tâches de vérification. Parmi les nouvelles méthodologies mises en place dans cette industrie, le « Design for verification » est en plein développement. Au sein de cette méthodologie, ses partisans soulignent que l'utilisation des assertions est l'élément central pour formaliser les hypothèses faites sur la fonctionnalité du circuit, les contraintes au niveau des interfaces et les propriétés de la conception. Pour utiliser ces assertions, on voit aussi apparaître sur le marché divers outils dits d'analyse formelle au niveau RTL, qu'il s'agisse de technologies strictement statiques (c'est-à-dire sans utilisation auxiliaire de la simulation), de technologies tirant parti des traces de simulations préexistantes (on parle d'outils semi-formels) ou encore de technologies plus avancées comme l'outil Magellan de Synopsys, qui met en &oelig;uvre une solution hybride intégrant outils de preuve formelle et simulation dans un seul environnement (figure 1). L'adoption de ces outils par les utilisateurs est en partie liée au mouvement actuel de disponibilité de langages puissants, tel OVA (Open Vera assertions) et aux efforts de standardisation des assertions SystemVerilog (SVA) ou du langage PSL au sein de l'organisme Accellera (Electronique n° 141, p. 40).Défauts de conception et vrais défautsUn des grands bénéfices de l'emploi de l'analyse formelle hybride RTL est qu'une fois qu'un défaut dans le design est découvert, il s'agit d'un vrai bogue et non d'une faute fantôme (« false negative »). Lorsqu'on intègre la vérification formelle RTL dans le flot de vérification, il y a trois causes possibles de « false negative » : l'analyse formelle commence à partir d'un état initial illégal, la représentation interne du design utilisé par l'analyse formelle est différente de la représentation au niveau RTL visible par l'utilisateur, ou bien le comportement des signaux d'entrée du design n'a pas été saisi correctement.Etat initial illégalLa première génération d'outils de preuve formelle était caractérisée par le fait que l'analyse démarrait de n'importe quel état du design. Une analyse formelle qui démarre d'un état qui est inaccessible par la simulation produit alors des résultats qui sont difficiles à valider, ce qui fait perdre du temps. La technologie hybride mise en &oelig;uvre au sein de Magellan évite cette catégorie de « false negative », car l'outil démarre son analyse formelle seulement à partir d'un état initial qui est atteignable par la simulation (qui fait partie intégrante de l'outil).Validation d'une trace de simulation avec le simulateurAvant de démarrer les algorithmes d'analyse, les outils d'analyse formelle réalisent généralement une transformation du design qui est très semblable à celle réalisée par la synthèse logique. L'analyse formelle opère en fait sur une représentation qui est très similaire à une représentation de la conception au niveau portes logiques et non pas sur le code RTL d'origine. Des fautes fantômes peuvent dès lors se produire sur des cas d'espèce où la représentation interne (dite « modèle formel ») n'est pas fonctionnellement équivalente à la représentation RTL d'origine. De telles inconsistances peuvent survenir dans le cas de listes de sensibilité incomplètes dans du code RTL, ou lorsque le code RTL présente des conditions d'ambiguïtés pour la simulation (« race conditions »).Une telle inconsistance peut se révéler problématique lorsque l'algorithme formel produit une trace de simulation correspondant à une falsification de propriété, par exemple en format VCD. Cette trace montre une transition d'états qui se produit dans le modèle formel mais qui ne peut être expliquée lors du débogage par le concepteur lors de la simulation (éventuellement il peut en conclure qu'il ne s'agit pas d'un vrai bogue du design). Au sein de l'outil Magellan, les violations de propriété détectées par l'analyse formelle sont reproductibles avec le simulateur qui lui est intégré. Le résultat est fourni à l'utilisateur seulement si la simulation est en accord avec l'analyse formelle. Les transitions qui ne peuvent être validées par la simulation sont ensuite automatiquement rejetées après notification à l'utilisateur de possibles inconsistances entre simulation et synthèse. Cette caractéristique offre des gains de productivité notoires, dans la mesure où l'utilisateur ne perd pas de temps à l'analyse de fautes fantômes.Contraintes correctes sur les entréesEn simulation, les contraintes sur les signaux d'entrée servent déjà à vérifier que le design n'est pas soumis à des stimuli illégaux. La génération de stimuli pseudo-aléatoires est réalisée en choisissant des stimuli légaux, à partir d'un ensemble beaucoup plus large, et en appliquant les contraintes sur la génération aléatoire de tests. Des outils tels que le simulateur Vera sont munis de telles capacités (solver de haute performance, générateur de stimuli…).Fournir à l'outil formel des contraintes similaires sur les entrées procure les mêmes bénéfices. La précision des résultats est obtenue en guidant l'exploration de l'espace d'états par l'analyse formelle avec un modèle décrivant les stimuli qui peuvent être légalement appliqués au design.(*) La bibliothèque d'assertions OVA pour « PCI Checker », que Synopsys fournit avec le simulateur VCS, est compatible avec la simulation et les outils formels comme Magellan.

Les méthodes formelles hybrides à la rescousse de la vérification des blocs RTL

Couverture ElectroniqueS n°127

IBM grave les premières puces en 2 nm en abandonnant les FinFET

Zeta, le protocole LPWAN made in China, arrive en Europe

Harting invente le connecteur électronique sur mesure

Les méthodes formelles hybrides à la rescousse de la vérification des blocs RTL

Dans la même rubrique

Couverture ElectroniqueS n°127

IBM grave les premières puces en 2 nm en abandonnant les FinFET

Zeta, le protocole LPWAN made in China, arrive en Europe

Harting invente le connecteur électronique sur mesure