YosysHQ/nerv

Formal checks error

Closed this issue · 1 comments

When following the instructions for running the formal checks, I get the following results:

root@f56472ae3ced:/riscv-formal/cores/nerv# make check 
python3 ../../checks/genchecks.py
Reading checks.cfg.
Creating checks directory.
Generated 43 checks.
make -C checks
make[1]: Entering directory '/riscv-formal/cores/nerv/checks'
sby reg_ch0.sby
SBY 16:50:57 [reg_ch0] Writing 'reg_ch0/src/defines.sv'.
SBY 16:50:57 [reg_ch0] Writing 'reg_ch0/src/reg_ch0.sv'.
SBY 16:50:57 [reg_ch0] Copy '/riscv-formal/checks/rvfi_macros.vh' to '/riscv-formal/cores/nerv/checks/reg_ch0/src/rvfi_macros.vh'.
SBY 16:50:57 [reg_ch0] Copy '/riscv-formal/checks/rvfi_channel.sv' to '/riscv-formal/cores/nerv/checks/reg_ch0/src/rvfi_channel.sv'.
SBY 16:50:57 [reg_ch0] Copy '/riscv-formal/checks/rvfi_testbench.sv' to '/riscv-formal/cores/nerv/checks/reg_ch0/src/rvfi_testbench.sv'.
SBY 16:50:57 [reg_ch0] Copy '/riscv-formal/checks/rvfi_reg_check.sv' to '/riscv-formal/cores/nerv/checks/reg_ch0/src/rvfi_reg_check.sv'.
SBY 16:50:57 [reg_ch0] engine_0: smtbmc boolector
SBY 16:50:57 [reg_ch0] base: starting process "cd reg_ch0/src; yosys -ql ../model/design.log ../model/design.ys"
SBY 16:50:57 [reg_ch0] base: rvfi_reg_check.sv:19: ERROR: syntax error, unexpected TOK_RAND
SBY 16:50:57 [reg_ch0] base: finished (returncode=1)
SBY 16:50:57 [reg_ch0] base: task failed. ERROR.
SBY 16:50:57 [reg_ch0] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 16:50:57 [reg_ch0] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 16:50:57 [reg_ch0] DONE (ERROR, rc=16)
make[1]: *** [makefile:4: reg_ch0/status] Error 16
make[1]: Leaving directory '/riscv-formal/cores/nerv/checks'
make: *** [Makefile:34: check] Error 2

Using the latest main branch of nerv.

Please update riscv-formal now. Both repos are updated and tests are passing now.