search

YosysHQ / riscv-formal

RISC-V Formal Verification Framework
ISC License
94 stars 21 forks source link

Picorv32 checks failing #5

Closed KasperHesse closed 1 year ago

KasperHesse commented 1 year ago

I have followed the instructions in cores/picorv32 and installed the oss-cad-suite from the latest tar-file. Running make -C checks -j1 generates the following error message:

make: Entering directory '/home/kasper/riscv-formal/cores/picorv32/checks'
sby reg_ch0.sby
SBY 11:02:07 [reg_ch0] ERROR: Option skip is only valid for smtbmc and btor engines.
make: *** [makefile:4: reg_ch0/status] Error 1
make: Leaving directory '/home/kasper/riscv-formal/cores/picorv32/checks'

I see that the same issue is apparent in the CI-flow for nerv.

jix commented 1 year ago

This was a now-fixed bug in SBY, see YosysHQ/sby#216