Archives de catégorie : Non classé

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
$ cd 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/ .

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 ?

Cocotb modules libraries

Cocotb take care of the core of cosimulation library. But for our design test some bus-test library are required. They are managed separately.

Here is a list of cocotb modules libraries

cocotb_usb

For testing USB 1.1 version.

cocotbext-wishbone

Read/write simulation master on wishbone bus

cocotbext-uart

For uart testing

cocotbext-spi

For SPI

cocotbext-fifointerface

To test some fifo interfaces

Further ressources on official wiki.

Cocotb Tips

Some tips for python HDL test module Cocotb.

Read and Write signal

Write:

clk.value = 1
dut.input_signal <= 12
dut.sub_block.memory.array[4] <= 2

Read:

count = dut.counter.value
print(count.binstr)
print(count.integer)
print(count.n_bits)
print(int(dut.counter))

See it under the official documentation.

Yielding a coroutine in a select list fashion

Question asked on stackoverflow.

Using latest python version with virtualenv

If you compile python yourself, don’t forget to add option --enable-shared at configure time (./configure --enable-shared)

$ virtualenv --python=/usr/local/bin/python3.7 ~/envp37
$ source ~/envp37/bin/activate
$ python -m pip install cocotb

Do not forget to re-source your environnement each time you open a new terminal :

$ source ~/envp37/bin/activate

Logging messages and main test class template

This is a template for declaring a class used for test in function @cocotb.test() :

import logging
from cocotb import SimLog
...

class MyDUTNameTest(object):
    """ Test class for MyDUTName"""
    LOGLEVEL = logging.INFO
    # clock frequency is 50Mhz
    PERIOD = (20, "ns")

    def __init__(self):
        if sys.version_info[0] < 3: # because python 2.7 is obsolete
            raise Exception("Must be using Python 3")
        self._dut = dut
        self.log = SimLog("RmiiDebug.{}".format(self.__class__.__name__))
        self.log.setLevel(self.LOGLEVEL)
        self._dut._log.setLevel(self.LOGLEVEL)
        self.clock = Clock(self._dut.clock, self.PERIOD[0], self.PERIOD[1])
        self._clock_thread = cocotb.fork(self.clock.start())

# ....

@cocotb.test()
def my_test(dut):
    mdutn = MyDUTNameTest()
    mdutn.log.info("Launching my test")

Réception du FireAnt

J’en avait déjà parlé dans les colonnes de ce blog. Une nouvelle société produit un FPGA nommé Trion T8. Ce FPGA est la base d’une petite carte de développement proposée par les HongKongais de XIPS Technology sur le site crowdsupply.

Évidemment je n’ai pas résisté à participer à la campagne. Quelques manifestations à HongKong et quelques déboire avec Fedex puis Mondial Relais, voici enfin le kit tant attendu arrivé chez moi.

Le carton était un peu disproportionné non ?

Le kit est arrivé dans un énorme carton, mais c’est presque habituel dans ce genre de cas. J’avais pris sans les headers soudés mais ils sont tout de même fournis. J’ai juste eu à les souder moi même.

Au branchement une led rouge qui semble être celle de l’alimentation s’allume. Les 4 LED oranges se mettent elles à compter en binaire.

Le FireAnt sous tension de l’interface USB

Dans les messages noyau nous avons la traditionnelle interface ttyUSB0 du FTDI :

$ dmesg
[97997.987953] usb 3-1: USB disconnect, device number 11
[97997.988359] ftdi_sio ttyUSB0: FTDI USB Serial Device converter now disconnected from ttyUSB0
[97997.988397] ftdi_sio 3-1:1.0: device disconnected
[98000.296737] usb 3-1: new high-speed USB device number 12 using xhci_hcd
[98000.445226] usb 3-1: New USB device found, idVendor=0403, idProduct=6014, bcdDevice= 9.00
[98000.445231] usb 3-1: New USB device strings: Mfr=1, Product=2, SerialNumber=0
[98000.445233] usb 3-1: Product: Single RS232-HS
[98000.445235] usb 3-1: Manufacturer: FTDI
[98000.446052] ftdi_sio 3-1:1.0: FTDI USB Serial Device converter detected
[98000.446118] usb 3-1: Detected FT232H
[98000.446278] usb 3-1: FTDI USB Serial Device converter now attached to ttyUSB0
Efinity software

J’avais déjà reçu la license de la part de Efinix et Xips technology, du coup mon blinking led design était près à télécharger. Le bitstream est au format *.hex et se flash super facilement avec le Efinity programmer (tools -> programmer).

