Archives par mot-clé : verilog

Découverte du FPGA européen, le GateMate de CologneChip

Nous l’attendions depuis au moins deux ans, le FPGA européen GateMate des allemands de CologneChip est désormais disponible dans votre crémerie habituelle.

Ça y est il est arrivé, le kit de développement GateMate !

La dimension européenne de ce FPGA n’est pas la seule nouveauté, c’est également un des premier (mais pas le premier) à privilégier les outils open source pour son utilisation. Que cela soit pour la simulation ou pour la synthèse tous les exemples donnés dans la documentation utilisent des logiciels libres (Icarus, GHDL et surtout Yosys). Même pour la visualisation des chronogrammes, gtkwave est utilisé par défaut en exemple.

[À noter que le kit de développement m’a été offert gracieusement par CologneChip]

Caractéristiques du GateMate

Les caractéristiques du GateMate le positionne au niveau d’un petit Spartan7 de Xilinx ou d’un Trion T20 de Efinix.

Le composant est gravé par GlobalFounderies en 28nm.

Architecture générale (DS1001)

La cellule de base est nommée CPE pour «Central Programming Element».

Structure du CPE (DS1001)

On notera l’absence remarqué de blocs multiplieurs. Cette absence est compensée par le «fast signal path routing» qui permet de chaîner les CPE afin de construire un multiplieur de dimension voulue.

Caractéristiques du kit

Pour le moment, seuls les trois petit FPGA de la gamme GateMate semblent être en production. CologneChip propose un kit de développement muni du plus petit GateMate : le CCGM1A1

Le schéma blocs de la carte de développement (source pdf officiel)

La carte de développement possède deux entrées USB:

  • une pour l’alimentation
  • et une pour la programmation et la communication avec le FPGA (FTDI 2232), mais qui peut également servir d’alimentation.

La magie du logiciel libre openFPGALoader permet de détecter le FPGA directement au branchement:

$ openFPGALoader --detect
Jtag frequency : requested 6.00MHz   -> real 6.00MHz  
index 0:
	idcode 0x20000001
	manufacturer colognechip
	family GateMate Series
	model  GM1Ax
	irlength 6

En effet, avant même la sortie du gatemate, CologneChip avait déjà proposé le support du composant sur le dépot openFPGALoader.

Toolchain

CologneChip fourni un guide d’installation de la chaîne de développement sur son site internet.

Hormis le logiciel de placement routage (GateMate), tous les outils sont des logiciels libre bien connus du monde du FPGA (source UG1002).

Tous les outils sont connus du monde du FPGA opensource et leurs installations sont intensivement décrites dans les différents dépôts des projets.

Si l’on souhaite éviter la case compilation, l’entreprise fournie même des versions binaires. Ces binaires ne sont téléchargeable que via un compte enregistré sur leur site pour le moment. Deux paquets de logiciels sont nécessaires :

  • Yosys compilé pour le gatemate: pour la synthèse Verilog
  • p_r: le logiciel de placement routage.

Pour le moment, la version binaire proposée en téléchargement sur le site n’est disponible que pour windows. Ces «.exe» s’exécutent cependant parfaitement sous Linux au moyen de l’émulateur wine bien connu des Linuxiens.

L’archive téléchargée se décompresse simplement avec unzip :

$ unzip cc-toolchain-win.zip 
Archive:  cc-toolchain-win.zip
 extracting: cc-toolchain-win/openFPGALoader-mingw64-v.0.8.0+80eeaef.zip  
 extracting: cc-toolchain-win/p_r-2022.04-001.zip  
  inflating: cc-toolchain-win/ug1002-toolchain-install-2022-04.pdf  
 extracting: cc-toolchain-win/yosys-win32-mxebin-0.15+57.zip  

La version windows de openFPGALoader ne fonctionne pas bien en émulation wine, il est préférable d’en compiler une version à jour à partir des sources officiels.

Pour le reste, on peut s’affranchir de compiler yosys en utilisant celle fournie. Et pour p_r, les sources n’étant pas fournies pour le moment, cette version est la seule que nous pourrons utiliser.

Pour les installer, il suffit de les décompresser :

$ cd cc-toolchain-win/
$ unzip p_r-2022.04-001.zip
$ unzip yosys-win32-mxebin-0.15+57.zip

La notice d’utilisation des commandes est données dans le pdf de l’archive nommé ug1002-toolchain-install-2022-04.pdf.

C’est l’installation la plus simple que j’ai pu avoir à faire pour des outils de développement FPGA. La place occupée sur le disque dur de son ordinateur est plusieurs milliers de fois plus petites que les logiciels habituels :

$ cd p_r-2022.04-001/
$ du -sh .
24M	.
$ cd yosys-win32-mxebin-0.15+57/
$ du -sh .
32M	.

Évidemment, c’est pour seulement un modèle de FPGA, mais cela reste beaucoup plus petit.

Clignotons

Il est temps de rentrer dans le vif du sujet et de faire clignoter les LED. L’exemple donné dans le document ug1002 est trop rapide pour voir les LED clignoter. Nous allons donc faire un clignoteur plus traditionnel comme visible ci-dessous en Verilog :

`timescale 1ns / 1ps

module blink(
		input wire clk,
		input wire rst,
		output reg led
	);

	localparam MAX_COUNT = 10_000_000;
	localparam CNT_TOP = $clog2(MAX_COUNT);

	wire i_clk;
	reg [CNT_TOP-1:0] counter;

	assign i_clk = clk;

	always @(posedge i_clk)
	begin
		if (!rst) begin
			led <= 0;
			counter <= 0;
		end else begin
			if(counter < MAX_COUNT/2)
				led <= 1;
			else
				led <= 0;

			if (counter >= MAX_COUNT)
				counter <= 0;
			else
				counter <= counter + 1'b1;
		end
	end

endmodule

Contrairement à beaucoup de FPGA, le GateMate ne définit pas d’états initial à 0 de ses registres. Une entrée reset est donc nécessaire.

Le pinout est décrit au moyen d’un fichier «ccf» :

## blink.ccf

Pin_in   "clk"  Loc = "IO_SB_A8" | SCHMITT_TRIGGER=true;
Pin_in   "rst"  Loc = "IO_EB_B0"; # SW3
Pin_out  "led"  Loc = "IO_EB_B1"; # D1

Une fois que ces deux fichiers sont prêt il suffit de lancer yosys pour la synthèse :

$ wine ../../cc-toolchain-win/yosys-win32-mxebin-0.15+57/yosys.exe -l yosys.log -p 'read_verilog blink.v; synth_gatemate -top blink -vlog blink_synth.v'

Wine génère tout un tas d’erreurs mais fini par nous lancer la synthèse tout de même

$ wine ../../cc-toolchain-win/yosys-win32-mxebin-0.15+57/yosys.exe -l yosys.log -p 'read_verilog blink.v; synth_gatemate -top blink -vlog blink_synth.v'
wine: created the configuration directory '/home/oem/.wine'
0012:err:ole:marshal_object couldn't get IPSFactory buffer for interface {00000131-0000-0000-c000-000000000046}
0012:err:ole:marshal_object couldn't get IPSFactory buffer for interface {6d5140c1-7436-11ce-8034-00aa006009fa}
0012:err:ole:StdMarshalImpl_MarshalInterface Failed to create ifstub, hres=0x80004002
0012:err:ole:CoMarshalInterface Failed to marshal the interface {6d5140c1-7436-11ce-8034-00aa006009fa}, 80004002
0012:err:ole:get_local_server_stream Failed: 80004002
0014:err:ole:marshal_object couldn't get IPSFactory buffer for interface {00000131-0000-0000-c000-000000000046}
0014:err:ole:marshal_object couldn't get IPSFactory buffer for interface {6d5140c1-7436-11ce-8034-00aa006009fa}
0014:err:ole:StdMarshalImpl_MarshalInterface Failed to create ifstub, hres=0x80004002
0014:err:ole:CoMarshalInterface Failed to marshal the interface {6d5140c1-7436-11ce-8034-00aa006009fa}, 80004002
0014:err:ole:get_local_server_stream Failed: 80004002
Could not find Wine Gecko. HTML rendering will be disabled.
Could not find Wine Gecko. HTML rendering will be disabled.
wine: configuration in L"/home/oem/.wine" has been updated.

On ne va pas recopier toute la trace de synthèse ici mais juste la partie ressources utilisées donnée en fin de synthèse :

2.49. Printing statistics.

=== blink ===

   Number of wires:                 49
   Number of wire bits:            294
   Number of public wires:           5
   Number of public wire bits:      28
   Number of memories:               0
   Number of memory bits:            0
   Number of processes:              0
   Number of cells:                159
     CC_ADDF                        65
     CC_BUFG                         1
     CC_DFF                         25
     CC_IBUF                         2
     CC_LUT1                        24
     CC_LUT2                         5
     CC_LUT4                        36
     CC_OBUF                         1

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

2.51. Executing OPT_CLEAN pass (remove unused cells and wires).
Finding unused cells or wires in module \blink..

2.52. Executing Verilog backend.

2.52.1. Executing BMUXMAP pass.

2.52.2. Executing DEMUXMAP pass.
Dumping module `\blink'.

End of script. Logfile hash: dcf7a4084e
Yosys 0.15+57 (git sha1 207417617, i686-w64-mingw32.static-g++ 11.2.0 -Os)
Time spent: 1% 19x opt_clean (0 sec), 1% 18x opt_expr (0 sec), ...

Le fichier de sortie blink_synth.v est au format … Verilog également! C’était bien la peine de lancer Yosys tient !

Mais non, Verilog est un excellent format pour décrire une netlist autant que du RTL. Et de fait, le code Verilog généré n’est pas hyper lisible. Il est constitué d’une série d’instanciations et de connections des primitives du FPGA :

