{"id":1203,"date":"2020-02-03T22:08:20","date_gmt":"2020-02-03T21:08:20","guid":{"rendered":"http:\/\/www.fabienm.eu\/flf\/?p=1203"},"modified":"2020-02-26T15:51:27","modified_gmt":"2020-02-26T14:51:27","slug":"prove-chisel-design-with-yosys-smtbmc","status":"publish","type":"post","link":"http:\/\/www.fabienm.eu\/flf\/prove-chisel-design-with-yosys-smtbmc\/","title":{"rendered":"Prove Chisel design with Yosys-smtbmc"},"content":{"rendered":"\n

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 <\/a>opened the method with it’s synthesis software Yosys<\/a>. Explanation about formal prove with Yosys-smtbmc and can be found in this presentation<\/a>. Dan Guisselquist (ZipCPU) give lot of great tutorials on formal prove with Verilog and SystemVerilog design on it’s blog<\/a>. It’s a good start to learn formal prove.<\/p>\n\n\n\n

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.<\/p>\n\n\n\n

How can we prove our VHDL, Clash<\/a> or Chisel<\/a> gateware ?<\/p>\n\n\n\n

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<\/a> for verifying it’s VHDL gateware. Its VHDL code is converted into Verilog with the new GHDL feature <\/a>not-yet-finished and a systemVerilog top component instantiate the VHDL gateware converted in verilog by GHDL synthesis<\/a> feature.<\/p>\n\n\n\n

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:<\/p>\n\n\n\n

`ifdef FORMAL\n\/\/ Declare some signal output ports\n`endif<\/code><\/pre>\n\n\n\n
It’s became little bit difficult to do that with chisel and its blackbox<\/a> 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. <\/p>\n\n\n\n
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 !<\/p>\n\n\n\n
To (temporarily) fix this problem a little python tools has been written by Martoni<\/a>  for injecting rules automatically under generated Verilog module. We will see how it’s work in this article with a simple project named ChisNesPad<\/a>. <\/p>\n\n\n\n
ChisNesPad project<\/h2>\n\n\n\n
ChisNesPad is a little project that aim to drive Super Nintendo Pad with an FPGA.<\/p>\n\n\n\n
\"\"
In electronic point of view, super nes controller is simply a 16 bits shift register.<\/figcaption><\/figure>\n\n\n\n
The gamepad pinout is relativelly easy to find on the web.<\/p>\n\n\n\n
\"\"
SuperNes gamePAD pinout<\/figcaption><\/figure><\/div>\n\n\n\n
 For FPGA point of view 3 signals interest us :<\/p>\n\n\n\n