picorv32_primes example bitrotted
nakengelhardt opened this issue · 1 comments
nakengelhardt commented
To reproduce:
cd examples/picorv32_primes
mcy init
mcy run
-
sby is now requiring a
[tasks]
section with regex (YosysHQ/sby#76), but this wasn't added toexamples/picorv32_primes/eq_bmc.sby
andexamples/picorv32_primes/eq_sim3.sby
- Side note:
[0-9]+
does not work as a task regex, but\d+
does
- Side note:
-
eq_bmc.sby fails in generating the smt2 model:
SBY 16:22:13 [eq_bmc_1] smt2: starting process "cd eq_bmc_1/model; yosys -ql design_smt2.log design_smt2.ys"
SBY 16:22:14 [eq_bmc_1] smt2: ERROR: Assert `bit_driver.count(bit) == 0' failed in backends/smt2/smt2.cc:397.
jix commented
I also tested running the full picorv32_primes example after applying the task name fix and with YosysHQ/yosys#3359 and it runs fine now.