//...
 
 CC_LUT2 #(
    .INIT(4'h8)
  ) _051_ (
    .I0(_041_[0]),
    .I1(_041_[1]),
    .O(_043_[2])
  );
  CC_LUT4 #(
    .INIT(16'h0001)
  ) _052_ (
    .I0(counter[15]),
    .I1(counter[20]),
    .I2(counter[23]),
    .I3(counter[13]),
    .O(_041_[0])
  );

//...

Code qui reste parfaitement simulable avec Icarus pour faire de la simulation post-synthèse comme expliqué dans la documentation officielle.

Maintenant que nous avons notre netlist passons aux choses sérieuses avec le placement routage :

$ wine ../../cc-toolchain-win/p_r-2022.04-001/p_r.exe -i blink_synth.v -o blink -lib ccag
GateMate (c) Place and Route
Version 4.0 (4 April 2022)
All Rights Reserved (c) Cologne Chip AG

...

Comme pour la synthèse, nous n’allons pas mettre tous les messages ici. Une des information qui nous intéresse en priorité pour le placement routage est la performance en vitesse.

...
Static Timing Analysis
Longest Path from Q of Component 25_1 to D-Input of Component 33/1 Delay: 18215 ps
Maximum Clock Frequency on CLK 230/3:   54.90 MHz
...

La vitesse d’horloge maximale est donc de 54.90Mhz. Cela peut sembler ridicule mais il faut prendre en compte que :

  • L’architecture du «clignoteur» avec un énorme compteur pour diviser l’horloge n’est absolument pas optimisée. Pour faire bien il faudrait pipeliner le compteur mais ça n’est pas le sujet ici. Ces mauvais résultats sont cohérent avec ce qu’on pourrait obtenir avec un autre FPGA «mainstream».
  • Ces performances sont «conservatrice» c’est le pire cas quand le FPGA est très chaud.

Bref, pour faire clignoter une LED, on peut raisonnablement doubler cette fréquence d’horloge si on veut 🙂 Mais comme nous n’utilisons pas de PLL ici, la fréquence d’entrée de 10Mhz rentre dans la specification.

Les statistiques d’utilisation du FPGA sont données à la fin de la synthèse :

CPE_USAGE_INPUT - CPE_COMBSEQ         1/8 :     0 /     21   (  0.0%)
CPE_USAGE_INPUT - CPE_COMBSEQ         2/8 :    11 /     21   ( 52.4%)
CPE_USAGE_INPUT - CPE_COMBSEQ         3/8 :     0 /     21   (  0.0%)
CPE_USAGE_INPUT - CPE_COMBSEQ         4/8 :     0 /     21   (  0.0%)
CPE_USAGE_INPUT - CPE_COMBSEQ         5/8 :     0 /     21   (  0.0%)
CPE_USAGE_INPUT - CPE_COMBSEQ         6/8 :    10 /     21   ( 47.6%)
CPE_USAGE_INPUT - CPE_COMBSEQ         7/8 :     0 /     21   (  0.0%)
CPE_USAGE_INPUT - CPE_COMBSEQ         8/8 :     0 /     21   (  0.0%)

CPE_USAGE_INPUT - CPE_COMB            1/8 :     3 /      3   ( 100.0%)
CPE_USAGE_INPUT - CPE_COMB            2/8 :     0 /      3   (  0.0%)
CPE_USAGE_INPUT - CPE_COMB            3/8 :     0 /      3   (  0.0%)
CPE_USAGE_INPUT - CPE_COMB            4/8 :     0 /      3   (  0.0%)
CPE_USAGE_INPUT - CPE_COMB            5/8 :     0 /      3   (  0.0%)
CPE_USAGE_INPUT - CPE_COMB            6/8 :     0 /      3   (  0.0%)
CPE_USAGE_INPUT - CPE_COMB            7/8 :     0 /      3   (  0.0%)
CPE_USAGE_INPUT - CPE_COMB            8/8 :     0 /      3   (  0.0%)

CPE_USAGE_INPUT - CPE COMBSEQ+COMB    1/8 :     3 /     24   ( 12.5%)
CPE_USAGE_INPUT - CPE COMBSEQ+COMB    2/8 :    11 /     24   ( 45.8%)
CPE_USAGE_INPUT - CPE COMBSEQ+COMB    3/8 :     0 /     24   (  0.0%)
CPE_USAGE_INPUT - CPE COMBSEQ+COMB    4/8 :     0 /     24   (  0.0%)
CPE_USAGE_INPUT - CPE COMBSEQ+COMB    5/8 :     0 /     24   (  0.0%)
CPE_USAGE_INPUT - CPE COMBSEQ+COMB    6/8 :    10 /     24   ( 41.7%)
CPE_USAGE_INPUT - CPE COMBSEQ+COMB    7/8 :     0 /     24   (  0.0%)
CPE_USAGE_INPUT - CPE COMBSEQ+COMB    8/8 :     0 /     24   (  0.0%)

IO_USAGE                         :      3 /   144    (  2.1%) of all IOs
IO_USAGE_TYPE - IBF              :      2 /   144    (  1.4%) of all IOs    ( 66.7%) of used IOs
IO_USAGE_TYPE - OBF              :      1 /   144    (  0.7%) of all IOs    ( 33.3%) of used IOs
IO_USAGE_TYPE - TOBF             :      0 /   144    (  0.0%) of all IOs    (  0.0%) of used IOs
IO_USAGE_TYPE - IOBF             :      0 /   144    (  0.0%) of all IOs    (  0.0%) of used IOs

CPE_USAGE_PHYS - CPE_COMB_ONLY   :     73 / 20480    (  0.4%) of all CPEs   ( 60.3%) of occupied CPEs
CPE_USAGE_PHYS - CPE_SEQ_ONLY    :      5 / 20480    (  0.0%) of all CPEs   (  4.1%) of occupied CPEs
CPE_USAGE_PHYS - CPE_BRIDGE_ONLY :      0 / 20480    (  0.0%) of all CPEs   (  0.0%) of occupied CPEs
CPE_USAGE_PHYS - CPE_CARRY_ONLY  :      0 / 20480    (  0.0%) of all CPEs   (  0.0%) of occupied CPEs
CPE_USAGE_PHYS - CPE_COMB+SEQ    :     10 / 20480    (  0.0%) of all CPEs   (  8.3%) of occupied CPEs
CPE_USAGE_PHYS - CPE_COMB+BRIDGE :      0 / 20480    (  0.0%) of all CPEs   (  0.0%) of occupied CPEs
CPE_USAGE_PHYS - CPE_COMBSEQ     :     21 / 20480    (  0.1%) of all CPEs   ( 17.4%) of occupied CPEs

CPE_USAGE_LOGIC - CPE_COMB       :      8 / 20480    (  0.0%) of all CPEs   (  6.6%) of occupied CPEs
CPE_USAGE_LOGIC - CPE_SEQ        :     15 / 20480    (  0.1%) of all CPEs   ( 12.4%) of occupied CPEs
CPE_USAGE_LOGIC - CPE_COMBSEQ    :     21 / 20480    (  0.1%) of all CPEs   ( 17.4%) of occupied CPEs
CPE_USAGE_LOGIC - CPE_BRIDGE     :      0 / 20480    (  0.0%) of all CPEs   (  0.0%) of occupied CPEs

CPE_USAGE_OVERALL                :    121 / 20480    (  0.6%) of all CPEs occupied
CPE_USAGE_LOGIC                  :     94 / 20480    (  0.5%) of all CPEs used for customer logic

Component Statistics:
         AND        32        19%
        ADDF         2         1%
       ADDF2        60        37%
        C_OR        48        29%
      Route1         4         2%
    CP_route        15         9%
              --------
Sum of COMB:       161

           D        25        92%
       C_0_1         2         7%
              --------
Sum of SEQ:         27

Sum of all:        188

Et le bitstream généré est au format *.cfg (ascii) ou *.cfg.bit (binaire).

$ ls -lha blink_00.*
-rw-rw-r-- 1 oem oem 121K May  1 08:38 blink_00.cdf
-rw-rw-r-- 1 oem oem 1.4M May  1 08:38 blink_00.cfg
-rw-rw-r-- 1 oem oem  48K May  1 08:38 blink_00.cfg.bit
-rw-rw-r-- 1 oem oem  465 May  1 08:38 blink_00.pin
-rw-rw-r-- 1 oem oem 6.0K May  1 08:38 blink_00.place
-rw-rw-r-- 1 oem oem  65K May  1 08:38 blink_00.SDF
-rw-rw-r-- 1 oem oem  42K May  1 08:38 blink_00.used
-rw-rw-r-- 1 oem oem  79K May  1 08:38 blink_00.V

Pour configurer le FPGA nous utiliserons openFPGALoader en «natif» :

$ openFPGALoader -b gatemate_evb_jtag blink_00.cfg.bit
Jtag frequency : requested 6.00MHz   -> real 6.00MHz  
Load SRAM via JTAG: [==================================================] 100.00%
Done
Wait for CFG_DONE DONE

Et la LED clignote :

Ressources

sv2chisel, le convertisseur (System)Verilog vers Chisel

Le monde du FPGA (et de l’ASIC) regorge aujourd’hui de langages de description matériel. Au Verilog et VHDL s’ajoute maintenant tout un tas de langages comme Migen, Clash, BlueSpec, Amaranth, Chisel, SpinalHDL, Silice, … et j’en oublie plein. Tous ces langages permettent de générer du Verilog. Les possibilité de conversion de VHDL vers Verilog ne sont maintenant plus une utopie grâce aux évolutions de GHDL et de Yosys.

Bref, il existe désormais toujours une possibilité de convertir l’intégralité du projet en Verilog de manière à le simuler et synthétiser avec les outils conçus pour lui.

C’est quelque chose de très appréciable pour faire de la réutilisation de code. Il n’est plus nécessaire de re-concevoir un composant en VHDL tout ça parce que le contrôleur open source qui nous est nécessaire est codé en Verilog.

