Reading from memory This post follows tutorial on https://vivonomicon.com/2020/04/14/learning-fpga-design-with-nmigen/
On the iCESugar-pro, there is a Winbond w25q256jv which is a 3V 256M-bit serial flash memory with dual/quad spi. Here is a document https://github.com/wuxx/icesugar-pro/blob/master/doc/w25q256jv.pdf of the SPI module. Using this module, we can program the FPGA by writing the bitstream into flash memory.
iCESugar-pro Offical github site: https://github.com/wuxx/icesugar-pro
Install Project Trellis The FPGA use EPC5 chips from lattice. We can use Trellis+ yosys+ nextpnr to develope our design. https://github.com/SymbiFlow/prjtrellis
This section will takes more than an hour to make it all done.
Install the dependencies for Project Trellis Install Boost 1 2 3 sudo apt-get install libboost-all-dev sudo apt install build-essential libboost-system-dev libboost-thread-dev libboost-program-options-dev libboost-test-dev sudo apt install libboost-filesystem1.
Perform formal verification What is a “formal verification” ?
Formal verification is a process of checking whether a design satisfies some requirements.
Example Here is an adder. It is different from previous one on day 8. In order to make sure the adder in the design satisfies “addition”.
Prerequisites If you would like to perform simulation with GTKwave, a opensource free waveform viewer. Download the software here
and put it under C:/gtkwave. Go to the windows path setting and add it under the $path variable.
The main function We create a simple 8-bit adder