Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Formal verfication failing #13

Open
Applepi opened this issue Dec 3, 2019 · 1 comment
Open

Formal verfication failing #13

Applepi opened this issue Dec 3, 2019 · 1 comment

Comments

@Applepi
Copy link

Applepi commented Dec 3, 2019

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'
@grahamedgecombe
Copy link
Owner

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?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@grahamedgecombe @Applepi