L’homogénéité de langage des sources d’un projet peut cependant être appréciable dans certain cas. Notamment quand le langage de description possède ses propres librairies de simulation comme c’est le cas en Chisel.

On peut certes instancier les «sous»-modules Verilog au moyen de BlackBox, mais ils ne seront pas simulable avec ChiselTest par exemple car treadle se cassera les dents dessus.

C’est là qu’intervient le nouveau projet nommé sv2chisel pour convertir du (system)Verilog en chisel.

Je vous propose ici de tester ensemble l’utilitaire dans un cas pratique. Je souhaite convertir le module Verilog fake_differential du projet d’exemple de l’ulx3s qui permet de générer un signal HDMI différentiel pour l’intégrer dans le projet HdmiCore écrit en Chisel. L’objectif étant de porter le projet HdmiCore sur la plate-forme ulx3s en restant dans du pure Chisel.

Installation de l’outil

Toutes les caractéristiques et limitations du convertisseur sont données sur le wiki. Pour l’installer nous allons cloner le projet github. Le projet n’en est pas à sa version 1.0, il est sans doute préférable de «travailler» sur le main du git plutôt que sur une release.

$ git clone https://github.com/ovh/sv2chisel.git
$ cd sv2chisel

Les étapes d’installations depuis les sources sont données dans le readme. Il faut publier localement sv2chisel ainsi que les «helpers» :

$ sbt publishLocal

Cette commande fonctionne pas chez moi, je pensais naïvement que c’était la même commande que celle consistant à lancer sbt puis taper «publishLocal» mais non 😉

Donc pour publier localement, on fera plutôt comme recommandé dans le readme :

$ sbt
sbt:sv2chisel> publishLocal
sbt:sv2chisel> helpers/publishLocal
sbt:sv2chisel> assembly

La commande «assembly» génère le fichier jar exécutable.

Le binaire de l’utilitaire est généré dans le répertoire utils/bin/ et se nomme tout simplement sv2chisel

$ ./sv2chisel -help
sv2chisel [Options] sv_files... or sv2chisel [Options] -c config_file

Commons Options:
    -l, --log-level <error|warn|struct|info|debug|trace>
                                     Logger verbosity level
    -L, --class-log-level CLASS_NAME:<error|warn|struct|info|debug|trace>
                                     Logger verbosity level within given CLASS_NAME (useful for transforms)
    -o, --emission-path PATH         Base emission path

Config File (prio over manually specified files):
    -c, --config-file FILE           Yaml Configuration File

Manual command-line configuration
    -i, --base-path PATH             Base path for files
    -n, --name NAME                  Project name
    -h, --help                       Show this message

Si l’on regarde dans le fichier on trouve un simple lien vers l’archive «jar» se trouvant dans le même répertoire:

$ ls 
sv2chisel  sv2chisel.jar

$ cat sv2chisel
#!/bin/bash

path=`dirname "$0"`
cmd="java -cp ${path}/sv2chisel.jar sv2chisel.Main ${@:1}"

Conversion

Pour convertir en Chisel, on peut simplement donner les noms des fichiers sources en arguments:

$ ./sv2chisel fake_differential.v
[log] ---- Processing project ----
[log] ############# Parsing fake_differential.v #############
[log] ######### Elapsed time for fake_differential.v #########
[log] # Lexing+Parsing Time : 335.206505 ms
[log] # Mapping to IR Time : 126.985877 ms
[log] ######### Executing 18 transforms #########
[log] ####### sv2chisel.transforms.CheckUseBeforeDecl #######
[log] # Elapsed time : 26.214516 ms
[log] ####### sv2chisel.transforms.CheckScopes #######
[log] # Elapsed time : 7.222317 ms
[log] ####### sv2chisel.transforms.CheckBlockingAssignments #######
[log] # Elapsed time : 1.448437 ms
[log] ####### sv2chisel.transforms.InferDefLogicClocks #######
[info] Registering a new clock clk_shift for module fake_differential (non blocking assignment) at fake_differential.v:3:0>>54:0
[warn] Unable to find module module ODDRX1F instanciated as ddr_p_instance in current module fake_differential for clock inference processing. at fake_differential.v:33:10>>41:11
[warn] Unable to find module module ODDRX1F instanciated as ddr_n_instance in current module fake_differential for clock inference processing. at fake_differential.v:42:10>>50:11
[log] # Elapsed time : 41.125895 ms
[log] ####### sv2chisel.transforms.PropagateClocks #######
[warn] Module ODDRX1F referenced by instance ddr_p_instance cannot be found in current design. Clock & Reset management might be inaccurate. at fake_differential.v:33:10>>41:11
[warn] Module ODDRX1F referenced by instance ddr_n_instance cannot be found in current design. Clock & Reset management might be inaccurate. at fake_differential.v:42:10>>50:11
[log] # Elapsed time : 1.878423 ms
[log] ####### sv2chisel.transforms.FlowReferences #######
[info] Declaring actual port directions for module fake_differential at fake_differential.v:5:2->8
[info] Running FlowReference Transform another time on module fake_differential at fake_differential.v:3:0>>54:0
[log] # Elapsed time : 28.311422 ms
[log] ####### sv2chisel.transforms.InferUInts #######
[info] Converting in_clock to UInt based on its usage in the module at fake_differential.v:7:9->11
[info] Converting tmds[_] to UInt based on its usage in the module at fake_differential.v:11:10->12
[log] # Elapsed time : 30.181078 ms
[log] ####### sv2chisel.transforms.InferParamTypes #######
[log] # Elapsed time : 5.803376 ms
[log] ####### sv2chisel.transforms.TypeReferences #######
[critical] Unsupported Type 'Bool' for subindex expression 'out_n[i]' at fake_differential.v:47:15->22
[log] # Elapsed time : 18.082934 ms
[log] ####### sv2chisel.transforms.LegalizeExpressions #######
[warn] Unknown remote type for port #2 (Q) of instance ddr_p_instance of module ODDRX1F: casting by reference by default at fake_differential.v:38:12->23
[critical] Unsupported Type 'Bool' for subindex expression 'out_n[i]' at fake_differential.v:47:15->22
[warn] Unknown remote type for port #2 (Q) of instance ddr_n_instance of module ODDRX1F: casting by reference by default at fake_differential.v:47:12->23
[log] # Elapsed time : 29.292823 ms
[log] ####### sv2chisel.transforms.FixFunctionImplicitReturns #######
[log] # Elapsed time : 1.314473 ms
[log] ####### sv2chisel.transforms.NameInstancePorts #######
[log] # Elapsed time : 2.628666 ms
[log] ####### sv2chisel.transforms.RemovePatterns #######
[log] # Elapsed time : 4.862502 ms
[log] ####### sv2chisel.transforms.RemoveConcats #######
[log] # Elapsed time : 3.143862 ms
[log] ####### sv2chisel.transforms.AddDontCare #######
[log] # Elapsed time : 1.28653 ms
[log] ####### sv2chisel.transforms.LegalizeParamDefaults #######
[warn] Cannot find module ODDRX1F in current project at fake_differential.v:33:10>>41:11
[warn] Cannot find module ODDRX1F in current project at fake_differential.v:42:10>>50:11
[log] # Elapsed time : 4.072062 ms
[log] ####### sv2chisel.transforms.FixReservedNames #######
[log] # Elapsed time : 4.126536 ms
[log] ####### sv2chisel.transforms.ToCamelCase #######
[log] # Elapsed time : 0.830815 ms
[log] # Total Elapsed time running transforms : 216.675871 ms
[log] ######### EMISSION #########
[log] ######### CHISELIZING fake_differential.v #########
[info] At fake_differential.v:11: Emitting unpacked for node tmds
[info] At fake_differential.v:18: Emitting unpacked for node R_tmds_p
[info] At fake_differential.v:18: Emitting unpacked for node R_tmds_n
[log] # Elapsed time : 21.267262 ms
[log] ######### EMITTING to /fake_differential.scala #########
Exception in thread "main" java.io.FileNotFoundException: /fake_differential.scala (Permission denied)
at java.base/java.io.FileOutputStream.open0(Native Method)
at java.base/java.io.FileOutputStream.open(FileOutputStream.java:291)
at java.base/java.io.FileOutputStream.(FileOutputStream.java:234)
at java.base/java.io.FileOutputStream.(FileOutputStream.java:123)
at java.base/java.io.FileWriter.(FileWriter.java:66)
at sv2chisel.Emitter$.$anonfun$emitChisel$9(Emitter.scala:174)
at sv2chisel.Utils$.time(Utils.scala:185)
at sv2chisel.Emitter$.$anonfun$emitChisel$1(Emitter.scala:163)
at scala.collection.TraversableLike.$anonfun$map$1(TraversableLike.scala:286)
at scala.collection.mutable.ResizableArray.foreach(ResizableArray.scala:62)
at scala.collection.mutable.ResizableArray.foreach$(ResizableArray.scala:55)
at scala.collection.mutable.ArrayBuffer.foreach(ArrayBuffer.scala:49)
at scala.collection.TraversableLike.map(TraversableLike.scala:286)
at scala.collection.TraversableLike.map$(TraversableLike.scala:279)
at scala.collection.AbstractTraversable.map(Traversable.scala:108)
at sv2chisel.Emitter$.emitChisel(Emitter.scala:134)
at sv2chisel.Driver$.emitChisel(Driver.scala:66)
at sv2chisel.Main$.$anonfun$new$10(Main.scala:159)
at scala.collection.immutable.List.foreach(List.scala:431)
at sv2chisel.Main$.delayedEndpoint$sv2chisel$Main$1(Main.scala:157)
at sv2chisel.Main$delayedInit$body.apply(Main.scala:55)
at scala.Function0.apply$mcV$sp(Function0.scala:39)
at scala.Function0.apply$mcV$sp$(Function0.scala:39)
at scala.runtime.AbstractFunction0.apply$mcV$sp(AbstractFunction0.scala:17)
at scala.App.$anonfun$main$1$adapted(App.scala:80)
at scala.collection.immutable.List.foreach(List.scala:431)
at scala.App.main(App.scala:80)
at scala.App.main$(App.scala:78)
at sv2chisel.Main$.main(Main.scala:55)
at sv2chisel.Main.main(Main.scala)

