Vérification formelle en VHDL avec PSL

Lors de la conception de VHDL pour des applications FPGA critiques pour la sécurité, il ne suffit pas d'écrire des bancs de test au mieux. Vous devez présenter la preuve que le module fonctionne comme prévu et sans effets secondaires indésirables.

Les techniques de vérification formelle peuvent vous aider à faire correspondre une exigence à un test, prouvant que votre module VHDL est conforme à la spécification. C'est un outil essentiel pour vérifier les applications de soins de santé ou obtenir la certification DO-254 pour les solutions FPGA aéroportées.

Pour démystifier la vérification formelle, VHDLwhiz fait appel à Michael Finn Jørgensen pour écrire ce billet invité. Michael a une expérience considérable sur le sujet et partage de nombreux conseils sur sa page GitHub.

L'appareil testé dans l'exemple téléchargeable de cet article provient du didacticiel existant :
Comment créer une FIFO AXI en bloc RAM à l'aide de la poignée de main prête/valide

Je vais laisser Michael prendre le relais et vous expliquer la vérification formelle dans le reste de cet article de blog.

Qu'est-ce qu'une vérification formelle ?

Le but de la vérification formelle (FV) est de s'assurer que votre module fonctionne comme prévu !

FV est quelque chose que vous faites dans le cadre de votre processus de développement avant de synthétiser votre module. Cela s'appelle parfois "Vérification des propriétés", ce qui est une meilleure description, je pense.

Dans FV vous spécifiez les propriétés votre module doit avoir, puis l'outil (appelé "Satisfiability Solver") va prouver que votre module satisfait les propriétés pour toutes les séquences possibles d'entrées .

En d'autres termes, l'outil recherchera toute transition à partir d'un valide état (où toutes les propriétés sont satisfaites) à un état invalide état (où une ou plusieurs propriétés sont violées). S'il n'y a pas une telle transition, c'est-à-dire qu'il n'y a aucun moyen de passer à un état invalide, il a été prouvé que les propriétés sont toujours satisfaites.

Le défi dans FV est d'exprimer les propriétés de votre module dans un langage que l'outil peut comprendre.

La vérification formelle est une alternative aux bancs de test écrits manuellement. L'objectif de la vérification formelle et des bancs de test manuels est d'éliminer les bogues de la conception, mais la vérification formelle le fait en examinant les propriétés et en générant automatiquement de nombreux bancs de test différents.

Les outils utilisent deux méthodes différentes :

Vérification du modèle limité (BMC) . Commence à partir de la réinitialisation et examine un nombre fixe de cycles d'horloge.
Épreuve d'induction . Commence à partir d'un état valide arbitraire et vérifie que tous les états suivants sont également valides.

La preuve par induction est plus difficile à satisfaire car elle nécessite tout propriétés à indiquer, alors que BMC peut être exécuté avec seulement quelques propriétés et donner des résultats utiles.

Pourquoi utiliser une vérification formelle ?

La vérification formelle est très efficace pour détecter les bogues difficiles à trouver ! En effet, la vérification formelle recherche automatiquement tout l'espace des entrées possibles.

Cela contraste avec l'écriture traditionnelle sur banc d'essai qui nécessite la fabrication manuelle de stimuli. Il est pratiquement impossible d'explorer l'ensemble de l'espace d'état à l'aide de bancs de test écrits manuellement.

De plus, lorsque la vérification formelle trouve un bogue, elle génère une forme d'onde très courte montrant le bogue et le fait beaucoup plus rapidement que lors de l'exécution d'une simulation basée sur un banc de test écrit manuellement. Cette forme d'onde courte est beaucoup plus facile à déboguer qu'une forme d'onde très longue qui résulte généralement de la simulation.

Cependant, la vérification formelle ne remplace pas l'écriture de testbench. D'après mon expérience, la vérification formelle est bien adaptée aux tests unitaires, alors qu'il est préférable de faire des tests d'intégration à l'aide de bancs de test fabriqués à la main. En effet, le temps d'exécution de la vérification formelle augmente de façon exponentielle avec la taille du module.

Il existe en effet une courbe d'apprentissage associée à la vérification formelle, mais cela en vaut la peine, et j'espère que cet article de blog vous aidera à surmonter cette courbe d'apprentissage. Vous terminerez votre design plus tôt et il y aura moins de bugs !

Comment écrire des propriétés dans PSL

