Day 28 (7th July 2019)

It’s time to review what was done this week and also what has been done so far. This week I can say I was formally introduced to formal verification - starting from ZipCPU’s intentionally broken txdata.v example and struggling and working my way through the example, I came to realize the significance of this practice as it eliminates bugs in the design process in the earliest stage possible. And after making the design pass formal verification I went on to simulate the design which told me about something I missed when I initially formally verified the design - that it was adding a leading ‘0’ to the output. Fixing this issue, and making the design re-pass formal was easy, but I wonder how I would have approached the issue had it not been for formal and simulation tools, GTKWave and would have headed straight on for the FPGA. I am also grateful to @zipcpu for offering me “Just-in-time” hints on the exercise that got me unstuck.

Interfacing USB-UART with the txdata.v module turned out to be a challenging exercise. This module used a valid, ready handshake whereas so far I had been introduced to stb & busy handshake through ZipCPU’s tutorials. It should have been easy theoretically - valid = stb and ready = !busy. But it turned out that ready does not go high unless valid is high, so the module didn’t accept inputs at all and I had to add some translation here. Yet that was not the fix as I had chosen to run the rest of the design at 16MHz and only the USB core at 48MHz which means clock domain crossing, and the fact that the pipeline could accept data every clock cycle meant that I was getting ‘000111222’ where I should have got ‘012’. The simple hack for this was to let the generated busy signal be high for a couple of more clock cycles, as bandwidth wasn’t the most important criteria here. Had it been, the solution would have been an async FIFO. It’s a hack for now that works, but later I would like to revisit async FIFOs, and find a way to introduce them in my exercises.

Looking back to Day 1, I’ve gotten more comfortable with Verilog, and also now with SymbiYosys for formally verifying designs. Verilator skills seem to be OK for now, but they would be well tested when I move on to the planned TFT Display example. I can deal with vcd traces and GTKWave well. With the limited time I have everyday (1-2 hours) I think this is good progress but I am also mindful that if I had more time, this would have been much faster.

Plan for the upcoming week

Next week I will be covering the 7th ZipCPU beginner’s tutorial - about 2FFs and button debouncing. After covering it I will be creating a rotary encoder example for the TinyFPGA BX board that prints the encoder value over USB-UART. This should follow as a natural extension to the current 6th tutorial that I just completed, I can reuse a lot of the modules here.

That’s it for today.