YosysHQ/mcy

picorv32_primes example bitrotted

nakengelhardt opened this issue · 1 comments

To reproduce:

cd examples/picorv32_primes
mcy init
mcy run
  1. sby is now requiring a [tasks] section with regex (YosysHQ/sby#76), but this wasn't added to examples/picorv32_primes/eq_bmc.sby and examples/picorv32_primes/eq_sim3.sby

    • Side note: [0-9]+ does not work as a task regex, but \d+ does
  2. 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.