Lors de la vérification formelle, vous devez exprimer les propriétés de votre module à l'aide du langage de spécification de propriété (PSL). Les propriétés sont généralement situées dans un fichier séparé avec la terminaison .psl , et ce fichier est utilisé uniquement lors de la vérification formelle.

Dans cette section, je décrirai les principales fonctionnalités du langage PSL en termes généraux, et dans une section ultérieure, je vous présenterai un exemple spécifique.

Il y a trois instructions dans PSL :

assert
assume
cover

Vous connaissez peut-être déjà le mot-clé assert lors de l'écriture des bancs de test. Ce même mot-clé est également utilisé dans PSL, mais avec une syntaxe légèrement différente. Le assert mot-clé est utilisé pour décrire les propriétés que ce module promet d'être toujours satisfaites. En particulier, le assert mot-clé est appliqué aux sorties du module, ou éventuellement à l'état interne également.

Le assume mot-clé est utilisé pour décrire toutes les exigences que ce module impose aux entrées. En d'autres termes, le assume mot-clé est appliqué aux entrées dans le module.

Le cover mot-clé est utilisé pour décrire des propriétés qui doivent pouvoir être atteintes d'une certaine manière.

Vous pouvez également écrire du code VHDL normal dans le fichier PSL, y compris des déclarations de signal et des processus (à la fois synchrones et combinatoires).

La première ligne du fichier PSL doit être

vunit INSTANCE_NAME(ENTITY_NAME(ARCHITECTURE_NAME)) {

Ici ENTITY_NAME et ARCHITECTURE_NAME reportez-vous au module que vous vérifiez. Le INSTANCE_NAME peut être tout ce que vous voulez. Le fichier doit se terminer par une accolade fermante :} .

La ligne suivante dans le .psl le fichier doit être :

default clock is rising_edge(clk);

Cela évite d'avoir à se référer fastidieusement au signal d'horloge dans chacune des déclarations de propriété.

La syntaxe du assert et assume déclarations est :

LABEL : assert always {PRECONDITION} |-&gt; {POSTCONDITION}
LABEL : assume always {PRECONDITION} |-&gt; {POSTCONDITION}

Cette déclaration se lit comme suit :Si le PRECONDITION tient (dans n'importe quel cycle d'horloge) puis le POSTCONDITION doit être satisfait dans le même cycle d'horloge.

Il existe un autre formulaire couramment utilisé :

LABEL : assert always {PRECONDITION} |=&gt; {POSTCONDITION}

Cette déclaration se lit comme suit :Si le PRECONDITION tient (dans n'importe quel cycle d'horloge) puis le POSTCONDITION doit être satisfait dans le prochain cycle d'horloge.

Les deux formes sont largement utilisées.

Dans le PRE- et POST-CONDITIONS , vous pouvez utiliser le mot clé stable . Ce mot-clé signifie :La valeur dans ceci cycle d'horloge est le même que la valeur dans le précédent cycle d'horloge.

Dans le PRE- et POST-CONDITIONS , vous pouvez également utiliser des séquences, en écrivant comme suit :

{CONDITION_1 ; CONDITION_2}

Cela signifie que CONDITION_1 doit être satisfait de ceci cycle d'horloge et que CONDITION_2 doit être satisfait le suivant cycle d'horloge.

La déclaration de couverture a la syntaxe suivante :

LABEL : cover {CONDITION}

Nous verrons de nombreux exemples de toutes ces déclarations dans l'exemple travaillé plus loin dans ce blog.

Installation des outils requis

La vérification formelle est prise en charge par les principaux fournisseurs d'outils, y compris ModelSim. Malheureusement, l'édition étudiante de ModelSim ne prend PAS en charge la vérification formelle. En effet, vous obtenez l'erreur suivante :

Donc, pour utiliser ModelSim pour une vérification formelle, il faut une licence payante.

Au lieu de cela, il existe des outils open source (gratuits) qui vous permettent d'effectuer une vérification formelle. Dans cette section, je vais vous guider tout au long du processus d'installation de ces outils.

Ce guide suppose que vous utilisez une plate-forme Linux. Si vous êtes sur une plate-forme Windows, je vous recommande d'utiliser le sous-système Windows pour Linux (WSL). Le guide suivant est vérifié avec Ubuntu 20.04 LTS.

Prérequis

Tout d'abord, nous devons mettre à jour le système pour obtenir les derniers correctifs :

sudo apt update
sudo apt upgrade

Ensuite, nous devons installer des packages de développement supplémentaires :

