Archives par mot-clé : yosys

Portage de TapTempo en VHDL

[Dépêche publiée initialement sur LinuxFr]

Ayant préparé tout le matériel pour faire du TapTempo en Verilog, il était trop tentant de réaliser la même chose en VHDL. L’occasion de se plonger dans ce langage de description matériel concurrent du Verilog.
L’occasion également de parler des avancées de GHDL, un simulateur libre du VHDL, et désormais également capable de faire la synthèse en conjonction avec Yosys.

Pour comprendre TapTempo dans la culture moulesque de LinuxFr.org, il est conseillé d’aller faire un petit tour sur la page wiki homonyme.

Sommaire

Comme l’indique le titre de cette dépêche, nous allons effectuer un « portage » du projet TapTempo, qui était écrit en Verilog, vers le language VHDL. Nous aurons donc l’avantage de profiter d’une architecture déjà conçue. Et comme une partie des stimulus de simulation (banc de test) ont été écrit en Python avec CocoTB, nous allons pouvoir les reprendre (presque) tels quels pour simuler notre version VHDL.

Vue d’ensemble du matériel pour TapTempo

Le VHDL

Le VHDL – pour VHSIC Hardware Description Language – est un langage de description matérielle issu d’une commande du ministère de la Défense américaine, c’est donc en toute logique qu’il soit surtout populaire… en Europe !

Le VHDL s’inspire fortement du langage ADA pour décrire le comportement des circuits intégrés numériques. Cela permet de décrire un modèle que l’on peut ensuite simuler au moyen d’un simulateur.
Le simulateur VHDL OpenSource le plus connu est GHDL, initialement développé par le français Tristan Gringold comme une surcouche à GCC.
Il existe également un simulateur opensource nommé nvc, mais il est moins mature que GHDL. Les autres simulateurs OpenSource, comme FreeHDL ou VerilatorVHDL, sont plus anecdotiques.

À partir d’une source VHDL il est également possible de générer un schéma de portes et de bascules logiques au moyen d’un logiciel de synthèse. Pendant longtemps, les seuls logiciels libres de synthèse HDL ciblaient le Verilog (OdinII et Yosys). Mais depuis cette année une extension GHDL est apparue pour Yosys. Si cette extension n’est pas encore vraiment stabilisée, elle n’en reste pas moins parfaitement utilisable comme nous allons le voir dans cet exemple.

Le VHDL est très hiérarchique, on décrit des modules avec leurs entrées-sorties que l’on assemble ensuite à la manière d’un schéma bloc dans un composant «top».

Dans le cas de TapTempo, l’interface du module «top» est déclarée dans une entité comme ceci :

entity taptempo is
    port (
        clk_i : in std_logic;
        btn_i : in std_logic;
        pwm_o : out std_logic
    );
end entity taptempo;

VHDL n’est pas sensible à la casse ! C’est quelque chose qui est très perturbant mais dans l’exemple ci-dessus Entity est exactement identique à entity ou ENTITY. En pratique, le simulateur mettra tout en minuscule.

Le module possède deux entrées : l’horloge (clk_i) et le bouton (btn_i) ainsi qu’une sortie pwm (pwm_o) pour l’affichage. Il est possible de définir des paramètres pour la génération du module en utilisant le mot clef generic de la même manière que le port. Pour plus de simplicité nous choisirons plutôt de mettre tous les paramètres dans un package séparé (nommé taptempo_pkg.vhd), à la manière des include du C/C++.

Le type std_logic est utilisé pour représenter les états que peut prendre un signal. En simulation, il peut prendre 9 valeurs différentes :
0 : 0 logique;
1 : 1 logique;
Z : Haute impédence;
X : inconnue, plusieurs pilotes en conflit -> erreur;
L : 0 faible, peut-être vu comme une résistance de tirage à la masse (pull-down);
H : 1 faible, peut-être vu comme une résistance de tirage à Vcc (pull-up);
W : signal faible inconnu, quand il y a un conflit entre L et H mais qu’un troisième pilote fort (0 ou 1) pourrait tout de même mettre le signal à une valeur déterminable;
- : pas d’importance;
U : non initialisé.

Dans la pratique on évitera d’utiliser toutes ces valeurs si on veut limiter les problèmes à la synthèse. Par exemple les valeurs ‘L’ et ‘H’ ne peuvent être synthétisées « à l’intérieur » d’un FPGA, les résistances de tirage ne sont disponibles que sur les entrées sorties.
Un bus de données bidirectionnel à l’extérieur du FPGA devra être séparé en deux bus dans le FPGA : un pour chaque direction.

En réalité on se limite à ‘0’ et ‘1’. Les valeurs ‘U’ et ‘X’ apparaissent dans les traces de simulation et nous avertissent d’un problème avec notre code (simulation ou synthèse).

Le type std_logic peut être étendu en tableau avec std_logic_vector très pratique pour représenter des bus.

Architecture de TapTempo

L’architecture global de TapTempo qui est exactement la même que celle de la version Verilog est présenté dans le schéma ci-dessous:

schema blocs taptempo

Le tempo en entrée est donné par une touche de morse

Schéma de la touche morse

qui peut aisément être remplacé par un simple bouton poussoir (c’est d’ailleurs monté en parallèle du bouton de la colorlight). Cette entrée est synchronisée avec l’horloge du FPGA au moyen d’une double bascule en série pour éviter la métastabilité :

    -- Synchronize btn
    btn_sync_p: process (clk_i, rst)
    begin
        if rst = '1' then
            btn_s <= '0';
            btn_old <= '0';
        elsif rising_edge(clk_i) then
            btn_s <= btn_old;
            btn_old <= btn_i;
        end if;
    end process btn_sync_p;

Le module debounce se charge ensuite de filtrer les rebonds et transfert le signal au module de mesure de la période d’appuis.

Cette période divise ensuite une constante de temps représentant le nombre de cycle de timepulse pour donner la fréquence en battement par minute (bpm).

Pour être « affichée », cette valeur est transformée en un signal périodique avec un rapport cyclique proportionnel au battement bpm.

Ce signal cyclique s’affiche ensuite très bien au moyen d’un voltmètre à aiguille comme celui-ci :

Photo du voltmètre à aiguille

La graduation qui nous intéresse ici est celle qui va de 0 à 250.

Les paramètres dans un package : taptempo_pkg

Pour configurer les différentes constantes et définir des fonctions utiles, on utilise un « package » nommé taptempo_pkg.vhd qui sera inclus dans tous les modules du projet :

use work.taptempo_pkg.all;

La déclaration d’un package en VHDL s’effectue en deux temps :

  • on déclare d’abord les «objets» que l’on va utiliser dans le package :
-- La déclaration de ce que le package rend visible
package taptempo_pkg is

    constant CLK_PER_NS : natural;
    constant BPM_MAX : natural;
    constant BPM_SIZE : natural;
    constant TP_CYCLE : natural;
    constant BTN_PER_MAX : natural;
    constant BTN_PER_SIZE : natural;
    constant BTN_PER_MIN : natural;
    constant MIN_US : natural;
    constant MAX_COUNT : natural;
    constant DEBOUNCE_PER_US: natural;
    constant DEB_MAX_COUNT : natural;
    constant DEB_MAX_COUNT_SIZE : natural;

    constant ZEROS : std_logic_vector(31 downto 0);

    -- Usefull function for register size
    function log2ceil(m : integer) return integer;

