Dans cet article, on se propose d’aborder la méthode de vérification formelle pour le VHDL. Cette méthode a récemment été rendue possible avec GHDL et Yosys grâce au projet d’extension ghdl-yosys-plugin qui fait le lien entre les deux logiciels. Nous allons également découvrir le langage PSL (Properties Specification Langage) qui permet de décrire efficacement les propriétés utilisées en preuve formelle. Le support du PSL ayant été ajouté dans GHDL, il sera possible de l’utiliser librement en VHDL.
Les FPGA sont très utilisés dans des domaines industriels critiques comme l’aéronautique, l’espace, le médical ou le ferroviaire. Ces domaines requièrent des méthodes de conception très exigeantes quant à la qualité du code produit. En plus de relectures par des tiers et le respect du cycle en V, il est nécessaire de simuler les systèmes et d’assurer une bonne couverture de tests. On pourra se référer au standard DO-254 [1] utilisé dans l’aéronautique, par exemple. La preuve formelle s’inscrit dans ces méthodes permettant de valider profondément le fonctionnement d’un système. Le principe consiste à décrire des propriétés au moyen d’assertions (assert()) et de lancer un « moteur de preuve » qui tentera de nous prouver qu’il peut les faire échouer.
Contrairement aux tests classiques, le cheminement qui nous mène à faire échouer une assertion n’est pas écrit par un humain. C’est la machine qui va parcourir l’ensemble des chemins...
- Accédez à tous les contenus de Connect en illimité
- Découvrez des listes de lecture et des contenus Premium
- Consultez les nouveaux articles en avant-première
