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 parcourir l’ensemble des chemins...

Cet article est réservé aux abonnés. Il vous reste 98% à découvrir.
S'abonner à Connect
  • 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
Je m'abonne


Article rédigé par

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

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 derniers articles Premiums

Les derniers articles Premium

Le combo gagnant de la virtualisation : QEMU et KVM

Magazine
Marque
Contenu Premium
Spécialité(s)
Résumé

C’est un fait : la virtualisation est partout ! Que ce soit pour la flexibilité des systèmes ou bien leur sécurité, l’adoption de la virtualisation augmente dans toutes les organisations depuis des années. Dans cet article, nous allons nous focaliser sur deux technologies : QEMU et KVM. En combinant les deux, il est possible de créer des environnements de virtualisation très robustes.

Brève introduction pratique à ZFS

Magazine
Marque
Contenu Premium
Spécialité(s)
Résumé

Il est grand temps de passer à un système de fichiers plus robuste et performant : ZFS. Avec ses fonctionnalités avancées, il assure une intégrité des données inégalée et simplifie la gestion des volumes de stockage. Il permet aussi de faire des snapshots, des clones, et de la déduplication, il est donc la solution idéale pour les environnements de stockage critiques. Découvrons ensemble pourquoi ZFS est LE choix incontournable pour l'avenir du stockage de données.

Générez votre serveur JEE sur-mesure avec Wildfly Glow

Magazine
Marque
Contenu Premium
Spécialité(s)
Résumé

Et, si, en une ligne de commandes, on pouvait reconstruire son serveur JEE pour qu’il soit configuré, sur mesure, pour les besoins des applications qu’il embarque ? Et si on pouvait aller encore plus loin, en distribuant l’ensemble, assemblé sous la forme d’un jar exécutable ? Et si on pouvait même déployer le tout, automatiquement, sur OpenShift ? Grâce à Wildfly Glow [1], c’est possible ! Tout du moins, pour le serveur JEE open source Wildfly [2]. Démonstration dans cet article.

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.
Voir les 32 listes de lecture

Abonnez-vous maintenant

et profitez de tous les contenus en illimité

Je découvre les offres

Déjà abonné ? Connectez-vous