end package taptempo_pkg;
  • Puis on définit leurs valeurs et comportement dans le corps (body) :
package body taptempo_pkg is

    constant CLK_PER_NS : natural := 40;
    constant BPM_MAX : natural := 250;

    -- period of tp in ns
    constant TP_CYCLE : natural := 5120;

    -- Debounce period in us
    constant DEBOUNCE_PER_US: natural := 50_000;
    constant DEB_MAX_COUNT : natural := (1000 * (DEBOUNCE_PER_US / TP_CYCLE));
    constant DEB_MAX_COUNT_SIZE : natural := log2ceil(DEB_MAX_COUNT);

    -- constant MIN_NS : natural := 60000000000;
    constant MIN_US : natural := 60_000_000;

    constant BPM_SIZE : natural := log2ceil(BPM_MAX + 1);

    constant BTN_PER_MAX : natural := 1000 * (MIN_US / TP_CYCLE);
    constant BTN_PER_SIZE : natural := log2ceil(BTN_PER_MAX + 1);
    constant BTN_PER_MIN : natural := 1000 * (MIN_US / TP_CYCLE) / BPM_MAX;
    constant MAX_COUNT : natural := TP_CYCLE / CLK_PER_NS;

    constant ZEROS : std_logic_vector(31 downto 0) := x"00000000";

    function log2ceil(m : integer) return integer is
    begin
      for i in 0 to integer'high loop
            if 2 ** i >= m then
                return i;
            end if;
        end loop;
    end function log2ceil;

end package body;

Vous noterez la lourdeur d’avoir à déclarer le type de la constante dans le package avant de donner sa valeur dans le body. Les mauvaises langues diront que ça n’est pas beaucoup plus lourd que le C++ et ses doubles fichier (*.h et *.cpp) pour définir une classe.

Un cadenceur (timer) pour tout le système : Timepulse

Nous allons avoir besoin de compter le temps dans plusieurs blocs du projet. L’horloge câblée sur la colorlight est de 25Mhz. Comme nous n’avons pas besoin de précisions à la quarantaine de nanoseconde nous allons utiliser un compteur global pour générer des « pulses » toutes les 5,12µs. Ces pulses seront utilisés en entrée des blocs ayant besoin de compter le temps. Cela réduira la taille des compteurs puisqu’ils n’auront pas à repartir de l’horloge globale.

Le code est suffisamment concis pour que nous puissions le reproduire ici dans son intégralité.

library ieee;
use ieee.std_logic_1164.all;
use ieee.numeric_std.all;

use work.taptempo_pkg.all;

entity timepulse is
    port (
        -- clock and reset
        clk_i : in std_logic;
        rst_i : in std_logic;
        -- timepulse output
        tp_o : out std_logic
    );
end entity timepulse;

architecture RTL of timepulse is
    signal counter : natural range 0 to MAX_COUNT + 1;
begin
    tp_o <= '1' when (counter = 0) else '0';

    counter_p: process (clk_i, rst_i)
    begin
        if rst_i = '1' then
            counter <= 0;
        elsif rising_edge(clk_i) then
            if counter < MAX_COUNT then
                counter <= counter + 1;
            else
                counter <= 0;
            end if;
        end if;
    end process counter_p;
end architecture RTL;

Tout module VHDL est constitué d’une partie entité entity pour décrire les interfaces d’entrées-sorties. Ici nous avons les deux entrées horloge clk_i et reset rst_i caractéristiques d’un système synchrone. L’unique sortie est le pulse généré toutes les 5,12µs.

La description du fonctionnement du module est donnée ensuite dans le bloc « architecture ». En plus des signaux d’entrées-sorties, il est possible de déclarer des signaux interne au bloc. Nous avons déclaré ici le signal counter qui est un entier naturel borné de 0 à MAX_COUNT + 1. La possibilité de borner les signaux que l’on déclare en integer permet d’aider l’outil de synthèse à générer un bus de taille adaptée quand on ne souhaite pas déclarer un std_logic_vector avec une taille explicite.

Attention, un signal n’a pas la même signification qu’une variable dans un programme procédural. Une variable prend une seule valeur qui changera au cours de l’exécution du programme. Un signal doit être vu comme une liste des différentes valeurs que prendra le signal au cours de la simulation. La première valeur de la liste sera son état initial, et à chaque événement sur le signal on ajoutera une valeur à la liste jusqu’à la fin de la simulation.

Nous aurions également pu déclarer des constantes à cet endroit, mais comme dit dans l’introduction, une constante étant un paramètre modifiable nous avons préféré le mettre dans le package taptempo_pkg.

Le corps de l’architecture de timepulse possède deux « process » concurrents qui s’exécutent en parallèle. Le premier est une assignation continue :

    tp_o <= '1' when (counter = 0) else '0';

Il fait passer tp_o à ‘1’ quand le compteur counter atteint la valeur 0. Ce « process » est activé à chaque évenement/changement sur le signal counter.

Le second process est plus étoffé :

    counter_p: process (clk_i, rst_i)
    begin
    --...
    end process counter_p;

Ce process est exécuté à chaque événement surgissant sur les signaux déclarés dans la liste de sensibilité (ici clk_i et rst_i). Le contenu du process est quant à lui exécuté de manière séquentielle.

        if rst_i = '1' then
            --...
        elsif rising_edge(clk_i) then
            --...
        end if;

Cette structure décrit une bascule D qui sera bien reconnue comme telle par le logiciel de synthèse.
Un reset asynchrone ré-initialise le compteur à 0:

            counter <= 0;

Et sur un front montant de l’horloge

        elsif rising_edge(clk_i) then

on incrémente le compteur jusqu’à son maximum.

            if counter < MAX_COUNT then
                counter <= counter + 1;
            else
                counter <= 0;
            end if;

Notez l’utilisation de l’opérateur d’affectation non bloquant <= qui n’affectera la valeur qu’à la fin de l’exécution du process.

Si par exemple nous avons le code suivant dans un process :

    counter <= 10;
    counter <= 5;

La valeur effective de counter à la fin de l’exécution de process sera 5. Et à aucun moment la valeur 10 n’apparaîtra dans counter.

Pour visualiser les signaux de sortie du module on pourra se rendre dans le répertoire cocotb/test_timepulse du projet et lancer le test en donnant ghdl comme simulateur:

$ cd test_timepulse
$ SIM=ghdl make

Le même principe pourra être appliqué pour simuler tous les autres modules de TapTempo.

La simulation consiste à laisser passer le temps pendant une miliseconde :

@cocotb.test()
async def double_push_test(dut):
    trg = TestTimePulse(dut)
    trg.display_config()
    trg.log.info("Running test!")
    await trg.reset()
    await Timer(1, units="ms")

La simulation génère un fichier nommé timepulse.fst visible avec gtkwave :

$ gtkwave timepulse.fst

Comme visible dans l’image ci-dessous.

Visualisation de la simulation timepulse avec gtkwave

Filtrage des rebonds : debounce

Le manipulateur morse génère des rebonds, le filtrage avait initialement été réglé à 20 ms sur la version Verilog. Pour être vraiment tranquille nous le monterons à 50 ms, mais c’est particulièrement long comme période. Comme pour le reste, cette configuration se trouve donc dans le package taptempo_pkg.vhd.

Le module debounce va se charger de filtrer les rebonds au moyen d’une machine à états et d’un compteur.

