Tous les articles par Fabien Marteau

CocoTB 1.4.0, la maturité

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

C’est dans la soirée du 8 juillet que l’annonce est tombée : la version 1.4.0 de CocoTB est sortie. Cette nouvelle version est une belle évolution de Cocotb avec une bonne intégration dans le système de paquets de Python ainsi que l’abandon de la prise en charge de Python 2. On peut aujourd’hui dire que CocoTB est une alternative sérieuse pour écrire ses bancs de test HDL.

Sommaire

Mais qu’est‑ce que c’est ?

CocoTB est une bibliothèque de cosimulation permettant d’écrire (en Python) des bancs de test pour la simulation numérique HDL (Hardware Description Language). Historiquement, les deux langages de descriptions HDL que sont Verilog et VHDL embarquent tout le nécessaire pour écrire des stimuli permettant de tester le composant en simulation. Cela permet d’avoir un seul langage pour décrire le composant et le tester. Le simulateur exécutera tout cela sans problème.

Mais cela amène beaucoup de confusion entre la partie du langage utilisable pour la simulation uniquement et la partie « description du matériel ». Dans le cas de la partie « matériel » on parle alors de code « synthétisable ». Cette confusion entre du code synthétisable ou non est source de grandes frustrations au moment de passer à la synthèse. En effet, cette belle structure de données que l’on aura développée et testée aux petits oignons s’écroulera au moment de la synthèse quand on se rendra compte que le code n’est pas synthétisable. Il faudra tout reprendre.

Une des idées derrière CocoTB est donc de changer de langage pour la simulation, comme cela les choses sont claires : on utilise le VHDL ou Verilog pour la partie du composant qui est synthétisable, et on passe au Python pour le banc de test. Ce n’est pas le seul logiciel à proposer ce genre d’approche. Avec Verilator, par exemple, on va écrire toute la partie banc de test en C++ ou en SystemC. La partie synthétisable sera écrite en Verilog et convertie en un objet C++ par Verilator.

La seconde idée de CocoTB est de ne pas réinventer la roue en réécrivant un énième simulateur HDL. Ce qui évite également d’avoir à choisir son camp entre Verilog et VHDL ou les deux (simulation mixte). Non, CocoTB va se contenter de piloter les simulateurs disponibles sur le marché. Les simulateurs libres que sont GHDL, Icarus et Verilator sont naturellement pris en charge, même si dans le cas de Verilator c’est très récent. La plupart des simulateurs commerciaux le sont également, ce qui est un argument pour l’introduire dans son bureau d’étude. En effet, les managers sont en général moyennement chauds pour virer un logiciel acquis à grands frais. Et l’on peut continuer à profiter des interfaces proposées par notre simulateur habituel pour exécuter le simulateur, visionner les chronogrammes, faire de la couverture de tests, etc.
La version 1.4 de CocoTB introduit la gestion complète du simulateur Aldec Active HDL qui vient s’ajouter aux classiques de Cadence et de Mentor, Modelsim…

Les changements dans le code

Un gros changement initié depuis quelque versions déjà est l’utilisation du mot clef async en lieu et place du yield et du décorateur @coroutine. Python 3 gérant désormais l’asynchronisme, CocoTB l’utilise et le prend désormais complètement en charge. L’exemple donné dans le courriel de la publication est le suivant :

    @cocotb.test()
    async def my_first_test(dut):
         """Try accessing the design."""

         dut._log.info("Running test!")
         for cycle in range(10):
             dut.clk <= 0
             await Timer(1, units='ns')
             dut.clk <= 1
             await Timer(1, units='ns')
         dut._log.info("Running test!")

Qui se serait écrit comme cela dans « l’ancien système » :

    @cocotb.test()
    def my_first_test(dut):
        """Try accessing the design."""
         dut._log.info("Running test!")
         for cycle in range(10):
             dut.clk <= 0
             yield Timer(1, units='ns')
             dut.clk <= 1
             yield Timer(1, units='ns')
         dut._log.info("Running test!")

Cette écriture restant cependant valable.

Le gros avantage de cette nouvelle écriture est de ne plus avoir a réinventer la roue avec des décorateurs inutiles. Avec async et await, on utilise des interfaces intégrées à Python 3, ce qui évite tout un travail de gestion.

Installation

CocoTB est, depuis maintenant un certain temps, partie intégrante du système de gestion de paquets de Python pip. Et vous pouvez dès à présent l’installer sur votre système via la commande pip install :

    $ python -m pip install cocotb
    # Pour celles et ceux qui ont installé la version précédente n’oubliez pas le --upgrade
    $ python -m pip install --upgrade cocotb

Et on peut vérifier la version grâce à la commande cocotb-config suivante :

cocotb-config --version
1.4.0

En plus de votre composant écrit en VHDL ou Verilog, deux fichiers supplémentaires sont nécessaires pour tester avec CocoTB : le Makefile et le script Python de test proprement dit.

Avec cette nouvelle version, le Makefile a encore été simplifié puisqu’il n’est plus nécessaire d’intégrer les en‑têtes C++. Ces en‑têtes sont nécessaires pour compiler les interfaces VPI/VHPI/FLI qui permettent de piloter les simulateurs. On compile désormais cette partie à l’installation de CocoTB. Dans les précédentes version, cette compilation ce faisait à chaque fois que l’on relançait les tests.

Si l’on prend l’exemple de l’antirebond en Verilog du Blinking Led Project, nous avons le Makefile suivant :

    SIM=icarus                                   # Nom du simulateur
    export COCOTB_REDUCED_LOG_FMT=1              # Pour avoir des traces de log qui rentre dans l’écran
    VERILOG_SOURCES = $(PWD)/../src/button_deb.v # Inclusion des fichiers HDL
    TOPLEVEL=button_deb                          # Nom de l’entité 
    MODULE=test_$(TOPLEVEL)                      # Nom du script Python de test
    include $(shell cocotb-config --makefile)/Makefile.sim