Après de multiple messages plus ou moins critiques, la commande se termine sur une étonnante erreur java de fichier non trouvé. Visiblement il faut lui fournir le path complet en argument (sans doute un bug) :

 ./sv2chisel /opt/chiselmod/sv2chisel/utils/bin/fake_differential.v 
[log]  ---- Processing project  ---- 
[log] ############# Parsing /opt/chiselmod/sv2chisel/utils/bin/fake_differential.v #############
[log] ######### Elapsed time for /opt/chiselmod/sv2chisel/utils/bin/fake_differential.v #########
[log] # Lexing+Parsing Time : 337.962186 ms
[log] # Mapping to IR Time  : 123.022396 ms
[log] ######### Executing 18 transforms #########
[log]    ####### sv2chisel.transforms.CheckUseBeforeDecl #######
[log]    # Elapsed time : 24.704003 ms
[log]    ####### sv2chisel.transforms.CheckScopes #######
[log]    # Elapsed time : 6.588446 ms
[log]    ####### sv2chisel.transforms.CheckBlockingAssignments #######
[log]    # Elapsed time : 1.838544 ms
[log]    ####### sv2chisel.transforms.InferDefLogicClocks #######
[info] Registering a new clock `clk_shift` for module fake_differential (non blocking assignment) at /opt/chiselmod/sv2chisel/utils/bin/fake_differential.v:3:0>>54:0
[warn] Unable to find module module ODDRX1F instanciated as ddr_p_instance in current module fake_differential for clock inference processing. at /opt/chiselmod/sv2chisel/utils/bin/fake_differential.v:33:10>>41:11
[warn] Unable to find module module ODDRX1F instanciated as ddr_n_instance in current module fake_differential for clock inference processing. at /opt/chiselmod/sv2chisel/utils/bin/fake_differential.v:42:10>>50:11
[log]    # Elapsed time : 37.088031 ms
[log]    ####### sv2chisel.transforms.PropagateClocks #######
[warn] Module ODDRX1F referenced by instance ddr_p_instance cannot be found in current design. Clock & Reset management might be inaccurate. at /opt/chiselmod/sv2chisel/utils/bin/fake_differential.v:33:10>>41:11
[warn] Module ODDRX1F referenced by instance ddr_n_instance cannot be found in current design. Clock & Reset management might be inaccurate. at /opt/chiselmod/sv2chisel/utils/bin/fake_differential.v:42:10>>50:11
[log]    # Elapsed time : 1.73635 ms
[log]    ####### sv2chisel.transforms.FlowReferences #######
[info] Declaring actual port directions for module fake_differential at /opt/chiselmod/sv2chisel/utils/bin/fake_differential.v:5:2->8
[info] Running FlowReference Transform another time on module fake_differential at /opt/chiselmod/sv2chisel/utils/bin/fake_differential.v:3:0>>54:0
[log]    # Elapsed time : 25.221955 ms
[log]    ####### sv2chisel.transforms.InferUInts #######
[info] Converting in_clock to UInt based on its usage in the module at /opt/chiselmod/sv2chisel/utils/bin/fake_differential.v:7:9->11
[info] Converting tmds[_] to UInt based on its usage in the module at /opt/chiselmod/sv2chisel/utils/bin/fake_differential.v:11:10->12
[log]    # Elapsed time : 29.58874 ms
[log]    ####### sv2chisel.transforms.InferParamTypes #######
[log]    # Elapsed time : 5.646461 ms
[log]    ####### sv2chisel.transforms.TypeReferences #######
[critical] Unsupported Type 'Bool' for subindex expression 'out_n[i]' at /opt/chiselmod/sv2chisel/utils/bin/fake_differential.v:47:15->22
[log]    # Elapsed time : 18.257447 ms
[log]    ####### sv2chisel.transforms.LegalizeExpressions #######
[warn] Unknown remote type for port #2 (Q) of instance ddr_p_instance of module ODDRX1F: casting by reference by default at /opt/chiselmod/sv2chisel/utils/bin/fake_differential.v:38:12->23
[critical] Unsupported Type 'Bool' for subindex expression 'out_n[i]' at /opt/chiselmod/sv2chisel/utils/bin/fake_differential.v:47:15->22
[warn] Unknown remote type for port #2 (Q) of instance ddr_n_instance of module ODDRX1F: casting by reference by default at /opt/chiselmod/sv2chisel/utils/bin/fake_differential.v:47:12->23
[log]    # Elapsed time : 21.168114 ms
[log]    ####### sv2chisel.transforms.FixFunctionImplicitReturns #######
[log]    # Elapsed time : 0.631086 ms
[log]    ####### sv2chisel.transforms.NameInstancePorts #######
[log]    # Elapsed time : 1.467731 ms
[log]    ####### sv2chisel.transforms.RemovePatterns #######
[log]    # Elapsed time : 5.09245 ms
[log]    ####### sv2chisel.transforms.RemoveConcats #######
[log]    # Elapsed time : 2.749951 ms
[log]    ####### sv2chisel.transforms.AddDontCare #######
[log]    # Elapsed time : 1.251281 ms
[log]    ####### sv2chisel.transforms.LegalizeParamDefaults #######
[warn] Cannot find module ODDRX1F in current project at /opt/chiselmod/sv2chisel/utils/bin/fake_differential.v:33:10>>41:11
[warn] Cannot find module ODDRX1F in current project at /opt/chiselmod/sv2chisel/utils/bin/fake_differential.v:42:10>>50:11
[log]    # Elapsed time : 3.092851 ms
[log]    ####### sv2chisel.transforms.FixReservedNames #######
[log]    # Elapsed time : 4.132691 ms
[log]    ####### sv2chisel.transforms.ToCamelCase #######
[log]    # Elapsed time : 0.890969 ms
[log] # Total Elapsed time running transforms : 195.82181 ms
[log] ######### EMISSION #########
[log] ######### CHISELIZING /opt/chiselmod/sv2chisel/utils/bin/fake_differential.v #########
[info] At /opt/chiselmod/sv2chisel/utils/bin/fake_differential.v:11: Emitting unpacked for node tmds
[info] At /opt/chiselmod/sv2chisel/utils/bin/fake_differential.v:18: Emitting unpacked for node R_tmds_p
[info] At /opt/chiselmod/sv2chisel/utils/bin/fake_differential.v:18: Emitting unpacked for node R_tmds_n
[log] # Elapsed time : 25.374274 ms
[log] ######### EMITTING to //opt/chiselmod/sv2chisel/utils/bin/fake_differential.scala #########
[log] # Elapsed time : 17.429649 ms

Il y a sans doute beaucoup de chose a parametrer aux petits oignons pour bien utiliser l’outils, mais le résultat «en l’état» est déjà assez intéressant (commentaires FLF ajoutés):

package // FLF: à rajouter à la main ?
// FLF: on comprend pourquoi il voulait un path complet,
//      il le prend pour le nom du package
package .opt.chiselmod.sv2chisel.utils.bin

import chisel3._
// FLF: commentaires gardés, bien.
// DDR mode uses Lattice ECP5 vendor-specific module ODDRX1F

class fake_differential() extends Module { // used only in DDR mode
  // [1:0]:DDR [0]:SDR TMDS
  val in_clock = IO(Input(UInt(2.W)))
  val in_red = IO(Input(Bool()))
  val in_green = IO(Input(Bool()))
  val in_blue = IO(Input(Bool()))
  // [3]:clock [2]:red [1]:green [0]:blue 
  val out_p = IO(Output(Vec(4, Bool())))
  val out_n = IO(Output(Bool()))
// FLF: hmm, j'aurais pas traduit un tableau «wire» par une Mem() 
//      chisel, pas sûr que ça marche bien cette affaire.
  val tmds = Mem(4,UInt(2.W)) 
  tmds(3) := in_clock
  tmds(2) := in_red
  tmds(1) := in_green
  tmds(0) := in_blue

  // register stage to improve timing of the fake differential
  val R_tmds_p = Mem(4,Vec(2, Bool())) 
  val R_tmds_n = Mem(4,Vec(2, Bool())) 
  // genvar i;
  for(i <- 0 until 4){
    R_tmds_p(i) := tmds(i).asBools
    R_tmds_n(i) := ( ~tmds(i)).asBools
  }

  // output SDR/DDR to fake differential

  // FLF: les generate sont détecté et traduit également.
  // genvar i;
  for(i <- 0 until 4){
    // FLF: connexion des primitives sans broncher
    //      Il faudra tout de même inclure la définition
    //      de la blackbox à la main par la suite (import)
    val ddr_p_instance = Module(new ODDRX1F)
    ddr_p_instance.D0 := R_tmds_p(i)(0)
    ddr_p_instance.D1 := R_tmds_p(i)(1)
    out_p(i) := ddr_p_instance.Q.asTypeOf(out_p(i))
    ddr_p_instance.SCLK := clock
    ddr_p_instance.RST := 0.U
    val ddr_n_instance = Module(new ODDRX1F)
    ddr_n_instance.D0 := R_tmds_n(i)(0)
    ddr_n_instance.D1 := R_tmds_n(i)(1)
    out_n(i) := ddr_n_instance.Q.asTypeOf(out_n(i))
    ddr_n_instance.SCLK := clock
    ddr_n_instance.RST := 0.U
  }

}

Conclusion

Visiblement, le code généré doit être passé en revue par un ou une humaine histoire de corriger quelques imprécisions.

Mais cette relecture est facile, le code est très lisible et bien indenté. On retrouve les noms des signaux, variables, registres, modules Verilog. On est loin des bouillies de conversion où le code généré ressemble plus à un binaire compilé qu’à un code source «versionnable». Et cette saine relecture est de toute manière indispensable si l’on souhaite se reposer sur ce nouveau code dans la suite de son projet.

