search

ZipCPU / wb2axip

Bus bridges and other odds and ends
483 stars 100 forks source link

xlnxdemo formal verification fails #15

Closed bluewww closed 5 years ago

bluewww commented 5 years ago

When I run sby -f xlnxdemo.sby with the FOSS yosys version (just built the master branch at 19d6b8846f55b4c7be705619f753bec86deadac8)

I get this:

SBY 14:52:58 [xlnxdemo_cvr] Removing direcory 'xlnxdemo_cvr'.
SBY 14:52:58 [xlnxdemo_cvr] Copy 'faxil_slave.v' to 'xlnxdemo_cvr/src/faxil_slave.v'.
SBY 14:52:58 [xlnxdemo_cvr] Copy 'xlnxdemo.v' to 'xlnxdemo_cvr/src/xlnxdemo.v'.
SBY 14:52:58 [xlnxdemo_cvr] engine_0: smtbmc
SBY 14:52:58 [xlnxdemo_cvr] base: starting process "cd xlnxdemo_cvr/src; yosys -ql ../model/design.log ../model/design.ys"
SBY 14:52:59 [xlnxdemo_cvr] base: finished (returncode=0)
SBY 14:52:59 [xlnxdemo_cvr] smt2: starting process "cd xlnxdemo_cvr/model; yosys -ql design_smt2.log design_smt2.ys"
SBY 14:52:59 [xlnxdemo_cvr] smt2: finished (returncode=0)
SBY 14:52:59 [xlnxdemo_cvr] engine_0: starting process "cd xlnxdemo_cvr; yosys-smtbmc --presat --unroll -c --noprogress -t 60 --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 14:52:59 [xlnxdemo_cvr] engine_0: ##   0:00:00  Solver: yices
SBY 14:52:59 [xlnxdemo_cvr] engine_0: ##   0:00:00  Checking cover reachability in step 0..
SBY 14:52:59 [xlnxdemo_cvr] engine_0: ##   0:00:00  Checking cover reachability in step 1..
SBY 14:53:00 [xlnxdemo_cvr] engine_0: ##   0:00:00  Reached cover statement at xlnxdemo.v:798 in step 1.
SBY 14:53:00 [xlnxdemo_cvr] engine_0: ##   0:00:00  Writing trace to VCD file: engine_0/trace0.vcd
SBY 14:53:00 [xlnxdemo_cvr] engine_0: ##   0:00:00  Writing trace to Verilog testbench: engine_0/trace0_tb.v
SBY 14:53:00 [xlnxdemo_cvr] engine_0: ##   0:00:00  Writing trace to constraints file: engine_0/trace0.smtc
SBY 14:53:00 [xlnxdemo_cvr] engine_0: ##   0:00:00  Checking cover reachability in step 1..
SBY 14:53:00 [xlnxdemo_cvr] engine_0: ##   0:00:00  Reached cover statement at xlnxdemo.v:788 in step 1.
SBY 14:53:00 [xlnxdemo_cvr] engine_0: ##   0:00:00  Writing trace to VCD file: engine_0/trace1.vcd
SBY 14:53:00 [xlnxdemo_cvr] engine_0: ##   0:00:00  Writing trace to Verilog testbench: engine_0/trace1_tb.v
SBY 14:53:00 [xlnxdemo_cvr] engine_0: ##   0:00:00  Writing trace to constraints file: engine_0/trace1.smtc
SBY 14:53:00 [xlnxdemo_cvr] engine_0: ##   0:00:00  Checking cover reachability in step 1..
SBY 14:53:00 [xlnxdemo_cvr] engine_0: ##   0:00:00  Checking cover reachability in step 2..
SBY 14:53:00 [xlnxdemo_cvr] engine_0: ##   0:00:00  Reached cover statement at xlnxdemo.v:1019 in step 2.
SBY 14:53:00 [xlnxdemo_cvr] engine_0: ##   0:00:00  Writing trace to VCD file: engine_0/trace2.vcd
SBY 14:53:00 [xlnxdemo_cvr] engine_0: ##   0:00:00  Writing trace to Verilog testbench: engine_0/trace2_tb.v
SBY 14:53:00 [xlnxdemo_cvr] engine_0: ##   0:00:00  Writing trace to constraints file: engine_0/trace2.smtc
SBY 14:53:00 [xlnxdemo_cvr] engine_0: ##   0:00:00  Checking cover reachability in step 2..
SBY 14:53:00 [xlnxdemo_cvr] engine_0: ##   0:00:00  Reached cover statement at xlnxdemo.v:901 in step 2.
SBY 14:53:00 [xlnxdemo_cvr] engine_0: ##   0:00:00  Writing trace to VCD file: engine_0/trace3.vcd
SBY 14:53:00 [xlnxdemo_cvr] engine_0: ##   0:00:00  Writing trace to Verilog testbench: engine_0/trace3_tb.v
SBY 14:53:00 [xlnxdemo_cvr] engine_0: ##   0:00:00  Writing trace to constraints file: engine_0/trace3.smtc
SBY 14:53:00 [xlnxdemo_cvr] engine_0: ##   0:00:00  Checking cover reachability in step 2..
SBY 14:53:00 [xlnxdemo_cvr] engine_0: ##   0:00:00  Checking cover reachability in step 3..
SBY 14:53:00 [xlnxdemo_cvr] engine_0: ##   0:00:01  Reached cover statement at xlnxdemo.v:902 in step 3.
SBY 14:53:00 [xlnxdemo_cvr] engine_0: ##   0:00:01  Writing trace to VCD file: engine_0/trace4.vcd
SBY 14:53:00 [xlnxdemo_cvr] engine_0: ##   0:00:01  Writing trace to Verilog testbench: engine_0/trace4_tb.v
SBY 14:53:00 [xlnxdemo_cvr] engine_0: ##   0:00:01  Writing trace to constraints file: engine_0/trace4.smtc
SBY 14:53:00 [xlnxdemo_cvr] engine_0: ##   0:00:01  Checking cover reachability in step 3..
SBY 14:53:00 [xlnxdemo_cvr] engine_0: ##   0:00:01  Reached cover statement at xlnxdemo.v:1020 in step 3.
SBY 14:53:00 [xlnxdemo_cvr] engine_0: ##   0:00:01  Writing trace to VCD file: engine_0/trace5.vcd
SBY 14:53:00 [xlnxdemo_cvr] engine_0: ##   0:00:01  Writing trace to Verilog testbench: engine_0/trace5_tb.v
SBY 14:53:00 [xlnxdemo_cvr] engine_0: ##   0:00:01  Writing trace to constraints file: engine_0/trace5.smtc
SBY 14:53:00 [xlnxdemo_cvr] engine_0: ##   0:00:01  Checking cover reachability in step 3..
SBY 14:53:01 [xlnxdemo_cvr] engine_0: ##   0:00:01  Checking cover reachability in step 4..
SBY 14:53:01 [xlnxdemo_cvr] engine_0: ##   0:00:01  Reached cover statement at xlnxdemo.v:1021 in step 4.
SBY 14:53:01 [xlnxdemo_cvr] engine_0: ##   0:00:01  Writing trace to VCD file: engine_0/trace6.vcd
SBY 14:53:01 [xlnxdemo_cvr] engine_0: ##   0:00:01  Writing trace to Verilog testbench: engine_0/trace6_tb.v
SBY 14:53:01 [xlnxdemo_cvr] engine_0: ##   0:00:01  Writing trace to constraints file: engine_0/trace6.smtc
SBY 14:53:01 [xlnxdemo_cvr] engine_0: ##   0:00:01  Checking cover reachability in step 4..
SBY 14:53:01 [xlnxdemo_cvr] engine_0: ##   0:00:01  Reached cover statement at xlnxdemo.v:903 in step 4.
SBY 14:53:01 [xlnxdemo_cvr] engine_0: ##   0:00:01  Writing trace to VCD file: engine_0/trace7.vcd
SBY 14:53:01 [xlnxdemo_cvr] engine_0: ##   0:00:01  Writing trace to Verilog testbench: engine_0/trace7_tb.v
SBY 14:53:01 [xlnxdemo_cvr] engine_0: ##   0:00:01  Writing trace to constraints file: engine_0/trace7.smtc
SBY 14:53:01 [xlnxdemo_cvr] engine_0: ##   0:00:01  Checking cover reachability in step 4..
SBY 14:53:01 [xlnxdemo_cvr] engine_0: ##   0:00:01  Checking cover reachability in step 5..
SBY 14:53:01 [xlnxdemo_cvr] engine_0: ##   0:00:01  Reached cover statement at faxil_slave.v:704 in step 5.
SBY 14:53:01 [xlnxdemo_cvr] engine_0: ##   0:00:01  Writing trace to VCD file: engine_0/trace8.vcd
SBY 14:53:01 [xlnxdemo_cvr] engine_0: ##   0:00:01  Writing trace to Verilog testbench: engine_0/trace8_tb.v
SBY 14:53:01 [xlnxdemo_cvr] engine_0: ##   0:00:01  Writing trace to constraints file: engine_0/trace8.smtc
SBY 14:53:01 [xlnxdemo_cvr] engine_0: ##   0:00:01  Checking cover reachability in step 5..
SBY 14:53:01 [xlnxdemo_cvr] engine_0: ##   0:00:02  Reached cover statement at xlnxdemo.v:904 in step 5.
SBY 14:53:01 [xlnxdemo_cvr] engine_0: ##   0:00:02  Writing trace to VCD file: engine_0/trace9.vcd
SBY 14:53:01 [xlnxdemo_cvr] engine_0: ##   0:00:02  Writing trace to Verilog testbench: engine_0/trace9_tb.v
SBY 14:53:01 [xlnxdemo_cvr] engine_0: ##   0:00:02  Writing trace to constraints file: engine_0/trace9.smtc
SBY 14:53:01 [xlnxdemo_cvr] engine_0: ##   0:00:02  Checking cover reachability in step 5..
SBY 14:53:01 [xlnxdemo_cvr] engine_0: ##   0:00:02  Reached cover statement at faxil_slave.v:697 in step 5.
SBY 14:53:02 [xlnxdemo_cvr] engine_0: ##   0:00:02  Writing trace to VCD file: engine_0/trace10.vcd
SBY 14:53:02 [xlnxdemo_cvr] engine_0: ##   0:00:02  Writing trace to Verilog testbench: engine_0/trace10_tb.v
SBY 14:53:02 [xlnxdemo_cvr] engine_0: ##   0:00:02  Writing trace to constraints file: engine_0/trace10.smtc
SBY 14:53:02 [xlnxdemo_cvr] engine_0: ##   0:00:02  Checking cover reachability in step 5..
SBY 14:53:02 [xlnxdemo_cvr] engine_0: ##   0:00:02  Reached cover statement at xlnxdemo.v:1022 in step 5.
SBY 14:53:02 [xlnxdemo_cvr] engine_0: ##   0:00:02  Writing trace to VCD file: engine_0/trace11.vcd
SBY 14:53:02 [xlnxdemo_cvr] engine_0: ##   0:00:02  Writing trace to Verilog testbench: engine_0/trace11_tb.v
SBY 14:53:02 [xlnxdemo_cvr] engine_0: ##   0:00:02  Writing trace to constraints file: engine_0/trace11.smtc
SBY 14:53:02 [xlnxdemo_cvr] engine_0: ##   0:00:02  Checking cover reachability in step 5..
SBY 14:53:02 [xlnxdemo_cvr] engine_0: ##   0:00:02  Checking cover reachability in step 6..
SBY 14:53:02 [xlnxdemo_cvr] engine_0: ##   0:00:02  Reached cover statement at xlnxdemo.v:1023 in step 6.
SBY 14:53:02 [xlnxdemo_cvr] engine_0: ##   0:00:02  Writing trace to VCD file: engine_0/trace12.vcd
SBY 14:53:02 [xlnxdemo_cvr] engine_0: ##   0:00:02  Writing trace to Verilog testbench: engine_0/trace12_tb.v
SBY 14:53:02 [xlnxdemo_cvr] engine_0: ##   0:00:02  Writing trace to constraints file: engine_0/trace12.smtc
SBY 14:53:02 [xlnxdemo_cvr] engine_0: ##   0:00:02  Checking cover reachability in step 6..
SBY 14:53:02 [xlnxdemo_cvr] engine_0: ##   0:00:02  Reached cover statement at xlnxdemo.v:792 in step 6.
SBY 14:53:02 [xlnxdemo_cvr] engine_0: ##   0:00:02  Writing trace to VCD file: engine_0/trace13.vcd
SBY 14:53:02 [xlnxdemo_cvr] engine_0: ##   0:00:03  Writing trace to Verilog testbench: engine_0/trace13_tb.v
SBY 14:53:02 [xlnxdemo_cvr] engine_0: ##   0:00:03  Writing trace to constraints file: engine_0/trace13.smtc
SBY 14:53:02 [xlnxdemo_cvr] engine_0: ##   0:00:03  Checking cover reachability in step 6..
SBY 14:53:02 [xlnxdemo_cvr] engine_0: ##   0:00:03  Reached cover statement at xlnxdemo.v:905 in step 6.
SBY 14:53:02 [xlnxdemo_cvr] engine_0: ##   0:00:03  Writing trace to VCD file: engine_0/trace14.vcd
SBY 14:53:02 [xlnxdemo_cvr] engine_0: ##   0:00:03  Writing trace to Verilog testbench: engine_0/trace14_tb.v
SBY 14:53:02 [xlnxdemo_cvr] engine_0: ##   0:00:03  Writing trace to constraints file: engine_0/trace14.smtc
SBY 14:53:03 [xlnxdemo_cvr] engine_0: ##   0:00:03  Checking cover reachability in step 6..
SBY 14:53:03 [xlnxdemo_cvr] engine_0: ##   0:00:03  Checking cover reachability in step 7..
SBY 14:53:03 [xlnxdemo_cvr] engine_0: ##   0:00:03  Reached cover statement at xlnxdemo.v:906 in step 7.
SBY 14:53:03 [xlnxdemo_cvr] engine_0: ##   0:00:03  Writing trace to VCD file: engine_0/trace15.vcd
SBY 14:53:03 [xlnxdemo_cvr] engine_0: ##   0:00:03  Writing trace to Verilog testbench: engine_0/trace15_tb.v
SBY 14:53:03 [xlnxdemo_cvr] engine_0: ##   0:00:03  Writing trace to constraints file: engine_0/trace15.smtc
SBY 14:53:03 [xlnxdemo_cvr] engine_0: ##   0:00:03  Checking cover reachability in step 7..
SBY 14:53:03 [xlnxdemo_cvr] engine_0: ##   0:00:03  Reached cover statement at xlnxdemo.v:817 in step 7.
SBY 14:53:03 [xlnxdemo_cvr] engine_0: ##   0:00:03  Writing trace to VCD file: engine_0/trace16.vcd
SBY 14:53:03 [xlnxdemo_cvr] engine_0: ##   0:00:03  Writing trace to Verilog testbench: engine_0/trace16_tb.v
SBY 14:53:03 [xlnxdemo_cvr] engine_0: ##   0:00:03  Writing trace to constraints file: engine_0/trace16.smtc
SBY 14:53:03 [xlnxdemo_cvr] engine_0: ##   0:00:03  Checking cover reachability in step 7..
SBY 14:53:03 [xlnxdemo_cvr] engine_0: ##   0:00:03  Reached cover statement at xlnxdemo.v:810 in step 7.
SBY 14:53:03 [xlnxdemo_cvr] engine_0: ##   0:00:03  Writing trace to VCD file: engine_0/trace17.vcd
SBY 14:53:03 [xlnxdemo_cvr] engine_0: ##   0:00:04  Writing trace to Verilog testbench: engine_0/trace17_tb.v
SBY 14:53:03 [xlnxdemo_cvr] engine_0: ##   0:00:04  Writing trace to constraints file: engine_0/trace17.smtc
SBY 14:53:03 [xlnxdemo_cvr] engine_0: ##   0:00:04  Checking cover reachability in step 7..
SBY 14:53:03 [xlnxdemo_cvr] engine_0: ##   0:00:04  Reached cover statement at xlnxdemo.v:1024 in step 7.
SBY 14:53:03 [xlnxdemo_cvr] engine_0: ##   0:00:04  Writing trace to VCD file: engine_0/trace18.vcd
SBY 14:53:03 [xlnxdemo_cvr] engine_0: ##   0:00:04  Writing trace to Verilog testbench: engine_0/trace18_tb.v
SBY 14:53:03 [xlnxdemo_cvr] engine_0: ##   0:00:04  Writing trace to constraints file: engine_0/trace18.smtc
SBY 14:53:04 [xlnxdemo_cvr] engine_0: ##   0:00:04  Checking cover reachability in step 7..
SBY 14:53:04 [xlnxdemo_cvr] engine_0: ##   0:00:04  Checking cover reachability in step 8..
SBY 14:53:04 [xlnxdemo_cvr] engine_0: ##   0:00:04  Reached cover statement at xlnxdemo.v:1025 in step 8.
SBY 14:53:04 [xlnxdemo_cvr] engine_0: ##   0:00:04  Writing trace to VCD file: engine_0/trace19.vcd
SBY 14:53:04 [xlnxdemo_cvr] engine_0: ##   0:00:04  Writing trace to Verilog testbench: engine_0/trace19_tb.v
SBY 14:53:04 [xlnxdemo_cvr] engine_0: ##   0:00:04  Writing trace to constraints file: engine_0/trace19.smtc
SBY 14:53:04 [xlnxdemo_cvr] engine_0: ##   0:00:04  Checking cover reachability in step 8..
SBY 14:53:04 [xlnxdemo_cvr] engine_0: ##   0:00:04  Reached cover statement at xlnxdemo.v:907 in step 8.
SBY 14:53:04 [xlnxdemo_cvr] engine_0: ##   0:00:04  Writing trace to VCD file: engine_0/trace20.vcd
SBY 14:53:04 [xlnxdemo_cvr] engine_0: ##   0:00:04  Writing trace to Verilog testbench: engine_0/trace20_tb.v
SBY 14:53:04 [xlnxdemo_cvr] engine_0: ##   0:00:04  Writing trace to constraints file: engine_0/trace20.smtc
SBY 14:53:04 [xlnxdemo_cvr] engine_0: ##   0:00:04  Checking cover reachability in step 8..
SBY 14:53:04 [xlnxdemo_cvr] engine_0: ##   0:00:05  Checking cover reachability in step 9..
SBY 14:53:04 [xlnxdemo_cvr] engine_0: ##   0:00:05  Reached cover statement at xlnxdemo.v:1026 in step 9.
SBY 14:53:04 [xlnxdemo_cvr] engine_0: ##   0:00:05  Writing trace to VCD file: engine_0/trace21.vcd
SBY 14:53:05 [xlnxdemo_cvr] engine_0: ##   0:00:05  Writing trace to Verilog testbench: engine_0/trace21_tb.v
SBY 14:53:05 [xlnxdemo_cvr] engine_0: ##   0:00:05  Writing trace to constraints file: engine_0/trace21.smtc
SBY 14:53:05 [xlnxdemo_cvr] engine_0: ##   0:00:05  Checking cover reachability in step 9..
SBY 14:53:05 [xlnxdemo_cvr] engine_0: ##   0:00:05  Reached cover statement at xlnxdemo.v:908 in step 9.
SBY 14:53:05 [xlnxdemo_cvr] engine_0: ##   0:00:05  Writing trace to VCD file: engine_0/trace22.vcd
SBY 14:53:05 [xlnxdemo_cvr] engine_0: ##   0:00:05  Writing trace to Verilog testbench: engine_0/trace22_tb.v
SBY 14:53:05 [xlnxdemo_cvr] engine_0: ##   0:00:05  Writing trace to constraints file: engine_0/trace22.smtc
SBY 14:53:05 [xlnxdemo_cvr] engine_0: ##   0:00:05  Checking cover reachability in step 9..
SBY 14:53:05 [xlnxdemo_cvr] engine_0: ##   0:00:05  Checking cover reachability in step 10..
SBY 14:53:05 [xlnxdemo_cvr] engine_0: ##   0:00:05  Reached cover statement at xlnxdemo.v:1027 in step 10.
SBY 14:53:05 [xlnxdemo_cvr] engine_0: ##   0:00:05  Writing trace to VCD file: engine_0/trace23.vcd
SBY 14:53:05 [xlnxdemo_cvr] engine_0: ##   0:00:05  Writing trace to Verilog testbench: engine_0/trace23_tb.v
SBY 14:53:05 [xlnxdemo_cvr] engine_0: ##   0:00:05  Writing trace to constraints file: engine_0/trace23.smtc
SBY 14:53:05 [xlnxdemo_cvr] engine_0: ##   0:00:05  Checking cover reachability in step 10..
SBY 14:53:05 [xlnxdemo_cvr] engine_0: ##   0:00:06  Reached cover statement at xlnxdemo.v:909 in step 10.
SBY 14:53:05 [xlnxdemo_cvr] engine_0: ##   0:00:06  Writing trace to VCD file: engine_0/trace24.vcd
SBY 14:53:05 [xlnxdemo_cvr] engine_0: ##   0:00:06  Writing trace to Verilog testbench: engine_0/trace24_tb.v
SBY 14:53:05 [xlnxdemo_cvr] engine_0: ##   0:00:06  Writing trace to constraints file: engine_0/trace24.smtc
SBY 14:53:05 [xlnxdemo_cvr] engine_0: ##   0:00:06  Checking cover reachability in step 10..
SBY 14:53:06 [xlnxdemo_cvr] engine_0: ##   0:00:06  Checking cover reachability in step 11..
SBY 14:53:06 [xlnxdemo_cvr] engine_0: ##   0:00:06  Reached cover statement at xlnxdemo.v:1028 in step 11.
SBY 14:53:06 [xlnxdemo_cvr] engine_0: ##   0:00:06  Writing trace to VCD file: engine_0/trace25.vcd
SBY 14:53:06 [xlnxdemo_cvr] engine_0: ##   0:00:06  Writing trace to Verilog testbench: engine_0/trace25_tb.v
SBY 14:53:06 [xlnxdemo_cvr] engine_0: ##   0:00:06  Writing trace to constraints file: engine_0/trace25.smtc
SBY 14:53:06 [xlnxdemo_cvr] engine_0: ##   0:00:06  Checking cover reachability in step 11..
SBY 14:53:06 [xlnxdemo_cvr] engine_0: ##   0:00:06  Reached cover statement at xlnxdemo.v:910 in step 11.
SBY 14:53:06 [xlnxdemo_cvr] engine_0: ##   0:00:06  Writing trace to VCD file: engine_0/trace26.vcd
SBY 14:53:06 [xlnxdemo_cvr] engine_0: ##   0:00:06  Writing trace to Verilog testbench: engine_0/trace26_tb.v
SBY 14:53:06 [xlnxdemo_cvr] engine_0: ##   0:00:06  Writing trace to constraints file: engine_0/trace26.smtc
SBY 14:53:06 [xlnxdemo_cvr] engine_0: ##   0:00:06  Checking cover reachability in step 11..
SBY 14:53:06 [xlnxdemo_cvr] engine_0: ##   0:00:07  Checking cover reachability in step 12..
SBY 14:53:06 [xlnxdemo_cvr] engine_0: ##   0:00:07  Reached cover statement at xlnxdemo.v:911 in step 12.
SBY 14:53:07 [xlnxdemo_cvr] engine_0: ##   0:00:07  Writing trace to VCD file: engine_0/trace27.vcd
SBY 14:53:07 [xlnxdemo_cvr] engine_0: ##   0:00:07  Writing trace to Verilog testbench: engine_0/trace27_tb.v
SBY 14:53:07 [xlnxdemo_cvr] engine_0: ##   0:00:07  Writing trace to constraints file: engine_0/trace27.smtc
SBY 14:53:07 [xlnxdemo_cvr] engine_0: ##   0:00:07  Checking cover reachability in step 12..
SBY 14:53:07 [xlnxdemo_cvr] engine_0: ##   0:00:07  Checking cover reachability in step 13..
SBY 14:53:07 [xlnxdemo_cvr] engine_0: ##   0:00:07  Reached cover statement at xlnxdemo.v:912 in step 13.
SBY 14:53:07 [xlnxdemo_cvr] engine_0: ##   0:00:07  Writing trace to VCD file: engine_0/trace28.vcd
SBY 14:53:07 [xlnxdemo_cvr] engine_0: ##   0:00:07  Writing trace to Verilog testbench: engine_0/trace28_tb.v
SBY 14:53:07 [xlnxdemo_cvr] engine_0: ##   0:00:07  Writing trace to constraints file: engine_0/trace28.smtc
SBY 14:53:07 [xlnxdemo_cvr] engine_0: ##   0:00:07  Checking cover reachability in step 13..
SBY 14:53:07 [xlnxdemo_cvr] engine_0: ##   0:00:08  Reached cover statement at xlnxdemo.v:1029 in step 13.
SBY 14:53:07 [xlnxdemo_cvr] engine_0: ##   0:00:08  Writing trace to VCD file: engine_0/trace29.vcd
SBY 14:53:08 [xlnxdemo_cvr] engine_0: ##   0:00:08  Writing trace to Verilog testbench: engine_0/trace29_tb.v
SBY 14:53:08 [xlnxdemo_cvr] engine_0: ##   0:00:08  Writing trace to constraints file: engine_0/trace29.smtc
SBY 14:53:08 [xlnxdemo_cvr] engine_0: ##   0:00:08  Checking cover reachability in step 13..
SBY 14:53:08 [xlnxdemo_cvr] engine_0: ##   0:00:08  Checking cover reachability in step 14..
SBY 14:53:08 [xlnxdemo_cvr] engine_0: ##   0:00:08  Reached cover statement at xlnxdemo.v:1030 in step 14.
SBY 14:53:08 [xlnxdemo_cvr] engine_0: ##   0:00:08  Writing trace to VCD file: engine_0/trace30.vcd
SBY 14:53:08 [xlnxdemo_cvr] engine_0: ##   0:00:08  Writing trace to Verilog testbench: engine_0/trace30_tb.v
SBY 14:53:08 [xlnxdemo_cvr] engine_0: ##   0:00:08  Writing trace to constraints file: engine_0/trace30.smtc
SBY 14:53:08 [xlnxdemo_cvr] engine_0: ##   0:00:08  Checking cover reachability in step 14..
SBY 14:53:08 [xlnxdemo_cvr] engine_0: ##   0:00:08  Reached cover statement at xlnxdemo.v:913 in step 14.
SBY 14:53:08 [xlnxdemo_cvr] engine_0: ##   0:00:08  Writing trace to VCD file: engine_0/trace31.vcd
SBY 14:53:08 [xlnxdemo_cvr] engine_0: ##   0:00:09  Writing trace to Verilog testbench: engine_0/trace31_tb.v
SBY 14:53:08 [xlnxdemo_cvr] engine_0: ##   0:00:09  Writing trace to constraints file: engine_0/trace31.smtc
SBY 14:53:08 [xlnxdemo_cvr] engine_0: ##   0:00:09  Checking cover reachability in step 14..
SBY 14:53:09 [xlnxdemo_cvr] engine_0: ##   0:00:09  Checking cover reachability in step 15..
SBY 14:53:09 [xlnxdemo_cvr] engine_0: ##   0:00:09  Reached cover statement at xlnxdemo.v:1031 in step 15.
SBY 14:53:09 [xlnxdemo_cvr] engine_0: ##   0:00:09  Writing trace to VCD file: engine_0/trace32.vcd
SBY 14:53:09 [xlnxdemo_cvr] engine_0: ##   0:00:09  Writing trace to Verilog testbench: engine_0/trace32_tb.v
SBY 14:53:09 [xlnxdemo_cvr] engine_0: ##   0:00:09  Writing trace to constraints file: engine_0/trace32.smtc
SBY 14:53:09 [xlnxdemo_cvr] engine_0: ##   0:00:09  Checking cover reachability in step 15..
SBY 14:53:09 [xlnxdemo_cvr] engine_0: ##   0:00:09  Checking cover reachability in step 16..
SBY 14:53:09 [xlnxdemo_cvr] engine_0: ##   0:00:10  Reached cover statement at xlnxdemo.v:1032 in step 16.
SBY 14:53:09 [xlnxdemo_cvr] engine_0: ##   0:00:10  Writing trace to VCD file: engine_0/trace33.vcd
SBY 14:53:10 [xlnxdemo_cvr] engine_0: ##   0:00:10  Writing trace to Verilog testbench: engine_0/trace33_tb.v
SBY 14:53:10 [xlnxdemo_cvr] engine_0: ##   0:00:10  Writing trace to constraints file: engine_0/trace33.smtc
SBY 14:53:10 [xlnxdemo_cvr] engine_0: ##   0:00:10  Checking cover reachability in step 16..
SBY 14:53:10 [xlnxdemo_cvr] engine_0: ##   0:00:10  Checking cover reachability in step 17..
SBY 14:53:10 [xlnxdemo_cvr] engine_0: ##   0:00:10  Reached cover statement at xlnxdemo.v:1033 in step 17.
SBY 14:53:10 [xlnxdemo_cvr] engine_0: ##   0:00:10  Writing trace to VCD file: engine_0/trace34.vcd
SBY 14:53:10 [xlnxdemo_cvr] engine_0: ##   0:00:10  Writing trace to Verilog testbench: engine_0/trace34_tb.v
SBY 14:53:10 [xlnxdemo_cvr] engine_0: ##   0:00:10  Writing trace to constraints file: engine_0/trace34.smtc
SBY 14:53:10 [xlnxdemo_cvr] engine_0: ##   0:00:10  Checking cover reachability in step 17..
SBY 14:53:10 [xlnxdemo_cvr] engine_0: ##   0:00:11  Checking cover reachability in step 18..
SBY 14:53:11 [xlnxdemo_cvr] engine_0: ##   0:00:11  Reached cover statement at xlnxdemo.v:1034 in step 18.
SBY 14:53:11 [xlnxdemo_cvr] engine_0: ##   0:00:11  Writing trace to VCD file: engine_0/trace35.vcd
SBY 14:53:11 [xlnxdemo_cvr] engine_0: ##   0:00:11  Writing trace to Verilog testbench: engine_0/trace35_tb.v
SBY 14:53:11 [xlnxdemo_cvr] engine_0: ##   0:00:11  Writing trace to constraints file: engine_0/trace35.smtc
SBY 14:53:11 [xlnxdemo_cvr] engine_0: ##   0:00:11  Checking cover reachability in step 18..
SBY 14:53:11 [xlnxdemo_cvr] engine_0: ##   0:00:11  Checking cover reachability in step 19..
SBY 14:53:11 [xlnxdemo_cvr] engine_0: ##   0:00:11  Reached cover statement at xlnxdemo.v:1035 in step 19.
SBY 14:53:11 [xlnxdemo_cvr] engine_0: ##   0:00:12  Writing trace to VCD file: engine_0/trace36.vcd
SBY 14:53:11 [xlnxdemo_cvr] engine_0: ##   0:00:12  Writing trace to Verilog testbench: engine_0/trace36_tb.v
SBY 14:53:11 [xlnxdemo_cvr] engine_0: ##   0:00:12  Writing trace to constraints file: engine_0/trace36.smtc
SBY 14:53:12 [xlnxdemo_cvr] engine_0: ##   0:00:12  Checking cover reachability in step 19..
SBY 14:53:12 [xlnxdemo_cvr] engine_0: ##   0:00:12  Checking cover reachability in step 20..
SBY 14:53:12 [xlnxdemo_cvr] engine_0: ##   0:00:12  Reached cover statement at xlnxdemo.v:1036 in step 20.
SBY 14:53:12 [xlnxdemo_cvr] engine_0: ##   0:00:12  Writing trace to VCD file: engine_0/trace37.vcd
SBY 14:53:12 [xlnxdemo_cvr] engine_0: ##   0:00:12  Writing trace to Verilog testbench: engine_0/trace37_tb.v
SBY 14:53:12 [xlnxdemo_cvr] engine_0: ##   0:00:12  Writing trace to constraints file: engine_0/trace37.smtc
SBY 14:53:12 [xlnxdemo_cvr] engine_0: ##   0:00:12  Checking cover reachability in step 20..
SBY 14:53:12 [xlnxdemo_cvr] engine_0: ##   0:00:13  Checking cover reachability in step 21..
SBY 14:53:13 [xlnxdemo_cvr] engine_0: ##   0:00:13  Reached cover statement at xlnxdemo.v:1037 in step 21.
SBY 14:53:13 [xlnxdemo_cvr] engine_0: ##   0:00:13  Writing trace to VCD file: engine_0/trace38.vcd
SBY 14:53:13 [xlnxdemo_cvr] engine_0: ##   0:00:13  Writing trace to Verilog testbench: engine_0/trace38_tb.v
SBY 14:53:13 [xlnxdemo_cvr] engine_0: ##   0:00:13  Writing trace to constraints file: engine_0/trace38.smtc
SBY 14:53:13 [xlnxdemo_cvr] engine_0: ##   0:00:13  Checking cover reachability in step 21..
SBY 14:53:13 [xlnxdemo_cvr] engine_0: ##   0:00:13  Checking cover reachability in step 22..
SBY 14:53:13 [xlnxdemo_cvr] engine_0: ##   0:00:14  Reached cover statement at xlnxdemo.v:1038 in step 22.
SBY 14:53:13 [xlnxdemo_cvr] engine_0: ##   0:00:14  Writing trace to VCD file: engine_0/trace39.vcd
SBY 14:53:14 [xlnxdemo_cvr] engine_0: ##   0:00:14  Writing trace to Verilog testbench: engine_0/trace39_tb.v
SBY 14:53:14 [xlnxdemo_cvr] engine_0: ##   0:00:14  Writing trace to constraints file: engine_0/trace39.smtc
SBY 14:53:14 [xlnxdemo_cvr] engine_0: ##   0:00:14  Checking cover reachability in step 22..
SBY 14:53:14 [xlnxdemo_cvr] engine_0: ##   0:00:14  Checking cover reachability in step 23..
SBY 14:53:14 [xlnxdemo_cvr] engine_0: ##   0:00:14  Reached cover statement at xlnxdemo.v:1039 in step 23.
SBY 14:53:14 [xlnxdemo_cvr] engine_0: ##   0:00:14  Writing trace to VCD file: engine_0/trace40.vcd
SBY 14:53:14 [xlnxdemo_cvr] engine_0: ##   0:00:15  Writing trace to Verilog testbench: engine_0/trace40_tb.v
SBY 14:53:14 [xlnxdemo_cvr] engine_0: ##   0:00:15  Writing trace to constraints file: engine_0/trace40.smtc
SBY 14:53:14 [xlnxdemo_cvr] engine_0: ##   0:00:15  Checking cover reachability in step 23..
SBY 14:53:15 [xlnxdemo_cvr] engine_0: ##   0:00:15  Checking cover reachability in step 24..
SBY 14:53:15 [xlnxdemo_cvr] engine_0: ##   0:00:15  Reached cover statement at xlnxdemo.v:1040 in step 24.
SBY 14:53:15 [xlnxdemo_cvr] engine_0: ##   0:00:15  Writing trace to VCD file: engine_0/trace41.vcd
SBY 14:53:15 [xlnxdemo_cvr] engine_0: ##   0:00:15  Writing trace to Verilog testbench: engine_0/trace41_tb.v
SBY 14:53:15 [xlnxdemo_cvr] engine_0: ##   0:00:16  Writing trace to constraints file: engine_0/trace41.smtc
SBY 14:53:15 [xlnxdemo_cvr] engine_0: ##   0:00:16  Checking cover reachability in step 24..
SBY 14:53:16 [xlnxdemo_cvr] engine_0: ##   0:00:16  Checking cover reachability in step 25..
SBY 14:53:16 [xlnxdemo_cvr] engine_0: ##   0:00:16  Reached cover statement at xlnxdemo.v:1041 in step 25.
SBY 14:53:16 [xlnxdemo_cvr] engine_0: ##   0:00:16  Writing trace to VCD file: engine_0/trace42.vcd
SBY 14:53:16 [xlnxdemo_cvr] engine_0: ##   0:00:16  Writing trace to Verilog testbench: engine_0/trace42_tb.v
SBY 14:53:16 [xlnxdemo_cvr] engine_0: ##   0:00:16  Writing trace to constraints file: engine_0/trace42.smtc
SBY 14:53:16 [xlnxdemo_cvr] engine_0: ##   0:00:16  Checking cover reachability in step 25..
SBY 14:53:16 [xlnxdemo_cvr] engine_0: ##   0:00:17  Checking cover reachability in step 26..
SBY 14:53:17 [xlnxdemo_cvr] engine_0: ##   0:00:17  Reached cover statement at xlnxdemo.v:1042 in step 26.
SBY 14:53:17 [xlnxdemo_cvr] engine_0: ##   0:00:17  Writing trace to VCD file: engine_0/trace43.vcd
SBY 14:53:17 [xlnxdemo_cvr] engine_0: ##   0:00:17  Writing trace to Verilog testbench: engine_0/trace43_tb.v
SBY 14:53:17 [xlnxdemo_cvr] engine_0: ##   0:00:17  Writing trace to constraints file: engine_0/trace43.smtc
SBY 14:53:17 [xlnxdemo_cvr] engine_0: ##   0:00:17  Checking cover reachability in step 26..
SBY 14:53:17 [xlnxdemo_cvr] engine_0: ##   0:00:17  Checking cover reachability in step 27..
SBY 14:53:17 [xlnxdemo_cvr] engine_0: ##   0:00:18  Checking cover reachability in step 28..
SBY 14:53:18 [xlnxdemo_cvr] engine_0: ##   0:00:18  Checking cover reachability in step 29..
SBY 14:53:18 [xlnxdemo_cvr] engine_0: ##   0:00:18  Checking cover reachability in step 30..
SBY 14:53:18 [xlnxdemo_cvr] engine_0: ##   0:00:18  Checking cover reachability in step 31..
SBY 14:53:18 [xlnxdemo_cvr] engine_0: ##   0:00:19  Checking cover reachability in step 32..
SBY 14:53:19 [xlnxdemo_cvr] engine_0: ##   0:00:19  Checking cover reachability in step 33..
SBY 14:53:19 [xlnxdemo_cvr] engine_0: ##   0:00:19  Checking cover reachability in step 34..
SBY 14:53:19 [xlnxdemo_cvr] engine_0: ##   0:00:20  Checking cover reachability in step 35..
SBY 14:53:20 [xlnxdemo_cvr] engine_0: ##   0:00:20  Checking cover reachability in step 36..
SBY 14:53:20 [xlnxdemo_cvr] engine_0: ##   0:00:20  Checking cover reachability in step 37..
SBY 14:53:20 [xlnxdemo_cvr] engine_0: ##   0:00:20  Checking cover reachability in step 38..
SBY 14:53:20 [xlnxdemo_cvr] engine_0: ##   0:00:21  Checking cover reachability in step 39..
SBY 14:53:21 [xlnxdemo_cvr] engine_0: ##   0:00:21  Checking cover reachability in step 40..
SBY 14:53:21 [xlnxdemo_cvr] engine_0: ##   0:00:21  Checking cover reachability in step 41..
SBY 14:53:21 [xlnxdemo_cvr] engine_0: ##   0:00:22  Checking cover reachability in step 42..
SBY 14:53:22 [xlnxdemo_cvr] engine_0: ##   0:00:22  Checking cover reachability in step 43..
SBY 14:53:22 [xlnxdemo_cvr] engine_0: ##   0:00:22  Checking cover reachability in step 44..
SBY 14:53:22 [xlnxdemo_cvr] engine_0: ##   0:00:22  Checking cover reachability in step 45..
SBY 14:53:23 [xlnxdemo_cvr] engine_0: ##   0:00:23  Checking cover reachability in step 46..
SBY 14:53:23 [xlnxdemo_cvr] engine_0: ##   0:00:23  Checking cover reachability in step 47..
SBY 14:53:23 [xlnxdemo_cvr] engine_0: ##   0:00:23  Checking cover reachability in step 48..
SBY 14:53:24 [xlnxdemo_cvr] engine_0: ##   0:00:24  Checking cover reachability in step 49..
SBY 14:53:24 [xlnxdemo_cvr] engine_0: ##   0:00:24  Checking cover reachability in step 50..
SBY 14:53:24 [xlnxdemo_cvr] engine_0: ##   0:00:24  Checking cover reachability in step 51..
SBY 14:53:25 [xlnxdemo_cvr] engine_0: ##   0:00:25  Checking cover reachability in step 52..
SBY 14:53:25 [xlnxdemo_cvr] engine_0: ##   0:00:25  Checking cover reachability in step 53..
SBY 14:53:25 [xlnxdemo_cvr] engine_0: ##   0:00:26  Checking cover reachability in step 54..
SBY 14:53:26 [xlnxdemo_cvr] engine_0: ##   0:00:26  Checking cover reachability in step 55..
SBY 14:53:26 [xlnxdemo_cvr] engine_0: ##   0:00:26  Checking cover reachability in step 56..
SBY 14:53:26 [xlnxdemo_cvr] engine_0: ##   0:00:27  Checking cover reachability in step 57..
SBY 14:53:27 [xlnxdemo_cvr] engine_0: ##   0:00:27  Checking cover reachability in step 58..
SBY 14:53:27 [xlnxdemo_cvr] engine_0: ##   0:00:27  Checking cover reachability in step 59..
SBY 14:53:27 [xlnxdemo_cvr] engine_0: ##   0:00:28  Unreached cover statement at xlnxdemo.v:829.
SBY 14:53:27 [xlnxdemo_cvr] engine_0: ##   0:00:28  Unreached cover statement at xlnxdemo.v:836.
SBY 14:53:27 [xlnxdemo_cvr] engine_0: ##   0:00:28  Status: FAILED (!)
SBY 14:53:27 [xlnxdemo_cvr] engine_0: finished (returncode=1)
SBY 14:53:27 [xlnxdemo_cvr] engine_0: Status returned by engine: FAIL
SBY 14:53:27 [xlnxdemo_cvr] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:29 (29)
SBY 14:53:27 [xlnxdemo_cvr] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:30 (30)
SBY 14:53:27 [xlnxdemo_cvr] summary: engine_0 (smtbmc) returned FAIL
SBY 14:53:27 [xlnxdemo_cvr] DONE (FAIL, rc=2)
SBY 14:53:27 [xlnxdemo_prf] Removing direcory 'xlnxdemo_prf'.
SBY 14:53:27 [xlnxdemo_prf] Copy 'faxil_slave.v' to 'xlnxdemo_prf/src/faxil_slave.v'.
SBY 14:53:27 [xlnxdemo_prf] Copy 'xlnxdemo.v' to 'xlnxdemo_prf/src/xlnxdemo.v'.
SBY 14:53:27 [xlnxdemo_prf] engine_0: smtbmc
SBY 14:53:27 [xlnxdemo_prf] base: starting process "cd xlnxdemo_prf/src; yosys -ql ../model/design.log ../model/design.ys"
SBY 14:53:28 [xlnxdemo_prf] base: finished (returncode=0)
SBY 14:53:28 [xlnxdemo_prf] smt2: starting process "cd xlnxdemo_prf/model; yosys -ql design_smt2.log design_smt2.ys"
SBY 14:53:29 [xlnxdemo_prf] smt2: finished (returncode=0)
SBY 14:53:29 [xlnxdemo_prf] engine_0.basecase: starting process "cd xlnxdemo_prf; yosys-smtbmc --presat --unroll --noprogress -t 40 --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 14:53:29 [xlnxdemo_prf] engine_0.induction: starting process "cd xlnxdemo_prf; yosys-smtbmc --presat --unroll -i --noprogress -t 40 --append 0 --dump-vcd engine_0/trace_induct.vcd --dump-vlogtb engine_0/trace_induct_tb.v --dump-smtc engine_0/trace_induct.smtc model/design_smt2.smt2"
SBY 14:53:29 [xlnxdemo_prf] engine_0.basecase: ##   0:00:00  Solver: yices
SBY 14:53:29 [xlnxdemo_prf] engine_0.induction: ##   0:00:00  Solver: yices
SBY 14:53:29 [xlnxdemo_prf] engine_0.basecase: ##   0:00:00  Checking assumptions in step 0..
SBY 14:53:29 [xlnxdemo_prf] engine_0.basecase: ##   0:00:00  Checking assertions in step 0..
SBY 14:53:29 [xlnxdemo_prf] engine_0.induction: ##   0:00:00  Trying induction in step 40..
SBY 14:53:29 [xlnxdemo_prf] engine_0.induction: ##   0:00:00  Trying induction in step 39..
SBY 14:53:29 [xlnxdemo_prf] engine_0.basecase: ##   0:00:00  Checking assumptions in step 1..
SBY 14:53:29 [xlnxdemo_prf] engine_0.basecase: ##   0:00:00  Checking assertions in step 1..
SBY 14:53:29 [xlnxdemo_prf] engine_0.induction: ##   0:00:00  Trying induction in step 38..
SBY 14:53:29 [xlnxdemo_prf] engine_0.basecase: ##   0:00:00  Checking assumptions in step 2..
SBY 14:53:29 [xlnxdemo_prf] engine_0.basecase: ##   0:00:00  Checking assertions in step 2..
SBY 14:53:29 [xlnxdemo_prf] engine_0.induction: ##   0:00:00  Trying induction in step 37..
SBY 14:53:29 [xlnxdemo_prf] engine_0.induction: ##   0:00:00  Trying induction in step 36..
SBY 14:53:29 [xlnxdemo_prf] engine_0.basecase: ##   0:00:00  Checking assumptions in step 3..
SBY 14:53:29 [xlnxdemo_prf] engine_0.basecase: ##   0:00:00  Checking assertions in step 3..
SBY 14:53:29 [xlnxdemo_prf] engine_0.induction: ##   0:00:00  Trying induction in step 35..
SBY 14:53:29 [xlnxdemo_prf] engine_0.basecase: ##   0:00:00  Checking assumptions in step 4..
SBY 14:53:29 [xlnxdemo_prf] engine_0.basecase: ##   0:00:00  Checking assertions in step 4..
SBY 14:53:29 [xlnxdemo_prf] engine_0.induction: ##   0:00:00  Trying induction in step 34..
SBY 14:53:29 [xlnxdemo_prf] engine_0.basecase: ##   0:00:00  Checking assumptions in step 5..
SBY 14:53:29 [xlnxdemo_prf] engine_0.basecase: ##   0:00:00  Checking assertions in step 5..
SBY 14:53:29 [xlnxdemo_prf] engine_0.induction: ##   0:00:00  Trying induction in step 33..
SBY 14:53:29 [xlnxdemo_prf] engine_0.induction: ##   0:00:00  Trying induction in step 32..
SBY 14:53:29 [xlnxdemo_prf] engine_0.basecase: ##   0:00:00  Checking assumptions in step 6..
SBY 14:53:29 [xlnxdemo_prf] engine_0.basecase: ##   0:00:00  Checking assertions in step 6..
SBY 14:53:29 [xlnxdemo_prf] engine_0.induction: ##   0:00:00  Trying induction in step 31..
SBY 14:53:29 [xlnxdemo_prf] engine_0.basecase: ##   0:00:00  BMC failed!
SBY 14:53:29 [xlnxdemo_prf] engine_0.basecase: ##   0:00:00  Assert failed in xlnxdemo: xlnxdemo.v:774
SBY 14:53:29 [xlnxdemo_prf] engine_0.basecase: ##   0:00:00  Writing trace to VCD file: engine_0/trace.vcd
SBY 14:53:29 [xlnxdemo_prf] engine_0.basecase: ##   0:00:00  Writing trace to Verilog testbench: engine_0/trace_tb.v
SBY 14:53:29 [xlnxdemo_prf] engine_0.basecase: ##   0:00:00  Writing trace to constraints file: engine_0/trace.smtc
SBY 14:53:30 [xlnxdemo_prf] engine_0.basecase: ##   0:00:00  Status: FAILED (!)
SBY 14:53:30 [xlnxdemo_prf] engine_0.basecase: finished (returncode=1)
SBY 14:53:30 [xlnxdemo_prf] engine_0: Status returned by engine for basecase: FAIL
SBY 14:53:30 [xlnxdemo_prf] engine_0.induction: terminating process
SBY 14:53:30 [xlnxdemo_prf] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:02 (2)
SBY 14:53:30 [xlnxdemo_prf] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:02 (2)
SBY 14:53:30 [xlnxdemo_prf] summary: engine_0 (smtbmc) returned FAIL for basecase
SBY 14:53:30 [xlnxdemo_prf] summary: counterexample trace: xlnxdemo_prf/engine_0/trace.vcd
SBY 14:53:30 [xlnxdemo_prf] DONE (FAIL, rc=2)

Unfortunately I'm too much of a beginner to figure out where the issues is. I can also provide the vcd files if you can't reproduce.

ZipCPU commented 5 years ago

The issue is that Xilinx's demo code is broken in the first place. This is why I wrote the demoaxi.v core--to fix the latent problems within their core, and to achieve higher throughput.

I can add some information to the README to point that out.

Dan

bluewww commented 5 years ago

Ah thanks for the quick answer, so I missed that part in the blog post :)

edit: I think a note in the readme would be nice

ZipCPU commented 5 years ago

See the updated note in the readme.

Dan