L’exemple est un composant permettant de ne pas compter les rebonds d’un bouton comme des appuis successifs.
Le script de test en Python se trouve dans le dépôt Git du projet et se nomme test_buton_deb.py. Pour le lancer, il suffit de se rendre dans le répertoire blp/verilog/cocotb/ et de taper make :

     $ make
     [...]
     0.00ns INFO     Running test!
     0.00ns INFO     freq value : 95000 kHz
     0.00ns INFO     debounce value : 20 ms
     0.00ns INFO     Period clock value : 10000 ps
     0.02ns INFO     Reset complete

Un fichier de traces (chronogrammes) button_deb.vcd au format VCD est créé. Il peut être visionné en « temps réel » alors même que la simulation n’est pas terminée, grâce au visualiseur gtkwave :

   $ gtkwave button_deb.vcd
Vue de traces VCD avec GTKWave

Une organisation qui tourne

Le projet CocoTB est chapeauté par la FOSSi foundation qui fournit le « chef de projet » Philipp Wagner ainsi que des moyens financiers pour faire tourner des machines virtuelles de tests ainsi que pour payer les licences des simulateurs commerciaux.

Les statistiques de modification de cette version sont les suivantes :

  • 346 fichiers modifiés, 14 012 insertions (+), 10 356 suppressions (−) ;
  • 554 commits ;
  • 31 contributeurs ;
  • 2 nouveaux mainteneurs : Colin Marquardt et Kaleb Barrett.

Ces chiffres montrent que CocoTB est un projet qui fédère désormais une grosse communauté. C’est un projet mature qui compte dans le paysage des logiciels libres pour le matériel (FPGA et ASIC).

Google libère les ASIC avec un PDK open source en 130 nm

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

La libération des FPGA s’accélère à grands pas, il devient presque difficile de suivre toutes les nouvelles sur le sujet. Mais les FPGA ne doivent pas nous faire oublier leurs grands frères que sont les ASIC.
Un FPGA est un composant ayant un silicium déjà « gravé » mais où il est possible de reconfigurer les connexions entre les éléments logiques à volonté. Dans le cas d’un ASIC, on va cette fois graver directement les transistors sur un silicium vierge et les relier via des couches métaliques une fois pour toutes. Il ne faut surtout pas se planter à l’étape de conception car on ne pourra pas modifier les interconnexions une fois la production lancée.

Pour réaliser un ASIC, il faut fournir un plan des masques de chaque couche de dopage du silicium ainsi que des couches métaliques. Voici par exemple la représentation d’une bascule D :
Une bascule D

Pour ce faire, on va partir d’une description RTL (Register Transfert Level) du composant, similaire aux descriptions utilisées pour les FPGA – la plupart du temps du Verilog ou du VHDL — que nous allons « synthétiser » en une Netlist. La suite va ressembler (de loin) à du placement‐routage et de la simulation analogique‐numérique, comme on peut le voir avec la conception de carte électronique.

Le flot de conception typique du monde du matériel est donné dans une des diapositives de la présentation de Tim Ansell ci‑dessous :
Flot de développement ASIC/FPGA

La partie langage de description du matériel et simulation est déjà largement libérée. Il existe des tas de composants open source décrits en VHDL et/ou en Verilog à présent. Les outils de synthèse libres arrivent aujourd’hui à maturité avec Yosys, bien sûr, pour le Verilog (et bientôt mature pour le VHDL grâce au greffon GHDL-yosys), mais aussi Alliance pour le VHDL.

Les trois piliers logiciels (EDA pour les outils, PDK les données et RTL le design) permettant de réaliser un ASIC sont donnés dans une autre diapo de Tim ci‑dessous :
Schéma de principe développement ASIC

Une fois la description « RTL » du composant synthétisée, il nous reste beaucoup d’étapes à franchir avant d’obtenir une description des masques de gravure permettant la fabrication proprement dite. Toutes ces étapes nécessitent l’utilisation de logiciels spécifiques pour réaliser les masques, construire l’arbre d’horloge, simuler en analogique certaines parties, concevoir les alimentations… Beaucoup de logiciels libres existent pour cela, tous ne sont pas matures ou restent très universitaire dans leur version open source. Mais il est possible de les utiliser tout de même pour réaliser un composant, comme l’a démontré Tim Edwards avec le Raven (un microcontrôleur RISC‑V à base de PicoRV32).

Cependant, même s’il n’a utilisé que des logiciels libres pour réaliser le Raven, Tim n’a pas pu accéder à la description physique des composants numériques qu’il utilisait. Il a dû se contenter de « boîtes noires » représentant chaque fonction logique à assembler pour réaliser le microcontrôleur. En effet, tous ces logiciels libres demeurent quasiment inutiles si l’on n’a pas accès à la description physique de la technologie cible utilisée. Les fondeurs de silicium fournissent un PDK (process design kit) contenant des bibliothèques de composants avec la description physique de leurs technologies, ainsi que la géométrie de chaque transistor et les modèles de simulations spice permettant de valider le comportement analogique. Et pour avoir accès à ces PDK, la vente de vos deux reins ne suffira pas, même si vous signez les triples NDA (accord de non‑divulgation) avec votre sang. Ce PDK reste le gros frein à la libération du matériel, un caillou dans la chaussure du matériel libre. C’est ce que Google a bien compris en finançant le développement d’un PDK libre via la société SkyWater : le SKY130.