C’est un outil qui va vite devenir indispensable lorsque le besoin de convertion de code open-source se fera sentir. Et c’est une belle passerelle pour tous les habitués du Verilog qui souhaiteraient se lancer dans ce langage de haut niveau qu’est Chisel.

Des dire de l’équipe, l’outil a été testé avec succès sur le code du processeur RISC-V PicoRV32 développé par Claire Clifford (autrice de Yosys) que l’on retrouve un peu partout dans les projets open-source hardware.

C’est également une surprise de voir que ce projet est né au sein du laboratoire OVHCloud. Où l’on découvre que le fleurons du Claude français (cocorico) finance la recherche sur le matériel libre. Ceux qui ont besoin d’un article plus académique pour découvrir l’outil iront lire le papier de l’équipe ici.

Une LED qui clignote sur ICEStick vite vite vite !

Historiquement le ICE40 soudé sur la carte icestick est le premier supporté par des outils libres.

Le célèbre icestick qui a libéré les FPGA

Il est maintenant possible d’utiliser plusieurs programmes open-source pour développer dessus. Voici une méthode avec yosys, nextpnr, icestorm et openFPGALoader.

Dans un premier temps, allez donc cloner, compiler makeInstaller les 4 programmes cités ci-avant :

  • Yosys: Logiciel de synthèse Verilog couteau suisse du monde du FPGA.
  • nextpnr: Logiciel de placement routage supportant de plus en plus de famille de FPGA
  • icestorm: La tempête à l’origine de la libération des ICE40 de Lattice.
  • openFPGALoader: Le configurateur universel pour FPGA.

N’oubliez pas l’option de compilation «ICE40» quand elle est requise, mais c’est expliqué dans les différents tutos de compilation des outils.

Une fois que tout est installé on peut prendre le source Verilog «Blinking Led Project» et le modifier comme ci-dessous :

module blink (
    // Horloge
    input clock,
    output led
);

// Icestick clock : 12Mhz
parameter clock_freq = 12_000_000; // clock frequency
localparam MAX_COUNT = clock_freq;
localparam MAX_COUNT_UPPER = $clog2(MAX_COUNT) - 1;

reg [MAX_COUNT_UPPER:0] counter;
reg led_reg;

assign led = led_reg;

always@(posedge clock)
begin
    if(counter < MAX_COUNT/2)
        led_reg <= 1;
    else
        led_reg <= 0;

    if(counter >= MAX_COUNT)
        counter <= 0;
    else
        counter <= counter + 1;
end

endmodule

Il faut ensuite ajouter les informations de pinout pour l’horloge et la LED dans un fichier pcf que nous nommerons blink.pcf:

set_io clock  21
set_io led 98

Puis enfin, lancer les différentes commande de synthèse/pnr/bitstream :

$ PROJECTNAME=blink
$ VERILOGS="$PROJECTNAME.v"
  • Synthèse avec yosys:
$ yosys -q -p "synth_ice40 -top $PROJECTNAME -json $PROJECTNAME.json" $VERILOGS
  • Placement routage avec nextpnr:
$ nextpnr-ice40 --force --json $PROJECTNAME.json --pcf $PROJECTNAME.pcf --asc $PROJECTNAME.asc --freq 12 --hx1k --package tq144 $1
  • Vérification des timings avec icetime:
$ icetime -p $PROJECTNAME.pcf -P tq144 -r $PROJECTNAME.timings -d hx1k -t $PROJECTNAME.asc
// Reading input .pcf file..
// Reading input .asc file..
// Reading 1k chipdb file..
// Creating timing netlist..
// Timing estimate: 6.12 ns (163.28 MHz)
  • Packaging du bitstream avec icepack :
$ icepack $PROJECTNAME.asc $PROJECTNAME.bin
  • Configuration du fpga avec openFPGALoader:
$ openFPGALoader -b ice40_generic blink.bin 
write to ram
Jtag frequency : requested 6.00MHz   -> real 6.00MHz  
Parse file DONE
00
Detail: 
Jedec ID          : 20
memory type       : ba
memory capacity   : 16
EDID + CFD length : 10
EDID              : 0000
CFD               : 
Erasing: [==================================================] 100.00%
Done
Writing: [==================================================] 100.00%
Done
Wait for CDONE DONE

Et voila, la LED clignote.

Convertir du VHDL en Verilog librement avec Yosys et GHDL

Il y a quelques années, nous parlions de l’utilitaire vhdl2vl sur ce blog. Cette solution est intéressante mais limitée car le projet est relativement au point mort.

Depuis quelques mois une solution beaucoup plus «hype» est disponible, alliant le couteau suisse du Verilog Yosys, la référence en simulation libre en VHDL GHDL et le plugin ghdl-yosys-plugin. Cette solution permet dès à présent de convertir la plupart des codes VHDL en Verilog.

Voyons comment faire avec le module de réception uart proposé par nandland : UART_RX.vhd.

$ mkdir vhdlconv
$ cd vhdlconv
$ ls
UART_RX.vhd

Il faut tout d’abord compiler et installer Yosys et GHDL selon la procédure donnée sur les sites respectif.

Un fois fait il faut installer et compiler le plugin ghdl-yosys-plugin comme expliqué sur le dépot. Dans notre cas, cette compilation sera faite dans le répertoire /opt/ghdl-yosys-plugin.

Un fois l’installation effectuée nous pouvons nous lancer dans la conversion avec le plugin :

$ export GHDL_YOSYS_PLUGIN=/opt/ghdl-yosys-plugin/ghdl.so

On élabore le vhdl avec ghdl :

$ ghdl -a UART_RX.vhd 
$ ls
UART_RX.vhd  work-obj93.cf

On lance yosys avec le module ghdl :

$ yosys -m $GHDL_YOSYS_PLUGIN 
...
 |  yosys -- Yosys Open SYnthesis Suite                                       
 |  Copyright (C) 2012 - 2020  Claire Xenia Wolf <claire@yosyshq.com>         
...
 Yosys 0.9+4081 (git sha1 862e84eb, clang 10.0.0-4ubuntu1 -fPIC -Os)

On lit le module fraîchement élaboré:

...
yosys> ghdl UART_RX
1. Executing GHDL.
Importing module UART_RX.

Puis on lance la synthèse :

yosys> proc; opt; fsm; opt; memory; opt;

2. Executing PROC pass (convert processes to netlists).

2.1. Executing PROC_CLEAN pass (remove empty switches from decision trees).
Cleaned up 0 empty switches.

2.2. Executing PROC_RMDEAD pass (remove dead branches from decision trees).
Removed a total of 0 dead cases.

[...]

7.8. Executing OPT_EXPR pass (perform const folding).
Optimizing module UART_RX.

7.9. Finished OPT passes. (There is nothing left to do.)

Et enfin, on peut écrire le Verilog du module converti :

yosys> write_verilog UART_RX.v

8. Executing Verilog backend.
Dumping module `\UART_RX'.

yosys> exit

Le module verilog ainsi généré possède les même noms d’interfaces:

$ head -n 20 UART_RX.v
/* Generated by Yosys 0.9+4081 (git sha1 862e84eb, clang 10.0.0-4ubuntu1 -fPIC -Os) */

module UART_RX(i_Clk, i_RX_Serial, o_RX_DV, o_RX_Byte);
  (* unused_bits = "7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31" *)
  wire [31:0] _00_;
  wire [2:0] _01_;
  wire [6:0] _02_;
  wire _03_;
  wire _04_;
  wire _05_;
  (* unused_bits = "3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31" *)
  wire [31:0] _06_;
  wire [2:0] _07_;
  wire [2:0] _08_;
  wire [2:0] _09_;
  wire [6:0] _10_;
  wire [2:0] _11_;
  wire _12_;
  wire [2:0] _13_;
  wire _14_;

$ head -n 20 UART_RX.vhd
library ieee;
use ieee.std_logic_1164.ALL;
use ieee.numeric_std.all;
 
entity UART_RX is
  generic (
    g_CLKS_PER_BIT : integer := 115     -- Needs to be set correctly
    );
  port (
    i_Clk       : in  std_logic;
    i_RX_Serial : in  std_logic;
    o_RX_DV     : out std_logic;
    o_RX_Byte   : out std_logic_vector(7 downto 0)
    );
end UART_RX;
 
 
architecture rtl of UART_RX is
 
  type t_SM_Main is (s_Idle, s_RX_Start_Bit, s_RX_Data_Bits,

Et même si le code n’est pas très lisible on retrouve ses petits avec le nom des signaux interne du module.

Ce qui est vraiment intéressant ici c’est que le code verilog généré est parfaitement synthétisable avec n’importe quel logiciel de synthèse verilog, on peut également utiliser Verilator pour accélérer nos simulation et enfin il est possible de faire de la preuve formelle avec Yosys.

Plus d’excuse pour ne pas mixer du code VHDL avec du Verilog maintenant puisque tout est convertible en Verilog !

TapTempo en Verilog

Il y a plus de deux ans et demi maintenant, mzf publiait un journal sur le site LinuxFR parlant de son projet «TapTempo». L’objectif de son programme était simplement de mesurer la cadence d’une musique en tapant sur une touche de son clavier, le résultat s’affichant simplement dans la console.

Ce journal fut le point de départ d’une série de «projets TapTempo» proposé par les lecteurs du site dans à peu prêt tous les langages informatique possible… Mais pas le Verilog.

Voici donc la lacune comblée avec TapTempo en Verilog.

[Dépêche parue initialement sur LinuxFR]

Le projet TapTempo semble faiblir depuis quelques mois maintenant. En panne de langage informatique pour en faire une dépêche ?
Laissez‑moi vous présenter un langage assez particulier puisqu’il ne sert pas à faire de la programmation. Ce langage permet de décrire le comportement numérique d’un composant électronique (on parle alors de langage de description de matériel — HDL) : le Verilog.

C’est aussi un langage utilisé pour faire de la synthèse numérique sur les circuits logiques programmables (FPGA). Dans cet exemple, nous utiliserons la carte de développement à bas coût ColorLight 5A‑75B.

Vue d'ensemble du montage TapTempo

Sommaire

Le Verilog

Le Verilog est un langage conçu à l’origine pour rédiger des spécifications de circuits logiques en électronique numérique. Le langage permet de décrire le comportement de sortie par rapport à des entrées logiques.

Un peu comme les logiciels de saisie de schéma électronique, le Verilog est très hiérarchique, on décrit des modules avec leurs entrées-sorties. Que l’on assemble ensuite dans d’autres modules pour finir dans un module « top » qui décrit le composant final.

Dans le cas de TapTempo, le module « top » est déclaré comme ceci :

module taptempo #(
    parameter CLK_PER_NS = 40, // 25Mhz clock (ns)
    parameter TP_CYCLE = 5120, // timepulse cycle period (ns)
    parameter BPM_MAX = 250 // BPM max (bpm)
)(
    input clk_i,
    input btn_i,
    output pwm_o
);
//corps du module
endmodule

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. Les paramètres seront vus comme des constantes au moment de la simulation, ils permettent de configurer les composants en fonction de la cible.

Le changement de valeur des signaux se fait dans des processus qui sont déclenchés sur événement. Ces processus sont décrits au moyen du mot clef always@() en Verilog.
Par exemple, dans le code suivant:

/* Detect rising edge*/
reg btn_old, btn_rise;
always@(posedge clk_i)
begin
    btn_old <= btn_i;
    if(btn_old == 0 && btn_i == 1)
        btn_rise <= 1;
    else
        btn_rise <= 0;
end

L’événement déclencheur du process est le front montant de l’horloge clk_i. À chaque fois qu’un front montant d’horloge se présente, le processus est exécuté de manière séquentielle.

L’opérateur <= est l’opérateur d’affectation dit « non bloquant ». Cela signifie que la valeur ne sera effectivement appliquée qu’a la fin de l’exécution du process. Donc la valeur du signal btn_old ne sera pas nécessairement égale à btn_i à la ligne du if() comme on aurait pu instinctivement le croire.

Le langage Verilog a beaucoup de succès dans le monde du logiciel libre. En effet il est relativement peu verbeux et ressemble au C pour de nombreux aspects.

Il est par exemple possible de décrire des macros de la même manière qu’en C, il suffit de remplacer le symbole # par ` pour créer des constantes qui seront remplacées par le pré-processeur.

