search

YosysHQ / mcy

Mutation Cover with Yosys (MCY)
ISC License
77 stars 9 forks source link

picorv32_primes example bitrotted #32

Closed nakengelhardt closed 2 years ago

nakengelhardt commented 2 years ago

To reproduce:

cd examples/picorv32_primes
mcy init
mcy run

  1. sby is now requiring a [tasks] section with regex (https://github.com/YosysHQ/sby/issues/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 2 years ago

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.