La publication du SKY130 vient d’être annoncée cette semaine par Tim Ansell lors d’un « dial‑up » de la FOSSi Foundation. Comme son nom l’indique, ce PDK cible la technologie 130 nm. Cette taille de gravure peut sembler obsolète quand on sait qu’Intel fabrique de plus en plus en 7 nm, et commence même à tester le 4 nm. Mais les chaînes de fabrication de silicium avec cette finesse de gravure permettent un coût de production très raisonnable pour des performances qui ne sont pas non plus ridicules. SiFive, par exemple, a sorti un microcontrôleur 32 bits RISC‑V (E310) gravé en 180 nm et tout de même cadencé à 320 MHz. Il est donc possible de réaliser beaucoup de chose avec du 130 nm.

Et pour promouvoir son PDK et fédérer une communauté de passionnés, hobbyistes, universitaires, « startupeuses », etc., Google a décidé de produire quarante projets à base de ce PDK tous les six mois et gratuitement. Le premier « shuttle » est prévu pour novembre. Pour être dans le wagon, il faut que son projet soit open source et le soumettre au site en ligne efabless.com. Visiblement, la méthode de choix des projets retenus n’est pas encore bien définie ; mais si vous êtes retenu, vous aurez une réponse par courriel.

Il est temps pour LinuxFr.org de faire passer TapTempo dans une autre sphère que le simple programme en Brainfuck et de proposer un composant électronique TapTempoASIC !

Et pourquoi ne pas proposer un FPGA en 130 nm ? Même si aujourd’hui les FPGA sont plus proches du 40 nm, un FPGA open source comme le kFPGA de killruana, ça aurait la classe.

Aller plus loin

Kit de développement QORC

Comme j’en parlais sur LinuxFR, la société QuickLogic propose un kit de développement avec son microcontrôleur EOS S3. Micro qui a la prétention de n’utiliser que des logiciels libre pour son développement.

Réception

Le site web indiquait des «précommande». Je ne m’attendais donc pas à recevoir l’objet en moins d’une semaine, et sans frais de douanes !

Le kit tient dans le creux de la main

Bref, si vous arrivez a trouver quelques amis pour faire une commande groupée (les frais de port pour la France sont plus cher que le kit lui même : $58 pour un kit à $49), n’hésitez pas ! Ça arrivera vite.

Branchement

Au branchement sur l’usb-mini du kit, la led RGB s’allume à fond puis s’éteint progressivement en moins d’une seconde. Et … rien sur les messages kernel.

Il va falloir regarder tout ça de plus près et aller lire la doc. Le code source des exemples est dispo sur un github.

Clignotage de LED

QuickLogic vient de faire une vidéo basique pour donner quelques trucs de mise en route.

Pour que le port série soit détecté dans le kernel il faut notamment appuyer sur le bouton reset. La led bleue va clignoter 5 secondes. Il faudra attendre à nouveau 5 seconde et le port /dev/ttyACM0 apparaîtra dans le dmesg :

[juin30 13:25] usb 3-3.1.2: new full-speed USB device number 17 using xhci_hcd
[  +0,100996] usb 3-3.1.2: New USB device found, idVendor=1d50, idProduct=6140
[  +0,000005] usb 3-3.1.2: New USB device strings: Mfr=0, Product=0, SerialNumber=0
[  +0,000575] cdc_acm 3-3.1.2:1.0: ttyACM0: USB ACM device

On peut ensuite simplement s’y connecter avec screen pour récupérer une invite de commande sur le micro :

$ screen /dev/ttyACM0 115200
####################
Quicklogic QuickFeather LED / User Button Test
SW Version: qorc-sdk/qf_apps/qf_helloworldsw
Jun  7 2020 12:04:51
##########################



Hello world!!

#*******************
Command Line Interface
App SW Version: qorc-sdk/qf_apps/qf_helloworldsw
#*******************
[0] > 

De la on peut piloter les trois LED et lire le bouton, pour cela il suffit de se mettre en mode diagnostique:

[0] > red
ERROR: no such command: red
[0] > help
help-path: (top)
diag           - QuickFeather diagnostic commands
exit           - exit/leave menu
help           - show help
?              - show help
help-end:
[0] > diag
[1] diag > exit
[0] > help
help-path: (top)
diag           - QuickFeather diagnostic commands
exit           - exit/leave menu
help           - show help
?              - show help
help-end:
[0] > diag
[1] diag > help
help-path: diag
red            - toggle red led
green          - toggle green led
blue           - toggle blue led
userbutton     - show state of user button
exit           - exit/leave menu
help           - show help
?              - show help
help-end:
[1] diag > red
[1] diag > blue
[1] diag > red
[1] diag > green
[1] diag > blue
[1] diag > userbutton
Not pressed
[1] diag > userbutton
Pressed
[1] diag > 

EOS S3, le bitstream libéré !

[Dépêche initialement paru sur LinuxFR]

Pour configurer les différentes connexions des blocs de logiques contenus dans un FPGA il faut lui fournir un fichier de configuration appelé «bitstream». Quand on parle de libération des FPGA, on pense principalement à la publication de ces spécifications .
Jusqu’à présent, cette « libération » s’est faite, pour une poignée de FPGA (majoritairement Lattice), par ingénierie inverse. Donc jamais à l’initiative du constructeur, ce dernier n’ayant même pas toujours connaissance de projet d’ingénierie inverse à destination de ses produits. Et il faut aller fouiller dans d’obscurs fils Twitter et autre forums de bidouilleurs pour les découvrir.

Mais la libération s’accélère, et une petite société peu connue dans le monde du FPGA vient de lancer un produit basé sur des outils opensource pour le développement : l’EOS S3.

Comme on peut le voir dans le diagramme bloc ci-dessous, le produit est en fait un microcontrôleur Cortex-M4 qui possède une zone périphérique «de FPGA» appelé eFPGA.

EOS S3 Block Diagram

La société Quicklogic a considéré que développer des logiciels de synthèse et de placement routage n’était pas son métier. Elle s’est donc « contenté » de l’adapter aux logiciels open source de la suite symbiflow.

