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

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

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

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

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

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

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

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

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

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

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

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

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

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

Aller plus loin

Kit de développement QORC

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

Réception

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

Le kit tient dans le creux de la main

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

Branchement

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

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

Clignotage de LED

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

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

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

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

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



Hello world!!

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

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

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

EOS S3, le bitstream libéré !

[Dépêche initialement paru sur LinuxFR]

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

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

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

EOS S3 Block Diagram

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

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

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

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

eFPGA

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

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

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

Kit de développement QuickFeather

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

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

[Édition le 17 juin 2020]

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

Le communiqué de Antmicro.

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

ULX3S ou OrangeCrab ?

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

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

OrangeCrab, de la DDR3 sur batterie.

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

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

Image provenant de groupgets

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

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

ULX3S la console de jeux à base de FPGA

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

Image provenant de la page crowdsupply

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

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

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

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

Célèbre mème Futurama

OrangeCrab

Ça y est, la carte à base d’ECP5 tant attendu est enfin disponible sur le site groupsget.

La carte qui est utilisable avec une chaîne de développement intégralement libre est constituée de:

  • 24kLut
  • 1008 Kb – Embedded Block RAM
  • 194 Kb – Distributed RAM
  • 28 – 18×18 Multipliers
  • PLLs: 2
  • Internal oscillator
  • 1Gbits DDR
  • Full-speed (12Mbit) USB with a direct connection to the FPGA
  • 128Mbit QSPI FLASH Memory
  • MicroSD socket
  • SAR ADC, external RC / input comparator of FPGA
  • Battery voltage sensing

Le tout pour des dimensions rikiki de 22.86mm x 50.8mm (0.9″ x 2.0″)

Ça fait quelques mois déjà que tout le monde l’attendait. Elle est disponible pour $99 à l’achat dès aujourd’hui.

Test your Chisel design in python with CocoTB

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

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

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

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

Then, let’s write Chisel testbench with CocoTB !

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

The directory structure is following :

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

To launch tests we needs following dependencies :

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

Once all dependencies installed we can clone the chisNesPad project :

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

Then launch simulation :


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

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

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

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

And we can see wave form with gtkwave:

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

Let’s see what happen

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

Chisel Module

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

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

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

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

This object will be called by SBT following command:

$ sbt "runMain chisnespad.ChisNesPad"

Generated Verilog

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

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

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

CocoTB testbench

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

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

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

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

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

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

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

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

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

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

Get Waveform

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

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

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

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

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

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

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

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

$ gtkwave ChisNesPad.vcd
Simulation traces

Conclusion

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

15$ ECP5 board kit

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

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

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

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

The Board as received

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

Removing the sticker unveil an ECP5 25k !

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

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

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

[Edit 1 March]

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

Jtag Uart pinout from Anton Blanchard (twitter)

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

Connect and configure with openFPGALoader

ECP5 is available in openFPGALoader list as we can see :

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

Open source synthesize and place&route tools

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

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

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

Then for next-pnr:

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

And finally Yosys

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

Synthesize blinker

The blinker projet can be found on this github repository :

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

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

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

And see the orange LED blinking !

Some links

[this article will be edited as I progress]

Prove Chisel design with Yosys-smtbmc

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

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

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

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

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

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

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

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

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

ChisNesPad project

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

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

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

SuperNes gamePAD pinout

For FPGA point of view 3 signals interest us :

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

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

Basic Chisel/Formal directory structure

The directory structure of the project is following :

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

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

sbt 'runMain chisnespad.ChisNesPad'

The generated file will be named ChisNesPad.v

smtbmcify tool

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

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

A command named smtbmcify will then be available on system :

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

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

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

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

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

//BeginModule:ChisNesPad

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

//EndModule:ChisNesPad

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

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

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

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

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

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

//EndModule:ChisNesPad
endmodule

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

Some naming convention should be know to write systemverilog rules:

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

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

[options]
mode bmc 
depth 30

[engines]
smtbmc

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

[files]
ChisNesPadFormal.sv

The launch command is :

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

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

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

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

Find bugs

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

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

This rule generate a FAIL :

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

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

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

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

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

initial
    assume(reset==1'b1);

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

With that rules, it pass :

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

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

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