search

YosysHQ / picorv32

PicoRV32 - A Size-Optimized RISC-V CPU
ISC License
3.08k stars 748 forks source link

yices? #258

Closed secworks closed 5 months ago

secworks commented 5 months ago

There is a target "check" that has "check-yices" as dependency. But that does not exists. Is this a typo?

https://github.com/YosysHQ/picorv32/blob/336cfca6e5f1c08788348aadc46b3581b9a5d585/Makefile#L87C1-L87C19

mmicko commented 5 months ago

Actually this is fine. check-yices will be matched with rule in line 89 ( check-% ) that will then first run check.smt2 and then execute itself. This rule just force using of yices solver when running yosys-smtbmc.

secworks commented 5 months ago

Thanks!