Pour la première fois dans l’histoire des FPGA, nous avons donc une société qui affirme documenter son « bitstream » et qui propose des outils libres pour le développement. C’est un événement que beaucoup attendaient depuis des dizaines d’années !

Bon le (tout petit) FPGA ne concerne qu’une partie du composant. Mais c’est un bon début, et l’utilisation de logiciels libres reste la philosophie de la société pour le développement de ce produit. Comme dit dans les avantages de la fiche marketing du kit de développement :

« No more multi Gigabyte software installs, no more of the hassles associated with proprietary tools, no more vendor-specific hardware incompatible with the industry. »

eFPGA

La datasheet nous dit que la partie FPGA (celle qui nous intéresse ici) est composée de :

  • 891 cellules logiques
  • 8 blocs de RAM double ports de 8Kbits
  • 2 multiplieurs câblés de 32×32 bits
  • 32 I/O configurables

Alors certes, on est très très bas dans la gamme des FPGA du marché. Mais on peut déjà envisager faire des petites choses intéressantes avec. Surtout qu’il n’y a pas que le FPGA dans ce microcontrôleur.

Kit de développement QuickFeather

Le kit est encore en phase de lancement, même s’il semble que certaines développeuses aient déjà reçu la carte pour faire des tests. Le tarif de $50 n’est pas prohibitif pour en envisager l’acquisition à des fin de tests. Les frais de port de $80 par contre posent problème, surtout s’il faut ajouter des frais de douane.

Bref, ça n’est pas du vaporware puisque les composants existent, mais il est pour l’instant difficile d’en dire plus concernant les outils. Dans tous les cas une nouvelle très rafraîchissante, et une accélération de la libération des FPGA qui fait plaisir !

[Édition le 17 juin 2020]

L’entreprise qui est derrière ce nouveau produit est Antmicro. Une entreprise qui fait de la conception FPGA/ASIC à base de logiciel libre.
Il semble également qu’ils aient été aidé par google.

Le communiqué de Antmicro.

Et en plus du EOS S3, Quicklogic lance une gamme de FPGA «discret» : le PolarPro 3E. Également basé sur une chaîne de développement libre \o/

Apicula : lancement de la libération du FPGA Gowin GW1N

[Dépèche écrite initialement pour LinuxFR]

Le lecteur assidu de LinuxFr.org sait déjà sans doute ce qu’est un FPGA. Rappelons‑en cependant brièvement la définition.

Les FPGA sont des composants constitués de « champs de portes programmables ». L’idée est de graver un certain nombre d’éléments logiques simples sous forme de matrice et de laisser au développeur le loisir de reconfigurer à l’infini les connexions entre ces portes. Une fois les connexions configurées, on se retrouve avec un composant numérique sur mesure qui ne ressemble à aucun composant disponible chez les fournisseurs classiques. C’est très pratique quand on a besoin d’architectures bâtardes, ou quand justement on développe un composant numérique : ça permet de reconfigurer à l’infini pour déverminer et évaluer les performances.

Pepijn de Vos a effectué un stage pour Symbiotic EDA. Et l’ingénierie inverse du GW1N était son sujet de stage. Il a rendu son rapport avant Noël sur GitHub et a publié le code source du projet Apicula.

Vous voulez en savoir plus, lisez la suite…

Sommaire

Parlons maintenant du grand drame des FPGA : ils sont complètement verrouillés car, pour reconfigurer ces fameuses connexions, il faut leur téléverser un fichier nommé bitstream qu’aucun constructeur de FPGA ne documente. Ce drame conduit les libristes que nous sommes à se taper des installations d’outils propriétaires particulièrement volumineux (surtout dans le cas de Xilinx et Altera) et pas toujours très stables. Tout ça pour générer le fameux bitstream.

Le format du bitstream n’est pourtant pas chiffré. Depuis plus d’une décennie, on sait qu’il est parfaitement possible d’en faire l’ingénierie inverse. Mais rien n’avait bougé jusqu’en 2015 quand Clifford (qui se prénomme maintenant Claire) Wolf a sorti sa suite open source pour le Lattice iCE40 : IceStorm. Le projet IceStorm avait pour but d’analyser toute la gamme des FPGA iCE40 pour en documenter le format du bitstream. Projet qui a parfaitement abouti et essaimé : toute la gamme des iCE40 est désormais accessible au moyen d’outils open source, ainsi que la gamme des ECP5 avec le Projet Trellis.

Presque tous les modèles de FPGA ont leur projet d’ingénierie inverse aujourd’hui. Tous ne sont pas terminés, loin s’en faut. Néanmoins, quelques‑uns avancent, comme le projet Apicula de Pepijn de Vos ciblant les FPGA du constructeur chinois Gowin. Dire que le projet Apicula est abouti serait un raccourci un peu rapide, il manque encore en effet un certain nombre de blocs à décoder. Cependant, il est possible aujourd’hui de réaliser un projet très simple (UNE LED QUI CLIGNOTE \o/) grâce au travail effectué.

Le Gowin GW1N

Voici l’architecture du GW1N donnée dans la documentation du composant :

Architecture global du GW1N

Oui, toi aussi, cher lecteur, tu te demandes bien l’intérêt de ce zoom. ;)

On voit différents éléments dans ce schéma, de la mémoire vive, des PLL pour générer les horloges, des multiplieurs câblés (DSP), des blocs d’entrées‑sorties (IOB) et surtout — ce que l’on voit le plus — des CFU (Configurable Function Unit).

Chez Gowin, le CFU est l’élément de base constitué ainsi :

Schéma d’architecture CFU

Les deux éléments qui nous intéressent ici sont : la LUT (Look Up Table) et le REG (registre). Ces deux éléments sont la base de la logique synchrone.

