icicle
icicle copied to clipboard
Published
20 hours ago •
grahamedgecombe
grahamedgecombe
Formal verfication failing
ERROR: Module `rv32_writeback' referenced in module `rv32' in cell `writeback' does not have a port named 'rvfi_ixl'.
It seems to not be passing verification with a clean install directory with no changes compared to a repo.
10738 git clone https://github.com/SymbioticEDA/riscv-formal
10739 cd riscv-formal/cores && git clone https://github.com/grahamedgecombe/icicle
10740 cd icicle && python ../../checks/genchecks.py && make -C checks -j `nproc`
python ../../checks/genchecks.py && make -C checks -j `nproc`
Reading checks.cfg.
Creating checks directory.
Generated 45 checks.
make: Entering directory '/home/nota/ice/riscv-formal/cores/icicle/checks'
sby causal_ch0.sby
sby hang.sby
sby ill_ch0.sby
sby liveness_ch0.sby
sby pc_bwd_ch0.sby
sby pc_fwd_ch0.sby
sby reg_ch0.sby
sby unique_ch0.sby
sby insn_add_ch0.sby
sby insn_addi_ch0.sby
sby insn_and_ch0.sby
sby insn_andi_ch0.sby
SBY 8:04:54 [pc_fwd_ch0] Writing 'pc_fwd_ch0/src/defines.sv'.
SBY 8:04:54 [pc_fwd_ch0] Writing 'pc_fwd_ch0/src/pc_fwd_ch0.sv'.
SBY 8:04:54 [pc_fwd_ch0] Copy '/home/nota/ice/riscv-formal/cores/icicle/../../checks/rvfi_macros.vh' to 'pc_fwd_ch0/src/rvfi_macros.vh'.
SBY 8:04:54 [pc_fwd_ch0] Copy '/home/nota/ice/riscv-formal/cores/icicle/../../checks/rvfi_channel.sv' to 'pc_fwd_ch0/src/rvfi_channel.sv'.
SBY 8:04:54 [pc_fwd_ch0] Copy '/home/nota/ice/riscv-formal/cores/icicle/../../checks/rvfi_testbench.sv' to 'pc_fwd_ch0/src/rvfi_testbench.sv'.
SBY 8:04:54 [ill_ch0] Writing 'ill_ch0/src/defines.sv'.
SBY 8:04:54 [causal_ch0] Writing 'causal_ch0/src/defines.sv'.
SBY 8:04:54 [pc_fwd_ch0] Copy '/home/nota/ice/riscv-formal/cores/icicle/../../checks/rvfi_pc_fwd_check.sv' to 'pc_fwd_ch0/src/rvfi_pc_fwd_check.sv'.
SBY 8:04:54 [causal_ch0] Writing 'causal_ch0/src/causal_ch0.sv'.
SBY 8:04:54 [ill_ch0] Writing 'ill_ch0/src/ill_ch0.sv'.
SBY 8:04:54 [causal_ch0] Copy '/home/nota/ice/riscv-formal/cores/icicle/../../checks/rvfi_macros.vh' to 'causal_ch0/src/rvfi_macros.vh'.
SBY 8:04:54 [ill_ch0] Copy '/home/nota/ice/riscv-formal/cores/icicle/../../checks/rvfi_macros.vh' to 'ill_ch0/src/rvfi_macros.vh'.
SBY 8:04:54 [causal_ch0] Copy '/home/nota/ice/riscv-formal/cores/icicle/../../checks/rvfi_channel.sv' to 'causal_ch0/src/rvfi_channel.sv'.
SBY 8:04:54 [ill_ch0] Copy '/home/nota/ice/riscv-formal/cores/icicle/../../checks/rvfi_channel.sv' to 'ill_ch0/src/rvfi_channel.sv'.
SBY 8:04:54 [causal_ch0] Copy '/home/nota/ice/riscv-formal/cores/icicle/../../checks/rvfi_testbench.sv' to 'causal_ch0/src/rvfi_testbench.sv'.
SBY 8:04:54 [ill_ch0] Copy '/home/nota/ice/riscv-formal/cores/icicle/../../checks/rvfi_testbench.sv' to 'ill_ch0/src/rvfi_testbench.sv'.
SBY 8:04:54 [causal_ch0] Copy '/home/nota/ice/riscv-formal/cores/icicle/../../checks/rvfi_causal_check.sv' to 'causal_ch0/src/rvfi_causal_check.sv'.
SBY 8:04:54 [ill_ch0] Copy '/home/nota/ice/riscv-formal/cores/icicle/../../checks/rvfi_ill_check.sv' to 'ill_ch0/src/rvfi_ill_check.sv'.
SBY 8:04:54 [pc_fwd_ch0] engine_0: smtbmc boolector
SBY 8:04:54 [reg_ch0] Writing 'reg_ch0/src/defines.sv'.
SBY 8:04:54 [unique_ch0] Writing 'unique_ch0/src/defines.sv'.
SBY 8:04:54 [reg_ch0] Writing 'reg_ch0/src/reg_ch0.sv'.
SBY 8:04:54 [unique_ch0] Writing 'unique_ch0/src/unique_ch0.sv'.
SBY 8:04:54 [reg_ch0] Copy '/home/nota/ice/riscv-formal/cores/icicle/../../checks/rvfi_macros.vh' to 'reg_ch0/src/rvfi_macros.vh'.
SBY 8:04:54 [unique_ch0] Copy '/home/nota/ice/riscv-formal/cores/icicle/../../checks/rvfi_macros.vh' to 'unique_ch0/src/rvfi_macros.vh'.
SBY 8:04:54 [reg_ch0] Copy '/home/nota/ice/riscv-formal/cores/icicle/../../checks/rvfi_channel.sv' to 'reg_ch0/src/rvfi_channel.sv'.
SBY 8:04:54 [unique_ch0] Copy '/home/nota/ice/riscv-formal/cores/icicle/../../checks/rvfi_channel.sv' to 'unique_ch0/src/rvfi_channel.sv'.
SBY 8:04:54 [insn_addi_ch0] Writing 'insn_addi_ch0/src/defines.sv'.
SBY 8:04:54 [hang] Writing 'hang/src/defines.sv'.
SBY 8:04:54 [reg_ch0] Copy '/home/nota/ice/riscv-formal/cores/icicle/../../checks/rvfi_testbench.sv' to 'reg_ch0/src/rvfi_testbench.sv'.
SBY 8:04:54 [causal_ch0] engine_0: smtbmc boolector
SBY 8:04:54 [unique_ch0] Copy '/home/nota/ice/riscv-formal/cores/icicle/../../checks/rvfi_testbench.sv' to 'unique_ch0/src/rvfi_testbench.sv'.
SBY 8:04:54 [insn_addi_ch0] Writing 'insn_addi_ch0/src/insn_addi_ch0.sv'.
SBY 8:04:54 [ill_ch0] engine_0: smtbmc boolector
SBY 8:04:54 [reg_ch0] Copy '/home/nota/ice/riscv-formal/cores/icicle/../../checks/rvfi_reg_check.sv' to 'reg_ch0/src/rvfi_reg_check.sv'.
SBY 8:04:54 [hang] Writing 'hang/src/hang.sv'.
SBY 8:04:54 [insn_addi_ch0] Copy '/home/nota/ice/riscv-formal/cores/icicle/../../checks/rvfi_macros.vh' to 'insn_addi_ch0/src/rvfi_macros.vh'.
SBY 8:04:54 [pc_bwd_ch0] Writing 'pc_bwd_ch0/src/defines.sv'.
SBY 8:04:54 [unique_ch0] Copy '/home/nota/ice/riscv-formal/cores/icicle/../../checks/rvfi_unique_check.sv' to 'unique_ch0/src/rvfi_unique_check.sv'.
SBY 8:04:54 [liveness_ch0] Writing 'liveness_ch0/src/defines.sv'.
SBY 8:04:54 [insn_add_ch0] Writing 'insn_add_ch0/src/defines.sv'.
SBY 8:04:54 [pc_bwd_ch0] Writing 'pc_bwd_ch0/src/pc_bwd_ch0.sv'.
SBY 8:04:54 [insn_addi_ch0] Copy '/home/nota/ice/riscv-formal/cores/icicle/../../checks/rvfi_channel.sv' to 'insn_addi_ch0/src/rvfi_channel.sv'.
SBY 8:04:54 [insn_and_ch0] Writing 'insn_and_ch0/src/defines.sv'.
SBY 8:04:54 [liveness_ch0] Writing 'liveness_ch0/src/liveness_ch0.sv'.
SBY 8:04:54 [insn_add_ch0] Writing 'insn_add_ch0/src/insn_add_ch0.sv'.
SBY 8:04:54 [insn_and_ch0] Writing 'insn_and_ch0/src/insn_and_ch0.sv'.
SBY 8:04:54 [pc_bwd_ch0] Copy '/home/nota/ice/riscv-formal/cores/icicle/../../checks/rvfi_macros.vh' to 'pc_bwd_ch0/src/rvfi_macros.vh'.
SBY 8:04:54 [insn_addi_ch0] Copy '/home/nota/ice/riscv-formal/cores/icicle/../../checks/rvfi_testbench.sv' to 'insn_addi_ch0/src/rvfi_testbench.sv'.
SBY 8:04:54 [liveness_ch0] Copy '/home/nota/ice/riscv-formal/cores/icicle/../../checks/rvfi_macros.vh' to 'liveness_ch0/src/rvfi_macros.vh'.
SBY 8:04:54 [insn_add_ch0] Copy '/home/nota/ice/riscv-formal/cores/icicle/../../checks/rvfi_macros.vh' to 'insn_add_ch0/src/rvfi_macros.vh'.
SBY 8:04:54 [insn_and_ch0] Copy '/home/nota/ice/riscv-formal/cores/icicle/../../checks/rvfi_macros.vh' to 'insn_and_ch0/src/rvfi_macros.vh'.
SBY 8:04:54 [insn_addi_ch0] Copy '/home/nota/ice/riscv-formal/cores/icicle/../../checks/rvfi_insn_check.sv' to 'insn_addi_ch0/src/rvfi_insn_check.sv'.
SBY 8:04:54 [pc_bwd_ch0] Copy '/home/nota/ice/riscv-formal/cores/icicle/../../checks/rvfi_channel.sv' to 'pc_bwd_ch0/src/rvfi_channel.sv'.
SBY 8:04:54 [liveness_ch0] Copy '/home/nota/ice/riscv-formal/cores/icicle/../../checks/rvfi_channel.sv' to 'liveness_ch0/src/rvfi_channel.sv'.
SBY 8:04:54 [insn_addi_ch0] Copy '/home/nota/ice/riscv-formal/cores/icicle/../../insns/insn_addi.v' to 'insn_addi_ch0/src/insn_addi.v'.
SBY 8:04:54 [insn_add_ch0] Copy '/home/nota/ice/riscv-formal/cores/icicle/../../checks/rvfi_channel.sv' to 'insn_add_ch0/src/rvfi_channel.sv'.
SBY 8:04:54 [insn_and_ch0] Copy '/home/nota/ice/riscv-formal/cores/icicle/../../checks/rvfi_channel.sv' to 'insn_and_ch0/src/rvfi_channel.sv'.
SBY 8:04:54 [pc_bwd_ch0] Copy '/home/nota/ice/riscv-formal/cores/icicle/../../checks/rvfi_testbench.sv' to 'pc_bwd_ch0/src/rvfi_testbench.sv'.
SBY 8:04:54 [liveness_ch0] Copy '/home/nota/ice/riscv-formal/cores/icicle/../../checks/rvfi_testbench.sv' to 'liveness_ch0/src/rvfi_testbench.sv'.
SBY 8:04:54 [insn_add_ch0] Copy '/home/nota/ice/riscv-formal/cores/icicle/../../checks/rvfi_testbench.sv' to 'insn_add_ch0/src/rvfi_testbench.sv'.
SBY 8:04:54 [insn_and_ch0] Copy '/home/nota/ice/riscv-formal/cores/icicle/../../checks/rvfi_testbench.sv' to 'insn_and_ch0/src/rvfi_testbench.sv'.
SBY 8:04:54 [pc_bwd_ch0] Copy '/home/nota/ice/riscv-formal/cores/icicle/../../checks/rvfi_pc_bwd_check.sv' to 'pc_bwd_ch0/src/rvfi_pc_bwd_check.sv'.
SBY 8:04:54 [liveness_ch0] Copy '/home/nota/ice/riscv-formal/cores/icicle/../../checks/rvfi_liveness_check.sv' to 'liveness_ch0/src/rvfi_liveness_check.sv'.
SBY 8:04:54 [insn_add_ch0] Copy '/home/nota/ice/riscv-formal/cores/icicle/../../checks/rvfi_insn_check.sv' to 'insn_add_ch0/src/rvfi_insn_check.sv'.
SBY 8:04:54 [insn_and_ch0] Copy '/home/nota/ice/riscv-formal/cores/icicle/../../checks/rvfi_insn_check.sv' to 'insn_and_ch0/src/rvfi_insn_check.sv'.
SBY 8:04:54 [insn_add_ch0] Copy '/home/nota/ice/riscv-formal/cores/icicle/../../insns/insn_add.v' to 'insn_add_ch0/src/insn_add.v'.
SBY 8:04:54 [insn_and_ch0] Copy '/home/nota/ice/riscv-formal/cores/icicle/../../insns/insn_and.v' to 'insn_and_ch0/src/insn_and.v'.
SBY 8:04:54 [reg_ch0] engine_0: smtbmc boolector
SBY 8:04:54 [unique_ch0] engine_0: smtbmc boolector
SBY 8:04:54 [insn_addi_ch0] engine_0: smtbmc boolector
SBY 8:04:54 [pc_fwd_ch0] base: starting process "cd pc_fwd_ch0/src; yosys -ql ../model/design.log ../model/design.ys"
SBY 8:04:54 [pc_bwd_ch0] engine_0: smtbmc boolector
SBY 8:04:54 [liveness_ch0] engine_0: smtbmc boolector
SBY 8:04:54 [insn_add_ch0] engine_0: smtbmc boolector
SBY 8:04:54 [insn_and_ch0] engine_0: smtbmc boolector
SBY 8:04:54 [hang] Copy '/home/nota/ice/riscv-formal/cores/icicle/../../checks/rvfi_macros.vh' to 'hang/src/rvfi_macros.vh'.
SBY 8:04:54 [causal_ch0] base: starting process "cd causal_ch0/src; yosys -ql ../model/design.log ../model/design.ys"
SBY 8:04:54 [ill_ch0] base: starting process "cd ill_ch0/src; yosys -ql ../model/design.log ../model/design.ys"
SBY 8:04:54 [hang] Copy '/home/nota/ice/riscv-formal/cores/icicle/../../checks/rvfi_channel.sv' to 'hang/src/rvfi_channel.sv'.
SBY 8:04:54 [insn_andi_ch0] Writing 'insn_andi_ch0/src/defines.sv'.
SBY 8:04:54 [hang] Copy '/home/nota/ice/riscv-formal/cores/icicle/../../checks/rvfi_testbench.sv' to 'hang/src/rvfi_testbench.sv'.
SBY 8:04:54 [insn_andi_ch0] Writing 'insn_andi_ch0/src/insn_andi_ch0.sv'.
SBY 8:04:54 [insn_andi_ch0] Copy '/home/nota/ice/riscv-formal/cores/icicle/../../checks/rvfi_macros.vh' to 'insn_andi_ch0/src/rvfi_macros.vh'.
SBY 8:04:54 [hang] Copy '/home/nota/ice/riscv-formal/cores/icicle/../../checks/rvfi_hang_check.sv' to 'hang/src/rvfi_hang_check.sv'.
SBY 8:04:54 [insn_andi_ch0] Copy '/home/nota/ice/riscv-formal/cores/icicle/../../checks/rvfi_channel.sv' to 'insn_andi_ch0/src/rvfi_channel.sv'.
SBY 8:04:54 [insn_andi_ch0] Copy '/home/nota/ice/riscv-formal/cores/icicle/../../checks/rvfi_testbench.sv' to 'insn_andi_ch0/src/rvfi_testbench.sv'.
SBY 8:04:54 [insn_andi_ch0] Copy '/home/nota/ice/riscv-formal/cores/icicle/../../checks/rvfi_insn_check.sv' to 'insn_andi_ch0/src/rvfi_insn_check.sv'.
SBY 8:04:54 [insn_addi_ch0] base: starting process "cd insn_addi_ch0/src; yosys -ql ../model/design.log ../model/design.ys"
SBY 8:04:54 [insn_andi_ch0] Copy '/home/nota/ice/riscv-formal/cores/icicle/../../insns/insn_andi.v' to 'insn_andi_ch0/src/insn_andi.v'.
SBY 8:04:54 [reg_ch0] base: starting process "cd reg_ch0/src; yosys -ql ../model/design.log ../model/design.ys"
SBY 8:04:54 [unique_ch0] base: starting process "cd unique_ch0/src; yosys -ql ../model/design.log ../model/design.ys"
SBY 8:04:54 [hang] engine_0: smtbmc boolector
SBY 8:04:54 [pc_bwd_ch0] base: starting process "cd pc_bwd_ch0/src; yosys -ql ../model/design.log ../model/design.ys"
SBY 8:04:54 [liveness_ch0] base: starting process "cd liveness_ch0/src; yosys -ql ../model/design.log ../model/design.ys"
SBY 8:04:54 [insn_add_ch0] base: starting process "cd insn_add_ch0/src; yosys -ql ../model/design.log ../model/design.ys"
SBY 8:04:54 [insn_and_ch0] base: starting process "cd insn_and_ch0/src; yosys -ql ../model/design.log ../model/design.ys"
SBY 8:04:54 [insn_andi_ch0] engine_0: smtbmc boolector
SBY 8:04:54 [hang] base: starting process "cd hang/src; yosys -ql ../model/design.log ../model/design.ys"
SBY 8:04:54 [insn_andi_ch0] base: starting process "cd insn_andi_ch0/src; yosys -ql ../model/design.log ../model/design.ys"
SBY 8:04:54 [pc_fwd_ch0] base: ERROR: Module `rv32_writeback' referenced in module `rv32' in cell `writeback' does not have a port named 'rvfi_ixl'.
SBY 8:04:54 [causal_ch0] base: ERROR: Module `rv32_writeback' referenced in module `rv32' in cell `writeback' does not have a port named 'rvfi_ixl'.
SBY 8:04:54 [ill_ch0] base: ERROR: Module `rv32_writeback' referenced in module `rv32' in cell `writeback' does not have a port named 'rvfi_ixl'.
SBY 8:04:54 [unique_ch0] base: ERROR: Module `rv32_writeback' referenced in module `rv32' in cell `writeback' does not have a port named 'rvfi_ixl'.
SBY 8:04:54 [liveness_ch0] base: ERROR: Module `rv32_writeback' referenced in module `rv32' in cell `writeback' does not have a port named 'rvfi_ixl'.
SBY 8:04:54 [hang] base: ERROR: Module `rv32_writeback' referenced in module `rv32' in cell `writeback' does not have a port named 'rvfi_ixl'.
SBY 8:04:54 [reg_ch0] base: ERROR: Module `rv32_writeback' referenced in module `rv32' in cell `writeback' does not have a port named 'rvfi_ixl'.
SBY 8:04:54 [pc_bwd_ch0] base: ERROR: Module `rv32_writeback' referenced in module `rv32' in cell `writeback' does not have a port named 'rvfi_ixl'.
SBY 8:04:54 [insn_andi_ch0] base: ERROR: Module `rv32_writeback' referenced in module `rv32' in cell `writeback' does not have a port named 'rvfi_ixl'.
SBY 8:04:54 [insn_and_ch0] base: ERROR: Module `rv32_writeback' referenced in module `rv32' in cell `writeback' does not have a port named 'rvfi_ixl'.
SBY 8:04:54 [insn_addi_ch0] base: ERROR: Module `rv32_writeback' referenced in module `rv32' in cell `writeback' does not have a port named 'rvfi_ixl'.
SBY 8:04:54 [insn_add_ch0] base: ERROR: Module `rv32_writeback' referenced in module `rv32' in cell `writeback' does not have a port named 'rvfi_ixl'.
SBY 8:04:54 [causal_ch0] base: finished (returncode=1)
SBY 8:04:54 [pc_fwd_ch0] base: finished (returncode=1)
SBY 8:04:54 [causal_ch0] base: job failed. ERROR.
SBY 8:04:54 [pc_fwd_ch0] base: job failed. ERROR.
SBY 8:04:54 [causal_ch0] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 8:04:54 [pc_fwd_ch0] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 8:04:54 [pc_fwd_ch0] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 8:04:54 [causal_ch0] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 8:04:54 [causal_ch0] DONE (ERROR, rc=16)
SBY 8:04:54 [pc_fwd_ch0] DONE (ERROR, rc=16)
SBY 8:04:54 [ill_ch0] base: finished (returncode=1)
SBY 8:04:54 [ill_ch0] base: job failed. ERROR.
SBY 8:04:54 [unique_ch0] base: finished (returncode=1)
SBY 8:04:54 [unique_ch0] base: job failed. ERROR.
SBY 8:04:54 [ill_ch0] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 8:04:54 [ill_ch0] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 8:04:54 [unique_ch0] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 8:04:54 [unique_ch0] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 8:04:54 [liveness_ch0] base: finished (returncode=1)
SBY 8:04:54 [liveness_ch0] base: job failed. ERROR.
SBY 8:04:54 [ill_ch0] DONE (ERROR, rc=16)
SBY 8:04:54 [liveness_ch0] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 8:04:54 [liveness_ch0] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 8:04:54 [unique_ch0] DONE (ERROR, rc=16)
SBY 8:04:54 [reg_ch0] base: finished (returncode=1)
SBY 8:04:54 [hang] base: finished (returncode=1)
SBY 8:04:54 [reg_ch0] base: job failed. ERROR.
SBY 8:04:54 [hang] base: job failed. ERROR.
SBY 8:04:54 [liveness_ch0] DONE (ERROR, rc=16)
SBY 8:04:54 [pc_bwd_ch0] base: finished (returncode=1)
SBY 8:04:54 [reg_ch0] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 8:04:54 [hang] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 8:04:54 [reg_ch0] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 8:04:54 [pc_bwd_ch0] base: job failed. ERROR.
SBY 8:04:54 [hang] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 8:04:54 [insn_addi_ch0] base: finished (returncode=1)
SBY 8:04:54 [pc_bwd_ch0] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 8:04:54 [insn_and_ch0] base: finished (returncode=1)
SBY 8:04:54 [insn_addi_ch0] base: job failed. ERROR.
SBY 8:04:54 [insn_andi_ch0] base: finished (returncode=1)
SBY 8:04:54 [pc_bwd_ch0] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 8:04:54 [reg_ch0] DONE (ERROR, rc=16)
SBY 8:04:54 [insn_and_ch0] base: job failed. ERROR.
SBY 8:04:54 [insn_andi_ch0] base: job failed. ERROR.
SBY 8:04:54 [insn_addi_ch0] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 8:04:54 [hang] DONE (ERROR, rc=16)
SBY 8:04:54 [insn_addi_ch0] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 8:04:54 [insn_and_ch0] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 8:04:54 [insn_andi_ch0] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 8:04:54 [insn_and_ch0] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 8:04:54 [insn_andi_ch0] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 8:04:54 [pc_bwd_ch0] DONE (ERROR, rc=16)
SBY 8:04:54 [insn_addi_ch0] DONE (ERROR, rc=16)
SBY 8:04:54 [insn_and_ch0] DONE (ERROR, rc=16)
SBY 8:04:54 [insn_andi_ch0] DONE (ERROR, rc=16)
SBY 8:04:54 [insn_add_ch0] base: finished (returncode=1)
SBY 8:04:54 [insn_add_ch0] base: job failed. ERROR.
SBY 8:04:54 [insn_add_ch0] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 8:04:54 [insn_add_ch0] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 8:04:54 [insn_add_ch0] DONE (ERROR, rc=16)
make: *** [makefile:24: pc_fwd_ch0/status] Error 16
make: *** Waiting for unfinished jobs....
make: *** [makefile:4: causal_ch0/status] Error 16
make: *** [makefile:8: hang/status] Error 16
make: *** [makefile:32: unique_ch0/status] Error 16
make: *** [makefile:20: pc_bwd_ch0/status] Error 16
make: *** [makefile:40: insn_addi_ch0/status] Error 16
make: *** [makefile:48: insn_andi_ch0/status] Error 16
make: *** [makefile:12: ill_ch0/status] Error 16
make: *** [makefile:44: insn_and_ch0/status] Error 16
make: *** [makefile:16: liveness_ch0/status] Error 16
make: *** [makefile:28: reg_ch0/status] Error 16
make: *** [makefile:36: insn_add_ch0/status] Error 16
make: Leaving directory '/home/nota/ice/riscv-formal/cores/icicle/checks'
I think rvfi_ixl is a new field introduced to riscv-formal (relatively) recently.
Does adding rvfi_ixl <= 1; to the writeback module fix it?