sudo apt install build-essential clang bison flex libreadline-dev \
                 gawk tcl-dev libffi-dev git mercurial graphviz   \
                 xdot pkg-config python python3 libftdi-dev gperf \
                 libboost-program-options-dev autoconf libgmp-dev \
                 cmake gnat gtkwave

Yosys et al.

git clone https://github.com/YosysHQ/yosys
cd yosys
make
sudo make install
cd ..

git clone https://github.com/YosysHQ/SymbiYosys
cd SymbiYosys
sudo make install
cd ..

git clone https://github.com/SRI-CSL/yices2
cd yices2
autoconf
./configure
make
sudo make install
cd ..

GHDL et al.

Il existe des binaires pré-emballés pour GHDL, mais je recommande de télécharger les derniers fichiers source et de les compiler comme suit :

git clone https://github.com/ghdl/ghdl
cd ghdl
./configure --prefix=/usr/local
make
sudo make install
cd ..

git clone https://github.com/ghdl/ghdl-yosys-plugin
cd ghdl-yosys-plugin
make
sudo make install
cd ..

Téléchargez l'exemple de projet

La section suivante de cet article vous guide dans la mise en œuvre de la vérification formelle pour un projet VHDL existant. Vous pouvez télécharger le code complet en saisissant votre adresse e-mail dans le formulaire ci-dessous.

Exemple concret avec vérification formelle

La section suivante décrira comment vérifier formellement le module axi_fifo dont il a été question précédemment sur ce blog.

Pour commencer la vérification formelle, nous devons nous demander quelles sont les propriétés du FIFO ? J'ai identifié quatre catégories de propriétés :

Gestion de la réinitialisation :que le module se réveille dans un état bien défini après la réinitialisation.
Signalisation FIFO plein et vide :ceci vérifie que le FIFO indique correctement les conditions plein et vide.
Protocole AXI :Que le module satisfait aux exigences de la poignée de main AXI valide/prêt.
Ordre FIFO :que le FIFO ne supprime pas/duplique/réorganise les éléments qui le traversent.

Je vais discuter de chacune de ces propriétés dans ce qui suit.

Gestion de la réinitialisation

Tout d'abord, nous déclarons que le module s'attend à ce que la réinitialisation soit affirmée pendant un cycle d'horloge :

f_reset : assume {rst};

Notez ici l'absence du mot clé always . Sans le always mot-clé, l'instruction n'est valable que pour le tout premier cycle d'horloge.

Il est d'usage (et très utile) de donner une étiquette à chaque énoncé formel. Lors de l'exécution de la vérification formelle, l'outil se référera à ces étiquettes lors du signalement des échecs. J'utilise la convention de faire précéder toutes ces étiquettes avec f_ .

Ensuite on précise que la FIFO doit être vide après reset :

f_after_reset_valid : assert always {rst} |=&gt; {not out_valid};
f_after_reset_ready : assert always {rst} |=&gt; {in_ready};
f_after_reset_head  : assert always {rst} |=&gt; {count = 0};

Notez qu'il est possible de référencer interne signaux dans le module et pas seulement les ports. Ici, nous faisons référence à count , qui est le niveau de remplissage actuel, c'est-à-dire le nombre d'éléments actuellement dans la FIFO. C'est possible car nous nous référons au nom de l'architecture dans la première ligne du fichier PSL.

Nous pourrions également avoir un processus séparé dans le fichier PSL comptant le nombre d'éléments entrant et sortant du FIFO. Bien que cela soit préférable, je vais utiliser le signal de comptage interne pour que ce billet de blog soit court et concis.

Signalisation FIFO plein et vide

La façon dont le FIFO AXI signale plein et vide est avec le out_valid et in_ready signaux. Le out_valid signal est affirmé chaque fois que le FIFO n'est pas vide, et le in_ready signal est affirmé chaque fois que le FIFO n'est pas plein. Vérifions ces propriétés :

f_empty : assert always {count = 0} |-&gt; {not out_valid};
f_full : assert always {count = ram_depth-1} |-&gt; {not in_ready};

Protocole AXI

La poignée de main AXI valide/prête indique que le transfert de données ne se produit que lorsque valid et ready s'affirment simultanément. Une erreur typique lors de l'utilisation de ce protocole est d'affirmer valide (et les données d'accompagnement) et de ne pas vérifier prêt. En d'autres termes, si valid est affirmé et ready n'est pas, alors valid doit rester affirmée le cycle d'horloge suivant, et les données doivent rester inchangées. Cela s'applique à la fois aux données entrant dans le FIFO et aux données sortant du FIFO. Pour les données entrant dans le FIFO, nous utilisons le assume mot-clé, et pour les données sortant du FIFO, on utilise le assert mot-clé.