Le registre recopie son entrée sur la sortie au front montant de l’horloge, la sortie restant stable le reste du temps.

La LUT, comme son nom anglais l’indique, est une table de vérité, qui, dans le cas de ce petit FPGA, comporte quatre entrées binaires et une sortie. La configuration du FPGA viendra remplir cette table de vérité pour réaliser une fonction logique. Le registre se trouvant derrière se charge ensuite de verrouiller le résultat au rythme de l’horloge.

Si l’on arrive à déchiffrer le bitstream pour pouvoir configurer ces LUT, ces registres ainsi que les blocs d’entrées‑sorties (IOB), alors on a (presque) gagné : on peut réaliser un composant simple mais fonctionnel.

Et c’est ce qu’a réalisé Pepijn de Vos, on peut donc dire qu’il a amorcé la libération du GW1N de Gowin !

Le projet n’est cependant pas terminé, il faut encore déchiffrer les autres blocs pour permettre l’utilisation complète du FPGA. Il faut également réussir à documenter les temps de propagation des signaux entre les différents blocs. L’information de ces temps de propagation permet au logiciel de placement routage (nextpnr, pour ne citer que le plus célèbre en libre) de faire son travail correctement.

Mais alors, cette LED clignotante, elle vient ?

Minute, papillon ! Dans un premier temps, il va falloir trouver une carte électronique munie d’un FPGA de Gowin. Nous allons ensuite nous servir des données déjà produites par le projet Apicula pour faire la synthèse avec Yosys, puis le placement‐routage avec nextpnr.

Pour le moment, deux kits de développement ont été utilisés dans le projet Apicula :

Nous allons tester avec le kit allemand TEC0117, mais le Tang Nano ne change pas grand’chose à la procédure (et il est moins cher).

On doit installer :

  • Yosys, le logiciel de synthèse Verilog. Pour le détail des dépendances et autres subtilités d’installation, voir le site officiel. Sinon, pour résumer :
git clone https://github.com/YosysHQ/yosys.git
cd yosys make sudo make install
  • nextpnr, le logiciel de placement routage. Il faut le compiler avec le paramètre «generic». Les deux autres paramètres possible à ma connaissance sont ice40 et ecp5 (les deux gammes de FPGA vraiment prises en charge par nextpnr) : git clone https://github.com/YosysHQ/nextpnr.git cd nextpnr/ cmake -DARCH=generic . make sudo make install Dans mon cas, j’ai dû forcer l’utilisation de Python 3.7 dans le fichier CMakeLists.txt : find_package(PythonInterp 3.7 REQUIRED); pour pouvoir exécuter les scripts en argument avec Python 3.7.
  • Apicula, dont il faut cloner le dépôt Git : git clone https://github.com/pepijndevos/apicula.git cd apicula
  • pour l’instant la « base de données » des éléments trouvés par ingénierie inverse n’est pas « commité » dans le projet Apicula, il faut donc avoir une installation de l’EDI officiel de Gowin ; les scripts du projet Apicula iront fouiller dans les données de l’IDE pour générer un fichier intelligible en JSON et pickle (Python), il n’est cependant pas nécessaire d’avoir la licence ;
  • il faut également aller chercher le « pinout » de nos FPGA sur le site officiel de Gowin et le mettre dans son répertoire local nommé ~/Documents/gowinsemi :

Maintenant que nous avons les outils installés, lançons l’exemple générique du projet Apicula :

  • d’abord, on génère la base de données des éléments du FPGA : export GOWINHOME=/chemin/de/linstallation/gowin/IDE/ export DEVICE="GW1NR-9" # TEC0117 python dat19_h4x.py # makes $DEVICE.json python tiled_fuzzer.py # makes $DEVICE.pickle
  • muni de cette base de données, on peut se lancer dans la synthèse du (pas si) simple porte‑gramme de clignotement de LED donné en Verilog ci‑dessous : module top; wire clk; (* BEL="R29C29_IOBA", keep *) GENERIC_IOB #(.INPUT_USED(1), .OUTPUT_USED(0)) clk_ibuf (.O(clk)); wire [7:0] leds; (* BEL="R1C8_IOBA", keep *) GENERIC_IOB #(.INPUT_USED(0), .OUTPUT_USED(1)) led7_obuf (.I(leds[7])); (* BEL="R1C8_IOBB", keep *) GENERIC_IOB #(.INPUT_USED(0), .OUTPUT_USED(1)) led6_obuf (.I(leds[6])); (* BEL="R1C10_IOBA", keep *) GENERIC_IOB #(.INPUT_USED(0), .OUTPUT_USED(1)) led5_obuf (.I(leds[5])); (* BEL="R1C10_IOBB", keep *) GENERIC_IOB #(.INPUT_USED(0), .OUTPUT_USED(1)) led4_obuf (.I(leds[4])); (* BEL="R1C11_IOBA", keep *) GENERIC_IOB #(.INPUT_USED(0), .OUTPUT_USED(1)) led3_obuf (.I(leds[3])); (* BEL="R1C11_IOBB", keep *) GENERIC_IOB #(.INPUT_USED(0), .OUTPUT_USED(1)) led2_obuf (.I(leds[2])); (* BEL="R1C12_IOBA", keep *) GENERIC_IOB #(.INPUT_USED(0), .OUTPUT_USED(1)) led1_obuf (.I(leds[1])); (* BEL="R1C12_IOBB", keep *) GENERIC_IOB #(.INPUT_USED(0), .OUTPUT_USED(1)) led0_obuf (.I(leds[0])); reg [25:0] ctr; always @(posedge clk) ctr <= ctr + 1'b1; assign leds = ctr[25:18]; endmodule Un habitué des LED qui clignotent en Verilog reconnaîtra tout de suite le compteur dans les dernières lignes (always, reg…) mais sera peut‑être perturbé par la déclaration des entrées‑sorties. Il faut juste avoir en tête que le projet n’est pas terminé et qu’il faut se taper le placement‐routage des entrées‑sorties « à la main », d’où les directives (* ... *) et les modules GENERIC_IOB().
  • le script pour la synthèse et le placement routage est donné dans l’exemple : $ cd generic $ bash simple.sh blinky.v # TEC0117 $ cd .. $ python gowin_pack.py generic/pnrblinky.json $ python gowin_unpack.py pack.fs $ yosys -p "read_verilog -lib +/gowin/cells_sim.v; clean -purge; show" unpack.v
  • on doit se retrouver avec un bitstream nommé pack.fs que l’on peut téléverser dans le FPGA au moyen de l’utilitaire libre openFPGALoader maintenu par Trabucayre (Gwenhael Goavec‑Merou) : openFPGALoader -m -b littleBee pack.fs # FOSS programmer Parse pack.fs: Done erase SRAM Done Flash SRAM: [==================================================] 100.000000% Done SRAM Flash: FAIL Le FAIL est connu et vient d’une sombre histoire de somme de contrôle que openFPGALoader ne sait pas encore calculer et qu’Apicula ne fournit pas. Un ticket est ouvert sur le sujet dans le projet, Trabucayre sera ravi d’accepter des correctifs.

