Maîtriser la vérification formelle de modules VHDL avec PSL

Lors de la conception VHDL pour des applications FPGA critiques en sécurité, la simple écriture de bancs de test ne suffit pas. Les ingénieurs doivent prouver qu'un module se comporte exactement comme spécifié, exempt d'effets de bord cachés. La vérification formelle fournit cette assurance mathématique.

La vérification formelle comble le fossé entre exigences et implémentation en prouvant que toute séquence d'entrées possible satisfait les propriétés du design. Elle est indispensable pour certifier des dispositifs médicaux, des systèmes avioniques, ou tout domaine où la certification DO‑254 est requise.

Dans cet article invité, Michael Finn Jørgensen – praticien expérimenté en vérification formelle – partage des insights pratiques et des conseils actionnables. L'exemple ci-dessous s'appuie sur le tutoriel familier AXI FIFO Comment faire un AXI FIFO en RAM de bloc en utilisant le handshake ready/valid et démontre comment appliquer PSL à une vraie conception VHDL.

Qu'est-ce que la vérification formelle ?

La vérification formelle (VF) est une méthode systématique, pré-synthèse, qui garantit la correction d'un design pour toutes les combinaisons d'entrées. Contrairement aux bancs de test conventionnels, qui reposent sur des stimuli manuellement conçus, la VF spécifie des propriétés qui doivent être vraies à chaque cycle d'horloge. Un solveur SAT prouve alors exhaustivement que ces propriétés sont satisfaites – ou identifie un contre-exemple si ce n'est pas le cas.

Deux techniques de base alimentent la VF :

• Vérification de modèle bornée (BMC) – vérifie un nombre fini de cycles, en partant de la réinitialisation.
• Preuve par récurrence – vérifie que si un état est valide, tous les états subséquents restent valides. Cela nécessite un ensemble complet de propriétés mais garantit la validité pour un nombre infini de cycles.

Comme le BMC peut être exécuté avec seulement quelques propriétés, c'est souvent la première ligne de défense. La récurrence, bien que plus exigeante, offre une certitude absolue.

Pourquoi utiliser la vérification formelle ?

La VF excelle à découvrir des bogues insaisissables car elle explore automatiquement tout l'espace d'entrées. Lorsqu'une faute est découverte, l'outil produit une forme d'onde concise qui identifie le cycle exact où la propriété a été violée – bien plus facile à déboguer qu'une longue trace de simulation.

Bien que la VF soit un puissant outil de test unitaire, elle ne remplace pas les tests d'intégration artisanaux. À mesure que la taille du module augmente, le temps d'exécution du solveur peut devenir prohibitif. Néanmoins, investir du temps dans la VF réduit l'effort global de débogage et accélère la mise sur le marché.

Écrire des propriétés en PSL

PSL (Property Specification Language) est la lingua franca de la vérification formelle en VHDL. Les propriétés sont généralement stockées dans un fichier .psl séparé que le solveur lit pendant la phase de vérification.

Trois mots-clés PSL décrivent les propriétés :

• assert – garantit qu'une condition sera toujours vraie.
• assume – énonce des hypothèses sur les entrées.
• cover – vérifie si un scénario particulier peut jamais se produire.

Les fichiers PSL peuvent également contenir des déclarations et processus VHDL ordinaires, vous permettant de créer des signaux auxiliaires pour des assertions complexes.

Chaque fichier PSL commence par un bloc vunit qui lie le fichier à une entité spécifique :

vunit INSTANCE_NAME(ENTITY_NAME(ARCHITECTURE_NAME)) { } 

Suivi d'une déclaration d'horloge par défaut :

default clock is rising_edge(clk); 

La syntaxe de propriété ressemble à ceci :

LABEL : assert always {PRECONDITION} |-> {POSTCONDITION} LABEL : assume always {PRECONDITION} |-> {POSTCONDITION} 

Utilisez |=> pour les assertions au cycle suivant :

LABEL : assert always {PRECONDITION} |=> {POSTCONDITION} 

À l'intérieur des conditions, vous pouvez utiliser stable pour forcer qu'un signal ne change pas entre cycles, et chaîner des conditions en utilisant {C1; C2} pour exprimer des contraintes séquentielles.

Installation des outils requis

Les outils commerciaux leaders (ex. ModelSim) supportent la vérification formelle, mais l'édition Student gratuite ne dispose pas de cette fonctionnalité. Heureusement, une pile open-source robuste est disponible pour Linux (et via WSL sur Windows). Le guide suivant utilise Ubuntu 20.04 LTS mais fonctionne sur toute distribution Debian récente.

