Archives par mot-clé : yosys

ULX3S ou OrangeCrab ?

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

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

OrangeCrab, de la DDR3 sur batterie.

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

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

Image provenant de groupgets

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

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

ULX3S la console de jeux à base de FPGA

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

Image provenant de la page crowdsupply

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

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

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

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

Célèbre mème Futurama

Prove Chisel design with Yosys-smtbmc

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

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

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

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

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

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

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

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

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

ChisNesPad project

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

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

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

SuperNes gamePAD pinout

For FPGA point of view 3 signals interest us :

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

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

Basic Chisel/Formal directory structure

The directory structure of the project is following :

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

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

sbt 'runMain chisnespad.ChisNesPad'

The generated file will be named ChisNesPad.v

smtbmcify tool

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

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

A command named smtbmcify will then be available on system :

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

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

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

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

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

//BeginModule:ChisNesPad

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

//EndModule:ChisNesPad

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

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

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

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

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

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

//EndModule:ChisNesPad
endmodule

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

Some naming convention should be know to write systemverilog rules:

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

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

[options]
mode bmc 
depth 30

[engines]
smtbmc

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

[files]
ChisNesPadFormal.sv

The launch command is :

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

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

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

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

Find bugs

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

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

This rule generate a FAIL :

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

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

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

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

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

initial
    assume(reset==1'b1);

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

With that rules, it pass :

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Projet IceStorm : le FPGA libéré !

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

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

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

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

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

Icestorm howto

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

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

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

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

$ icepack rot.txt rot.bin

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

$ sudo iceprog rot.bin

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

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

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