Le flashage passe comme une lettre à la poste (… heu mieux que la poste en fait 😉

Par contre ma led ne clignote pas, je pense avoir encore quelques soucis avec les configs d’I/O et de PLL pour l’instant. Je doit encore me former à l’Efinity Interface Designer de Efinix qui est assez déroutant par rapport aux autres IDE.

[ToBeEdited]

Réception du kit AnalogMax-01

Arrow propose un kit de développement nommé AnalogMax pour 80$ environ. L’entreprise qui fabrique la carte est Trenz Electronic qui réalise également le kit gowin.

Cette fois la carte est arrivée par lettre, et non par gros colis.

Le FPGA est relativement gros et la carte possède un certain nombre de périphérique analogiques sympathique comme un détecteur de fumée, un capteur de température, quelque canaux ADC et DAC ainsi que des GPIO.

Au branchement du kit sur l’usb on a juste la led verte allumée. L’appuie sur le bouton à droite allume une des huit leds de la rangée, et l’appui sur l’autre bouton allume l’autre led rouge et inscrit un message sur l’uart (115200):

UHSA R1.0

[TO BE EDITED]

Retour de Conférence ORConf 2019

Je remercie mon entreprise Armadeus Systems de m’avoir permit d’assister à cette septième conférence OpenRisc 2019.

Libérez vos flip-flop !

L’ORConf est organisée par la fondation FOSSi qui promeut la liberté dans le matériel, que l’on parle d’outils ou de composants matériel. L’objet de la première conférence fut justement sur l’histoire de cette organisation.

FOSSi foundation est une évolution de l’association opencore, les fondateurs de FOSSi n’étaient pas satisfait de cette structure et de l’organisation de la gestion des projets. La fondation FOSSi a pour but de promouvoir le logiciel libre et le matériel libre et de servir de support aux différents projets libres. Elle apporte un soutien logistique pour l’hébergement elle sert d’interface avec le projet google summer of code. Sa mission est également d’organiser des événements comme l’ORConf pour faciliter les rencontres entre les différents acteurs du matériel libre.

C’est la première fois que la conférence se déroulait en France, à Bordeaux dans les locaux de l’école d’ingénieur ENSEIRB-MATMECA. Une école que je connais bien puisque c’est l’école dans laquelle j’ai passé mon diplôme d’ingénieur 😉

Une fois l’introduction de la fondation passée, la journée du vendredi s’est enchaînée avec une présentation de la Chips Alliance pas Zvonimir Z bandic employé de Western Digital puis avec une discussion autour des licences open sources du CERN à destination spécifiquement du matériel.

Nous avons eu la chance d’avoir une présentation de la fondation RISC-V par Calista Redmond – récemment nommée CEO de l’organisation – pour nous parler de la révolution en cours.

Mais les conférences ne sont pas réservées au jeux d’instruction RISC-V, nous avons pu avoir un aperçu d’un processeur autour du jeux d’instructions OpenPower (de plus en plus libre) ainsi que du processeur OpenRisc (le samedi) développé sur le temps libre de Stafford Horne principalement (temps pas si libre que ça puisqu’il a des enfants;).

Après quelques discussions à propos des outils disponibles autour du VHDL pour la vérification de la syntaxe et des règles de codage la journée du vendredi s’est terminée par une présentation de l’avancée des outils libres pour le développement sur ASIC par Luis Eduardo Rueda Gruerrero de Symbiotic EDA. Luis participe au développement d’un processeurs RISC-V 32bits nommé ASICone en ayant – comme son nom l’indique– la fabrication d’un silicium avec le plus possible de logiciels libres comme objectif. Le développement intégralement open source est encore compliqué, notamment en ce qui concerne l’analyse de la consommation, l’arbre d’horloge ainsi que la description des librairies de composants.

Cette demi-journée fut bien chargée en informations annonçant bien la suite le samedi.

Beaucoup de choses à digérer de la journée de samedi. À titre personnel je retiens surtout les avancées de Cocotb version 1.2 dont le mainteneur est un membre de la fondation FOSSI. En plus du support complet de Python3 et les directives «async», cocotb 1.2 permet désormais d’être utilisé sans Makefile car intégré complètement dans le système de packaging Python.

Mais le futur de Cocotb semble très intéressant avec le support de verilator comme simulateur. Le travail pour le support de verilator était surtout à faire coté verilator et non Cocotb, mais un patch semble être sur les rails chez Wilson.

Malgré son nom très «vacances à la plage», cocotb est le nouveau système permettant d’écrire des testbenchs qui est de plus en plus utilisé en entreprise aujourd’hui. Il remplace allègrement les UVM, VUNIT qui font si mal à la tête.

Jeremy Bennett nous a présenté un nouveau banc de test nommée emBench en cours de définition pour que les différentes architectures de processeurs puissent comparer leurs zizi. L’objectif étant d’avoir un testbench libre et gratuit pour pouvoir l’exécuter sur toutes les plate-formes et faire de beaux tableaux comparatif.

L’après midi fut marqué par une série de «ligthning talks» de 3 minutes chacune. Avec les avancées du développement de SymbiFlow (impressionnantes) notamment pour le support de l’artix7 ainsi que par une présentation de Clash qui vient de passer à sa version 1.0. Sans oublier la présentation des cœurs RISC-V pour ASIC développés par la société russe syntacore et les avancées du langage Chisel3.

À noter aussi la remarquable performance de Pepin de Vos avec sa présentation intégralement réalisés sur un softCore tournant sur FPGA (GOWIN). Il est désormais possible grâce au travail de Tristan Gringold de synthétiser du VHDL avec Yosys. C’est ce qu’a utilisé Pepin pour réaliser son système à base de logique 7400. Cependant le nombre de composant étant trop important il s’est contenté d’une synthèse sur FPGA pour cette présentation.

Pour que toute la chaîne de développement sur FPGA soit libérée, un bon logiciel de placement routage est nécessaire. C’est le rôle du nouveau logiciel Nextpnr que David Shah nous a présenté. Le développement de nextpnr avance bien. N’hésitez pas à le soutenir sur patreon.

Enfin, la journée s’est terminé sur les berges de la Garonne par un dîner concert dans la guinguette «chez alriq». Cela qui m’a permis de passer de l’autre coté du fleuve, ce qui ne m’était jamais arrivé durant mes trois ans de scolarité à Bordeaux !

Pour le restaurant, c’est Google qui régale

Le dimanche ne fut pas sans repos non plus et fut marqué par une conférence très dynamique de Jose E. Marchesi et son nouveau logiciel d’édition de binaire (ELF, mp3, …) poke. Une présentation très vivante et passionnante, tout le monde achète 😉

Les interfaces (connecteurs) présenté par Alan J.Wood sont aussi très intéressantes. L’objectif des connecteurs mixMOD et Blackedge présentés est de pouvoir s’adapter aux PMOD très présent dans les kits de développement FPGA tout en ajoutant des pins analogique. L’idée est d’avoir un standard pour bricoler dans son garage et pour équiper les salles de TP pour l’éducation.

N’oublions pas la présentation de l’impressionnant travail abattu par l’université de Zurich avec leur projet PULP. Le travail de l’équipe PULP est de concevoir et produire des ASIC pour l’embarqué à base d’architectures parallèle. L’objectif est de publier en open source le plus possible les outils utilisés. Leur processeur nommé Arnold est particulièrement remarquable car il intègre une matrice FPGA nommée eFPGA fournie par QuickLogic. Pour l’instant les outils de synthèse et de placement routage sont en source fermés, mais il est prévu de fournir des outils libre pour cette matrice.

Todd Strader nous a parlé de son projet de protection d’IP Verilog à base de verilator permettant d’éviter l’horrible système de chiffrement des IP proposé habituellement par les constructeurs et empêchant l’utilisation de simulateur libre. Tout en ayant une sécurité très relative quand au piratage de la dite IP chiffrée.

Dan Gisselquist nous a démontré que la plupart des IP proposées par les fondeurs à base de bus AXI ne respectent pas le standard et sont souvent buggé ! Ces bug ressortent très facilement grâce à la vérification formelle.

Et enfin, n’oublions pas la présentation de la nouvelle entreprise local Hiventive et son système de coordination de simulateurs en ligne.

Pour conclure, cette conférence fut très intense en présentations. Beaucoup d’acteurs du matériel libre étaient présent. Un des grand intérêt de cette conférence était aussi de pouvoir rencontrer en personne des acteurs que l’on ne côtoyait avant qu’a travers des messagerie.

Une question reste sur toutes les langues : Où se passera l’ORConf 2020 ?

[Edit: 12 novembre 2019]

Les vidéos des conférences sont désormais disponible sur youtube.