f_in_data_stable : assume always
   {in_valid and not in_ready and not rst} |=&gt;
   {stable(in_valid) and stable(in_data)};

f_out_data_stable : assert always
   {out_valid and not out_ready and not rst} |=&gt;
   {stable(out_valid) and stable(out_data)};

Notez ici l'utilisation du stable mot-clé en combinaison avec le |=> opérateur. Ces instructions font référence à deux cycles d'horloge consécutifs. Au premier cycle d'horloge, il vérifie si valid est affirmé et ready n'est pas affirmé. Puis au cycle d'horloge suivant (deuxième) (indiqué par le |=> opérateur), les valeurs de valid et data doit être le même que le cycle d'horloge précédent (c'est-à-dire le premier).

Deuxièmement, pour le protocole AXI, nous exigeons que le ready signal est stable. Cela signifie que si le FIFO peut accepter des données (ready est affirmé) mais aucune donnée n'est entrée (valid n'est pas affirmé), puis au cycle d'horloge suivant ready doit rester affirmé.

f_out_ready_stable : assume always
   {out_ready and not out_valid and not rst} |=&gt;
   {stable(out_ready)};

f_in_ready_stable : assert always
   {in_ready and not in_valid and not rst} |=&gt;
   {stable(in_ready)};

Ordre FIFO

Une autre propriété importante d'un FIFO est que les données ne sont pas dupliquées/supprimées/permutées. Exprimer cette propriété en PSL est assez complexe, et c'est la partie la plus difficile de cette vérification formelle. Parcourons attentivement cette propriété étape par étape.

Nous pouvons dire en général que si des données D1 entrent dans le FIFO avant d'autres données D2, alors du côté de la sortie, les mêmes données D1 doivent quitter le FIFO avant D2.

Pour exprimer cela en PSL, nous avons besoin de quelques signaux auxiliaires :f_sampled_in_d1 , f_sampled_in_d2 , f_sampled_out_d1 , et f_sampled_out_d2 . Ces signaux sont effacés lors de la réinitialisation et affirmés chaque fois que D1 ou D2 entre ou quitte le FIFO. Une fois affirmés, ces signaux restent affirmés.

Nous exprimons donc la propriété d'ordre FIFO en deux parties :d'abord une hypothèse qu'une fois que D2 entre dans le FIFO, alors D1 a déjà entré :

f_fifo_ordering_in : assume always
   {f_sampled_in_d2} |-&gt;
   {f_sampled_in_d1};

Et deuxièmement une affirmation qu'une fois que D2 quitte le FIFO, alors D1 est déjà parti auparavant :

f_fifo_ordering_out : assert always
   {f_sampled_out_d2} |-&gt;
   {f_sampled_out_d1};

Nous devons encore déclarer et remplir les signaux d'échantillonnage référencés ci-dessus. Nous procédons comme suit pour les signaux d'échantillonnage d'entrée :

signal f_sampled_in_d1  : std_logic := '0';
signal f_sampled_in_d2  : std_logic := '0';

...

p_sampled : process (clk)
begin
   if rising_edge(clk) then
      if in_valid then
         if in_data = f_value_d1 then
            f_sampled_in_d1 &lt;= '1';
         end if;
         if in_data = f_value_d2 then
            f_sampled_in_d2 &lt;= '1';
         end if;
      end if;

      if out_valid then
         if out_data = f_value_d1 then
            f_sampled_out_d1 &lt;= '1';
         end if;
         if out_data = f_value_d2 then
            f_sampled_out_d2 &lt;= '1';
         end if;
      end if;

      if rst = '1' then
         f_sampled_in_d1  &lt;= '0';
         f_sampled_in_d2  &lt;= '0';
         f_sampled_out_d1 &lt;= '0';
         f_sampled_out_d2 &lt;= '0';
      end if;
   end if;
end process p_sampled;

Ici, nous faisons référence à deux autres signaux, f_value_d1 et f_value_d2 . Ils contiennent les valeurs de données D1 et D2. Ces signaux peuvent contenir n'importe quel élément arbitraire valeurs, et il existe une manière spéciale de l'indiquer à l'outil de vérification formelle :