entity debounce is
    port (
        -- clock and reset
        clk_i : in std_logic;
        rst_i : in std_logic;
        -- inputs
        tp_i  : in std_logic;
        btn_i : in std_logic;
        -- outputs
        btn_o : out std_logic
    );
end entity;

Le comptage des pulsations du module timepulse s’effectue dans un process :

counter_p: process (clk_i, rst_i)
begin
    if rst_i = '1' then
        counter <= 0;
    elsif rising_edge(clk_i) then
        if tp_i = '1' then
            if (state_reg = s_cnt_high) or (state_reg = s_cnt_low) then
                counter <= counter + 1;
            else
                counter <= 0;
            end if;
        end if;
    end if;
end process counter_p;

La machine à états est constituée de 4 états :

    type t_state is (s_wait_low, s_wait_high, s_cnt_high, s_cnt_low);
    signal state_reg : t_state;

Deux états d’attentes et deux états de comptages. Dans un état d’attente s_wait_ on attend un front du bouton. Quand un front survient on passe dans un état de comptage s_cnt_.

Dans un état de comptage, le compteur s’incrémente et passe à l’état d’attente lorsqu’il arrive à son maximum.

De cette manière, seuls les fronts intervenant dans un état d’attente sont pris en compte. Une fois la machine à états dans un état de comptage, plus aucun front du bouton n’est « écouté ».

Mesure de la période d’appuis : percount

Le module percount (period counter) va compter le temps d’une période entre deux appuis sur le bouton.

Si on passe sur les signaux désormais bien connus clk_i, rst_i et tp_i; l’entrée du module est btn_i qui représente la valeur du bouton (appuyé ou non) sans rebond.

Les deux signaux de sortie sont :
– Un vecteur btn_per_o représentant la valeur de la période mesurée
– Un signal btn_per_valid donnant la validité de la valeur précédente. La valeur de btn_per_o est considérée comme bonne uniquement si btn_per_valid est à ‘1’.

Dans un premier process détecte les fronts descendants du bouton :

    btn_fall <= btn_old and (not btn_i);

    btn_p: process (clk_i, rst_i)
    begin
        if rst_i = '1' then
            btn_old <= '0';
        elsif rising_edge(clk_i) then
            btn_old <= btn_i;
        end if;
    end process btn_p;

Puis dans un second process on compte le temps et on remet à 0 le compteur quand un front descendant du bouton surgit :

        --...
        elsif rising_edge(clk_i) then
            if btn_fall = '1' then
                counter_valid <= '1';
            elsif counter_valid = '1' then
                counter <= 0;
                counter_valid <= '0';
            elsif (tp_i = '1') and (counter < BTN_PER_MAX) then
                counter <= counter + 1;
            end if;
        end if;
        -- ...

Conversion période/fréquence (division) : per2bpm

C’est la partie « dure » du système, il va falloir faire une division d’une constante par la période mesurée.

Pour éviter d’avoir à utiliser les blocs multiplieurs dédiés de l’ECP5 et rester « portable » nous allons poser cette division comme on le ferait à la main.

Pour ce faire, on va mettre le dividende dans un registre nommé remainder (pour le reste) :