Prérequis

sudo apt update && sudo apt upgrade 

Installer les bibliothèques de développement essentielles :

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 SymbiYosys

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 Plugin Yosys

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écharger le projet d'exemple

Remplissez le formulaire ci-dessous pour recevoir une archive ZIP contenant la source complète AXI FIFO, le fichier PSL et les scripts de vérification.

Exemple travaillé : Vérification formelle d'un AXI FIFO

Ci-dessous, nous décrivons les catégories de propriétés clés pour une FIFO et illustrons comment les encoder en PSL.

Gestion de la réinitialisation

f_reset : assume {rst}; 

Comme le mot-clé always est omis, cette hypothèse ne s'applique qu'au premier cycle après réinitialisation. Une convention d'étiquetage (f_) aide à identifier les échecs.

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

Notez que des signaux internes tels que count peuvent être référencés car la déclaration vunit inclut le nom de l'architecture.

Signalisation FIFO plein et vide

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

Conformité au protocole AXI

f_in_data_stable : assume always {in_valid and not in_ready and not rst} |=> {stable(in_valid) and stable(in_data)}; f_out_data_stable : assert always {out_valid and not out_ready and not rst} |=> {stable(out_valid) and stable(out_data)}; 

Pour la stabilité du signal ready :

f_out_ready_stable : assume always {out_ready and not out_valid and not rst} |=> {stable(out_ready)}; f_in_ready_stable : assert always {in_ready and not in_valid and not rst} |=> {stable(in_ready)}; 

Ordre FIFO

L'ordre garantit que les écritures antérieures sortent avant les écritures ultérieures. Nous modélisons cela avec des signaux auxiliaires qui se souviennent quand des valeurs de données particulières sont entrées ou sorties.

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 <= '1'; end if; if in_data = f_value_d2 then f_sampled_in_d2 <= '1'; end if; end if; if out_valid then if out_data = f_value_d1 then f_sampled_out_d1 <= '1'; end if; if out_data = f_value_d2 then f_sampled_out_d2 <= '1'; end if; end if; if rst = '1' then f_sampled_in_d1 <= '0'; f_sampled_in_d2 <= '0'; f_sampled_out_d1 <= '0'; f_sampled_out_d2 <= '0'; end if; end if; end process p_sampled; 

Déclarez les valeurs de données comme constantes non contraintes pour que le solveur puisse choisir n'importe quel motif de bits :

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; 

Enfin, encodez les contraintes d'ordre :

f_fifo_ordering_in : assume always {f_sampled_in_d2} |-> {f_sampled_in_d1}; f_fifo_ordering_out : assert always {f_sampled_out_d2} |-> {f_sampled_out_d1}; 

Exécution de la vérification formelle

Créez un script axi_fifo.sby pour l'outil 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 

Lancez la vérification :

sby --yosys ";yosys -m ghdl" -f axi_fifo.sby 

Une exécution réussie affiche :

[axi_fifo_bmc] DONE (PASS, rc=0) 

Ajuster depth au-delà de la profondeur de la FIFO assure que le solveur explore les scénarios de pleine capacité.

Test de mutation

Pour évaluer la complétude de votre ensemble de propriétés, injectez délibérément un petit bogue – comme supprimer la logique qui pilote out_valid – et relancez la VF. Si le solveur signale un échec d'assertion, vous avez vérifié que vos propriétés sont assez expressives pour attraper cette erreur.

Exemple de message d'échec :

Assert failed in axi_fifo: i_axi_fifo.f_out_data_stable 

Ouvrez le trace.vcd généré dans GTKWave pour identifier le cycle exact où la propriété a été violée.

Instructions cover

Les instructions cover sont utiles pour affirmer qu'un scénario particulier est atteignable. Par exemple, pour vérifier que la FIFO peut être remplie puis vidée :

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

Ajustez le script sby pour inclure la tâche cover :

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

Une couverture réussie produit :

Reached cover statement at i_axi_fifo.f_full_to_empty in step 15. 

Changer count = ram_depth-1 en count = ram_depth rendra le cover inatteignable, démontrant la sensibilité de l'outil à la précision des propriétés.

Prochaines étapes

• Introduction au langage PSL
• Fondamentaux de la vérification formelle
• Série vidéo : Démarrer avec la vérification formelle
• Articles avancés de vérification formelle
• Dépôt mini-projet pour la vérification formelle