De la preuve formelle en VHDL, librement

Magazine
Marque
Hackable
Numéro
42
Mois de parution
mai 2022
Spécialité(s)


Résumé

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…

La suite est réservée aux abonnés. Il vous reste 98% à découvrir.
  • 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
Envie de lire la suite ? Rejoignez Connect
Je m'abonne maintenant


Article rédigé par

Par le(s) même(s) auteur(s)

Pimp my LED counter, les performances de l’addition

Magazine
Marque
Hackable
Numéro
55
Mois de parution
juillet 2024
Spécialité(s)
Résumé

Pour évaluer un nouveau FPGA, on commence généralement avec la conception d’un compteur pour faire clignoter une LED. Ce HelloWorld simpliste nous amène à utiliser toute la chaîne de développement, de la conception du circuit en langage HDL jusqu’à la configuration du FPGA sur le kit. En passant bien sûr par la synthèse, le placement routage et le bitstream. On se penche rarement sur les performances du compteur utilisé pour le clignotement ni comment l’optimiser de manière à augmenter la fréquence de cadencement au maximum qu’il est possible d’obtenir avec le modèle étudié. C’est pourtant ce qu’on se propose de faire dans cet article à partir du kit iCEstick de chez Lattice.

Un oscilloscope à pédale

Magazine
Marque
Hackable
Numéro
55
Mois de parution
juillet 2024
Spécialité(s)
Résumé

Les électroniciennes et électroniciens sont des humains comme les autres, ils ont deux mains, deux pieds et une tête. Quand il s’agit de faire des mesures avec les deux sondes de l’oscilloscope, les deux mains sont vite prises. Comment peut-on encore appuyer sur les boutons de l’engin alors que toutes nos mains sont occupées ? Et si nous utilisions nos pieds ? À l’heure de la démocratisation du vélo utilitaire, il est temps d’ajouter une pédale à votre oscilloscope.

Accélérez vos simulations VHDL avec Verilator

Magazine
Marque
Hackable
Numéro
45
Mois de parution
novembre 2022
Spécialité(s)
Résumé

Dans un précédent article, nous avons présenté le simulateur Verilator. C’est un simulateur un peu particulier qui convertit le modèle HDL en une classe C++. Le banc de test est ensuite écrit sous la forme d’un programme en C++. Nous avons montré qu’avec cette méthode, on accélère énormément la simulation. Le problème de Verilator, c’est qu’il cible le langage Verilog. Or, l’industrie utilise également le VHDL comme standard de description matériel. Nous allons voir dans cet article qu’il est tout de même possible d’utiliser Verilator avec du VHDL grâce au couple de logiciels Yosys et GHDL. Nous en profiterons pour comparer trois méthodes de simulation, une avec GHDL, une avec NVC et enfin avec Verilator.

Transformez votre vieille Game Boy en console de salon HDMI

Magazine
Marque
Hackable
Numéro
44
Mois de parution
septembre 2022
Spécialité(s)
Résumé

On se propose ici d’utiliser un FPGA GW1NSR de la société chinoise Gowin pour transformer sa Game Boy en véritable console de salon, avec le branchement HDMI ainsi que la manette de Super NES. Le (relatif) plug & play du montage transforme ainsi la Game Boy en une Game Boy-Switch rétro à la sauce Formicapunk. On peut y jouer en mode portable comme à l’époque et si on l’insère dans le montage, il est possible d’y jouer sur sa télé HDMI avec une manette de Super NES.

Les listes de lecture

7 article(s) - ajoutée le 01/07/2020
La SDR permet désormais de toucher du doigt un domaine qui était jusqu'alors inaccessible : la réception et l'interprétation de signaux venus de l'espace. Découvrez ici différentes techniques utilisables, de la plus simple à la plus avancée...
8 article(s) - ajoutée le 01/07/2020
Au-delà de l'aspect nostalgique, le rétrocomputing est l'opportunité unique de renouer avec les concepts de base dans leur plus simple expression. Vous trouverez ici quelques-unes des technologies qui ont fait de l'informatique ce qu'elle est aujourd'hui.
9 article(s) - ajoutée le 01/07/2020
S'initier à la SDR est une activité financièrement très accessible, mais devant l'offre matérielle il est parfois difficile de faire ses premiers pas. Découvrez ici les options à votre disposition et les bases pour aborder cette thématique sereinement.
Plus de listes de lecture