Et les huit LED doivent clignoter. Enfin, disons plutôt qu’elles comptent en binaire. Pour voir la vidéo des LED clignotantes, c’est sur YouTube.

Architectures de développement hétéroclites

Comme nous avons des outils open source, il est possible de développer sur des ordinateurs à base d’architectures différentes de x86. Voici un petit exemple de téléchargement d’un bitstream sur Tang Nano au moyen d’un Raspberry Pi (architecture ARM). Le bitstream en question permet de piloter un écran à cristaux liquides.

Chose impossible à faire avec les Vivado, Diamond et autres Quartus.

LCD sur Tang Nano

C’est encore très expérimental

Comme nous venons de le voir, le projet Apicula est encore très expérimental. Cependant, tous les ingrédients sont là et la preuve de fonctionnement est faite. Donc, à condition de mettre un minimum les mains dans le cambouis, on peut désormais générer des bitstreams pour les GW1Nx avec des outils open source.

Super ! Comment je fais pour contribuer ?

Autant d’enthousiasme fait plaisir à voir. Pour contribuer, le mieux est d’acquérir l’une des deux cartes citées dans cette dépêche et d’installer le logiciel officiel de Gowin.
Ensuite, différentes commandes permettant de mettre le pied à l’étrier de l’ingénierie inverse sont données sur le README.md du projet Apicula.

Sinon, n’hésitez pas à laisser une issue sur le projet GitHub ou d’interpeller Pepijn directement sur le « silo social Twitter ». Pepijn est super content de voir des gens s’intéresser au projet et répond très vite.

Aller plus loin

Test your Chisel design in python with CocoTB

Chisel is a hardware description language embedded in Scala language. Compared to VHDL/Verilog Chisel it’s a high-level language. With Chisel it’s easier to parametrize and to abstract your hardware. It’s the language used for all SiFive RISC-V cores and for Google Edge TPU.

What’s great with chisel that it generate Verilog sources for synthesis. And we can use this Verilog generated design for simulation or formal prove.

Simulation can be done in Scala with chisel.testers. But this tester is mostly under development project for the moment. And there is no test library for common busses and devices like SPI, Wishbone, AXI, PWM, …

CocoTB is a cosimulation testbench framework written in Python. Main advantage of CocoTB is that you write your testbench stimulis in python language. Python is really comfortable programming language. The other advantage of using CocoTB is that there is a growing library of modules available to test devices like SPI, Wishbone, USB, uart, … And its easier to use a library than to reinvent the wheel.

Then, let’s write Chisel testbench with CocoTB !

As an example we will use the ChisNesPad project (yes, same as formal prove article).

The directory structure is following :

/
|-- build.sbt  <- scala build configuration
|-- src/   <- all chisel sources
|   |-- main/
|       |-- scala/
|           |-- chisnespad.scala <- Chisel module we will test
|           |-- snespadled.scala <- "top" module to test with
|                                    tang nano (gowin)
|-- formal/   <- formal directory 
|-- platform/ <- some usefull files for synthesis with 
|                final platform (gowin).
|-- cocotb/   <- python cocotb tests
    |-- chisnespad/ <- test for chisnespad core
    |   |-- Makefile    <- makefile to compile and launch simulation
    |   |-- test_chisnespad.py <- cocotb stimulis
    |-- snespadled/ <- test for «top» project that toggle leds
        |              when push buttons
        |-- Makefile
        |-- test_snespadled.py

To launch tests we needs following dependencies :

  • Icarus Verilog : for simulation
  • Python 3: This example use python 3.7. It can be compiled and used with virtualenv
  • sbt: The scala build system
  • Chisel : The official website explain how to use it
  • CocoTB: and of course it need CocoTB that can be installed with python (python -m pip install cocotb)
  • cocotbify: python package included in repository chisverilogutil. Its used to inject some Verilog code in top module to generate VCD traces.
  • fpgamacro: it’s a Chisel library used to instantiate some fpga-specific RawModule. In our case it’s for ResetGen block.
  • gtkwave: VCD waveforms viewer.

Once all dependencies installed we can clone the chisNesPad project :

$ git clone https://github.com/Martoni/chisNesPad.git

Then launch simulation :


$ cd chisNesPad/cocotb/chisnespad/
$ make 
make[1]: Entering directory '/home/fabien/myapp/chisNesPad/cocotb/chisnespad'

[...] lots of compilation lines [...]