/* count tap period */
`define MIN_NS 60_000_000_000
`define BTN_PER_MAX (`MIN_NS/TP_CYCLE)
`define BTN_PER_SIZE ($clog2(1 + `BTN_PER_MAX))

Le Verilog reprend également les opérateurs booléen et binaire &,&&, |,||, etc. du C.

C’est le langage HDL le mieux supporté par les différents logiciels libres. Si l’on souhaite se lancer dans le domaine des FPGA et/ou des ASIC, il est préférable de commencer par lui. C’est également le langage « de sortie » de quasiment tous les générateurs de code HDL.

Architecture de TapTempo

L’outil indispensable pour commencer un projet en Verilog est… le papier et le crayon. Il est en effet indispensable d’avoir une vue d’ensemble assez claire de ce que l’on souhaite réaliser avant de se lancer dans le code.

Voici donc l’architecture générale du composant TapTempo :

Schema TapTempo au Crayon

Même si l’on doit revenir plusieurs fois (ce qui est le cas ici puisque les constantes ne sont pas à jour) sur ce schéma général en cours de développement, cette partie est très importante. Si elle est bien pensée, le reste coule de source.

Le composant va nécessiter quelques compteurs, mais l’horloge utilisée ici étant très rapide nous allons d’abord factoriser le comptage au moyen du module nommé timepulse, ce module va distribuer un pulse qui servira de base aux autres compteurs pour leur fonctionnement interne.

L’entrée utilisateur se compose d’un bouton (touche télégraphique « morse »). Les fronts montant et descendant de cette entrée n’étant pas synchronisés sur l’horloge du système nous allons devoir le faire au moyen de deux bascules en série pour éviter la métastabilité.

/* Synchronize btn_i to avoid metastability*/
reg btn_old, btn_s;
always@(posedge clk_i or posedge rst)
begin
    if(rst) begin
        btn_old <= 1'b0;
        btn_s <= 1'b0;
    end else begin
        btn_old <= btn_i;
        btn_s <= btn_old;
    end
end

Le second problème que pose notre entrée est que l’appui sur le bouton ne génère pas des changements francs de son état. Chaque « appui et relâche » génère une série de rebonds et donc une série de 0 et de 1 avant de se stabiliser. Pour lisser le signal il va donc falloir faire passer le signal dans le bloc « anti-rebond » debounce.

Le bloc percount va ensuite se charger de mesurer le temps entre deux appuis sur le bouton. Cette période va devoir être transformée en fréquence « BPM » (Beat Per Minute) via le module per2bpm puis en une valeur pseudo-analogique (PWM) grâce au module pwmgen.

La carte cible ne possédant pas de bouton « reset », il va falloir le générer grâce au module rstgen de manière à s’assurer de l’état de départ de notre système au démarrage.

Entrée sortie

La plupart des programmes TapTempo proposés jusqu’ici supposaient – en plus d’un CPU – la présence d’un clavier et d’une console texte de sortie (avec toute la pile de pilotes et de système d’exploitation associés). Ici, nous allons devoir tout définir dans le « portegramme » – Dans l’industrie on va parler d’IP pour Intellectual Property, quel horrible nom –.

L’idée est donc de simplifier au maximum l’entrée « clavier » et la sortie histoire de pouvoir les décrire simplement.

Pour l’entrée nous allons nous contenter d’un contact de type bouton, ou d’une touche de type télégraphe « morse ».

TapTempoEntreeMorse

Comme on peut le voir dans le schéma ci-dessus, quand la touche est appuyée, l’entrée « bouton » est mise à la masse et donne un niveau logique à 0 sur notre système. Lorsque l’on relâche le bouton, la résistance de tirage ramène le niveau de tension à Vcc pour avoir un niveau 1 sur l’entrée.

Pour la sortie, l’idée de mettre un écran complexifie énormément le système. En effet, il est nécessaire de faire une machine d’état assez complexe pour initialiser l’écran puis rafraîchir l’affichage. Il est souvent nécessaire d’ajouter un processeur « soft » rien que pour ça d’ailleurs. (Bon il est vrai que le VGA n’est pas si compliqué, mais il reste plus complexe que la solution proposée ici).

Non, l’idée ici est d’utiliser les graduations de l’antique voltmètre à aiguille trouvé dans une cave et qui gradue de 0 à 300 comme on peut le voir sur la photo :

vuemetretaptempo

Et comme un système numérique ne sort que des 0 et des 1 sur ses broches, on va « simuler » une valeur analogique au moyen d’une PWM (Pulse With Modulation). Il suffit de changer le rapport cyclique entre le temps haut et le temps bas de notre signal pour faire varier la tension moyenne qui sera vue par le voltmètre. Si on l’ajuste correctement avec une résistance en série, il est relativement facile de forcer la valeur maximale (5V) à 250.

pwm

La période de la pwm sera configurée suffisamment rapide pour que l’aiguille n’oscille pas.

Pulsation de temporisation (timepulse)

Le module ne prend pas de valeur d’entrée hormis l’horloge et le reset qui sont de rigueur dans tout le projet. Son signal de sortie tp_o est une pulsation de l’horloge émise toutes les 5120 ns :

module timepulse #(
    parameter CLK_PER_NS = 40,
    parameter PULSE_PER_NS = 5120
)(
    /* clock and reset */
    input clk_i,
    input rst_i,
    /* output */
    output tp_o);

Pour pouvoir compter des périodes de 5120ns on définit un registre de comptage :

`define MAX_COUNT (PULSE_PER_NS/CLK_PER_NS)
`define MAX_COUNT_SIZE ($clog2(`MAX_COUNT))

reg [`MAX_COUNT_SIZE-1:0] counter = 0;

Puis on compte de manière synchronisée avec l’horloge :

always@(posedge clk_i or posedge rst_i)
begin
    if(rst_i)
    begin
        counter <= 0;
    end else begin
        if (counter < `MAX_COUNT)
        begin
            counter <= counter + 1'b1;
        end else begin
            counter <= 0;
        end
    end
end

La pulsation est émise lorsque le compteur passe par 0 :

assign tp_o = (counter == 0);

Gestion des rebonds (debounce)

L’entrée de ce module est le signal de bouton préalablement synchronisé avec l’horloge du système btn_s. Le compteur utilisera la pulsation tp_i généré par le module timepulse décrit ci-avant.

La sortie du module est un signal btn_o proprement lissé. La période de temporisation de 20 ms est donné ici en paramètre DEBOUNCE_PER_NS.

module debounce #(
    parameter PULSE_PER_NS = 5120,
    parameter DEBOUNCE_PER_NS = 20_971_520
)(
    /* clock and reset */
    input clk_i,
    input rst_i,
    /* inputs */
    input tp_i,
    input btn_i,
    /* output */
    output btn_o
);

La gestion des rebonds est réalisée au moyen d’un compteur utilisé pour temporiser.