signal f_value_d1 : std_logic_vector(ram_width - 1 downto 0);
signal f_value_d2 : std_logic_vector(ram_width - 1 downto 0);
attribute anyconst : boolean;
attribute anyconst of f_value_d1 : signal is true;
attribute anyconst of f_value_d2 : signal is true;

Le anyconst l'attribut est reconnu par l'outil de vérification formelle. Il indique que l'outil peut insérer n'importe quelle valeur constante à sa place.

Avec ce qui précède, nous avons spécifié les propriétés du FIFO.

Exécution d'une vérification formelle

Avant de pouvoir exécuter l'outil de vérification formelle, nous devons écrire un petit script axi_fifo.sby :

[tasks]
bmc

[options]
bmc: mode bmc
bmc: depth 10

[engines]
smtbmc

[script]
ghdl --std=08 -gram_width=4 -gram_depth=8 axi_fifo.vhd axi_fifo.psl -e axi_fifo
prep -top axi_fifo

[files]
axi_fifo.psl
axi_fifo.vhd

La rubrique [tasks] déclare que nous voulons Bounded Model Checking. La rubrique [options] spécifie que BMC doit fonctionner pendant 10 cycles d'horloge. La valeur par défaut est 20. La section [engines] choisit lequel des différents solveurs utiliser. Il peut y avoir des différences dans la vitesse d'exécution des différents moteurs possibles, en fonction de votre conception particulière. Pour l'instant, laissez cette valeur inchangée.

Le [script] section est la partie intéressante. Nous spécifions ici la norme VHDL (2008), les valeurs des génériques, les fichiers à traiter et le nom de l'entité de niveau supérieur. Enfin, le [files] section contient à nouveau les noms de fichiers.

Avec ce script prêt, nous pouvons exécuter la vérification formelle réelle à l'aide de cette commande :

sby --yosys &quot;;yosys -m ghdl&quot;; -f axi_fifo.sby

L'exécution de l'outil de vérification formelle se termine par la déclaration sans cérémonie :

[axi_fifo_bmc] DONE (PASS, rc=0)

Et cela signifie simplement que toutes les propriétés que nous avons spécifiées sont satisfaites de toutes les entrées arbitraires jusqu'à 10 cycles d'horloge. L'augmentation de la profondeur entraîne des temps d'exécution plus longs pour le solveur. Cependant, notez que la profondeur est supérieure à la profondeur du FIFO, ce qui signifie que le BMC rencontrera une situation FIFO complète pour certaines séquences d'entrée. Si nous avions seulement choisi, disons, 5 cycles d'horloge, la vérification formelle ne rencontrerait jamais un FIFO plein et n'attraperait aucun bogue lié à cela.

Il est possible de prouver que les propriétés sont satisfaites pour tous cycles d'horloge à l'aide de la preuve d'induction. Cependant, cela nécessite plus de travail pour écrire les propriétés. Le défi est que jusqu'à présent, nous venons d'écrire quelques Propriétés. Mais pour l'induction, nous devons spécifier tous propriétés (ou du moins suffisamment nombreuses). Cela prendrait beaucoup de temps, donc à la place, je vais discuter d'une stratégie alternative pour augmenter notre confiance.

Mutation

Alors maintenant, nous avons décrit certaines des propriétés que le axi_fifo module doit satisfaire, et notre outil confirme rapidement ces propriétés, c'est-à-dire prouve qu'elles sont satisfaites. Mais nous pouvons toujours avoir ce sentiment de malaise :sommes-nous sûrs qu'il n'y a pas de bogues ? Avons-nous vraiment exprimé toutes les propriétés du axi_fifo module ?

Pour aider à répondre à ces questions et à avoir plus confiance dans l'exhaustivité des propriétés spécifiées, nous pouvons appliquer une technique appelée mutation :Nous apportons délibérément une petite modification à l'implémentation, c'est-à-dire que nous introduisons délibérément un bogue, puis voyons si la vérification formelle détectera le bogue !

Un tel changement pourrait être de supprimer une partie de la logique contrôlant le out_valid signal. Par exemple, nous pourrions commenter ces trois lignes :

if count = 1 and read_while_write_p1 = '1' then
  out_valid_i &lt;= '0';
end if;

Lorsque nous exécutons la vérification formelle maintenant, nous obtenons un échec avec le message

Assert failed in axi_fifo: i_axi_fifo.f_out_data_stable
Writing trace to VCD file: engine_0/trace.vcd

À l'aide de l'outil GTKwave, nous pouvons afficher la forme d'onde qui l'accompagne, et elle se présente comme suit :