/myapp/chisNesPad/cocotb/chisnespad/build/libs/x86_64:/usr/local/lib:/usr/local/lib:/usr/local/lib:/usr/local/lib:/usr/local/lib MODULE=test_chisnespad \
        TESTCASE= TOPLEVEL=ChisNesPad TOPLEVEL_LANG=verilog COCOTB_SIM=1 \
        /usr/local/bin/vvp -M /home/fabien/myapp/chisNesPad/cocotb/chisnespad/build/libs/x86_64 -m gpivpi sim_build/sim.vvp   
     -.--ns INFO     cocotb.gpi                                  gpi_embed.c:103  in embed_init_python               Using virtualenv at /home/fabien/pyenv/pyenv37/bin/python.
     -.--ns INFO     cocotb.gpi                                GpiCommon.cpp:91   in gpi_print_registered_impl       VPI registered
     0.00ns INFO     Running tests with Cocotb v1.2.0 from /home/fabien/pyenv/pyenv37/lib/python3.7/site-packages
     0.00ns INFO     Seeding Python random module with 1583180134
     0.00ns INFO     Found test test_chisnespad.always_ready
     0.00ns INFO     Found test test_chisnespad.double_test
     0.00ns INFO     Found test test_chisnespad.simple_test
     0.00ns INFO     Running test 1/3: always_ready
     0.00ns INFO     Starting test: "always_ready"
                     Description: None
VCD info: dumpfile ChisNesPad.vcd opened for output.
401300.00ns INFO     Test Passed: always_ready
401300.00ns INFO     Running test 2/3: double_test
401300.00ns INFO     Starting test: "double_test"
                     Description: None
436000.00ns INFO     Value read CAFE
470420.00ns INFO     Value read DECA
471440.00ns INFO     Test Passed: double_test
471440.00ns INFO     Running test 3/3: simple_test
471440.00ns INFO     Starting test: "simple_test"
                     Description: None
506140.00ns INFO     Value read CAFE
507160.00ns INFO     Test Passed: simple_test
507160.00ns INFO     Passed 3 tests (0 skipped)
507160.00ns INFO     *************************************************************************
                     ** TEST                          PASS/FAIL  SIM TIME(NS)  REAL TIME(S)  RATIO(NS/S) **
                     *************************************************************************
                     ** test_chisnespad.always_ready    PASS       401300.00          2.78    144519.92  **
                     ** test_chisnespad.double_test     PASS        70140.00          0.49    143736.56  **
                     ** test_chisnespad.simple_test     PASS        35720.00          0.25    144120.85  **
                     **************************************************************************************
                     
507160.00ns INFO     *************************************************************************************
                     **                                 ERRORS : 0                                      **
                     *************************************************************************************
                     **                               SIM TIME : 507160.00 NS                           **
                     **                              REAL TIME : 3.52 S                                 **
                     **                        SIM / REAL TIME : 144276.59 NS/S                         **
                     *************************************************************************************
                     
507160.00ns INFO     Shutting down...
make[1]: Leaving directory '/home/fabien/myapp/chisNesPad/cocotb/chisnespad'

