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.

Dans cet article, on se propose de découvrir une autre méthode de validation d’un composant écrit en Verilog. L’idée est de décrire les propriétés du composant et de laisser l’ordinateur chercher les stimuli qui feront échouer des propriétés. Ça n’est plus le développeur qui écrit les tests, mais la machine. Cette méthode a récemment été rendue possible avec des logiciels libres grâce à la suite d’outils Yosys (synthèse Verilog), Yosys-SMTBMC (solveur) ainsi que SymbiYosys qui les chapeaute.

Chisel est un langage de description de matériel (HDL pour Hardware Description Language) née à l’université de Berkeley en même temps que le jeu d’instructions RISC-V. Chisel est basé sur le langage de programmation multiparadigme Scala. Ce langage permet de décrire un système synchrone et de générer du code Verilog pour la synthèse sur FPGA ou ASIC.

Il existe ! Le premier FPGA avec une chaîne intégralement open source est désormais une réalité. Parler de FPGA est peut-être un peu prétentieux concernant le EOS S3. Disons plutôt que c’est un microcontrôleur à cœur ARM Cortex-M4 qui possède une zone configurable (appelée souvent eFPGA). Mais ce qui est intéressant ici, c’est que les outils de synthèse ainsi que le format du fichier de configuration sont documentés. Ils sont donc utilisables avec des logiciels libres !

Pour prendre en main un nouveau FPGA, il est d’usage de faire clignoter des LED. C’est amusant, mais ne montre pas réellement l’intérêt des FPGA. Pour présenter le FPGA Trion T8 de la jeune société Efinix, nous allons donc sortir de ces éternels clignotements et réaliser une interface vidéo pour la Game Boy de Nintendo. L’occasion également de découvrir concrètement le langage de description matériel Chisel promu par l’université de Berkeley.

Dans cet article, nous allons vous proposer un Hack au sens noble du terme, qui consiste à détourner un produit de son usage prévu initialement pour en faire autre chose. Le produit en question est une carte de contrôle de panneaux de LED disponible pour 15 $ sur le site chinois de vente en ligne AliExpress. Il s’avère que la Colorlight 5A-75B est constituée d’un FPGA ECP5. Voilà qui peut faire un excellent kit de développement ECP5 à très bas coût.