remainder <= std_logic_vector(to_unsigned((MIN_US / TP_CYCLE) * 1000, remainder'length));

Et le diviseur dans un registre divisor:

if to_integer(unsigned(btn_per_i)) < BTN_PER_MIN then
    divisor <= std_logic_vector(to_unsigned(BTN_PER_MIN, BTN_PER_SIZE)) & ZEROS(DIVIDENTWIDTH-1 downto 0);
else
    divisor <= btn_per_i & ZEROS(DIVIDENTWIDTH-1 downto 0);
end if;

Notez la la valeur minimum de btn_per_i qui nous évitera les problèmes de division par 0 ainsi que des valeurs de bpm trop élevées.

La division est cadencée par une machine à états de 3 états :

type t_state is (s_init, s_compute, s_result);
signal state_reg : t_state;

Un état initial pour démarrer, un état de calcul et un état durant lequel la valeur de sortie est considérée comme bonne.

L’algorithme de division consiste en une série de décalage à droite du diviseur :

divisor <= "0" & divisor(REGWIDTH-1 downto 1);

Et de décalages à gauche du quotient :

if (unsigned(divisor) <= unsigned(remainder)) then
    remainder <= std_logic_vector(unsigned(remainder) - unsigned(divisor));
    quotient <= quotient(REGWIDTH-2 downto 0) & "1";
else
    quotient <= quotient(REGWIDTH-2 downto 0) & "0";
end if;

Avec ajout d’un ‘1’ ou d’un ‘0’ en fonction de la valeur du diviseur et du reste. Lorsque le reste est supérieur au diviseur, on le soustrait du diviseur et on ajoute un bit ‘1’ au moment du décalage du quotient. Sinon on ajoute le bit ‘0’ sans toucher au registre de reste (remainder).

Les registres remainder, divisor et quotient sont des std_logic_vector qui ne représente rien d’autre qu’un « paquet de bits » pour le langage. Si l’on souhaite effectuer des opérations de comparaison ou des additions soustraction dessus il faut donc dire au VHDL que ses bits représentent un nombre (ici non signé) en les « castant » avec unsigned(). Et si l’on souhaite assigner le résultat à un std_logic_vector il faut « caster » à nouveau avec std_logic_vector. Ces multiples conversion de type peuvent vite devenir un casse-tête quand on fait du VHDL.

L’esperluette & est ici un opérateur de concaténation de deux vecteurs std_logic_vector.

Le résultat de la division est donné en continu par les bits de poids faible du registre divisor :

bpm_o <= quotient(BPM_SIZE-1 downto 0);
bpm_valid <= '1' when state_reg = s_result else '0';

bpm_o est considéré comme valide lorsque l’état de la machine à états est s_result.

Sortie «affichage» en rapport cyclique : pwmgen

La sortie « d’affichage » de la valeur consiste à générer un signal périodique pwm_o dont le rapport cyclique est proportionnel à la valeur de bpm_o.

On va pour cela compter de 0 à BPM_MAX :

-- count
count_p: process (clk_i, rst_i)
begin
    if rst_i = '1' then
        count <= BPM_MAX;
    elsif rising_edge(clk_i) then
        if tp_i = '1' then
            if count = 0 then
                count <= BPM_MAX;
            else
                count <= count - 1;
            end if ;
        end if ;
    end if;
end process count_p;

Tant que la valeur du compteur se trouvera en dessous d’un seuil pwmthreshold elle sera à ‘1’, une fois le seuil dépassé elle passera à ‘0’:

-- pwm output
pwm_o <= '1' when (count < pwmthreshold) else '0';

Ce seuil ne doit pas changer de valeur pendant le comptage, on va donc devoir utiliser un registre intermédiaire bpm_reg pour stocker la valeur de bpm_i d’entrée :

-- Latching bpm_i on bpm_valid
bpm_register_p: process (clk_i, rst_i)
begin
    if rst_i = '1' then
        bpm_reg <= BPM_RESET;
        pwmthreshold <= BPM_RESET;
    elsif rising_edge(clk_i) then
        if bpm_valid = '1' then
            bpm_reg <= to_integer(unsigned(bpm_i));
        end if;
        if (count = BPM_MAX) then
            pwmthreshold <= bpm_reg;
        end if;
    end if;
end process bpm_register_p;

Notez, à nouveau, la conversion d’un std_logic_vector (bpm_i) vers un entier naturel (bpm_reg) par le double « cast » to_integer(unsigned())

Synthèse, placement-routage et configuration

Nous voici arrivé à la véritable information de cette dépêche : il est désormais possible de faire de la synthèse VHDL avec un logiciel libre.
Le VHDL est le langage avec lequel les étudiants français abordent le monde du FPGA en général. Je l’ai personnellement beaucoup pratiqué en utilisant ghdl pour la simulation et gtkwave pour visualiser les chronogrammes. Mais jusqu’à cette année, j’ai toujours dû passer sur les monstres propriétaires fournis gratuitement par les fabricants de FPGA pour la partie synthèse. Monstres de plusieurs dizaines de Giga-octets à télécharger, souvent précompilé pour une architecture 32 ou 64 bits mais pas les deux, incluant des machines virtuelles java et autres librairies graphique bugués quand on change la langue du système (coucou le MIG de Vivado). Quand ils ne sont tout simplement pas compatibles Linux (de plus en plus rare cependant). Bref, la synthèse VHDL n’était pas une sinécure.

La simulation n’était pas en reste non plus, car si GHDL fonctionnait plutôt bien, il n’était pas des plus rapides à l’époque. Et impossible de faire de la simulation mixte en mélangeant du VHDL et du Verilog.

Impossible également d’utiliser la formule 1 de la simulation qu’est Verilator, un simulateur un peu spécial qui converti son design en un objet C++, le testbench étant ensuite écrit comme du C++ «normal». Le rapport de performance est d’au moins 100 fois plus rapide.

Pour être honnête, signalons qu’il existe bien le logiciel français Alliance, mais c’est très orienté ASIC, et je n’ai jamais réussi à le faire fonctionner correctement. Peut-être que si des développeurs d’Alliance traînent sur LinuxFR, ils pourront nous en parler.

Bref, la lumière est arrivée cette année avec le développement du greffon ghdl pour yosys ainsi que les avancées à toute vapeur de la partie «synthèse» de ghdl. Comme nous allons le voir dans la section suivante.

GHDL + Yosys, la lune de miel

Pour pouvoir synthétiser TapTempo il va falloir compiler et installer les trois projet suivant :

  • GHDL : Le logiciel de simulation ainsi que de synthèse (ne pas oublier d’option de synthèse dans la configuration avant compilation) ;
  • Yosys : le logiciel de synthèse Verilog, véritable couteau suisse pour le FPGA et plus si affinité ;
  • ghdl-yosys-plugin : le greffon qui permet de compiler une librairie ghdl.so à copier dans le répertoire YOSYS_PREFIX/share/yosys/plugins/ de yosys.

Il est fortement conseillé de prendre les dernières versions du code des projets ci-dessus et de les compiler « à la main » car ces projets avancent vite et bougent beaucoup, les paquets des différentes distributions linux sont déjà largement obsolètes.

Une fois installé on peut lancer yosys avec le greffon ghdl comme ceci :

$ yosys -m ghdl

[...]

 Yosys 0.9+3686 (git sha1 bc085761, clang 8.0.0-svn345496-1~exp1+0~20181029105533.852~1.gbpf10f36 -fPIC -Os)

yosys>

Puis charger nos sources VHDL avec la commande ghdl, en précisant bien le nom du « top » que l’on souhaite élaborer avec l’option -e.

yosys> ghdl --std=08 debounce.vhd  per2bpm.vhd  percount.vhd  pwmgen.vhd  rstgen.vhd  taptempo_pkg.vhd  taptempo.vhd  timepulse.vhd -e taptempo
1. Executing GHDL.
Importing module taptempo.
Importing module rstgen.
Importing module timepulse.
Importing module debounce.
Importing module percount.
Importing module per2bpm.
Importing module pwmgen_250.

Et c’est tout ! Maintenant on peut reprendre les commandes et la procédure que l’on avait utilisée dans le cas de TapTempo en Verilog pour faire la synthèse, le placement routage et le chargement.

Notez que comme les sources ont été chargées et parsé dans yosys, il est parfaitement possible de le convertir en Verilog grâce à la commande write_verilog:

yosys> write_verilog taptempo_converted.v

2. Executing Verilog backend.
Dumping module `\debounce'.
Dumping module `\per2bpm'.
Dumping module `\percount'.
Dumping module `\pwmgen_250'.
Dumping module `\rstgen'.
Dumping module `\taptempo'.
Dumping module `\timepulse'.

La version Verilog ainsi générée pourra être simulée avec verilator ou icarus par exemple pour faire de la simulation mixte, ou tout simplement pour accélérer la simulation dans le cas de verilator.

Pour synthétiser sur la colorlight qui est munie d’un FPGA ECP5 de chez Lattice, on utilisera la commande synth_ecp5 avec une sortie netlist au format json.

yosys>  synth_ecp5 -json taptempo.json
[...]
=== taptempo ===

   Number of wires:                540
   Number of wire bits:           1515
   Number of public wires:         540
   Number of public wire bits:    1515
   Number of memories:               0
   Number of memory bits:            0
   Number of processes:              0
   Number of cells:                785
     CCU2C                         109
     L6MUX21                         9
     LUT4                          452
     PFUMX                          25
     TRELLIS_FF                    190

2.50. Executing CHECK pass (checking for obvious problems).
Checking module taptempo...
Found and reported 0 problems.

2.51. Executing JSON backend.

Arrivé à cette étape il peut être intéressant de comparer avec la version Verilog les ressources utilisées par le même projet :

$ yosys
yosys> read_verilog debounce.v  per2bpm.v  percount.v  pwmgen.v  rstgen.v  taptempo.v  timepulse.v
yosys> synth_ecp5 -json taptempo.json
...
=== taptempo ===

   Number of wires:                487
   Number of wire bits:           1435
   Number of public wires:         487
   Number of public wire bits:    1435
   Number of memories:               0
   Number of memory bits:            0
   Number of processes:              0
   Number of cells:                751
     CCU2C                         105
     L6MUX21                         1
     LUT4                          441
     PFUMX                          13
     TRELLIS_FF                    191

8.50. Executing CHECK pass (checking for obvious problems).
Checking module taptempo...
Found and reported 0 problems.

8.51. Executing JSON backend.

Nous obtenons un design légèrement plus petit avec la version Verilog, mais les ordres de grandeurs sont tout de même respecté.

Placement routage avec NextPnR

NextPnR est un logiciel de placement routage qui prend le schéma (netlist) de cellules «primitives» généré par le logiciel de synthèse et associe chaque cellule à une cellule disponible dans le FPGA. NextPnR effectue également le routage qui consiste à établir les connexions entre les différentes cellules.

C’est également à cette étape que l’on va préciser la configuration du FPGA (taille, IO…). En plus du fichier json de synthèse nous donnerons un second fichier de configuration des IO nommé taptempo.lpf décrivant nos trois signaux d’entrées-sortie :

LOCATE COMP "clk_i" SITE "P6";
IOBUF PORT "clk_i" IO_TYPE=LVCMOS33;
FREQUENCY PORT "clk_i" 25 MHZ;

LOCATE COMP "btn_i" SITE "M13";
IOBUF PORT "btn_i" IO_TYPE=LVCMOS33;

LOCATE COMP "pwm_o" SITE "P4";
IOBUF PORT "pwm_o" IO_TYPE=LVCMOS33;

Toutes les commandes de synthèse données ici sont bien évidemment disponibles dans un Makefile sur le dépot. Pour faire le placement routage nous pourrions taper la commande suivante :

$ nextpnr-ecp5 --25k --package CABGA256 --speed 6 --json taptempo.json --textcfg taptempo_out.config --lpf taptempo.lpf --freq 25

Qui ne donnera pas le fichier de configuration nommé bitstream permettant de configurer le FPGA !

Car les spécifications des FPGA sont gardées jalousement par les constructeurs, et il faut des heures et des heures d’ingénieries inverses pour venir à bout de ces informations. Travail qui a été effectué via le projet Trellis et qui nous permet de convertir la sortie texte précédente taptempo_out.config en un bitstream reconnu par l’EPC5 :

$ ecppack taptempo_out.config taptempo.bit

Et l’on décroche enfin le Saint Grââl permettant de configurer la colorlight : le bitstream taptempo.bit.

En avant la musique avec openFPGALoader

Arrivé à cette étape il serait vraiment dommage d’être contraint de relancer l’ide proprio du constructeur juste pour télécharger le bitstream dans le FPGA via une sonde USB-Jtag !

C’est là que l’on peut dégainer le projet openFPGALoader qui a pour ambition de permettre la configuration de tous les FPGA existant avec toutes les sondes disponibles sur le marché.

$ openFPGALoader taptempo.bit 
Open file taptempo.bit DONE
Parse file DONE
Enable configuration: DONE
SRAM erase: DONE
Loading: [==================================================] 100.000000%
Done
Disable configuration: DONE

Et voila, on peut maintenant taper taper taper jusqu’au bout de la nuit.

Conclusion

Le VHDL est très verbeux, les évolutions du langage ont tenté de corriger un peu le tir mais cela reste tout de même verbeux. Certaine caractéristiques comme l’insensibilité à la casse font un peu penser à un langage d’un autre âge. Cependant, l’héritage du langage Ada fait de VHDL un langage très strict et déterministe de part sa conception contrairement au Verilog.

Le typage fort peut-être considéré à première vu comme un défaut ralentissant l’écriture du code. Mais il n’en est rien, après avoir souffert de « compiler » votre porte-gramme pour la simulation, vous aurez l’agréable surprise de voir votre système fonctionner parfaitement sur le FPGA du (presque) premier coup.

Le vocabulaire VHDL est très vaste et on se contente en général des structures de code connue dont on sait qu’elles « synthétiseront » correctement, ce qui donne une impression de ne jamais pouvoir atteindre la maîtrise du langage.

Il y a quelques années je m’étais posé la question de la popularité du VHDL par rapport au Verilog. En effet, même si le VHDL est presque aussi bien supporté que le Verilog par les outils des constructeurs, ça n’était pas le cas des logiciels libres. C’est encore largement le cas aujourd’hui, même certain logiciels non libre supportent en priorité le Verilog. Le constructeur Gowin par exemple ne permettait que la synthèse Verilog avec son outil maison. Il fallait installer le logiciel tier synplify de synopsis pour pouvoir accéder à la synthèse VHDL.

Cette extension de ghdl pour Yosys change la donne. Car, comme nous l’avons vu, il est possible de l’utiliser pour convertir son projet en Verilog et avoir accès à tous l’écosystème libre Verilog. Il est également possible de faire de la vérification formelle pour le VHDL.

Avoir la compétence VHDL dans son CV est une assez bonne idée car c’est souvent par ce mot que l’on résume le développement ASIC/FPGA/SoC. En Europe, le VHDL est très apprécié de l’industrie et particulièrement de l’industrie de défense.

Mais si c’est juste pour mesurer le tempo, ce n’est peut-être pas la voie la plus rapide et la plus simple 😉

Aller plus loin

ULX3S ou OrangeCrab ?

Deux cartes à base d’ECP5 ont été lancée coup sur coup le même weekend pour fêter le début du confinement : OrangeCrab et ULX3S. Ces deux cartes sont accessibles via un financement participatif, l’une avec groupsget et l’autre avec crowdsupply. Les deux cartes supportent à 100% toute la chaine de développement open source Yosys + NextPnR + Trellis.

Et les deux sont proposées au même prix de départ : $99. Vu qu’elles sont toutes les deux à base d’ECP5 et au même prix voyons voir un peu ce qu’elles ont dans le ventre.

OrangeCrab, de la DDR3 sur batterie.

Ce qui frappe avec l’OrangeCrab c’est sa capacité mémoire avec un chip DDR3 de 1Gbits. C’est également une toute petite carte qui tiens presque sur le doigt (à condition de choisir le bon).

Et elle possède un connecteur de batterie permettant de la rendre autonome et «portable».

Image provenant de groupgets

Le détails des caractéristiques est donné sur le site :

  • 24kLut
  • 1008 Kb –de blocs RAM
  • 194 Kb – RAM Distribuée
  • 28 – 18×18 Multiplieurs
  • PLLs: 2
  • oscillateur interne
  • 1Gbits DDR
  • Full-speed (12Mbit) USB avec connection direct sur le FPGA
  • 128Mbit QSPI de mémoire FLASH
  • Connecteur MicroSD
  • SAR ADC, external RC / input comparateur
  • Système de gestion de batterie

ULX3S la console de jeux à base de FPGA

L’ULX3S est nettement plus grosse que l’OrangeCrab sur beaucoup de points. Sur le nombre de composants ajoutés déjà. Puisque l’on peut noter la présence d’un connecteur microSD, de 8 leds, d’un port USB connecté au FPGA via un convertisseur FTDI plus un USB connecté en direct, d’un module Wifi/Bt, d’un port vidéo GPDI d’une sortie audio, de 6 boutons, de …. mais dites donc ne serait-ce pas là tous les élements nécessaire pour faire une console de jeu ?!

Image provenant de la page crowdsupply

Par contre, la version à 99$ démarre avec le plus petit FPGA de la gamme, le ECP5 12F, deux fois plus petit que celui de l’OrangeCrab. Il est cependant possible d’acquérir la carte avec des FPGA (nettement) plus gros comme le 45F (135$) et le 85F (155$).

Mais même avec le 12F, l’équipement de cette ULX3S tel que copié/collé ci-dessous reste impressionnant:

  • FPGA: Lattice ECP5
    • LFE5U-85F-6BG381C (84 K LUT)
    • LFE5U-45F-6BG381C (44 K LUT)
    • LFE5U-12F-6BG381C (12 K LUT)
  • USB: FTDI FT231XS (500 kbit JTAG and 3 Mbit USB-serial)
  • GPIO: 56 pins (28 differential pairs), PMOD-friendly with power out 3.3 V at 1 A or 2.5 V at 1.5 A
  • RAM: 32 MB SDRAM 166 MHz
  • Flash: 4-16 MB Quad-SPI Flash for FPGA config and user data storage
  • Mass Storage: Micro-SD slot
  • LEDs: 11 (8 user LEDs, 2 USB LEDs, 1 Wi-Fi LED)
  • Buttons: 7 (4 direction, 2 fire, 1 power button)
  • Audio: 3.5 mm jack with 4 contacts (analog stereo + digital audio or composite video)
  • Video: Digital video (GPDI General-Purpose Differential Interface) with 3.3 V to 5 V I²C bidirectional level shifter
  • Display: Placeholder for 0.96″ SPI COLOR OLED SSD1331
  • Wi-Fi & Bluetooth: ESP32-WROOM-32 supports a standalone JTAG web interface over Wi-Fi
  • Antenna: 27, 88-108, 144, 433 MHz FM/ASK onboard
  • ADC: 8 channels, 12 bit, 1 MS a/s MAX11125
  • Power: 3 Switching voltage regulators: 1.1 V, 2.5 V, and 3.3 V
  • Clock: 25 MHz onboard, external differential clock input
  • Low-Power Sleep: 5 µA at 5 V standby, RTC MCP7940N clock wake-up, power button, 32768 Hz quartz with CR1225 battery backup
  • Dimensions: 94 mm × 51 mm

Soyons sage, patientons avant de dégainer sa monnaie 😉

Célèbre mème Futurama

Prove Chisel design with Yosys-smtbmc

Formal prove is a great method to find bugs into our gateware. But for many years, this was reserved to big companies with lot of $$. Some years ago, Clifford opened the method with it’s synthesis software Yosys. Explanation about formal prove with Yosys-smtbmc and can be found in this presentation. Dan Guisselquist (ZipCPU) give lot of great tutorials on formal prove with Verilog and SystemVerilog design on it’s blog. It’s a good start to learn formal prove.

But, Yosys-smtbmc is made for Verilog (and a bit of SystemVerilog). It’s too bad but it’s the only open source formal tool available for gateware.

How can we prove our VHDL, Clash or Chisel gateware ?

One of the solution consist of writing a TOP component in SystemVerilog that integrate the assume/assert/cover method and instantiate our DUT in it. It’s the way Pepijn De Vos choose for verifying it’s VHDL gateware. Its VHDL code is converted into Verilog with the new GHDL feature not-yet-finished and a systemVerilog top component instantiate the VHDL gateware converted in verilog by GHDL synthesis feature.

That’s an interesting way to do it and it can be done in the same way with Chisel. But it’s a bit limited to input/output ports of our gateware. If we want to add some property about internal counters or flags or others internals states machines registers, we have to export it with some conditional preprocessor value like follows:

`ifdef FORMAL
// Declare some signal output ports
`endif

It’s became little bit difficult to do that with chisel and its blackbox system. Then if we want to include formal property under the verilog generated module, we have to open the generated verilog code and write it directly.

It’s not a lasting solution. Because each time we regenerate Verilog code from Chisel, each time we have to re-write formal properties. It’s rapidly become a pain !

To (temporarily) fix this problem a little python tools has been written by Martoni for injecting rules automatically under generated Verilog module. We will see how it’s work in this article with a simple project named ChisNesPad.

ChisNesPad project

ChisNesPad is a little project that aim to drive Super Nintendo Pad with an FPGA.

In electronic point of view, super nes controller is simply a 16 bits shift register.

The gamepad pinout is relativelly easy to find on the web.

SuperNes gamePAD pinout

For FPGA point of view 3 signals interest us :

  • DATA : Gamepad output for serial datas
  • LATCH: Game pad input to take a “picture” of 16 buttons
  • CLOCK: To synchronize shifter

Internally, the game pad is composed of two 4021 chips serialized.

Basic Chisel/Formal directory structure

The directory structure of the project is following :

/
|-- build.sbt  <- scala build configuration
|-- src/   <- all chisel sources
|   |-- main/
|       |-- scala/
|           |-- chisnespad.scala <- Chisel module we will prove
|           |-- snespadled.scala <- "top" module to test with
|                                    tang nano (gowin)
|-- formal/   <- formal directory where systemVerilog
|                and sby yosys configuration are.
|-- platform/ <- some usefull file for synthesis with 
                 final platform (gowin).

To generate Verilog file we just have to launch following command in main project directory:

sbt 'runMain chisnespad.ChisNesPad'

The generated file will be named ChisNesPad.v

smtbmcify tool

smtbmcify tool is a python3 module that can be found on this github project. It can be installed on the dev machine as follow:

$ git clone https://github.com/Martoni/chisverilogutils
$ cd chisverilogutils/smtbmcify
$ python -m pip install -e .

A command named smtbmcify will then be available on system :

$  smtbmcify -h
Usages:
$ python smtbmcify.py [options]
-h, --help             print this help message
-v, --verilog=module.v verilog module to read
-f, --formal=formal.sv formals rules
-o, --output=name.sv   output filename, default is moduleFormal.sv

To use smtbmc formal tools with smtbmcify we will need two more source/configuration files :

  • ChisNesPadRules.sv That contain SystemVerilog formals properties
  • ChisNesPadRules.sby That contain yosys-smtbmc script configuration

These two files must be saved in formal/ directory. sby files are SymbiYosys configuration files, installation instruction of SymbiYosys can be found here.

For simply testing, the rule (written in file ChisNesPadRules.sv) we want to “inject” is following:

//BeginModule:ChisNesPad

always@(posedge clock) begin
    assume(io_dlatch == 1'b1);
    assert(stateReg == 2'b00); 
end

//EndModule:ChisNesPad

With this rule, we assert that if io.dlatch output is 1, the internal stateReg will be set to sInit state (00).

The comments BeginModule and EndModule must be set with the exact chisel module name :

//...
class ChisNesPad (val mainClockFreq: Int = 100,
                  val clockFreq: Int = 1,
                  val regLen: Int = 16) extends Module {
  val io = IO(new Bundle{
//...

Hence, the tool smtbmcify will find the module in verilog generated module and inject the rules at the end of it:

$ cd formal
$ smtbmcify -v ../ChisNesPad.v -f ChisNesPadRules.sv -o ChisNesPadFormal.sv
...
    end else begin
      validReg <= _T_19;
    end
    _T_21 <= stateReg == 2'h1;
    _T_23 <= stateReg == 2'h0;
  end
//BeginModule:ChisNesPad

always@(posedge clock) begin
    assume(io_dlatch == 1'b1);
    assert(stateReg == 2'b00); 
end

//EndModule:ChisNesPad
endmodule

The module name is mandatory because a Chisel Verilog generated module can contain several module.

Some naming convention should be know to write systemverilog rules:

  • dot ‘.’ syntax is replaced with ‘_’ in Verilog: for this example io.dlatch chisel signal is replaced with io_dlatch.
  • Some registers can disappear (be simplified) in generated Verilog. dontTouch() can be used to keep it in generated Verilog.

To launch the formal engine we are using a sby script like it (named ChisNesPad.sby:

[options]
mode bmc 
depth 30

[engines]
smtbmc

[script]
read -formal ChisNesPadFormal.sv
prep -top ChisNesPad

[files]
ChisNesPadFormal.sv

The launch command is :

$ sby ChisNesPad.sby
SBY 21:12:00 [ChisNesPad] Copy 'ChisNesPadFormal.sv' to 'ChisNesPad/src/ChisNesPadFormal.sv'.
SBY 21:12:00 [ChisNesPad] engine_0: smtbmc
SBY 21:12:00 [ChisNesPad] base: starting process "cd ChisNesPad/src; yosys -ql ../model/design.log ../model/design.ys"
SBY 21:12:00 [ChisNesPad] base: finished (returncode=0)
SBY 21:12:00 [ChisNesPad] smt2: starting process "cd ChisNesPad/model; yosys -ql design_smt2.log design_smt2.ys"
SBY 21:12:00 [ChisNesPad] smt2: finished (returncode=0)
SBY 21:12:00 [ChisNesPad] engine_0: starting process "cd ChisNesPad; yosys-smtbmc --presat --unroll --noprogress -t 30 --append 0 --dump-vcd engine_0/trace.vcd --dump-vlogtb engine_0/trace_tb.v --dump-smtc engine_0/trace.smtc model/design_smt2.smt2"
SBY 21:12:01 [ChisNesPad] engine_0: ##   0:00:00  Solver: yices
SBY 21:12:01 [ChisNesPad] engine_0: ##   0:00:00  Checking assumptions in step 0..
SBY 21:12:01 [ChisNesPad] engine_0: ##   0:00:00  Checking assertions in step 0..
[...]
SBY 21:12:01 [ChisNesPad] engine_0: ##   0:00:00  Checking assumptions in step 29..
SBY 21:12:01 [ChisNesPad] engine_0: ##   0:00:00  Checking assertions in step 29..
SBY 21:12:01 [ChisNesPad] engine_0: ##   0:00:00  Status: passed
SBY 21:12:01 [ChisNesPad] engine_0: finished (returncode=0)
SBY 21:12:01 [ChisNesPad] engine_0: Status returned by engine: pass
SBY 21:12:01 [ChisNesPad] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 21:12:01 [ChisNesPad] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 21:12:01 [ChisNesPad] summary: engine_0 (smtbmc) returned pass
SBY 21:12:01 [ChisNesPad] DONE (PASS, rc=0)

This simple rule finish with success (PASS) and create a directory with all generated file under it.

Rapidly, we will need a Makefile to launch each step of this procedure and to clean generated file.

Of course, all code described so far is available on the github ChisNesPad project.

Find bugs

Ok the test we done so far PASS without problem. Let’s find a bug adding this rules in ChisNesPadRules.sv :

always@(posedge clock) begin
    assert(regCount <= 16); 
end

This rule generate a FAIL :

$ make
cd ..;sbt "runMain chisnespad.ChisNesPad"
[info] Loading project definition from /home/fabien/myapp/chisNesPad/project
[info] Loading settings for project chisnespad from build.sbt ...
[info] Set current project to chisNesPad (in build file:/home/fabien/myapp/chisNesPad/)
[warn] Multiple main classes detected.  Run 'show discoveredMainClasses' to see the list
[info] running chisnespad.ChisNesPad 
Generating Verilog sources for ChisNesPad Module
[info] [0.004] Elaborating design...
[info] [1.735] Done elaborating.
Total FIRRTL Compile Time: 1396.1 ms
[success] Total time: 5 s, completed Feb 3, 2020 9:49:48 PM
smtbmcify -v ../ChisNesPad.v -f ChisNesPadRules.sv -o ChisNesPadFormal.sv
Generating file ChisNesPadFormal.sv
1 module will be filled :
ChisNesPad
rm -rf ChisNesPad
sby ChisNesPad.sby
SBY 21:49:48 [ChisNesPad] Copy 'ChisNesPadFormal.sv' to 'ChisNesPad/src/ChisNesPadFormal.sv'.
SBY 21:49:48 [ChisNesPad] engine_0: smtbmc
SBY 21:49:48 [ChisNesPad] base: starting process "cd ChisNesPad/src; yosys -ql ../model/design.log ../model/design.ys"
SBY 21:49:49 [ChisNesPad] base: finished (returncode=0)
SBY 21:49:49 [ChisNesPad] smt2: starting process "cd ChisNesPad/model; yosys -ql design_smt2.log design_smt2.ys"
SBY 21:49:49 [ChisNesPad] smt2: finished (returncode=0)
SBY 21:49:49 [ChisNesPad] engine_0: starting process "cd ChisNesPad; yosys-smtbmc --presat --unroll --noprogress -t 30 --append 0 --dump-vcd engine_0/trace.vcd --dump-vlogtb engine_0/trace_tb.v --dump-smtc engine_0/trace.smtc model/design_smt2.smt2"
SBY 21:49:49 [ChisNesPad] engine_0: ##   0:00:00  Solver: yices
SBY 21:49:49 [ChisNesPad] engine_0: ##   0:00:00  Checking assumptions in step 0..
SBY 21:49:49 [ChisNesPad] engine_0: ##   0:00:00  Checking assertions in step 0..
SBY 21:49:49 [ChisNesPad] engine_0: ##   0:00:00  Checking assumptions in step 1..
SBY 21:49:49 [ChisNesPad] engine_0: ##   0:00:00  Checking assertions in step 1..
SBY 21:49:49 [ChisNesPad] engine_0: ##   0:00:00  BMC failed!
SBY 21:49:49 [ChisNesPad] engine_0: ##   0:00:00  Assert failed in ChisNesPad: ChisNesPadFormal.sv:230
SBY 21:49:49 [ChisNesPad] engine_0: ##   0:00:00  Writing trace to VCD file: engine_0/trace.vcd
SBY 21:49:49 [ChisNesPad] engine_0: ##   0:00:00  Writing trace to Verilog testbench: engine_0/trace_tb.v
SBY 21:49:49 [ChisNesPad] engine_0: ##   0:00:00  Writing trace to constraints file: engine_0/trace.smtc
SBY 21:49:49 [ChisNesPad] engine_0: ##   0:00:00  Status: failed (!)
SBY 21:49:49 [ChisNesPad] engine_0: finished (returncode=1)
SBY 21:49:49 [ChisNesPad] engine_0: Status returned by engine: FAIL
SBY 21:49:49 [ChisNesPad] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 21:49:49 [ChisNesPad] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 21:49:49 [ChisNesPad] summary: engine_0 (smtbmc) returned FAIL
SBY 21:49:49 [ChisNesPad] summary: counterexample trace: ChisNesPad/engine_0/trace.vcd
SBY 21:49:49 [ChisNesPad] DONE (FAIL, rc=2)
make: *** [Makefile:10: ChisNesPad/PASS] Error 2

An error is found at second step. A vcd trace is generated that we can see with gtkwave:

$ gtkwave ChisNesPad/engine_0/trace.vcd
Formal engine found a bug, and print it as a VCD trace

We can also get verilog testbench that reproduce the bug under the same directory (trace_tb.v).

The problem here is that we didn’t define initial reset condition as explained in ZipCPU course. To solve this problem we have to change the rule adding initial rules (reset should be set at the begining) and assert counter value only when reset is not set :

initial
    assume(reset==1'b1);

always@(posedge clock) begin
    if(reset == 1'b0) 
        assert(regCount <= 16); 
end

With that rules, it pass :

$ make
cd ..;sbt "runMain chisnespad.ChisNesPad"
[info] Loading project definition from /home/fabien/myapp/chisNesPad/project
[info] Loading settings for project chisnespad from build.sbt ...
[info] Set current project to chisNesPad (in build file:/home/fabien/myapp/chisNesPad/)
[warn] Multiple main classes detected.  Run 'show discoveredMainClasses' to see the list
[info] running chisnespad.ChisNesPad 
Generating Verilog sources for ChisNesPad Module
[info] [0.004] Elaborating design...
[info] [1.612] Done elaborating.
Total FIRRTL Compile Time: 1324.0 ms
[success] Total time: 5 s, completed Feb 3, 2020 10:04:37 PM
smtbmcify -v ../ChisNesPad.v -f ChisNesPadRules.sv -o ChisNesPadFormal.sv
Generating file ChisNesPadFormal.sv
1 module will be filled :
ChisNesPad
rm -rf ChisNesPad
sby ChisNesPad.sby
SBY 22:04:38 [ChisNesPad] Copy 'ChisNesPadFormal.sv' to 'ChisNesPad/src/ChisNesPadFormal.sv'.
SBY 22:04:38 [ChisNesPad] engine_0: smtbmc
SBY 22:04:38 [ChisNesPad] base: starting process "cd ChisNesPad/src; yosys -ql ../model/design.log ../model/design.ys"
SBY 22:04:38 [ChisNesPad] base: finished (returncode=0)
SBY 22:04:38 [ChisNesPad] smt2: starting process "cd ChisNesPad/model; yosys -ql design_smt2.log design_smt2.ys"
SBY 22:04:38 [ChisNesPad] smt2: finished (returncode=0)
SBY 22:04:38 [ChisNesPad] engine_0: starting process "cd ChisNesPad; yosys-smtbmc --presat --unroll --noprogress -t 30 --append 0 --dump-vcd engine_0/trace.vcd --dump-vlogtb engine_0/trace_tb.v --dump-smtc engine_0/trace.smtc model/design_smt2.smt2"
SBY 22:04:38 [ChisNesPad] engine_0: ##   0:00:00  Solver: yices
SBY 22:04:38 [ChisNesPad] engine_0: ##   0:00:00  Checking assumptions in step 0..
[...]
SBY 22:04:39 [ChisNesPad] engine_0: ##   0:00:00  Checking assertions in step 29..
SBY 22:04:39 [ChisNesPad] engine_0: ##   0:00:00  Status: passed
SBY 22:04:39 [ChisNesPad] engine_0: finished (returncode=0)
SBY 22:04:39 [ChisNesPad] engine_0: Status returned by engine: pass
SBY 22:04:39 [ChisNesPad] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 22:04:39 [ChisNesPad] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 22:04:39 [ChisNesPad] summary: engine_0 (smtbmc) returned pass
SBY 22:04:39 [ChisNesPad] DONE (PASS, rc=0)

This is just a little introduction on how to use yosys-smtbmc and symbiYosys to formally prove your chisel design.

Maybe this formal rules injector will be integrated in Chisel a day ?

Un ASIC conçu intégralement avec des logiciels libres

Les FPGA sont très liés aux ASIC. En effet, la plupart des outils utilisés en FPGA pour la synthèse HDL, la preuve formel, le placement routage ou l’analyse des timings sont les même que ceux à destination des ASIC. Seuls les librairies et les configurations changent. La grosse différence (de taille) avec les FPGA c’est que l’ASIC n’est pas reconfigurable, et les «frais d’initialisations» sont très élevés. Les délais de productions sont très long également (on parle en trimestre voir en semestre de délais).

Avec de telles contraintes, on comprend pourquoi les développeurs ne se mouillent pas trop avec des logiciels exotiques et restent sur ceux qu’ils connaissent. Vu les tarif de production, le coût des licences des logiciels est assez négligeable. Pourquoi «grenouiller» avec des outils open-source dans ce cas ?

Vue «silicium» du Raven, un microcontrôleur Risc-V conçu avec des outils open-sources

Toutes ces contraintes n’ont pas découragé Tim Edwards de se lancer dans la conception et la fabrication d’un microcontrôleurs intégralement avec des outils open-sources.

Synoptique du Raven avec ses différents périphériques

C’est comme cela qu’est né le Raven, un microcontrôleur basé sur un cœur picoRV32 (conçu par Clifford Wolf) et réalisé principalement avec les outils qflow d’opencircuitdesign.com :

Grande surprise quand on se plonge dans ces outils open-source : Beaucoup sont très vieux. Les pages web de ses outils sont encore codé en web95 avec des frames et autre fonds hideux datant de l’époque frontpage.

Pourtant à y regarder de plus prêt, ces outils semblent toujours activement maintenus.

Mais alors pourquoi aucun fondeur FPGA ne les proposent dans leurs IDE ?

Une première série du microcontrôleur gravé en 180nm a été produite en mai 2018. Le composant est désormais fonctionnel avec les caractéristiques suivantes:

  • Cadencé à 100 MHz
  • 16 GPIO
  • 2 ADCs
  • 1 DAC
  • 1 Comparateur
  • Alarme de température
  • Oscillateur RC de 100 kHz
  • Fonction configurables pour les sorties GPIO
  • Interruptions configurable sur les entrées GPIO

Il n’est pas possible d’acheter le composant pour se faire un montage chez soit pour le moment. Par contre l’«IP» est disponible dans la bibliothèque du fondeur efabless et peut être utilisé comme base pour réaliser son propre composant selon les besoins.

Projet IceStorm : le FPGA libéré !

Le jour du 27 mai 2015 sera à marquer d’une pierre blanche, en effet, c’est le jour où un FPGA a été libéré du joug des logiciels privateurs.

C’est le jour où Wolf Clifford a sorti une première version fonctionnelle du projet IceStorm permettant de synthétiser un design écrit en Verilog via Yosys et de faire le placement routage grâce à Arachne-pnr.

La conversion en bitstream et la programmation du chip se fait grâce aux utilitaires icepack et iceprog du projet IceStorm.

Pour l’instant le composant ciblé est le Lattice iCE40 HX1K-TQ144 pouvant être trouvé sur le kit d’évaluation lowcost (~$20) iCEstick.

Voici ci-dessous un petit howto rapide permettant de faire les manipulations se trouvant dans la vidéo de Clifford.

Icestorm howto

  • Installation de Yosys
$ cd /opt
$ git clone https://github.com/cliffordwolf/yosys.git 
$ yosys_deps="build-essential clang bison flex libreadline-dev gawk
	       tcl-dev libffi-dev git mercurial graphviz xdot pkg-config python"
$ sudo apt-get install $yosys_deps
$ make config-gcc
$ make
$ make test
$ sudo make install
  • Installation d’IceStorm
$ sudo apt-get install libftdi-dev
$ cd /opt/
$ mkdir icestorm
$ wget http://www.clifford.at/icestorm/icestorm-snapshot-150526.zip
$ unzip icestorm-snapshot-150526.zip
$ make
$ sudo make install
  • Et enfin arachne-pnr
$ cd /opt/
$ git clone https://github.com/cseed/arachne-pnr.git
$ make && sudo make install
  • Synthèse, placement-routage, bitstream et programmation

Un exemple de «programme» est donné avec arachne-pnr dans le répertoire
example/rot. Cet exemple est composé du source en vérilog rot.v ainsi que du
placement des pin rot.pcf.

  • Synthèse (Génération du blif)
$ cd /opt/arachne-pnr/example/rot/
$ yosys -p "synth_ice40 -blif rot.blif" rot.v
  • Placement routage (Génération du txt)
$ arachne-pnr -d 1k -p rot.pcf rot.blif -o rot.txt

Le fichier généré rot.txt est la description finale du placement et du routage
du design dans le fpga. Cette description est parfaitement lisible en ascii
avec n’importe quel éditeur de texte.
Pour le télécharger dans le fpga nous devons le convertir en format binaire au
moyen de la commande «icepack» :

$ icepack rot.txt rot.bin

Nous avons un bitstream parfaitement compatible avec le ice40, il
nous faut maintenant le télécharger dans le fpga.
Et même pour cela, un logiciel libre est fourni : iceprog !

$ sudo iceprog rot.bin

On peut faire le tout en une seule ligne aussi si on veut :

yosys -p "synth_ice40 -blif rot.blif" rot.v;arachne-pnr -d 1k -p rot.pcf rot.blif -o rot.txt;icepack rot.txt rot.bin;sudo iceprog rot.bin

Et voila, bienvenue dans ce monde nouveau du FPGA libre !