`define MAX_COUNT ((DEBOUNCE_PER_NS/PULSE_PER_NS)-1'b1)
`define MAX_COUNT_SIZE ($clog2(`MAX_COUNT))

/* Counter */
reg [`MAX_COUNT_SIZE-1:0] counter = 0;

Ainsi que d’une machine d’états à 4 états :

/* State machine */
localparam [1:0] s_wait_low  = 2'h0,
                 s_wait_high = 2'h1,
                 s_cnt_high  = 2'h2,
                 s_cnt_low   = 2'h3;

reg [1:0] state_reg, state_next;

Les transitions de la machine d’états sont données dans le code ci-dessous dans un processus dit « combinatoire » (always@*) par opposition à un processus « synchrone ».

always@*
begin
    case(state_reg)
        s_wait_low:
            if(btn_i)
                state_next = s_cnt_high;
            else
                state_next = s_wait_low;
        s_wait_high:
            if(!btn_i)
                state_next = s_cnt_low;
            else
                state_next = s_wait_high;
        s_cnt_high:
            /* verilator lint_off WIDTH */
            if(counter == `MAX_COUNT)
            /* verilator lint_on WIDTH */
                state_next = s_wait_high;
            else
                state_next = s_cnt_high;
        s_cnt_low:
            /* verilator lint_off WIDTH */
            if(counter == `MAX_COUNT)
            /* verilator lint_on WIDTH */
                state_next = s_wait_low;
            else
                state_next = s_cnt_low;
    endcase;
end

L’état de la machine est tout de même synchronisé dans un second processus :

always@(posedge clk_i or posedge rst_i)
    if(rst_i)
        state_reg <= s_wait_low;
    else
        state_reg <= state_next;

Le principe de « lissage » des rebonds est donc le suivant : Dans l’état initial s_wait_low on attend que le bouton passe à la valeur 1. Lorsque le signal passe à 1, on change d’état pour s_cnt_high.

Le passage dans l’état s_cnt_high a pour effet de faire passer le signal de sortie à 1 et déclencher le compteur. Tant que le compteur compte et n’a pas atteint la valeur MAX_COUNT, on reste dans cet état quelles que soient les variations du signal d’entrée.
Lorsque le compteur atteint la valeur maximale, la machine d’état passe dans l’état s_wait_high (en attente de valeurs hautes).

Dans l’état s_wait_high on surveille la valeur du bouton d’entrée, si elle passe à 0 on change d’état pour s_cnt_low.

De manière symétrique à s_cnt_high on déclenche donc le compteur en ignorant la valeur d’entrée. Et, lorsqu’elle atteint son maximum on passe à l’état initial s_wait_low.

La valeur « lissée » du bouton en sortie est donnée par l’état de la machine d’état :

assign btn_o = (state_reg == s_cnt_high) || (state_reg == s_wait_high);

Mesure de la période de tempo (percount)

L’interface du module percount se compose des entrées habituelles d’horloge clk_i, de reset rst_i ainsi que de la pulsation tp_i.

Le signal de mesure en entrée est btn_i et la sortie est un vecteur btn_per_o donnant la valeur mesurée. La valeur est considérée comme valide uniquement lorsque la sortie btn_per_valid est à 1. Cette astuce permet d’économiser un registre si la sauvegarde de la valeur mesurée est inutile comme c’est le cas ici.

`define MIN_NS 60_000_000_000
`define BTN_PER_MAX (`MIN_NS/TP_CYCLE)
`define BTN_PER_SIZE ($clog2(1 + `BTN_PER_MAX))

module percount #(
    parameter CLK_PER_NS = 40,
    parameter TP_CYCLE = 5120,
    parameter PULSE_PER_NS = 5120,
)(
    /* clock and reset */
    input clk_i,
    input rst_i,
    /* time pulse */
    input tp_i,
    /* input button */
    input btn_i,
    /* output period */
    output [(`BTN_PER_SIZE-1):0] btn_per_o,
    output btn_per_valid);

Maintenant que nous avons un signal de bouton btn_b propre et lissé, nous pouvons entamer la mesure de la période entre deux appuis au moyen de… devinez quoi ? D’un compteur pardi !

reg [($clog2(`BTN_PER_MAX+1)-1):0] counter = 0;
reg counter_valid = 0;

assign btn_per_valid = counter_valid;
assign btn_per_o = counter;

Il nous faut tout d’abord détecter le front descendant du bouton  :

reg btn_old;
wire btn_fall = btn_old & (!btn_i);

always@(posedge clk_i or posedge rst_i)
begin
    if(rst_i)
        btn_old <= 1'b0;
    else
        btn_old <= btn_i;     
end

Le signal btn_fall sert de remise à zéro du compteur ainsi que de validation de la valeur de sortie :

always@(posedge clk_i or posedge rst_i)
begin
    if(rst_i)
    begin
        counter <= 0;
    end else begin
        if(btn_fall) begin
            counter_valid <= 1'b1;
        end else if(counter_valid) begin
            counter <= 0;
            counter_valid <= 1'b0;
        end else begin
            /* stop counting if max, count tp_i */
            if(tp_i && counter < `BTN_PER_MAX)
                counter <= counter + 1'b1;
        end
    end
end

Le compteur compte le nombre de pulsations de tp_i jusqu’à atteindre la saturation BTN_PER_MAX. Si un front montant du bouton se présente avec btn_fall, on valide le compteur avec counter_valid. Et si le signal de validation passe à 1 (donc le coup d’horloge suivant) on remet le compteur à zéro et on recommence à compter.

Calcul de la fréquence en Beat Per Minute (per2bpm)

Avec le module per2bpm on arrive dans la partie critique du projet, car il va nous falloir faire une division. On entre une période dans le module :

    /* inputs */
    input [(`BTN_PER_SIZE-1):0] btn_per_i,
    input btn_per_valid,

Et on doit en ressortir une fréquence (BPM) :

    /* outputs */
    output [`BPM_SIZE - 1:0] bpm_o,
    output bpm_valid

Suivant la formule :

Il faut donc diviser la constante

par la variable btn\_per\_i

La division (tout comme la multiplication) est un point sensible en Verilog. En effet, l’opérateur de division existe bien dans le langage et il se peut que cela simule parfaitement.

C’est lorsque arrivera l’étape de la synthèse que l’on risque d’avoir quelques surprises. Il est possible que certains logiciels de synthèse réussiront à faire quelque chose en un coup d’horloge. Mais il est certain que cela se fera au prix de très mauvaises performances en matière de ressources utilisées et de fréquence d’horloge. Il est surtout probable que votre logiciel de synthèse jette l’éponge.

Pour réaliser cette division, nous allons donc en revenir aux fondamentaux appris au primaire et poser la division. Une division, c’est la recherche du Quotient et du Reste de l’équation suivante :

Dividend = Quotient \times Divisor + Remainder
reg [(`REGWIDTH-1):0] divisor;
reg [(`REGWIDTH-1):0] remainder;
reg [(`REGWIDTH-1):0] quotient;

La taille des registres sera celle de la période en entrée BTN_PER_SIZE additionné à la constante à diviser.

`define DIVIDENTWITH ($clog2(1 + `MIN_NS/(TP_CYCLE)))
`define REGWIDTH (`BTN_PER_SIZE + `DIVIDENTWITH)

La division s’effectue avec une série de soustraction du reste (remainder) et de décalage du diviseur.

À l’étape initiale, on place le diviseur à gauche du registre divisor et le dividende dans le reste remainder :

     divisor <= {btn_per_i, (`DIVIDENTWITH)'h0};
     remainder <= `MIN_NS/TP_CYCLE;
     // le résultat est initialisé à 0:
     quotient <= 0;

Puis on effectue une série de comparaison-soustraction-décalage avec l’algorithme comme décrit ci-dessous :

  • si le diviseur (divisor) inférieur ou égal au reste (remainder), on soustrait le reste avec le diviseur et on décale le quotient à gauche en ajoutant 1 :
            if(divisor <= remainder)
            begin
                remainder <= remainder - divisor;
                quotient <= {quotient[(`DIVIDENTWITH-2):0], 1'b1};
  • si le diviseur (divisor) est supérieur au reste, on décale le quotient à gauche en ajoutant 0. On ne touche pas au reste :
                quotient <= {quotient[(`DIVIDENTWITH-2):0], 1'b0};
  • dans tous les cas, on décale le diviseur à droite.
            divisor <= {1'b0, divisor[(`REGWIDTH-1):1]};

La division est orchestrée par une machine à trois états :

localparam [1:0] s_init    = 2'h0,
                 s_compute = 2'h1,
                 s_result  = 2'h2;

reg [1:0] state_reg, state_next;

Et le résultat est disponible en sortie quand state_reg est dans l’état s_result:

assign bpm_o = quotient[(`BPM_SIZE-1):0];
assign bpm_valid = (state_reg == s_result);

Génération de la tension de sortie (pwmgen)

La génération du signal pseudo analogique décrite en introduction est presque la partie la plus simple.

On compte (oui encore) de 0 à 250 (BPM_MAX) :

/* count */
always@(posedge clk_i or posedge rst_i)
begin
    if(rst_i)
        count <= BPM_MAX;
    else begin
        if(tp_i)
        begin
            if (count == 0)
                count <= BPM_MAX;
            else
                count <= count - 1'b1;
        end
    end
end

Et on passe le signal de sortie pwm_o à 1 lorsque le compteur est inférieur à la fréquence demandée :

assign pwm_o = (count <= pwmthreshold);

Il y a juste une subtilité consistant à sauvegarder la valeur de la fréquence donnée en entrée dans deux registres pwmthreshold et bpm_reg :

reg [($clog2(BPM_MAX+1)-1):0] bpm_reg;
reg [($clog2(BPM_MAX+1)-1):0] pwmthreshold;

/* Latching bpm_i on bpm_valid */
always@(posedge clk_i or posedge rst_i)
begin
    if(rst_i)
    begin
        bpm_reg <= 0;
        pwmthreshold <= 0;
    end else begin
        if(bpm_valid)
            bpm_reg <= bpm_i;
        if(count == BPM_MAX)
            pwmthreshold <= bpm_reg;
    end
end

Le premier registre bpm_reg est mis à jour lorsque le signal d’entrée bpm_valid est à 1. Pour mémoriser la valeur d’entrée et pouvoir l’utiliser au moment où l’on en a besoin.
Et le second pwmthreshold est rafraîchi en fin de cycle d’une période de la pwm. Pour éviter d’avoir un changement de valeur en cours de période, et donc un rapport cyclique faux.

Simulation de l’ensemble avec Cocotb

Jusqu’ici nous avons décrit le comportement du composant final en Verilog. Toutes les développeuses ou développeurs HDL le savent très bien, il est impossible de réaliser un projet Verilog (ou autre HDL) sans faire un minimum de simulation.

Pour simuler le composant, il est nécessaire de décrire les stimuli en entrée du composant et de lire/valider les sorties. On va généralement créer un composant hiérarchiquement au-dessus du top de notre composant appelé « testbench » dans lequel nous décrirons les changements de valeurs des entrées au cours du temps. Cette partie peut tout à fait se faire en Verilog.

Cependant, l’idée de mélanger la partie banc de test et composant « synthétisable » n’est pas terrible. En effet on va très vite confondre les deux parties et mélanger les codes. L’exemple de la division est criant : l’opérateur diviser « / » fonctionne très bien dans la partie testbench mais elle pose de gros problèmes dans la partie « synthétisable ».

Pour éviter ce mélange des genres, une solution radicale consiste à utiliser un autre langage pour la partie banc de test. Le C++ et le SystemC sont utilisés depuis longtemps pour cela. S’ils sont utilisés en conjonction avec Verilator ils permettent d’atteindre des puissance/rapidité de simulation inégalées par les simulateurs « propriétaires ».

Une autre méthode consiste à piloter le simulateur Verilog avec un autre programme, on parle alors de cosimulation. C’est le cœur du fonctionnement du module python CocoTB. L’idée ici est d’écrire son banc de test en python, ce qui est nettement plus confortable que du Verilog ou même du C++ (SystemC est une librairie C++ également).

Le testbench pour simuler l’ensemble du projet taptempo se trouve dans le répertoire cocotb/test_taptempo. Pour le simuler il suffit de s’y rendre et d’y exécuter un make.
À condition cependant d’avoir installé cocotb (en python3) et Icarus pour la partie simulateur (On laissera l’appréciation de l’installation au lecteur en fonction de ses affinités linuxdistributive).

La simulation consiste à tester trois appuis sur le bouton à des intervalles différents :

@cocotb.test()
async def debounce_upanddown(dut):
    td = TestTapTempo(dut)
    td.log.info("Running test!")
    await td.reset()
    td.log.info("System reseted!")
    await Timer(1000, units="us")
    td.log.info("up")
    await td.bounce_up(10, bounce_per=(10000, "ns"))
    await Timer(24, units="ms")
    td.log.info("down")
    await td.bounce_down(10, bounce_per=(10000, "ns"))
    await Timer(300, units="ms")
    td.log.info("up")
    await td.bounce_up(10, bounce_per=(10000, "ns"))
    await Timer(30, units="ms")
    td.log.info("down")
    await td.bounce_down(10, bounce_per=(10000, "ns"))
    await Timer(800, units="ms")
    td.log.info("up")
    await td.bounce_up(10, bounce_per=(10000, "ns"))
    await Timer(30, units="ms")

    td.log.info("Wait stable")
    await Timer(1000, units="us")

Cela génère un fichier de « traces » au format VCD particulièrement volumineux de 2,3 Go (qui se compresse à 70 Mo avec xz !) permettant de visionner les signaux au cours du temps grâce à gtkwave:

$ gtkwave -g taptempo.vcd

Et donne la trace suivante :
simulation_taptempo_full

Cette simulation est particulièrement longue (il m’a fallu environ une heure et demie sur mon vieux T430) et génère un fichier de trace monstrueux. En phase de développement on va généralement lancer de petites simulations par modules comme on peut le voir pour le module debounce dans le répertoire cocotb/test_debounce. On changera également certaines constantes de temps pour limiter les «  pas » de simulation consommant inutilement du calcul processeur.

Il est également possible de laisser l’ordinateur écrire les stimuli grâce à la méthode de preuve formelle. C’est la méthode qui a été utilisée ici pour les modules. Les fichiers de configuration se trouvent dans le répertoire formal/*.

Synthèse sur ColorLight

La Colorlight n’est pas initialement une carte de développement pour les FPGA. C’est une carte permettant de piloter des panneaux de LED qui nous agressent un peu partout dans les rues commerçantes. Cependant, un petit malin s’est rendu compte qu’elle était munie d’un FPGA de chez Lattice : l’ECP5.

Ce FPGA possède deux gros avantages :

  • il est relativement gros, suffisamment pour posséder des multiplieurs câblés, des sérialiseurs-désérialiseurs…
  • on peut développer dessus avec une chaîne de développement intégralement opensource !

Jusqu’à la colorlight, les kits de développement ECP5 n’étaient pas donnés puisque les premières cartes débutaient à 100 $ minimum. Mais avec la colorlight, on tombe à 15 $, ce qui en fait un kit de développement ultra bon marché pour se faire la main avec des FPGA.

Et comme tout est opensource, il est aisé d’aller installer les logiciels permettant de synthétiser TapTempo sur sa distribution Linux préférée.
L’explication de l’installation des outils est hors de propos de cet article (un article détaillé sur la colorlight est disponible dans le Hackable 35), mais une fois les outils installés, il suffit de se rendre dans le répertoire synthesis/colorlight du projet et de faire make :

$ make
[...]
Info: Device utilisation:
Info:          TRELLIS_SLICE:   328/12144     2%
Info:             TRELLIS_IO:     3/  197     1%
Info:                   DCCA:     1/   56     1%
Info:                 DP16KD:     0/   56     0%
Info:             MULT18X18D:     0/   28     0%
Info:                 ALU54B:     0/   14     0%
Info:                EHXPLLL:     0/    2     0%
Info:                EXTREFB:     0/    1     0%
Info:                   DCUA:     0/    1     0%
Info:              PCSCLKDIV:     0/    2     0%
Info:                IOLOGIC:     0/  128     0%
Info:               SIOLOGIC:     0/   69     0%
Info:                    GSR:     0/    1     0%
Info:                  JTAGG:     0/    1     0%
Info:                   OSCG:     0/    1     0%
Info:                  SEDGA:     0/    1     0%
Info:                    DTR:     0/    1     0%
Info:                USRMCLK:     0/    1     0%
Info:                CLKDIVF:     0/    4     0%
Info:              ECLKSYNCB:     0/   10     0%
Info:                DLLDELD:     0/    8     0%
Info:                 DDRDLL:     0/    4     0%
Info:                DQSBUFM:     0/    8     0%
Info:        TRELLIS_ECLKBUF:     0/    8     0%
Info:           ECLKBRIDGECS:     0/    2     0%
[...]
ecppack --svf taptempo.svf taptempo_out.config taptempo.bit

On voit ici que les ressources utilisées pour TapTempo sont ridicules par rapport au FPGA utilisé. La curieuse ou le curieux qui voudra « voir » le placement routage dans le FPGA utilisera l’option --gui dans la commande NextPnR pour avoir l’interface graphique :

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

Ce qui donne un autre aperçu du remplissage du FPGA.

taptempo routage

Pour télécharger le bitstream dans le FPGA, on pourra utiliser openFPGALoader en donnant simplement le nom du bitstream :

$ openFPGALoader taptempo.bit

Exercices de travaux pratiques

Pour celles et ceux qui ont suivi jusqu’ici et qui voudraient se faire la main avec ce projet, voici quelques propositions de « sujet de TP » :) :

  • utilisation d’un multiplieur câblé de l’ECP5 pour faire la division dans per2bpm ;
  • ajout un module de moyennage sur cinq échantillons pour coller à la spécification initiale de TapTempo ;
  • utilisation d’autres plates‑formes FPGA à bas coût : QuickFeather, FireAnt, Tang Nano

N’hésitez pas à me proposer des demandes d’intégration Git pour améliorer le projet.

Conclusion

On voit que dès que l’on passe dans le domaine de l’embarqué les choses se compliquent et prennent plus de temps. Alors que sur un PC on aurait pu faire ça en une ligne de code, quand on embarque ça dans un microcontrôleur, c’est déjà plus compliqué. Mais si l’on passe dans le monde des FPGA et des ASIC, le projet prend une toute autre dimension. C’est la raison pour laquelle il faut toujours se demander si un FPGA est bien à propos pour notre projet, non seulement cela coûtera plus cher en composant qu’une solution sur étagère, mais en plus le temps de développement (et donc le coût) sera nettement supérieur.

L’idée d’utiliser une touche de télégraphe pour mesurer le tempo n’était peut‑être pas la meilleure, compte tenu des rebonds qui sont relativement violents. Même avec le module lisseur de rebond (debounce), il subsiste quelques rebonds trop longs. Un tempo maximum à 250 n’est pas si rapide et l’on est vite frustré de l’atteindre alors qu’on pourrait mesurer des tempos de musiques plus… rythmées. On peut facilement passer à 300, mais ça reste lent. Si l’on veut un tempo plus rapide, il faut tout d’abord changer la graduation sur le voltmètre, puis modifier le paramètre BPM_MAX dans le code.

On a ici un modèle de projet qui est facile à synthétiser sur n’importe quel petit FPGA. C’est un projet qui peut être intéressant si l’on souhaite se sortir un peu les doigts des LED qui clignotent. La démonstration étant faite du fonctionnement de l’architecture globale, il est aisé de s’en servir pour la réécrire dans d’autres langages de description de matériel comme le VHDL, Chisel (même s’il y en a déjà une pour taptempo), Migen/Litex, MyHDL, Clash (en plus, ça permettrait de débloquer la dépêche LinuxFr.org sur le sujet)…

Pour le curieux, ou la curieuse, qui sera allé voir le code sur le projet GitHub, ce projet a été développé avec une dose de preuves formelles grâce au logiciel libre Yosys-SMTBMC.

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

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 ?