(Note : I can’t find how to change width of code text in this #*/% wordpress )

And we can see wave form with gtkwave:

$ gtkwave ChisNesPad.vcd
Waveform of CocoTB stimulis for NES Pad controller

Let’s see what happen

All commands are described in the Makefile in directory chisNesPad/cocotb/chisnespad/.

Chisel Module

The Chisel Module we test here is in directory src/main/scala/chisnespad/ and is named chisnespad.scala with following interfaces :

class ChisNesPad (val mainClockFreq: Int = 100,
                  val clockFreq: Int = 1,
                  val regLen: Int = 16) extends Module {
  val io = IO(new Bundle{
    /* SNES Pinout */
    val dclock = Output(Bool())
    val dlatch = Output(Bool())
    val sdata  = Input(Bool())
    /* read/valid output */
    val data = Decoupled(Output(UInt(16.W)))
  })
//...
}

The scala verilog generator driver is given at the end of file :

object ChisNesPad extends App {
  println("Generating Verilog sources for ChisNesPad Module")
  chisel3.Driver.execute(Array[String](), () => new ChisNesPad)
}

This object will be called by SBT following command:

$ sbt "runMain chisnespad.ChisNesPad"

Generated Verilog

This will generate the Verilog file named ChisNesPad.v in root directory. With following interfaces :

module ChisNesPad(
  input         clock,
  input         reset,
  output        io_dclock,
  output        io_dlatch,
  input         io_sdata,
  input         io_data_ready,
  output        io_data_valid,
  output [15:0] io_data_bits
);
//...
endmodule

As we can see, all bundled ports are kept but with little modification : dot ‘.’ are replaced by underscore ‘_’. clock and reset has been added and we can retrieve our decoupled signal io.data.{ready, valid, bits} -> io_data_{ready, valid, bits} .

CocoTB testbench

With these changes in mind, we can read/write our chisel ports signals with CocoTB.

CocoTB tests are described in file test_chisnespad.py. This file describe a class to store all method and data for testing ChisNesPad Module then list cocotb test function :

# main class for all test
class ChisNesPadTest(object):
    """
    """
    LOGLEVEL = logging.INFO
    PERIOD = (20, "ns")
    SUPER_NES_LEN = 16
    NES_LEN = 8

    def __init__(self, dut, reg_init_value=0xcafe, reg_len=16):
        if sys.version_info[0] < 3:
            raise Exception("Must be using Python 3")
        self._dut = dut
#...
# all tests
@cocotb.test()
def simple_test(dut):
    cnpt = ChisNesPadTest(dut)
    yield cnpt.reset()
    yield Timer(1, units="us")
    dut.io_data_ready <= 1
#...

@cocotb.test()#skip=True)
def double_test(dut):
    cnpt = ChisNesPadTest(dut)
    yield cnpt.reset()
#...

@cocotb.test()
def always_ready(dut):
    cnpt = ChisNesPadTest(dut)
    yield cnpt.reset()
#...

Here we see tree tests decorated with @cocotb.test(). The our module ChisNesPad is the Device Under Test (DUT) and is passed in test function arguments : dut.

To access input/output ports we just have to use dot on our dut object.

  • set io.data.ready to logic level ‘1’ :
    dut.io_data_ready <= 1
  • read io.data.bits
    vread = int(dut.io_data_bits)
  • We can also read register under the module or a submodule :
    countvalue = int(dut.countReg)

It’s also possible to write register under the module, but be careful of the race condition when you doing that. It can be re-written by simulation with 0-delay.

Get Waveform

All tests can be done with procedure describe above. But with Icarus as simulator we don’t get the waveforms.

It’s not easy to develop HDL without any waveform. To get waveform we can use another simulator that will generate the traces (mainly in VCD format) but Icarus is mature and free then it’s cheaper to use it.

The solution given in CocoTB documentation is to add following verilog code in top module :

`ifdef COCOTB_SIM
initial begin
  $dumpfile ("ChisNesPad.vcd");
  $dumpvars (0, ChisNesPad);
  #1;
end
`endif

With this $dumpX() function we will records all signals under the file named ChisNesPad.vcd. If we had to add this code by hand each time we re-generate verilog from Chisel module, it would quickly become painful.

That why we use the tool cocotbify, included in package chisverilogutils.

$ cocotbify
Usages:
cocotbify.py [options]
-h, --help             print this help
-v, --verilog          verilog filename to modify (filename is used 
                       as module name)
-o, --output filename  output filename

This tool will take a verilog source as input and generate an output with dumpvars code added for cocotb. In the example makefile the output name will be ChisNesPadCocotb.v. This file will be used by CocoTB and Icarus for simulation. VCD file can then be view with gtkwave:

$ gtkwave ChisNesPad.vcd
Simulation traces

Conclusion

As we can see, it’s perfectly possible to use CocoTB framework for testing Chisel components. CocoTB has more library test modules available than chisel.tester and we can code in Python. Python is used by lots of peoples through the world and is less scary than Scala or SystemVerilog for hardware engineers that develop digital hardware.

15$ ECP5 board kit

ECP5 is a great FPGA, it was reversed in Trellis, it’s bigger than ICE40 that was reversed before in icestorm project. And it have lots of cool stuff like

  • multipliers
  • serdes
  • 25klut min (85 max)
  • and lots of memory bits

But ECP5 board available on the web are little bit expensive (if you have nothing to do with it ;). Even the OrangeCrab will be about 80$ minimum (but with DDR3 and USB on it).

There is a rumor on the web that this leds display board include an ECP5 :

The Board as received

It’s really interesting, because this board cost only $15 ! With the dual SDRAM (M12L16161A) provided and its dual gigabit ethernet phy (Boardcom B50612D B1KMLG). For this low-cost price I order one of course.

Removing the sticker unveil an ECP5 25k !

I just received it and if we remove the sticker we see a Lattice ECP5 ( LFE5U-25F-6BG256C).

\o/ It’s a really lowcost ECP5 dev kit !

But without schematics. Mike Walter began to reverse it and document the board on its github project.

[Edit 1 March]

Anton Blanchard give the jtag+uart pinout on its twitter profile :

Jtag Uart pinout from Anton Blanchard (twitter)

I configured the FPGA with this adapter from seeedstudio (7.6$), which is a simple FT2232 adapter.

Connect and configure with openFPGALoader

ECP5 is available in openFPGALoader list as we can see :

$ openFPGALoader --list-fpga
IDCode      manufacturer  family         model               
0x81113043  lattice       ECP5-5G        LFE5UM5G-85F-8BG381 
0x100381b   Gowin         GW1N           GW1N-4              
0x20f30dd   altera        cyclone 10 LP  10CL025             
0x3620093   xilinx        spartan7       xc7s15ftgb196-1     
0x362d093   xilinx        artix a7 35t   xc7a35              
0x900281b   Gowin         GW1N           GW1N-1              
0x1100581b  Gowin         GW1N           GW1NR-9             
0x13631093  xilinx        artix a7 100t  xc7a100             
0x41111043  lattice       ECP5           LFE5U-25F-6BG256C   
0x612bd043  lattice       MachXO3LF      LCMX03LF-6900C   
   
$ openFPGALoader -cdigilent --detect
idcode 0x41111043
manufacturer lattice
model  LFE5U-25F-6BG256C
family ECP5

Open source synthesize and place&route tools

We can then load a simple blinker bitstream with openFPGALoader. But first, we have to synthesize one. Trabucayre gave me a simple blinker project I added to the BLP (Blinking Led Project).

This project require yosys, nextpnr and trellis to be installed. Installations instructions are given on trellis repository.

$ git clone --recursive https://github.com/SymbiFlow/prjtrellis
$ cd prjtrellis/libtrellis
$ cmake -DCMAKE_INSTALL_PREFIX=/usr .
$ make
$ sudo make install

Then for next-pnr:

$ git clone https://github.com/YosysHQ/nextpnr.git
$ cd nextpnr
$ cmake -DARCH=ecp5 -DTRELLIS_INSTALL_PREFIX=/usr/ .
$ make
$ sudo make install

And finally Yosys

$ git clone https://github.com/YosysHQ/yosys
$ cd yosys
$ make
$ sudo make install

Synthesize blinker

The blinker projet can be found on this github repository :

$ git clone https://github.com/Martoni/blp.git
$ cd blp/platforms/colorlight/
$ make
...
ecppack --svf blink.svf blink_out.config blink.bit

Then, once JTAG is plugged we can download it with openFPGALoader :

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

And see the orange LED blinking !

Some links

[this article will be edited as I progress]

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 ?