Ici on voit qu'à 40 ns, le out_valid le signal devrait aller à zéro, mais ce n'est pas le cas. L'assertion qui échoue est à 50 ns, où out_valid reste élevé, mais le out_data changements de signal, indiquant des données en double. Les données dupliquées n'ont pas été réellement transmises dans cette trace particulière car out_ready est faible à 40 ns, mais la vérification formelle détecte néanmoins le bogue.

Déclaration de couverture

Passons enfin à une application différente de l'outil de vérification formelle :la déclaration de couverture. Le but de la déclaration de couverture est de vérifier s'il existe une séquence d'entrées qui satisfait une propriété particulière. Puisque nous avons affaire à un FIFO, voyons si nous pouvons le remplir complètement puis le vider à nouveau. Cela peut être exprimé dans une seule déclaration de couverture :

f_full_to_empty : cover {
   rst = '1';
   rst = '0'[*];
   rst = '0' and count = ram_depth-1;
   rst = '0'[*];
   rst = '0' and count = 0};

C'est une bouche pleine ! Notez les points-virgules dans le {} . Pour plus de lisibilité, j'ai placé chaque section sur une ligne distincte. Cette déclaration de couverture se lit comme suit :Recherchez une séquence d'entrées qui satisfait :

La réinitialisation est affirmée pour un cycle d'horloge.
N'importe quel nombre de cycles d'horloge (où la réinitialisation n'est pas affirmée) peut alors passer.
Un cycle d'horloge où la réinitialisation n'est pas affirmée et le FIFO est plein.
N'importe quel nombre de cycles d'horloge (où la réinitialisation n'est pas affirmée) peut alors passer.
Un cycle d'horloge où la réinitialisation n'est pas affirmée et la FIFO est vide.

Donc la syntaxe [*] signifie répéter (zéro ou plusieurs fois) la condition précédente. A la ligne 3, on aurait pu supprimer la condition rst = '0' devant [*] . Les résultats seront les mêmes. La raison en est que le vérificateur formel essaiera de trouver le plus court séquence qui satisfait l'instruction de couverture, et affirmer la réinitialisation tout en remplissant le FIFO ne fera que retarder cela. Cependant, lors du vidage du FIFO à la ligne 5, il est essentiel que la réinitialisation ne soit pas affirmée.

Pour exécuter le vérificateur formel maintenant, nous devons apporter une petite modification au script axi_fifo.sby . Remplacez les sections du haut par les suivantes :

[tasks]
bmc
cover

[options]
bmc: mode bmc
bmc: depth 10
cover: mode cover

Maintenant, le solveur exécutera le BMC, puis exécutera l'analyse de la couverture. Dans la sortie, vous verrez ces deux lignes :

Reached cover statement at i_axi_fifo.f_full_to_empty in step 15.
Writing trace to VCD file: engine_0/trace5.vcd

Cela signifie que la déclaration de couverture peut en effet être satisfaite d'une séquence de 15 cycles d'horloge, et le solveur a généré une forme d'onde spécifiquement pour cette déclaration de couverture :

Ici on voit à 80 ns la FIFO est pleine et in_ready est désaffirmé. Et à 150 ns le FIFO est vide et out_valid est désaffirmé. Notez comment pendant la période 30 ns à 80 ns que out_ready est tenu bas. Cela est nécessaire pour s'assurer que le FIFO se remplit.

Si on remplace la condition count = ram_depth-1 avec count = ram_depth , la déclaration de couverture ne peut pas être satisfaite. L'outil signale alors une erreur.

Unreached cover statement at i_axi_fifo.f_full_to_empty.

Ainsi, le message d'erreur contient l'étiquette de la déclaration de couverture qui échoue. C'est une des raisons pour lesquelles les étiquettes sont si utiles ! Nous interprétons l'erreur ci-dessus comme indiquant que le FIFO ne peut jamais contenir ram_depth nombre d'éléments. C'est exactement comme indiqué dans le billet de blog AXI FIFO d'origine.

Où aller à partir d'ici

Une introduction au langage PSL
Une introduction à la vérification formelle
Une série de petites vidéos pour démarrer avec la vérification formelle
Un blog lié à la vérification formelle
Une série d'articles avec des sujets plus avancés en vérification formelle
Une collection de petits exemples utilisant la vérification formelle

Premiers pas avec VUnit Utilisation de l'analyseur logique intégré (ILA) et de l'entrée/sortie virtuelle (VIO)

VHDL