make: Entering directory '/home/dsleung/riscv-formal/cores/picorv32/checks'
sby reg_ch0.sby
sby causal_ch0.sby
sby cover.sby
sby csrw_mcycle_ch0.sby
sby csrw_minstret_ch0.sby
sby liveness_ch0.sby
sby pc_bwd_ch0.sby
sby pc_fwd_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 insn_auipc_ch0.sby
sby insn_beq_ch0.sby
sby insn_bge_ch0.sby
SBY 15:54:17 [pc_fwd_ch0] Writing 'pc_fwd_ch0/src/defines.sv'.
SBY 15:54:17 [cover] Writing 'cover/src/defines.sv'.
SBY 15:54:17 [csrw_minstret_ch0] Writing 'csrw_minstret_ch0/src/defines.sv'.
SBY 15:54:17 [cover] Writing 'cover/src/cover.sv'.
SBY 15:54:17 [csrw_minstret_ch0] Writing 'csrw_minstret_ch0/src/csrw_minstret_ch0.sv'.
SBY 15:54:17 [pc_fwd_ch0] Writing 'pc_fwd_ch0/src/pc_fwd_ch0.sv'.
SBY 15:54:17 [csrw_minstret_ch0] Copy '/home/dsleung/riscv-formal/cores/picorv32/../../checks/rvfi_macros.vh' to 'csrw_minstret_ch0/src/rvfi_macros.vh'.
SBY 15:54:17 [cover] Writing 'cover/src/cover_stmts.vh'.
SBY 15:54:17 [csrw_mcycle_ch0] Writing 'csrw_mcycle_ch0/src/defines.sv'.
SBY 15:54:17 [pc_fwd_ch0] Copy '/home/dsleung/riscv-formal/cores/picorv32/../../checks/rvfi_macros.vh' to 'pc_fwd_ch0/src/rvfi_macros.vh'.
SBY 15:54:17 [cover] Copy '/home/dsleung/riscv-formal/cores/picorv32/../../checks/rvfi_macros.vh' to 'cover/src/rvfi_macros.vh'.
SBY 15:54:17 [csrw_mcycle_ch0] Writing 'csrw_mcycle_ch0/src/csrw_mcycle_ch0.sv'.
SBY 15:54:17 [csrw_minstret_ch0] Copy '/home/dsleung/riscv-formal/cores/picorv32/../../checks/rvfi_channel.sv' to 'csrw_minstret_ch0/src/rvfi_channel.sv'.
SBY 15:54:17 [pc_fwd_ch0] Copy '/home/dsleung/riscv-formal/cores/picorv32/../../checks/rvfi_channel.sv' to 'pc_fwd_ch0/src/rvfi_channel.sv'.
SBY 15:54:17 [cover] Copy '/home/dsleung/riscv-formal/cores/picorv32/../../checks/rvfi_channel.sv' to 'cover/src/rvfi_channel.sv'.
SBY 15:54:17 [csrw_mcycle_ch0] Copy '/home/dsleung/riscv-formal/cores/picorv32/../../checks/rvfi_macros.vh' to 'csrw_mcycle_ch0/src/rvfi_macros.vh'.
SBY 15:54:17 [pc_fwd_ch0] Copy '/home/dsleung/riscv-formal/cores/picorv32/../../checks/rvfi_testbench.sv' to 'pc_fwd_ch0/src/rvfi_testbench.sv'.
SBY 15:54:17 [csrw_minstret_ch0] Copy '/home/dsleung/riscv-formal/cores/picorv32/../../checks/rvfi_testbench.sv' to 'csrw_minstret_ch0/src/rvfi_testbench.sv'.
SBY 15:54:17 [cover] Copy '/home/dsleung/riscv-formal/cores/picorv32/../../checks/rvfi_testbench.sv' to 'cover/src/rvfi_testbench.sv'.
SBY 15:54:17 [csrw_mcycle_ch0] Copy '/home/dsleung/riscv-formal/cores/picorv32/../../checks/rvfi_channel.sv' to 'csrw_mcycle_ch0/src/rvfi_channel.sv'.
SBY 15:54:17 [pc_fwd_ch0] Copy '/home/dsleung/riscv-formal/cores/picorv32/../../checks/rvfi_pc_fwd_check.sv' to 'pc_fwd_ch0/src/rvfi_pc_fwd_check.sv'.
SBY 15:54:17 [csrw_minstret_ch0] Copy '/home/dsleung/riscv-formal/cores/picorv32/../../checks/rvfi_csrw_check.sv' to 'csrw_minstret_ch0/src/rvfi_csrw_check.sv'.
SBY 15:54:17 [csrw_mcycle_ch0] Copy '/home/dsleung/riscv-formal/cores/picorv32/../../checks/rvfi_testbench.sv' to 'csrw_mcycle_ch0/src/rvfi_testbench.sv'.
SBY 15:54:17 [cover] Copy '/home/dsleung/riscv-formal/cores/picorv32/../../checks/rvfi_cover_check.sv' to 'cover/src/rvfi_cover_check.sv'.
SBY 15:54:17 [csrw_mcycle_ch0] Copy '/home/dsleung/riscv-formal/cores/picorv32/../../checks/rvfi_csrw_check.sv' to 'csrw_mcycle_ch0/src/rvfi_csrw_check.sv'.
SBY 15:54:17 [pc_bwd_ch0] Writing 'pc_bwd_ch0/src/defines.sv'.
SBY 15:54:17 [pc_bwd_ch0] Writing 'pc_bwd_ch0/src/pc_bwd_ch0.sv'.
SBY 15:54:17 [pc_bwd_ch0] Copy '/home/dsleung/riscv-formal/cores/picorv32/../../checks/rvfi_macros.vh' to 'pc_bwd_ch0/src/rvfi_macros.vh'.
SBY 15:54:17 [liveness_ch0] Writing 'liveness_ch0/src/defines.sv'.
SBY 15:54:17 [pc_bwd_ch0] Copy '/home/dsleung/riscv-formal/cores/picorv32/../../checks/rvfi_channel.sv' to 'pc_bwd_ch0/src/rvfi_channel.sv'.
SBY 15:54:17 [reg_ch0] Writing 'reg_ch0/src/defines.sv'.
SBY 15:54:17 [pc_bwd_ch0] Copy '/home/dsleung/riscv-formal/cores/picorv32/../../checks/rvfi_testbench.sv' to 'pc_bwd_ch0/src/rvfi_testbench.sv'.
SBY 15:54:17 [liveness_ch0] Writing 'liveness_ch0/src/liveness_ch0.sv'.
SBY 15:54:17 [reg_ch0] Writing 'reg_ch0/src/reg_ch0.sv'.
SBY 15:54:17 [pc_bwd_ch0] Copy '/home/dsleung/riscv-formal/cores/picorv32/../../checks/rvfi_pc_bwd_check.sv' to 'pc_bwd_ch0/src/rvfi_pc_bwd_check.sv'.
SBY 15:54:17 [reg_ch0] Copy '/home/dsleung/riscv-formal/cores/picorv32/../../checks/rvfi_macros.vh' to 'reg_ch0/src/rvfi_macros.vh'.
SBY 15:54:17 [liveness_ch0] Copy '/home/dsleung/riscv-formal/cores/picorv32/../../checks/rvfi_macros.vh' to 'liveness_ch0/src/rvfi_macros.vh'.
SBY 15:54:17 [reg_ch0] Copy '/home/dsleung/riscv-formal/cores/picorv32/../../checks/rvfi_channel.sv' to 'reg_ch0/src/rvfi_channel.sv'.
SBY 15:54:17 [causal_ch0] Writing 'causal_ch0/src/defines.sv'.
SBY 15:54:17 [csrw_minstret_ch0] engine_0: smtbmc boolector
SBY 15:54:17 [pc_fwd_ch0] engine_0: smtbmc boolector
SBY 15:54:17 [reg_ch0] Copy '/home/dsleung/riscv-formal/cores/picorv32/../../checks/rvfi_testbench.sv' to 'reg_ch0/src/rvfi_testbench.sv'.
SBY 15:54:17 [causal_ch0] Writing 'causal_ch0/src/causal_ch0.sv'.
SBY 15:54:17 [csrw_mcycle_ch0] engine_0: smtbmc boolector
SBY 15:54:17 [cover] engine_0: smtbmc boolector
SBY 15:54:17 [liveness_ch0] Copy '/home/dsleung/riscv-formal/cores/picorv32/../../checks/rvfi_channel.sv' to 'liveness_ch0/src/rvfi_channel.sv'.
SBY 15:54:17 [reg_ch0] Copy '/home/dsleung/riscv-formal/cores/picorv32/../../checks/rvfi_reg_check.sv' to 'reg_ch0/src/rvfi_reg_check.sv'.
SBY 15:54:17 [causal_ch0] Copy '/home/dsleung/riscv-formal/cores/picorv32/../../checks/rvfi_macros.vh' to 'causal_ch0/src/rvfi_macros.vh'.
SBY 15:54:17 [liveness_ch0] Copy '/home/dsleung/riscv-formal/cores/picorv32/../../checks/rvfi_testbench.sv' to 'liveness_ch0/src/rvfi_testbench.sv'.
SBY 15:54:17 [causal_ch0] Copy '/home/dsleung/riscv-formal/cores/picorv32/../../checks/rvfi_channel.sv' to 'causal_ch0/src/rvfi_channel.sv'.
SBY 15:54:17 [liveness_ch0] Copy '/home/dsleung/riscv-formal/cores/picorv32/../../checks/rvfi_liveness_check.sv' to 'liveness_ch0/src/rvfi_liveness_check.sv'.
SBY 15:54:17 [causal_ch0] Copy '/home/dsleung/riscv-formal/cores/picorv32/../../checks/rvfi_testbench.sv' to 'causal_ch0/src/rvfi_testbench.sv'.
SBY 15:54:17 [causal_ch0] Copy '/home/dsleung/riscv-formal/cores/picorv32/../../checks/rvfi_causal_check.sv' to 'causal_ch0/src/rvfi_causal_check.sv'.
SBY 15:54:17 [pc_bwd_ch0] engine_0: smtbmc boolector
SBY 15:54:17 [reg_ch0] engine_0: smtbmc boolector
SBY 15:54:17 [liveness_ch0] engine_0: smtbmc boolector
SBY 15:54:17 [causal_ch0] engine_0: smtbmc boolector
SBY 15:54:17 [insn_addi_ch0] Writing 'insn_addi_ch0/src/defines.sv'.
SBY 15:54:17 [insn_add_ch0] Writing 'insn_add_ch0/src/defines.sv'.
SBY 15:54:17 [insn_addi_ch0] Writing 'insn_addi_ch0/src/insn_addi_ch0.sv'.
SBY 15:54:17 [insn_add_ch0] Writing 'insn_add_ch0/src/insn_add_ch0.sv'.
SBY 15:54:17 [unique_ch0] Writing 'unique_ch0/src/defines.sv'.
SBY 15:54:17 [insn_addi_ch0] Copy '/home/dsleung/riscv-formal/cores/picorv32/../../checks/rvfi_macros.vh' to 'insn_addi_ch0/src/rvfi_macros.vh'.
SBY 15:54:17 [insn_add_ch0] Copy '/home/dsleung/riscv-formal/cores/picorv32/../../checks/rvfi_macros.vh' to 'insn_add_ch0/src/rvfi_macros.vh'.
SBY 15:54:17 [csrw_minstret_ch0] base: starting process "cd csrw_minstret_ch0/src; yosys -ql ../model/design.log ../model/design.ys"
SBY 15:54:17 [unique_ch0] Writing 'unique_ch0/src/unique_ch0.sv'.
SBY 15:54:17 [pc_fwd_ch0] base: starting process "cd pc_fwd_ch0/src; yosys -ql ../model/design.log ../model/design.ys"
SBY 15:54:17 [insn_addi_ch0] Copy '/home/dsleung/riscv-formal/cores/picorv32/../../checks/rvfi_channel.sv' to 'insn_addi_ch0/src/rvfi_channel.sv'.
SBY 15:54:17 [unique_ch0] Copy '/home/dsleung/riscv-formal/cores/picorv32/../../checks/rvfi_macros.vh' to 'unique_ch0/src/rvfi_macros.vh'.
SBY 15:54:17 [csrw_mcycle_ch0] base: starting process "cd csrw_mcycle_ch0/src; yosys -ql ../model/design.log ../model/design.ys"
SBY 15:54:17 [insn_add_ch0] Copy '/home/dsleung/riscv-formal/cores/picorv32/../../checks/rvfi_channel.sv' to 'insn_add_ch0/src/rvfi_channel.sv'.
SBY 15:54:17 [insn_addi_ch0] Copy '/home/dsleung/riscv-formal/cores/picorv32/../../checks/rvfi_testbench.sv' to 'insn_addi_ch0/src/rvfi_testbench.sv'.
SBY 15:54:17 [unique_ch0] Copy '/home/dsleung/riscv-formal/cores/picorv32/../../checks/rvfi_channel.sv' to 'unique_ch0/src/rvfi_channel.sv'.
SBY 15:54:17 [insn_add_ch0] Copy '/home/dsleung/riscv-formal/cores/picorv32/../../checks/rvfi_testbench.sv' to 'insn_add_ch0/src/rvfi_testbench.sv'.
SBY 15:54:17 [unique_ch0] Copy '/home/dsleung/riscv-formal/cores/picorv32/../../checks/rvfi_testbench.sv' to 'unique_ch0/src/rvfi_testbench.sv'.
SBY 15:54:17 [insn_addi_ch0] Copy '/home/dsleung/riscv-formal/cores/picorv32/../../checks/rvfi_insn_check.sv' to 'insn_addi_ch0/src/rvfi_insn_check.sv'.
SBY 15:54:17 [insn_add_ch0] Copy '/home/dsleung/riscv-formal/cores/picorv32/../../checks/rvfi_insn_check.sv' to 'insn_add_ch0/src/rvfi_insn_check.sv'.
SBY 15:54:17 [insn_addi_ch0] Copy '/home/dsleung/riscv-formal/cores/picorv32/../../insns/insn_addi.v' to 'insn_addi_ch0/src/insn_addi.v'.
SBY 15:54:17 [insn_add_ch0] Copy '/home/dsleung/riscv-formal/cores/picorv32/../../insns/insn_add.v' to 'insn_add_ch0/src/insn_add.v'.
SBY 15:54:17 [unique_ch0] Copy '/home/dsleung/riscv-formal/cores/picorv32/../../checks/rvfi_unique_check.sv' to 'unique_ch0/src/rvfi_unique_check.sv'.
SBY 15:54:17 [cover] base: starting process "cd cover/src; yosys -ql ../model/design.log ../model/design.ys"
SBY 15:54:17 [pc_bwd_ch0] base: starting process "cd pc_bwd_ch0/src; yosys -ql ../model/design.log ../model/design.ys"
SBY 15:54:17 [reg_ch0] base: starting process "cd reg_ch0/src; yosys -ql ../model/design.log ../model/design.ys"
SBY 15:54:17 [liveness_ch0] base: starting process "cd liveness_ch0/src; yosys -ql ../model/design.log ../model/design.ys"
SBY 15:54:17 [insn_addi_ch0] engine_0: smtbmc boolector
SBY 15:54:17 [insn_add_ch0] engine_0: smtbmc boolector
SBY 15:54:17 [causal_ch0] base: starting process "cd causal_ch0/src; yosys -ql ../model/design.log ../model/design.ys"
SBY 15:54:17 [unique_ch0] engine_0: smtbmc boolector
SBY 15:54:17 [insn_addi_ch0] base: starting process "cd insn_addi_ch0/src; yosys -ql ../model/design.log ../model/design.ys"
SBY 15:54:17 [insn_add_ch0] base: starting process "cd insn_add_ch0/src; yosys -ql ../model/design.log ../model/design.ys"
SBY 15:54:17 [insn_and_ch0] Writing 'insn_and_ch0/src/defines.sv'.
SBY 15:54:17 [unique_ch0] base: starting process "cd unique_ch0/src; yosys -ql ../model/design.log ../model/design.ys"
SBY 15:54:17 [insn_and_ch0] Writing 'insn_and_ch0/src/insn_and_ch0.sv'.
SBY 15:54:17 [insn_and_ch0] Copy '/home/dsleung/riscv-formal/cores/picorv32/../../checks/rvfi_macros.vh' to 'insn_and_ch0/src/rvfi_macros.vh'.
SBY 15:54:17 [insn_and_ch0] Copy '/home/dsleung/riscv-formal/cores/picorv32/../../checks/rvfi_channel.sv' to 'insn_and_ch0/src/rvfi_channel.sv'.
SBY 15:54:17 [insn_and_ch0] Copy '/home/dsleung/riscv-formal/cores/picorv32/../../checks/rvfi_testbench.sv' to 'insn_and_ch0/src/rvfi_testbench.sv'.
SBY 15:54:17 [insn_and_ch0] Copy '/home/dsleung/riscv-formal/cores/picorv32/../../checks/rvfi_insn_check.sv' to 'insn_and_ch0/src/rvfi_insn_check.sv'.
SBY 15:54:17 [insn_bge_ch0] Writing 'insn_bge_ch0/src/defines.sv'.
SBY 15:54:17 [insn_and_ch0] Copy '/home/dsleung/riscv-formal/cores/picorv32/../../insns/insn_and.v' to 'insn_and_ch0/src/insn_and.v'.
SBY 15:54:17 [insn_bge_ch0] Writing 'insn_bge_ch0/src/insn_bge_ch0.sv'.
SBY 15:54:17 [insn_beq_ch0] Writing 'insn_beq_ch0/src/defines.sv'.
SBY 15:54:17 [insn_bge_ch0] Copy '/home/dsleung/riscv-formal/cores/picorv32/../../checks/rvfi_macros.vh' to 'insn_bge_ch0/src/rvfi_macros.vh'.
SBY 15:54:17 [insn_beq_ch0] Writing 'insn_beq_ch0/src/insn_beq_ch0.sv'.
SBY 15:54:17 [insn_andi_ch0] Writing 'insn_andi_ch0/src/defines.sv'.
SBY 15:54:17 [insn_beq_ch0] Copy '/home/dsleung/riscv-formal/cores/picorv32/../../checks/rvfi_macros.vh' to 'insn_beq_ch0/src/rvfi_macros.vh'.
SBY 15:54:17 [insn_bge_ch0] Copy '/home/dsleung/riscv-formal/cores/picorv32/../../checks/rvfi_channel.sv' to 'insn_bge_ch0/src/rvfi_channel.sv'.
SBY 15:54:17 [insn_andi_ch0] Writing 'insn_andi_ch0/src/insn_andi_ch0.sv'.
SBY 15:54:17 [insn_andi_ch0] Copy '/home/dsleung/riscv-formal/cores/picorv32/../../checks/rvfi_macros.vh' to 'insn_andi_ch0/src/rvfi_macros.vh'.
SBY 15:54:17 [insn_beq_ch0] Copy '/home/dsleung/riscv-formal/cores/picorv32/../../checks/rvfi_channel.sv' to 'insn_beq_ch0/src/rvfi_channel.sv'.
SBY 15:54:17 [insn_bge_ch0] Copy '/home/dsleung/riscv-formal/cores/picorv32/../../checks/rvfi_testbench.sv' to 'insn_bge_ch0/src/rvfi_testbench.sv'.
SBY 15:54:17 [insn_beq_ch0] Copy '/home/dsleung/riscv-formal/cores/picorv32/../../checks/rvfi_testbench.sv' to 'insn_beq_ch0/src/rvfi_testbench.sv'.
SBY 15:54:17 [insn_bge_ch0] Copy '/home/dsleung/riscv-formal/cores/picorv32/../../checks/rvfi_insn_check.sv' to 'insn_bge_ch0/src/rvfi_insn_check.sv'.
SBY 15:54:17 [insn_andi_ch0] Copy '/home/dsleung/riscv-formal/cores/picorv32/../../checks/rvfi_channel.sv' to 'insn_andi_ch0/src/rvfi_channel.sv'.
SBY 15:54:17 [insn_andi_ch0] Copy '/home/dsleung/riscv-formal/cores/picorv32/../../checks/rvfi_testbench.sv' to 'insn_andi_ch0/src/rvfi_testbench.sv'.
SBY 15:54:17 [insn_bge_ch0] Copy '/home/dsleung/riscv-formal/cores/picorv32/../../insns/insn_bge.v' to 'insn_bge_ch0/src/insn_bge.v'.
SBY 15:54:17 [insn_beq_ch0] Copy '/home/dsleung/riscv-formal/cores/picorv32/../../checks/rvfi_insn_check.sv' to 'insn_beq_ch0/src/rvfi_insn_check.sv'.
SBY 15:54:17 [insn_andi_ch0] Copy '/home/dsleung/riscv-formal/cores/picorv32/../../checks/rvfi_insn_check.sv' to 'insn_andi_ch0/src/rvfi_insn_check.sv'.
SBY 15:54:17 [insn_beq_ch0] Copy '/home/dsleung/riscv-formal/cores/picorv32/../../insns/insn_beq.v' to 'insn_beq_ch0/src/insn_beq.v'.
SBY 15:54:17 [insn_andi_ch0] Copy '/home/dsleung/riscv-formal/cores/picorv32/../../insns/insn_andi.v' to 'insn_andi_ch0/src/insn_andi.v'.
SBY 15:54:17 [insn_and_ch0] engine_0: smtbmc boolector
SBY 15:54:17 [insn_bge_ch0] engine_0: smtbmc boolector
SBY 15:54:17 [insn_beq_ch0] engine_0: smtbmc boolector
SBY 15:54:17 [insn_andi_ch0] engine_0: smtbmc boolector
SBY 15:54:17 [insn_auipc_ch0] Writing 'insn_auipc_ch0/src/defines.sv'.
SBY 15:54:17 [insn_auipc_ch0] Writing 'insn_auipc_ch0/src/insn_auipc_ch0.sv'.
SBY 15:54:17 [insn_auipc_ch0] Copy '/home/dsleung/riscv-formal/cores/picorv32/../../checks/rvfi_macros.vh' to 'insn_auipc_ch0/src/rvfi_macros.vh'.
SBY 15:54:17 [insn_auipc_ch0] Copy '/home/dsleung/riscv-formal/cores/picorv32/../../checks/rvfi_channel.sv' to 'insn_auipc_ch0/src/rvfi_channel.sv'.
SBY 15:54:17 [insn_and_ch0] base: starting process "cd insn_and_ch0/src; yosys -ql ../model/design.log ../model/design.ys"
SBY 15:54:17 [insn_auipc_ch0] Copy '/home/dsleung/riscv-formal/cores/picorv32/../../checks/rvfi_testbench.sv' to 'insn_auipc_ch0/src/rvfi_testbench.sv'.
SBY 15:54:17 [insn_auipc_ch0] Copy '/home/dsleung/riscv-formal/cores/picorv32/../../checks/rvfi_insn_check.sv' to 'insn_auipc_ch0/src/rvfi_insn_check.sv'.
SBY 15:54:17 [insn_auipc_ch0] Copy '/home/dsleung/riscv-formal/cores/picorv32/../../insns/insn_auipc.v' to 'insn_auipc_ch0/src/insn_auipc.v'.
SBY 15:54:17 [insn_auipc_ch0] engine_0: smtbmc boolector
SBY 15:54:17 [insn_bge_ch0] base: starting process "cd insn_bge_ch0/src; yosys -ql ../model/design.log ../model/design.ys"
SBY 15:54:17 [insn_beq_ch0] base: starting process "cd insn_beq_ch0/src; yosys -ql ../model/design.log ../model/design.ys"
SBY 15:54:17 [insn_andi_ch0] base: starting process "cd insn_andi_ch0/src; yosys -ql ../model/design.log ../model/design.ys"
SBY 15:54:17 [insn_auipc_ch0] base: starting process "cd insn_auipc_ch0/src; yosys -ql ../model/design.log ../model/design.ys"
SBY 15:54:21 [cover] base: finished (returncode=0)
SBY 15:54:21 [cover] smt2: starting process "cd cover/model; yosys -ql design_smt2.log design_smt2.ys"
SBY 15:54:21 [unique_ch0] base: finished (returncode=0)
SBY 15:54:21 [unique_ch0] smt2: starting process "cd unique_ch0/model; yosys -ql design_smt2.log design_smt2.ys"
SBY 15:54:21 [pc_bwd_ch0] base: finished (returncode=0)
SBY 15:54:21 [pc_bwd_ch0] smt2: starting process "cd pc_bwd_ch0/model; yosys -ql design_smt2.log design_smt2.ys"
SBY 15:54:21 [cover] smt2: finished (returncode=0)
SBY 15:54:21 [cover] engine_0: starting process "cd cover; yosys-smtbmc -s boolector --presat --unroll -c --noprogress -t 15:16 --append 0 --dump-vcd engine_0/trace%.vcd --dump-vlogtb engine_0/trace%_tb.v --dump-smtc engine_0/trace%.smtc model/design_smt2.smt2"
SBY 15:54:21 [insn_addi_ch0] base: finished (returncode=0)
SBY 15:54:21 [insn_addi_ch0] smt2: starting process "cd insn_addi_ch0/model; yosys -ql design_smt2.log design_smt2.ys"
SBY 15:54:21 [reg_ch0] base: finished (returncode=0)
SBY 15:54:21 [reg_ch0] smt2: starting process "cd reg_ch0/model; yosys -ql design_smt2.log design_smt2.ys"
SBY 15:54:21 [cover] engine_0: ##   0:00:00  Solver: boolector
SBY 15:54:21 [pc_fwd_ch0] base: finished (returncode=0)
SBY 15:54:21 [pc_fwd_ch0] smt2: starting process "cd pc_fwd_ch0/model; yosys -ql design_smt2.log design_smt2.ys"
SBY 15:54:21 [insn_auipc_ch0] base: finished (returncode=0)
SBY 15:54:21 [insn_auipc_ch0] smt2: starting process "cd insn_auipc_ch0/model; yosys -ql design_smt2.log design_smt2.ys"
SBY 15:54:21 [insn_add_ch0] base: finished (returncode=0)
SBY 15:54:21 [insn_add_ch0] smt2: starting process "cd insn_add_ch0/model; yosys -ql design_smt2.log design_smt2.ys"
SBY 15:54:21 [insn_andi_ch0] base: finished (returncode=0)
SBY 15:54:21 [insn_andi_ch0] smt2: starting process "cd insn_andi_ch0/model; yosys -ql design_smt2.log design_smt2.ys"
SBY 15:54:21 [insn_bge_ch0] base: finished (returncode=0)
SBY 15:54:21 [insn_bge_ch0] smt2: starting process "cd insn_bge_ch0/model; yosys -ql design_smt2.log design_smt2.ys"
SBY 15:54:21 [liveness_ch0] base: finished (returncode=0)
SBY 15:54:21 [liveness_ch0] smt2: starting process "cd liveness_ch0/model; yosys -ql design_smt2.log design_smt2.ys"
SBY 15:54:21 [insn_and_ch0] base: finished (returncode=0)
SBY 15:54:21 [insn_and_ch0] smt2: starting process "cd insn_and_ch0/model; yosys -ql design_smt2.log design_smt2.ys"
SBY 15:54:21 [causal_ch0] base: finished (returncode=0)
SBY 15:54:21 [causal_ch0] smt2: starting process "cd causal_ch0/model; yosys -ql design_smt2.log design_smt2.ys"
SBY 15:54:21 [insn_beq_ch0] base: finished (returncode=0)
SBY 15:54:21 [insn_beq_ch0] smt2: starting process "cd insn_beq_ch0/model; yosys -ql design_smt2.log design_smt2.ys"
SBY 15:54:21 [pc_bwd_ch0] smt2: finished (returncode=0)
SBY 15:54:21 [pc_bwd_ch0] engine_0: starting process "cd pc_bwd_ch0; yosys-smtbmc -s boolector --presat --unroll --noprogress -t 30:31 --append 0 --dump-vcd engine_0/trace.vcd --dump-vlogtb engine_0/trace_tb.v --dump-smtc engine_0/trace.smtc model/design_smt2.smt2"
SBY 15:54:21 [unique_ch0] smt2: finished (returncode=0)
SBY 15:54:21 [unique_ch0] engine_0: starting process "cd unique_ch0; yosys-smtbmc -s boolector --presat --unroll --noprogress -t 30:31 --append 0 --dump-vcd engine_0/trace.vcd --dump-vlogtb engine_0/trace_tb.v --dump-smtc engine_0/trace.smtc model/design_smt2.smt2"
SBY 15:54:21 [csrw_minstret_ch0] base: finished (returncode=0)
SBY 15:54:21 [csrw_minstret_ch0] smt2: starting process "cd csrw_minstret_ch0/model; yosys -ql design_smt2.log design_smt2.ys"
SBY 15:54:21 [csrw_mcycle_ch0] base: finished (returncode=0)
SBY 15:54:21 [csrw_mcycle_ch0] smt2: starting process "cd csrw_mcycle_ch0/model; yosys -ql design_smt2.log design_smt2.ys"
SBY 15:54:21 [reg_ch0] smt2: finished (returncode=0)
SBY 15:54:21 [reg_ch0] engine_0: starting process "cd reg_ch0; yosys-smtbmc -s boolector --presat --unroll --noprogress -t 25:26 --append 0 --dump-vcd engine_0/trace.vcd --dump-vlogtb engine_0/trace_tb.v --dump-smtc engine_0/trace.smtc model/design_smt2.smt2"
SBY 15:54:21 [insn_addi_ch0] smt2: finished (returncode=0)
SBY 15:54:21 [insn_addi_ch0] engine_0: starting process "cd insn_addi_ch0; yosys-smtbmc -s boolector --presat --unroll --noprogress -t 20:21 --append 0 --dump-vcd engine_0/trace.vcd --dump-vlogtb engine_0/trace_tb.v --dump-smtc engine_0/trace.smtc model/design_smt2.smt2"
SBY 15:54:21 [pc_bwd_ch0] engine_0: ##   0:00:00  Solver: boolector
SBY 15:54:21 [unique_ch0] engine_0: ##   0:00:00  Solver: boolector
SBY 15:54:21 [pc_fwd_ch0] smt2: finished (returncode=0)
SBY 15:54:21 [pc_fwd_ch0] engine_0: starting process "cd pc_fwd_ch0; yosys-smtbmc -s boolector --presat --unroll --noprogress -t 30:31 --append 0 --dump-vcd engine_0/trace.vcd --dump-vlogtb engine_0/trace_tb.v --dump-smtc engine_0/trace.smtc model/design_smt2.smt2"
SBY 15:54:21 [insn_auipc_ch0] smt2: finished (returncode=0)
SBY 15:54:21 [insn_auipc_ch0] engine_0: starting process "cd insn_auipc_ch0; yosys-smtbmc -s boolector --presat --unroll --noprogress -t 20:21 --append 0 --dump-vcd engine_0/trace.vcd --dump-vlogtb engine_0/trace_tb.v --dump-smtc engine_0/trace.smtc model/design_smt2.smt2"
SBY 15:54:21 [cover] engine_0: ##   0:00:00  Checking cover reachability in step 0..
SBY 15:54:21 [reg_ch0] engine_0: ##   0:00:00  Solver: boolector
SBY 15:54:21 [insn_addi_ch0] engine_0: ##   0:00:00  Solver: boolector
SBY 15:54:21 [insn_add_ch0] smt2: finished (returncode=0)
SBY 15:54:21 [insn_add_ch0] engine_0: starting process "cd insn_add_ch0; yosys-smtbmc -s boolector --presat --unroll --noprogress -t 20:21 --append 0 --dump-vcd engine_0/trace.vcd --dump-vlogtb engine_0/trace_tb.v --dump-smtc engine_0/trace.smtc model/design_smt2.smt2"
SBY 15:54:21 [insn_andi_ch0] smt2: finished (returncode=0)
SBY 15:54:21 [pc_fwd_ch0] engine_0: ##   0:00:00  Solver: boolector
SBY 15:54:21 [insn_andi_ch0] engine_0: starting process "cd insn_andi_ch0; yosys-smtbmc -s boolector --presat --unroll --noprogress -t 20:21 --append 0 --dump-vcd engine_0/trace.vcd --dump-vlogtb engine_0/trace_tb.v --dump-smtc engine_0/trace.smtc model/design_smt2.smt2"
SBY 15:54:21 [causal_ch0] smt2: finished (returncode=0)
SBY 15:54:21 [causal_ch0] engine_0: starting process "cd causal_ch0; yosys-smtbmc -s boolector --presat --unroll --noprogress -t 30:31 --append 0 --dump-vcd engine_0/trace.vcd --dump-vlogtb engine_0/trace_tb.v --dump-smtc engine_0/trace.smtc model/design_smt2.smt2"
SBY 15:54:21 [liveness_ch0] smt2: finished (returncode=0)
SBY 15:54:21 [insn_and_ch0] smt2: finished (returncode=0)
SBY 15:54:21 [liveness_ch0] engine_0: starting process "cd liveness_ch0; yosys-smtbmc -s boolector --presat --unroll --noprogress -t 30:31 --append 0 --dump-vcd engine_0/trace.vcd --dump-vlogtb engine_0/trace_tb.v --dump-smtc engine_0/trace.smtc model/design_smt2.smt2"
SBY 15:54:21 [insn_and_ch0] engine_0: starting process "cd insn_and_ch0; yosys-smtbmc -s boolector --presat --unroll --noprogress -t 20:21 --append 0 --dump-vcd engine_0/trace.vcd --dump-vlogtb engine_0/trace_tb.v --dump-smtc engine_0/trace.smtc model/design_smt2.smt2"
SBY 15:54:21 [insn_bge_ch0] smt2: finished (returncode=0)
SBY 15:54:21 [insn_bge_ch0] engine_0: starting process "cd insn_bge_ch0; yosys-smtbmc -s boolector --presat --unroll --noprogress -t 20:21 --append 0 --dump-vcd engine_0/trace.vcd --dump-vlogtb engine_0/trace_tb.v --dump-smtc engine_0/trace.smtc model/design_smt2.smt2"
SBY 15:54:21 [insn_auipc_ch0] engine_0: ##   0:00:00  Solver: boolector
SBY 15:54:21 [insn_beq_ch0] smt2: finished (returncode=0)
SBY 15:54:21 [insn_beq_ch0] engine_0: starting process "cd insn_beq_ch0; yosys-smtbmc -s boolector --presat --unroll --noprogress -t 20:21 --append 0 --dump-vcd engine_0/trace.vcd --dump-vlogtb engine_0/trace_tb.v --dump-smtc engine_0/trace.smtc model/design_smt2.smt2"
SBY 15:54:21 [insn_add_ch0] engine_0: ##   0:00:00  Solver: boolector
SBY 15:54:21 [csrw_minstret_ch0] smt2: finished (returncode=0)
SBY 15:54:21 [csrw_minstret_ch0] engine_0: starting process "cd csrw_minstret_ch0; yosys-smtbmc -s boolector --presat --unroll --noprogress -t 30:31 --append 0 --dump-vcd engine_0/trace.vcd --dump-vlogtb engine_0/trace_tb.v --dump-smtc engine_0/trace.smtc model/design_smt2.smt2"
SBY 15:54:21 [insn_andi_ch0] engine_0: ##   0:00:00  Solver: boolector
SBY 15:54:21 [causal_ch0] engine_0: ##   0:00:00  Solver: boolector
SBY 15:54:21 [insn_and_ch0] engine_0: ##   0:00:00  Solver: boolector
SBY 15:54:21 [insn_bge_ch0] engine_0: ##   0:00:00  Solver: boolector
SBY 15:54:21 [liveness_ch0] engine_0: ##   0:00:00  Solver: boolector
SBY 15:54:21 [csrw_mcycle_ch0] smt2: finished (returncode=0)
SBY 15:54:21 [csrw_mcycle_ch0] engine_0: starting process "cd csrw_mcycle_ch0; yosys-smtbmc -s boolector --presat --unroll --noprogress -t 30:31 --append 0 --dump-vcd engine_0/trace.vcd --dump-vlogtb engine_0/trace_tb.v --dump-smtc engine_0/trace.smtc model/design_smt2.smt2"
SBY 15:54:21 [pc_bwd_ch0] engine_0: ##   0:00:00  Skipping step 0..
SBY 15:54:21 [unique_ch0] engine_0: ##   0:00:00  Skipping step 0..
SBY 15:54:21 [insn_beq_ch0] engine_0: ##   0:00:00  Solver: boolector
SBY 15:54:21 [csrw_minstret_ch0] engine_0: ##   0:00:00  Solver: boolector
SBY 15:54:21 [reg_ch0] engine_0: ##   0:00:00  Skipping step 0..
SBY 15:54:21 [csrw_mcycle_ch0] engine_0: ##   0:00:00  Solver: boolector
SBY 15:54:21 [cover] engine_0: ##   0:00:00  Checking cover reachability in step 1..
SBY 15:54:21 [pc_fwd_ch0] engine_0: ##   0:00:00  Skipping step 0..
SBY 15:54:21 [insn_addi_ch0] engine_0: ##   0:00:00  Skipping step 0..
SBY 15:54:21 [insn_auipc_ch0] engine_0: ##   0:00:00  Skipping step 0..
SBY 15:54:21 [insn_andi_ch0] engine_0: ##   0:00:00  Skipping step 0..
SBY 15:54:21 [causal_ch0] engine_0: ##   0:00:00  Skipping step 0..
SBY 15:54:21 [pc_bwd_ch0] engine_0: ##   0:00:00  Skipping step 1..
SBY 15:54:21 [insn_add_ch0] engine_0: ##   0:00:00  Skipping step 0..
SBY 15:54:21 [liveness_ch0] engine_0: ##   0:00:00  Skipping step 0..
SBY 15:54:21 [unique_ch0] engine_0: ##   0:00:00  Skipping step 1..
SBY 15:54:21 [insn_and_ch0] engine_0: ##   0:00:00  Skipping step 0..
SBY 15:54:21 [insn_bge_ch0] engine_0: ##   0:00:00  Skipping step 0..
SBY 15:54:21 [reg_ch0] engine_0: ##   0:00:00  Skipping step 1..
SBY 15:54:22 [insn_beq_ch0] engine_0: ##   0:00:00  Skipping step 0..
SBY 15:54:22 [pc_fwd_ch0] engine_0: ##   0:00:00  Skipping step 1..
SBY 15:54:22 [csrw_minstret_ch0] engine_0: ##   0:00:00  Skipping step 0..
SBY 15:54:22 [insn_addi_ch0] engine_0: ##   0:00:00  Skipping step 1..
SBY 15:54:22 [csrw_mcycle_ch0] engine_0: ##   0:00:00  Skipping step 0..
SBY 15:54:22 [insn_auipc_ch0] engine_0: ##   0:00:00  Skipping step 1..
SBY 15:54:22 [pc_bwd_ch0] engine_0: ##   0:00:00  Skipping step 2..
SBY 15:54:22 [insn_andi_ch0] engine_0: ##   0:00:00  Skipping step 1..
SBY 15:54:22 [cover] engine_0: ##   0:00:00  Checking cover reachability in step 2..
SBY 15:54:22 [causal_ch0] engine_0: ##   0:00:00  Skipping step 1..
SBY 15:54:22 [insn_add_ch0] engine_0: ##   0:00:00  Skipping step 1..
SBY 15:54:22 [unique_ch0] engine_0: ##   0:00:00  Skipping step 2..
SBY 15:54:22 [liveness_ch0] engine_0: ##   0:00:00  Skipping step 1..
SBY 15:54:22 [insn_and_ch0] engine_0: ##   0:00:00  Skipping step 1..
SBY 15:54:22 [insn_bge_ch0] engine_0: ##   0:00:00  Skipping step 1..
SBY 15:54:22 [reg_ch0] engine_0: ##   0:00:00  Skipping step 2..
SBY 15:54:22 [insn_beq_ch0] engine_0: ##   0:00:00  Skipping step 1..
SBY 15:54:22 [pc_fwd_ch0] engine_0: ##   0:00:00  Skipping step 2..
SBY 15:54:22 [insn_addi_ch0] engine_0: ##   0:00:00  Skipping step 2..
SBY 15:54:22 [csrw_minstret_ch0] engine_0: ##   0:00:00  Skipping step 1..
SBY 15:54:22 [insn_auipc_ch0] engine_0: ##   0:00:00  Skipping step 2..
SBY 15:54:22 [csrw_mcycle_ch0] engine_0: ##   0:00:00  Skipping step 1..
SBY 15:54:22 [pc_bwd_ch0] engine_0: ##   0:00:00  Skipping step 3..
SBY 15:54:22 [insn_andi_ch0] engine_0: ##   0:00:00  Skipping step 2..
SBY 15:54:22 [causal_ch0] engine_0: ##   0:00:00  Skipping step 2..
SBY 15:54:22 [insn_add_ch0] engine_0: ##   0:00:00  Skipping step 2..
SBY 15:54:22 [insn_and_ch0] engine_0: ##   0:00:00  Skipping step 2..
SBY 15:54:22 [unique_ch0] engine_0: ##   0:00:00  Skipping step 3..
SBY 15:54:22 [liveness_ch0] engine_0: ##   0:00:00  Skipping step 2..
SBY 15:54:22 [insn_bge_ch0] engine_0: ##   0:00:00  Skipping step 2..
SBY 15:54:22 [reg_ch0] engine_0: ##   0:00:00  Skipping step 3..
SBY 15:54:22 [insn_beq_ch0] engine_0: ##   0:00:00  Skipping step 2..
SBY 15:54:22 [pc_fwd_ch0] engine_0: ##   0:00:00  Skipping step 3..
SBY 15:54:22 [insn_addi_ch0] engine_0: ##   0:00:00  Skipping step 3..
SBY 15:54:22 [csrw_minstret_ch0] engine_0: ##   0:00:00  Skipping step 2..
SBY 15:54:22 [insn_auipc_ch0] engine_0: ##   0:00:00  Skipping step 3..
SBY 15:54:22 [csrw_mcycle_ch0] engine_0: ##   0:00:00  Skipping step 2..
SBY 15:54:22 [cover] engine_0: ##   0:00:00  Checking cover reachability in step 3..
SBY 15:54:22 [pc_bwd_ch0] engine_0: ##   0:00:00  Skipping step 4..
SBY 15:54:22 [insn_andi_ch0] engine_0: ##   0:00:00  Skipping step 3..
SBY 15:54:22 [insn_and_ch0] engine_0: ##   0:00:00  Skipping step 3..
SBY 15:54:22 [causal_ch0] engine_0: ##   0:00:00  Skipping step 3..
SBY 15:54:22 [insn_add_ch0] engine_0: ##   0:00:00  Skipping step 3..
SBY 15:54:22 [unique_ch0] engine_0: ##   0:00:00  Skipping step 4..
SBY 15:54:22 [liveness_ch0] engine_0: ##   0:00:00  Skipping step 3..
SBY 15:54:22 [insn_bge_ch0] engine_0: ##   0:00:00  Skipping step 3..
SBY 15:54:22 [reg_ch0] engine_0: ##   0:00:00  Skipping step 4..
SBY 15:54:22 [insn_beq_ch0] engine_0: ##   0:00:00  Skipping step 3..
SBY 15:54:22 [pc_fwd_ch0] engine_0: ##   0:00:00  Skipping step 4..
SBY 15:54:22 [insn_addi_ch0] engine_0: ##   0:00:00  Skipping step 4..
SBY 15:54:22 [csrw_minstret_ch0] engine_0: ##   0:00:00  Skipping step 3..
SBY 15:54:22 [insn_auipc_ch0] engine_0: ##   0:00:00  Skipping step 4..
SBY 15:54:22 [csrw_mcycle_ch0] engine_0: ##   0:00:00  Skipping step 3..
SBY 15:54:22 [insn_and_ch0] engine_0: ##   0:00:00  Skipping step 4..
SBY 15:54:22 [insn_andi_ch0] engine_0: ##   0:00:00  Skipping step 4..
SBY 15:54:22 [pc_bwd_ch0] engine_0: ##   0:00:00  Skipping step 5..
SBY 15:54:22 [causal_ch0] engine_0: ##   0:00:00  Skipping step 4..
SBY 15:54:22 [insn_add_ch0] engine_0: ##   0:00:00  Skipping step 4..
SBY 15:54:22 [unique_ch0] engine_0: ##   0:00:00  Skipping step 5..
SBY 15:54:22 [liveness_ch0] engine_0: ##   0:00:00  Skipping step 4..
SBY 15:54:22 [insn_bge_ch0] engine_0: ##   0:00:00  Skipping step 4..
SBY 15:54:22 [reg_ch0] engine_0: ##   0:00:00  Skipping step 5..
SBY 15:54:22 [insn_beq_ch0] engine_0: ##   0:00:00  Skipping step 4..
SBY 15:54:22 [cover] engine_0: ##   0:00:01  Checking cover reachability in step 4..
SBY 15:54:22 [pc_fwd_ch0] engine_0: ##   0:00:00  Skipping step 5..
SBY 15:54:22 [insn_addi_ch0] engine_0: ##   0:00:00  Skipping step 5..
SBY 15:54:22 [csrw_minstret_ch0] engine_0: ##   0:00:00  Skipping step 4..
SBY 15:54:22 [insn_auipc_ch0] engine_0: ##   0:00:00  Skipping step 5..
SBY 15:54:22 [csrw_mcycle_ch0] engine_0: ##   0:00:00  Skipping step 4..
SBY 15:54:22 [insn_andi_ch0] engine_0: ##   0:00:00  Skipping step 5..
SBY 15:54:22 [insn_and_ch0] engine_0: ##   0:00:00  Skipping step 5..
SBY 15:54:22 [pc_bwd_ch0] engine_0: ##   0:00:01  Skipping step 6..
SBY 15:54:22 [causal_ch0] engine_0: ##   0:00:00  Skipping step 5..
SBY 15:54:22 [insn_add_ch0] engine_0: ##   0:00:00  Skipping step 5..
SBY 15:54:22 [unique_ch0] engine_0: ##   0:00:01  Skipping step 6..
SBY 15:54:22 [liveness_ch0] engine_0: ##   0:00:00  Skipping step 5..
SBY 15:54:22 [insn_bge_ch0] engine_0: ##   0:00:00  Skipping step 5..
SBY 15:54:22 [reg_ch0] engine_0: ##   0:00:01  Skipping step 6..
SBY 15:54:22 [insn_beq_ch0] engine_0: ##   0:00:00  Skipping step 5..
SBY 15:54:22 [pc_fwd_ch0] engine_0: ##   0:00:01  Skipping step 6..
SBY 15:54:22 [insn_addi_ch0] engine_0: ##   0:00:01  Skipping step 6..
SBY 15:54:22 [csrw_minstret_ch0] engine_0: ##   0:00:00  Skipping step 5..
SBY 15:54:22 [insn_auipc_ch0] engine_0: ##   0:00:01  Skipping step 6..
SBY 15:54:22 [csrw_mcycle_ch0] engine_0: ##   0:00:00  Skipping step 5..
SBY 15:54:22 [insn_andi_ch0] engine_0: ##   0:00:01  Skipping step 6..
SBY 15:54:22 [pc_bwd_ch0] engine_0: ##   0:00:01  Skipping step 7..
SBY 15:54:22 [insn_and_ch0] engine_0: ##   0:00:01  Skipping step 6..
SBY 15:54:22 [unique_ch0] engine_0: ##   0:00:01  Skipping step 7..
SBY 15:54:22 [insn_add_ch0] engine_0: ##   0:00:01  Skipping step 6..
SBY 15:54:22 [causal_ch0] engine_0: ##   0:00:01  Skipping step 6..
SBY 15:54:22 [cover] engine_0: ##   0:00:01  Checking cover reachability in step 5..
SBY 15:54:22 [liveness_ch0] engine_0: ##   0:00:01  Skipping step 6..
SBY 15:54:22 [insn_bge_ch0] engine_0: ##   0:00:01  Skipping step 6..
SBY 15:54:22 [reg_ch0] engine_0: ##   0:00:01  Skipping step 7..
SBY 15:54:22 [insn_beq_ch0] engine_0: ##   0:00:01  Skipping step 6..
SBY 15:54:22 [pc_fwd_ch0] engine_0: ##   0:00:01  Skipping step 7..
SBY 15:54:22 [insn_addi_ch0] engine_0: ##   0:00:01  Skipping step 7..
SBY 15:54:22 [csrw_minstret_ch0] engine_0: ##   0:00:01  Skipping step 6..
SBY 15:54:22 [insn_auipc_ch0] engine_0: ##   0:00:01  Skipping step 7..
SBY 15:54:22 [csrw_mcycle_ch0] engine_0: ##   0:00:01  Skipping step 6..
SBY 15:54:23 [insn_andi_ch0] engine_0: ##   0:00:01  Skipping step 7..
SBY 15:54:23 [pc_bwd_ch0] engine_0: ##   0:00:01  Skipping step 8..
SBY 15:54:23 [insn_add_ch0] engine_0: ##   0:00:01  Skipping step 7..
SBY 15:54:23 [unique_ch0] engine_0: ##   0:00:01  Skipping step 8..
SBY 15:54:23 [causal_ch0] engine_0: ##   0:00:01  Skipping step 7..
SBY 15:54:23 [insn_and_ch0] engine_0: ##   0:00:01  Skipping step 7..
SBY 15:54:23 [liveness_ch0] engine_0: ##   0:00:01  Skipping step 7..
SBY 15:54:23 [insn_bge_ch0] engine_0: ##   0:00:01  Skipping step 7..
SBY 15:54:23 [reg_ch0] engine_0: ##   0:00:01  Skipping step 8..
SBY 15:54:23 [insn_beq_ch0] engine_0: ##   0:00:01  Skipping step 7..
SBY 15:54:23 [pc_fwd_ch0] engine_0: ##   0:00:01  Skipping step 8..
SBY 15:54:23 [insn_addi_ch0] engine_0: ##   0:00:01  Skipping step 8..
SBY 15:54:23 [csrw_minstret_ch0] engine_0: ##   0:00:01  Skipping step 7..
SBY 15:54:23 [insn_auipc_ch0] engine_0: ##   0:00:01  Skipping step 8..
SBY 15:54:23 [csrw_mcycle_ch0] engine_0: ##   0:00:01  Skipping step 7..
SBY 15:54:23 [cover] engine_0: ##   0:00:01  Checking cover reachability in step 6..
SBY 15:54:23 [insn_andi_ch0] engine_0: ##   0:00:01  Skipping step 8..
SBY 15:54:23 [pc_bwd_ch0] engine_0: ##   0:00:01  Skipping step 9..
SBY 15:54:23 [unique_ch0] engine_0: ##   0:00:01  Skipping step 9..
SBY 15:54:23 [insn_add_ch0] engine_0: ##   0:00:01  Skipping step 8..
SBY 15:54:23 [causal_ch0] engine_0: ##   0:00:01  Skipping step 8..
SBY 15:54:23 [insn_bge_ch0] engine_0: ##   0:00:01  Skipping step 8..
SBY 15:54:23 [insn_and_ch0] engine_0: ##   0:00:01  Skipping step 8..
SBY 15:54:23 [liveness_ch0] engine_0: ##   0:00:01  Skipping step 8..
SBY 15:54:23 [reg_ch0] engine_0: ##   0:00:01  Skipping step 9..
SBY 15:54:23 [insn_beq_ch0] engine_0: ##   0:00:01  Skipping step 8..
SBY 15:54:23 [pc_fwd_ch0] engine_0: ##   0:00:01  Skipping step 9..
SBY 15:54:23 [insn_addi_ch0] engine_0: ##   0:00:01  Skipping step 9..
SBY 15:54:23 [csrw_minstret_ch0] engine_0: ##   0:00:01  Skipping step 8..
SBY 15:54:23 [insn_auipc_ch0] engine_0: ##   0:00:01  Skipping step 9..
SBY 15:54:23 [csrw_mcycle_ch0] engine_0: ##   0:00:01  Skipping step 8..
SBY 15:54:23 [insn_andi_ch0] engine_0: ##   0:00:01  Skipping step 9..
SBY 15:54:23 [pc_bwd_ch0] engine_0: ##   0:00:01  Skipping step 10..
SBY 15:54:23 [unique_ch0] engine_0: ##   0:00:01  Skipping step 10..
SBY 15:54:23 [insn_add_ch0] engine_0: ##   0:00:01  Skipping step 9..
SBY 15:54:23 [causal_ch0] engine_0: ##   0:00:01  Skipping step 9..
SBY 15:54:23 [insn_bge_ch0] engine_0: ##   0:00:01  Skipping step 9..
SBY 15:54:23 [liveness_ch0] engine_0: ##   0:00:01  Skipping step 9..
SBY 15:54:23 [reg_ch0] engine_0: ##   0:00:01  Skipping step 10..
SBY 15:54:23 [insn_and_ch0] engine_0: ##   0:00:01  Skipping step 9..
SBY 15:54:23 [insn_beq_ch0] engine_0: ##   0:00:01  Skipping step 9..
SBY 15:54:23 [pc_fwd_ch0] engine_0: ##   0:00:01  Skipping step 10..
SBY 15:54:23 [insn_addi_ch0] engine_0: ##   0:00:01  Skipping step 10..
SBY 15:54:23 [cover] engine_0: ##   0:00:01  Checking cover reachability in step 7..
SBY 15:54:23 [insn_auipc_ch0] engine_0: ##   0:00:01  Skipping step 10..
SBY 15:54:23 [csrw_minstret_ch0] engine_0: ##   0:00:01  Skipping step 9..
SBY 15:54:23 [csrw_mcycle_ch0] engine_0: ##   0:00:01  Skipping step 9..
SBY 15:54:23 [insn_andi_ch0] engine_0: ##   0:00:01  Skipping step 10..
SBY 15:54:23 [pc_bwd_ch0] engine_0: ##   0:00:01  Skipping step 11..
SBY 15:54:23 [unique_ch0] engine_0: ##   0:00:01  Skipping step 11..
SBY 15:54:23 [insn_add_ch0] engine_0: ##   0:00:01  Skipping step 10..
SBY 15:54:23 [causal_ch0] engine_0: ##   0:00:01  Skipping step 10..
SBY 15:54:23 [insn_bge_ch0] engine_0: ##   0:00:01  Skipping step 10..
SBY 15:54:23 [reg_ch0] engine_0: ##   0:00:01  Skipping step 11..
SBY 15:54:23 [liveness_ch0] engine_0: ##   0:00:01  Skipping step 10..
SBY 15:54:23 [insn_and_ch0] engine_0: ##   0:00:01  Skipping step 10..
SBY 15:54:23 [insn_beq_ch0] engine_0: ##   0:00:01  Skipping step 10..
SBY 15:54:23 [pc_fwd_ch0] engine_0: ##   0:00:01  Skipping step 11..
SBY 15:54:23 [insn_addi_ch0] engine_0: ##   0:00:01  Skipping step 11..
SBY 15:54:23 [insn_auipc_ch0] engine_0: ##   0:00:01  Skipping step 11..
SBY 15:54:23 [csrw_minstret_ch0] engine_0: ##   0:00:01  Skipping step 10..
SBY 15:54:23 [csrw_mcycle_ch0] engine_0: ##   0:00:01  Skipping step 10..
SBY 15:54:23 [insn_andi_ch0] engine_0: ##   0:00:01  Skipping step 11..
SBY 15:54:23 [insn_add_ch0] engine_0: ##   0:00:01  Skipping step 11..
SBY 15:54:23 [unique_ch0] engine_0: ##   0:00:01  Skipping step 12..
SBY 15:54:23 [pc_bwd_ch0] engine_0: ##   0:00:01  Skipping step 12..
SBY 15:54:23 [causal_ch0] engine_0: ##   0:00:01  Skipping step 11..
SBY 15:54:23 [insn_bge_ch0] engine_0: ##   0:00:01  Skipping step 11..
SBY 15:54:23 [insn_and_ch0] engine_0: ##   0:00:01  Skipping step 11..
SBY 15:54:23 [reg_ch0] engine_0: ##   0:00:01  Skipping step 12..
SBY 15:54:23 [liveness_ch0] engine_0: ##   0:00:01  Skipping step 11..
SBY 15:54:23 [insn_beq_ch0] engine_0: ##   0:00:01  Skipping step 11..
SBY 15:54:23 [pc_fwd_ch0] engine_0: ##   0:00:01  Skipping step 12..
SBY 15:54:23 [insn_addi_ch0] engine_0: ##   0:00:01  Skipping step 12..
SBY 15:54:23 [insn_auipc_ch0] engine_0: ##   0:00:01  Skipping step 12..
SBY 15:54:23 [csrw_minstret_ch0] engine_0: ##   0:00:01  Skipping step 11..
SBY 15:54:23 [csrw_mcycle_ch0] engine_0: ##   0:00:01  Skipping step 11..
SBY 15:54:23 [insn_andi_ch0] engine_0: ##   0:00:01  Skipping step 12..
SBY 15:54:23 [pc_bwd_ch0] engine_0: ##   0:00:02  Skipping step 13..
SBY 15:54:23 [unique_ch0] engine_0: ##   0:00:02  Skipping step 13..
SBY 15:54:23 [insn_add_ch0] engine_0: ##   0:00:02  Skipping step 12..
SBY 15:54:23 [insn_and_ch0] engine_0: ##   0:00:01  Skipping step 12..
SBY 15:54:23 [causal_ch0] engine_0: ##   0:00:02  Skipping step 12..
SBY 15:54:23 [insn_bge_ch0] engine_0: ##   0:00:02  Skipping step 12..
SBY 15:54:23 [reg_ch0] engine_0: ##   0:00:02  Skipping step 13..
SBY 15:54:23 [insn_beq_ch0] engine_0: ##   0:00:01  Skipping step 12..
SBY 15:54:23 [liveness_ch0] engine_0: ##   0:00:02  Skipping step 12..
SBY 15:54:23 [pc_fwd_ch0] engine_0: ##   0:00:02  Skipping step 13..
SBY 15:54:23 [insn_addi_ch0] engine_0: ##   0:00:02  Skipping step 13..
SBY 15:54:23 [insn_auipc_ch0] engine_0: ##   0:00:02  Skipping step 13..
SBY 15:54:23 [csrw_minstret_ch0] engine_0: ##   0:00:02  Skipping step 12..
SBY 15:54:23 [csrw_mcycle_ch0] engine_0: ##   0:00:02  Skipping step 12..
SBY 15:54:23 [insn_andi_ch0] engine_0: ##   0:00:02  Skipping step 13..
SBY 15:54:23 [insn_and_ch0] engine_0: ##   0:00:02  Skipping step 13..
SBY 15:54:23 [pc_bwd_ch0] engine_0: ##   0:00:02  Skipping step 14..
SBY 15:54:23 [unique_ch0] engine_0: ##   0:00:02  Skipping step 14..
SBY 15:54:23 [insn_add_ch0] engine_0: ##   0:00:02  Skipping step 13..
SBY 15:54:23 [causal_ch0] engine_0: ##   0:00:02  Skipping step 13..
SBY 15:54:23 [reg_ch0] engine_0: ##   0:00:02  Skipping step 14..
SBY 15:54:23 [insn_bge_ch0] engine_0: ##   0:00:02  Skipping step 13..
SBY 15:54:23 [liveness_ch0] engine_0: ##   0:00:02  Skipping step 13..
SBY 15:54:23 [insn_beq_ch0] engine_0: ##   0:00:02  Skipping step 13..
SBY 15:54:23 [pc_fwd_ch0] engine_0: ##   0:00:02  Skipping step 14..
SBY 15:54:23 [insn_addi_ch0] engine_0: ##   0:00:02  Skipping step 14..
SBY 15:54:23 [insn_auipc_ch0] engine_0: ##   0:00:02  Skipping step 14..
SBY 15:54:24 [csrw_minstret_ch0] engine_0: ##   0:00:02  Skipping step 13..
SBY 15:54:24 [csrw_mcycle_ch0] engine_0: ##   0:00:02  Skipping step 13..
SBY 15:54:24 [insn_and_ch0] engine_0: ##   0:00:02  Skipping step 14..
SBY 15:54:24 [insn_andi_ch0] engine_0: ##   0:00:02  Skipping step 14..
SBY 15:54:24 [pc_bwd_ch0] engine_0: ##   0:00:02  Skipping step 15..
SBY 15:54:24 [unique_ch0] engine_0: ##   0:00:02  Skipping step 15..
SBY 15:54:24 [insn_add_ch0] engine_0: ##   0:00:02  Skipping step 14..
SBY 15:54:24 [causal_ch0] engine_0: ##   0:00:02  Skipping step 14..
SBY 15:54:24 [reg_ch0] engine_0: ##   0:00:02  Skipping step 15..
SBY 15:54:24 [insn_bge_ch0] engine_0: ##   0:00:02  Skipping step 14..
SBY 15:54:24 [insn_beq_ch0] engine_0: ##   0:00:02  Skipping step 14..
SBY 15:54:24 [liveness_ch0] engine_0: ##   0:00:02  Skipping step 14..
SBY 15:54:24 [pc_fwd_ch0] engine_0: ##   0:00:02  Skipping step 15..
SBY 15:54:24 [insn_addi_ch0] engine_0: ##   0:00:02  Skipping step 15..
SBY 15:54:24 [insn_auipc_ch0] engine_0: ##   0:00:02  Skipping step 15..
SBY 15:54:24 [csrw_minstret_ch0] engine_0: ##   0:00:02  Skipping step 14..
SBY 15:54:24 [csrw_mcycle_ch0] engine_0: ##   0:00:02  Skipping step 14..
SBY 15:54:24 [insn_and_ch0] engine_0: ##   0:00:02  Skipping step 15..
SBY 15:54:24 [insn_andi_ch0] engine_0: ##   0:00:02  Skipping step 15..
SBY 15:54:24 [pc_bwd_ch0] engine_0: ##   0:00:02  Skipping step 16..
SBY 15:54:24 [insn_add_ch0] engine_0: ##   0:00:02  Skipping step 15..
SBY 15:54:24 [unique_ch0] engine_0: ##   0:00:02  Skipping step 16..
SBY 15:54:24 [causal_ch0] engine_0: ##   0:00:02  Skipping step 15..
SBY 15:54:24 [reg_ch0] engine_0: ##   0:00:02  Skipping step 16..
SBY 15:54:24 [insn_bge_ch0] engine_0: ##   0:00:02  Skipping step 15..
SBY 15:54:24 [insn_beq_ch0] engine_0: ##   0:00:02  Skipping step 15..
SBY 15:54:24 [liveness_ch0] engine_0: ##   0:00:02  Skipping step 15..
SBY 15:54:24 [pc_fwd_ch0] engine_0: ##   0:00:02  Skipping step 16..
SBY 15:54:24 [insn_addi_ch0] engine_0: ##   0:00:02  Skipping step 16..
SBY 15:54:24 [insn_auipc_ch0] engine_0: ##   0:00:02  Skipping step 16..
SBY 15:54:24 [csrw_minstret_ch0] engine_0: ##   0:00:02  Skipping step 15..
SBY 15:54:24 [csrw_mcycle_ch0] engine_0: ##   0:00:02  Skipping step 15..
SBY 15:54:24 [insn_and_ch0] engine_0: ##   0:00:02  Skipping step 16..
SBY 15:54:24 [insn_andi_ch0] engine_0: ##   0:00:02  Skipping step 16..
SBY 15:54:24 [insn_add_ch0] engine_0: ##   0:00:02  Skipping step 16..
SBY 15:54:24 [pc_bwd_ch0] engine_0: ##   0:00:02  Skipping step 17..
SBY 15:54:24 [causal_ch0] engine_0: ##   0:00:02  Skipping step 16..
SBY 15:54:24 [unique_ch0] engine_0: ##   0:00:02  Skipping step 17..
SBY 15:54:24 [reg_ch0] engine_0: ##   0:00:02  Skipping step 17..
SBY 15:54:24 [insn_bge_ch0] engine_0: ##   0:00:02  Skipping step 16..
SBY 15:54:24 [insn_beq_ch0] engine_0: ##   0:00:02  Skipping step 16..
SBY 15:54:24 [liveness_ch0] engine_0: ##   0:00:02  Skipping step 16..
SBY 15:54:24 [cover] engine_0: ##   0:00:02  Checking cover reachability in step 8..
SBY 15:54:24 [pc_fwd_ch0] engine_0: ##   0:00:02  Skipping step 17..
SBY 15:54:24 [insn_addi_ch0] engine_0: ##   0:00:02  Skipping step 17..
SBY 15:54:24 [insn_auipc_ch0] engine_0: ##   0:00:02  Skipping step 17..
SBY 15:54:24 [csrw_minstret_ch0] engine_0: ##   0:00:02  Skipping step 16..
SBY 15:54:24 [csrw_mcycle_ch0] engine_0: ##   0:00:02  Skipping step 16..
SBY 15:54:24 [insn_and_ch0] engine_0: ##   0:00:02  Skipping step 17..
SBY 15:54:24 [insn_andi_ch0] engine_0: ##   0:00:02  Skipping step 17..
SBY 15:54:24 [pc_bwd_ch0] engine_0: ##   0:00:02  Skipping step 18..
SBY 15:54:24 [insn_add_ch0] engine_0: ##   0:00:02  Skipping step 17..
SBY 15:54:24 [unique_ch0] engine_0: ##   0:00:02  Skipping step 18..
SBY 15:54:24 [reg_ch0] engine_0: ##   0:00:02  Skipping step 18..
SBY 15:54:24 [causal_ch0] engine_0: ##   0:00:02  Skipping step 17..
SBY 15:54:24 [insn_beq_ch0] engine_0: ##   0:00:02  Skipping step 17..
SBY 15:54:24 [insn_bge_ch0] engine_0: ##   0:00:02  Skipping step 17..
SBY 15:54:24 [liveness_ch0] engine_0: ##   0:00:02  Skipping step 17..
SBY 15:54:24 [pc_fwd_ch0] engine_0: ##   0:00:02  Skipping step 18..
SBY 15:54:24 [insn_addi_ch0] engine_0: ##   0:00:02  Skipping step 18..
SBY 15:54:24 [insn_auipc_ch0] engine_0: ##   0:00:02  Skipping step 18..
SBY 15:54:24 [csrw_minstret_ch0] engine_0: ##   0:00:02  Skipping step 17..
SBY 15:54:24 [csrw_mcycle_ch0] engine_0: ##   0:00:02  Skipping step 17..
SBY 15:54:24 [insn_andi_ch0] engine_0: ##   0:00:02  Skipping step 18..
SBY 15:54:24 [insn_and_ch0] engine_0: ##   0:00:02  Skipping step 18..
SBY 15:54:24 [pc_bwd_ch0] engine_0: ##   0:00:03  Skipping step 19..
SBY 15:54:24 [insn_add_ch0] engine_0: ##   0:00:02  Skipping step 18..
SBY 15:54:24 [unique_ch0] engine_0: ##   0:00:03  Skipping step 19..
SBY 15:54:24 [reg_ch0] engine_0: ##   0:00:03  Skipping step 19..
SBY 15:54:24 [causal_ch0] engine_0: ##   0:00:02  Skipping step 18..
SBY 15:54:24 [insn_beq_ch0] engine_0: ##   0:00:02  Skipping step 18..
SBY 15:54:24 [insn_bge_ch0] engine_0: ##   0:00:02  Skipping step 18..
SBY 15:54:24 [cover] engine_0: ##   0:00:03  Checking cover reachability in step 9..
SBY 15:54:24 [liveness_ch0] engine_0: ##   0:00:02  Skipping step 18..
SBY 15:54:24 [pc_fwd_ch0] engine_0: ##   0:00:03  Skipping step 19..
SBY 15:54:24 [insn_addi_ch0] engine_0: ##   0:00:03  Skipping step 19..
SBY 15:54:24 [insn_auipc_ch0] engine_0: ##   0:00:03  Skipping step 19..
SBY 15:54:24 [csrw_minstret_ch0] engine_0: ##   0:00:02  Skipping step 18..
SBY 15:54:24 [csrw_mcycle_ch0] engine_0: ##   0:00:02  Skipping step 18..
SBY 15:54:24 [insn_andi_ch0] engine_0: ##   0:00:03  Skipping step 19..
SBY 15:54:24 [insn_and_ch0] engine_0: ##   0:00:03  Skipping step 19..
SBY 15:54:24 [pc_bwd_ch0] engine_0: ##   0:00:03  Skipping step 20..
SBY 15:54:24 [insn_add_ch0] engine_0: ##   0:00:03  Skipping step 19..
SBY 15:54:24 [unique_ch0] engine_0: ##   0:00:03  Skipping step 20..
SBY 15:54:24 [reg_ch0] engine_0: ##   0:00:03  Skipping step 20..
SBY 15:54:24 [insn_beq_ch0] engine_0: ##   0:00:03  Skipping step 19..
SBY 15:54:24 [causal_ch0] engine_0: ##   0:00:03  Skipping step 19..
SBY 15:54:24 [insn_bge_ch0] engine_0: ##   0:00:03  Skipping step 19..
SBY 15:54:24 [pc_fwd_ch0] engine_0: ##   0:00:03  Skipping step 20..
SBY 15:54:24 [liveness_ch0] engine_0: ##   0:00:03  Skipping step 19..
SBY 15:54:24 [insn_auipc_ch0] engine_0: ##   0:00:03  Checking assumptions in step 20..
SBY 15:54:24 [insn_addi_ch0] engine_0: ##   0:00:03  Checking assumptions in step 20..
SBY 15:54:24 [csrw_minstret_ch0] engine_0: ##   0:00:03  Skipping step 19..
SBY 15:54:24 [csrw_mcycle_ch0] engine_0: ##   0:00:03  Skipping step 19..
SBY 15:54:24 [insn_andi_ch0] engine_0: ##   0:00:03  Checking assumptions in step 20..
SBY 15:54:24 [insn_and_ch0] engine_0: ##   0:00:03  Checking assumptions in step 20..
SBY 15:54:24 [unique_ch0] engine_0: ##   0:00:03  Skipping step 21..
SBY 15:54:24 [pc_bwd_ch0] engine_0: ##   0:00:03  Skipping step 21..
SBY 15:54:24 [reg_ch0] engine_0: ##   0:00:03  Skipping step 21..
SBY 15:54:24 [insn_add_ch0] engine_0: ##   0:00:03  Checking assumptions in step 20..
SBY 15:54:24 [cover] engine_0: ##   0:00:03  Checking cover reachability in step 10..
SBY 15:54:24 [insn_beq_ch0] engine_0: ##   0:00:03  Checking assumptions in step 20..
SBY 15:54:24 [causal_ch0] engine_0: ##   0:00:03  Skipping step 20..
SBY 15:54:24 [insn_bge_ch0] engine_0: ##   0:00:03  Checking assumptions in step 20..
SBY 15:54:25 [pc_fwd_ch0] engine_0: ##   0:00:03  Skipping step 21..
SBY 15:54:25 [liveness_ch0] engine_0: ##   0:00:03  Skipping step 20..
SBY 15:54:25 [csrw_minstret_ch0] engine_0: ##   0:00:03  Skipping step 20..
SBY 15:54:25 [csrw_mcycle_ch0] engine_0: ##   0:00:03  Skipping step 20..
SBY 15:54:25 [pc_bwd_ch0] engine_0: ##   0:00:03  Skipping step 22..
SBY 15:54:25 [unique_ch0] engine_0: ##   0:00:03  Skipping step 22..
SBY 15:54:25 [reg_ch0] engine_0: ##   0:00:03  Skipping step 22..
SBY 15:54:25 [causal_ch0] engine_0: ##   0:00:03  Skipping step 21..
SBY 15:54:25 [pc_fwd_ch0] engine_0: ##   0:00:03  Skipping step 22..
SBY 15:54:25 [csrw_minstret_ch0] engine_0: ##   0:00:03  Skipping step 21..
SBY 15:54:25 [liveness_ch0] engine_0: ##   0:00:03  Skipping step 21..
SBY 15:54:25 [csrw_mcycle_ch0] engine_0: ##   0:00:03  Skipping step 21..
SBY 15:54:25 [pc_bwd_ch0] engine_0: ##   0:00:03  Skipping step 23..
SBY 15:54:25 [unique_ch0] engine_0: ##   0:00:03  Skipping step 23..
SBY 15:54:25 [reg_ch0] engine_0: ##   0:00:03  Skipping step 23..
SBY 15:54:25 [causal_ch0] engine_0: ##   0:00:03  Skipping step 22..
SBY 15:54:25 [cover] engine_0: ##   0:00:03  Checking cover reachability in step 11..
SBY 15:54:25 [pc_fwd_ch0] engine_0: ##   0:00:03  Skipping step 23..
SBY 15:54:25 [csrw_minstret_ch0] engine_0: ##   0:00:03  Skipping step 22..
SBY 15:54:25 [liveness_ch0] engine_0: ##   0:00:03  Skipping step 22..
SBY 15:54:25 [csrw_mcycle_ch0] engine_0: ##   0:00:03  Skipping step 22..
SBY 15:54:25 [pc_bwd_ch0] engine_0: ##   0:00:03  Skipping step 24..
SBY 15:54:25 [unique_ch0] engine_0: ##   0:00:03  Skipping step 24..
SBY 15:54:25 [reg_ch0] engine_0: ##   0:00:03  Skipping step 24..
SBY 15:54:25 [causal_ch0] engine_0: ##   0:00:03  Skipping step 23..
SBY 15:54:25 [pc_fwd_ch0] engine_0: ##   0:00:03  Skipping step 24..
SBY 15:54:25 [csrw_minstret_ch0] engine_0: ##   0:00:03  Skipping step 23..
SBY 15:54:25 [csrw_mcycle_ch0] engine_0: ##   0:00:03  Skipping step 23..
SBY 15:54:25 [liveness_ch0] engine_0: ##   0:00:03  Skipping step 23..
SBY 15:54:25 [pc_bwd_ch0] engine_0: ##   0:00:03  Skipping step 25..
SBY 15:54:25 [reg_ch0] engine_0: ##   0:00:03  Checking assumptions in step 25..
SBY 15:54:25 [unique_ch0] engine_0: ##   0:00:03  Skipping step 25..
SBY 15:54:25 [causal_ch0] engine_0: ##   0:00:03  Skipping step 24..
SBY 15:54:25 [pc_fwd_ch0] engine_0: ##   0:00:03  Skipping step 25..
SBY 15:54:25 [csrw_minstret_ch0] engine_0: ##   0:00:03  Skipping step 24..
SBY 15:54:25 [csrw_mcycle_ch0] engine_0: ##   0:00:03  Skipping step 24..
SBY 15:54:25 [liveness_ch0] engine_0: ##   0:00:03  Skipping step 24..
SBY 15:54:25 [unique_ch0] engine_0: ##   0:00:04  Skipping step 26..
SBY 15:54:25 [pc_bwd_ch0] engine_0: ##   0:00:04  Skipping step 26..
SBY 15:54:25 [pc_fwd_ch0] engine_0: ##   0:00:04  Skipping step 26..
SBY 15:54:25 [causal_ch0] engine_0: ##   0:00:03  Skipping step 25..
SBY 15:54:25 [csrw_minstret_ch0] engine_0: ##   0:00:03  Skipping step 25..
SBY 15:54:25 [csrw_mcycle_ch0] engine_0: ##   0:00:03  Skipping step 25..
SBY 15:54:25 [liveness_ch0] engine_0: ##   0:00:04  Skipping step 25..
SBY 15:54:25 [pc_bwd_ch0] engine_0: ##   0:00:04  Skipping step 27..
SBY 15:54:25 [unique_ch0] engine_0: ##   0:00:04  Skipping step 27..
SBY 15:54:25 [pc_fwd_ch0] engine_0: ##   0:00:04  Skipping step 27..
SBY 15:54:25 [causal_ch0] engine_0: ##   0:00:04  Skipping step 26..
SBY 15:54:25 [csrw_minstret_ch0] engine_0: ##   0:00:04  Skipping step 26..
SBY 15:54:25 [csrw_mcycle_ch0] engine_0: ##   0:00:04  Skipping step 26..
SBY 15:54:25 [pc_bwd_ch0] engine_0: ##   0:00:04  Skipping step 28..
SBY 15:54:25 [unique_ch0] engine_0: ##   0:00:04  Skipping step 28..
SBY 15:54:25 [liveness_ch0] engine_0: ##   0:00:04  Skipping step 26..
SBY 15:54:26 [pc_fwd_ch0] engine_0: ##   0:00:04  Skipping step 28..
SBY 15:54:26 [causal_ch0] engine_0: ##   0:00:04  Skipping step 27..
SBY 15:54:26 [csrw_minstret_ch0] engine_0: ##   0:00:04  Skipping step 27..
SBY 15:54:26 [csrw_mcycle_ch0] engine_0: ##   0:00:04  Skipping step 27..
SBY 15:54:26 [pc_bwd_ch0] engine_0: ##   0:00:04  Skipping step 29..
SBY 15:54:26 [unique_ch0] engine_0: ##   0:00:04  Skipping step 29..
SBY 15:54:26 [pc_fwd_ch0] engine_0: ##   0:00:04  Skipping step 29..
SBY 15:54:26 [liveness_ch0] engine_0: ##   0:00:04  Skipping step 27..
SBY 15:54:26 [causal_ch0] engine_0: ##   0:00:04  Skipping step 28..
SBY 15:54:26 [csrw_minstret_ch0] engine_0: ##   0:00:04  Skipping step 28..
SBY 15:54:26 [csrw_mcycle_ch0] engine_0: ##   0:00:04  Skipping step 28..
SBY 15:54:26 [pc_bwd_ch0] engine_0: ##   0:00:04  Checking assumptions in step 30..
SBY 15:54:26 [unique_ch0] engine_0: ##   0:00:04  Checking assumptions in step 30..
SBY 15:54:26 [pc_fwd_ch0] engine_0: ##   0:00:04  Checking assumptions in step 30..
SBY 15:54:26 [causal_ch0] engine_0: ##   0:00:04  Skipping step 29..
SBY 15:54:26 [liveness_ch0] engine_0: ##   0:00:04  Skipping step 28..
SBY 15:54:26 [csrw_minstret_ch0] engine_0: ##   0:00:04  Skipping step 29..
SBY 15:54:26 [csrw_mcycle_ch0] engine_0: ##   0:00:04  Skipping step 29..
SBY 15:54:26 [causal_ch0] engine_0: ##   0:00:04  Checking assumptions in step 30..
SBY 15:54:26 [csrw_minstret_ch0] engine_0: ##   0:00:04  Checking assumptions in step 30..
SBY 15:54:26 [liveness_ch0] engine_0: ##   0:00:04  Skipping step 29..
SBY 15:54:26 [csrw_mcycle_ch0] engine_0: ##   0:00:04  Checking assumptions in step 30..
SBY 15:54:26 [liveness_ch0] engine_0: ##   0:00:04  Checking assumptions in step 30..
SBY 15:54:28 [cover] engine_0: ##   0:00:07  Reached cover statement at rvfi_testbench.sv:39|cover_stmts.vh:1 in step 11.
SBY 15:54:28 [cover] engine_0: ##   0:00:07  Writing trace to VCD file: engine_0/trace0.vcd
SBY 15:54:29 [cover] engine_0: ##   0:00:07  Writing trace to Verilog testbench: engine_0/trace0_tb.v
SBY 15:54:29 [cover] engine_0: ##   0:00:07  Writing trace to constraints file: engine_0/trace0.smtc
SBY 15:54:29 [cover] engine_0: ##   0:00:08  Status: passed
SBY 15:54:29 [cover] engine_0: finished (returncode=0)
SBY 15:54:29 [cover] engine_0: Status returned by engine: pass
SBY 15:54:29 [cover] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:12 (12)
SBY 15:54:29 [cover] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:12 (12)
SBY 15:54:29 [cover] summary: engine_0 (smtbmc boolector) returned pass
SBY 15:54:29 [cover] DONE (PASS, rc=0)
sby insn_bgeu_ch0.sby
SBY 15:54:29 [insn_bgeu_ch0] Writing 'insn_bgeu_ch0/src/defines.sv'.
SBY 15:54:29 [insn_bgeu_ch0] Writing 'insn_bgeu_ch0/src/insn_bgeu_ch0.sv'.
SBY 15:54:29 [insn_bgeu_ch0] Copy '/home/dsleung/riscv-formal/cores/picorv32/../../checks/rvfi_macros.vh' to 'insn_bgeu_ch0/src/rvfi_macros.vh'.
SBY 15:54:29 [insn_bgeu_ch0] Copy '/home/dsleung/riscv-formal/cores/picorv32/../../checks/rvfi_channel.sv' to 'insn_bgeu_ch0/src/rvfi_channel.sv'.
SBY 15:54:29 [insn_bgeu_ch0] Copy '/home/dsleung/riscv-formal/cores/picorv32/../../checks/rvfi_testbench.sv' to 'insn_bgeu_ch0/src/rvfi_testbench.sv'.
SBY 15:54:29 [insn_bgeu_ch0] Copy '/home/dsleung/riscv-formal/cores/picorv32/../../checks/rvfi_insn_check.sv' to 'insn_bgeu_ch0/src/rvfi_insn_check.sv'.
SBY 15:54:29 [insn_bgeu_ch0] Copy '/home/dsleung/riscv-formal/cores/picorv32/../../insns/insn_bgeu.v' to 'insn_bgeu_ch0/src/insn_bgeu.v'.
SBY 15:54:29 [insn_bgeu_ch0] engine_0: smtbmc boolector
SBY 15:54:29 [insn_bgeu_ch0] base: starting process "cd insn_bgeu_ch0/src; yosys -ql ../model/design.log ../model/design.ys"
SBY 15:54:34 [csrw_mcycle_ch0] engine_0: ##   0:00:11  Assumptions are unsatisfiable!
SBY 15:54:34 [csrw_mcycle_ch0] engine_0: ##   0:00:12  Status: PREUNSAT
SBY 15:54:34 [csrw_mcycle_ch0] engine_0: finished (returncode=1)
SBY 15:54:34 [csrw_mcycle_ch0] engine_0: Status returned by engine: ERROR
SBY 15:54:34 [csrw_mcycle_ch0] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:17 (17)
SBY 15:54:34 [csrw_mcycle_ch0] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:17 (17)
SBY 15:54:34 [csrw_mcycle_ch0] summary: engine_0 (smtbmc boolector) returned ERROR
SBY 15:54:34 [csrw_mcycle_ch0] DONE (ERROR, rc=16)
SBY 15:54:35 [insn_bgeu_ch0] base: finished (returncode=0)
SBY 15:54:35 [insn_bgeu_ch0] smt2: starting process "cd insn_bgeu_ch0/model; yosys -ql design_smt2.log design_smt2.ys"
SBY 15:54:35 [insn_bgeu_ch0] smt2: finished (returncode=0)
SBY 15:54:35 [insn_bgeu_ch0] engine_0: starting process "cd insn_bgeu_ch0; yosys-smtbmc -s boolector --presat --unroll --noprogress -t 20:21 --append 0 --dump-vcd engine_0/trace.vcd --dump-vlogtb engine_0/trace_tb.v --dump-smtc engine_0/trace.smtc model/design_smt2.smt2"
SBY 15:54:35 [insn_bgeu_ch0] engine_0: ##   0:00:00  Solver: boolector
SBY 15:54:36 [insn_bgeu_ch0] engine_0: ##   0:00:00  Skipping step 0..
SBY 15:54:36 [insn_bgeu_ch0] engine_0: ##   0:00:00  Skipping step 1..
SBY 15:54:36 [insn_bgeu_ch0] engine_0: ##   0:00:00  Skipping step 2..
SBY 15:54:36 [insn_bgeu_ch0] engine_0: ##   0:00:00  Skipping step 3..
SBY 15:54:36 [insn_bgeu_ch0] engine_0: ##   0:00:00  Skipping step 4..
SBY 15:54:36 [insn_bgeu_ch0] engine_0: ##   0:00:00  Skipping step 5..
SBY 15:54:36 [insn_bgeu_ch0] engine_0: ##   0:00:00  Skipping step 6..
SBY 15:54:36 [insn_bgeu_ch0] engine_0: ##   0:00:01  Skipping step 7..
SBY 15:54:37 [insn_bgeu_ch0] engine_0: ##   0:00:01  Skipping step 8..
SBY 15:54:37 [insn_bgeu_ch0] engine_0: ##   0:00:01  Skipping step 9..
SBY 15:54:37 [insn_bgeu_ch0] engine_0: ##   0:00:01  Skipping step 10..
SBY 15:54:37 [insn_bgeu_ch0] engine_0: ##   0:00:01  Skipping step 11..
SBY 15:54:37 [insn_bgeu_ch0] engine_0: ##   0:00:01  Skipping step 12..
SBY 15:54:37 [insn_bgeu_ch0] engine_0: ##   0:00:01  Skipping step 13..
SBY 15:54:37 [insn_bgeu_ch0] engine_0: ##   0:00:01  Skipping step 14..
SBY 15:54:37 [insn_bgeu_ch0] engine_0: ##   0:00:01  Skipping step 15..
SBY 15:54:37 [insn_bgeu_ch0] engine_0: ##   0:00:02  Skipping step 16..
SBY 15:54:38 [insn_bgeu_ch0] engine_0: ##   0:00:02  Skipping step 17..
SBY 15:54:38 [insn_bgeu_ch0] engine_0: ##   0:00:02  Skipping step 18..
SBY 15:54:38 [insn_bgeu_ch0] engine_0: ##   0:00:02  Skipping step 19..
SBY 15:54:38 [insn_bgeu_ch0] engine_0: ##   0:00:02  Checking assumptions in step 20..
SBY 15:54:38 [insn_andi_ch0] engine_0: ##   0:00:16  Checking assertions in step 20..
SBY 15:54:41 [csrw_minstret_ch0] engine_0: ##   0:00:19  Assumptions are unsatisfiable!
SBY 15:54:41 [csrw_minstret_ch0] engine_0: ##   0:00:19  Status: PREUNSAT
SBY 15:54:41 [csrw_minstret_ch0] engine_0: finished (returncode=1)
SBY 15:54:41 [csrw_minstret_ch0] engine_0: Status returned by engine: ERROR
SBY 15:54:41 [csrw_minstret_ch0] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:24 (24)
SBY 15:54:41 [csrw_minstret_ch0] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:24 (24)
SBY 15:54:41 [csrw_minstret_ch0] summary: engine_0 (smtbmc boolector) returned ERROR
SBY 15:54:41 [csrw_minstret_ch0] DONE (ERROR, rc=16)
SBY 15:54:44 [insn_auipc_ch0] engine_0: ##   0:00:22  Checking assertions in step 20..
SBY 15:54:47 [insn_addi_ch0] engine_0: ##   0:00:25  Checking assertions in step 20..
SBY 15:54:50 [insn_bge_ch0] engine_0: ##   0:00:29  Checking assertions in step 20..
SBY 15:54:53 [insn_add_ch0] engine_0: ##   0:00:31  Checking assertions in step 20..
SBY 15:54:53 [insn_beq_ch0] engine_0: ##   0:00:31  Checking assertions in step 20..
SBY 15:54:59 [insn_bgeu_ch0] engine_0: ##   0:00:23  Checking assertions in step 20..
SBY 15:55:24 [insn_and_ch0] engine_0: ##   0:01:02  Checking assertions in step 20..
SBY 15:55:25 [reg_ch0] engine_0: ##   0:01:03  waiting for solver (1 minute)
SBY 15:55:26 [pc_bwd_ch0] engine_0: ##   0:01:04  waiting for solver (1 minute)
SBY 15:55:26 [unique_ch0] engine_0: ##   0:01:04  waiting for solver (1 minute)
SBY 15:55:26 [pc_fwd_ch0] engine_0: ##   0:01:04  waiting for solver (1 minute)
SBY 15:55:26 [causal_ch0] engine_0: ##   0:01:04  waiting for solver (1 minute)
SBY 15:55:26 [liveness_ch0] engine_0: ##   0:01:04  waiting for solver (1 minute)
SBY 15:55:33 [insn_andi_ch0] engine_0: ##   0:01:12  Status: passed
SBY 15:55:33 [insn_andi_ch0] engine_0: finished (returncode=0)
SBY 15:55:33 [insn_andi_ch0] engine_0: Status returned by engine: pass
SBY 15:55:33 [insn_andi_ch0] summary: Elapsed clock time [H:MM:SS (secs)]: 0:01:16 (76)
SBY 15:55:33 [insn_andi_ch0] summary: Elapsed process time [H:MM:SS (secs)]: 0:01:16 (76)
SBY 15:55:33 [insn_andi_ch0] summary: engine_0 (smtbmc boolector) returned pass
SBY 15:55:33 [insn_andi_ch0] DONE (PASS, rc=0)
SBY 15:55:44 [insn_auipc_ch0] engine_0: ##   0:01:22  waiting for solver (1 minute)
SBY 15:55:47 [insn_addi_ch0] engine_0: ##   0:01:25  waiting for solver (1 minute)
SBY 15:55:50 [insn_bge_ch0] engine_0: ##   0:01:29  waiting for solver (1 minute)
SBY 15:55:53 [insn_add_ch0] engine_0: ##   0:01:31  waiting for solver (1 minute)
SBY 15:55:53 [insn_beq_ch0] engine_0: ##   0:01:31  waiting for solver (1 minute)
SBY 15:56:00 [insn_bgeu_ch0] engine_0: ##   0:01:24  waiting for solver (1 minute)
SBY 15:56:11 [insn_auipc_ch0] engine_0: ##   0:01:49  Status: passed
SBY 15:56:11 [insn_auipc_ch0] engine_0: finished (returncode=0)
SBY 15:56:11 [insn_auipc_ch0] engine_0: Status returned by engine: pass
SBY 15:56:11 [insn_auipc_ch0] summary: Elapsed clock time [H:MM:SS (secs)]: 0:01:54 (114)
SBY 15:56:11 [insn_auipc_ch0] summary: Elapsed process time [H:MM:SS (secs)]: 0:01:54 (114)
SBY 15:56:11 [insn_auipc_ch0] summary: engine_0 (smtbmc boolector) returned pass
SBY 15:56:11 [insn_auipc_ch0] DONE (PASS, rc=0)
SBY 15:56:12 [insn_and_ch0] engine_0: ##   0:01:50  Status: passed
SBY 15:56:12 [insn_and_ch0] engine_0: finished (returncode=0)
SBY 15:56:12 [insn_and_ch0] engine_0: Status returned by engine: pass
SBY 15:56:12 [insn_and_ch0] summary: Elapsed clock time [H:MM:SS (secs)]: 0:01:55 (115)
SBY 15:56:12 [insn_and_ch0] summary: Elapsed process time [H:MM:SS (secs)]: 0:01:55 (115)
SBY 15:56:12 [insn_and_ch0] summary: engine_0 (smtbmc boolector) returned pass
SBY 15:56:12 [insn_and_ch0] DONE (PASS, rc=0)
SBY 15:56:16 [reg_ch0] engine_0: ##   0:01:54  Checking assertions in step 25..
SBY 15:56:42 [insn_addi_ch0] engine_0: ##   0:02:20  Status: passed
SBY 15:56:42 [insn_addi_ch0] engine_0: finished (returncode=0)
SBY 15:56:42 [insn_addi_ch0] engine_0: Status returned by engine: pass
SBY 15:56:42 [insn_addi_ch0] summary: Elapsed clock time [H:MM:SS (secs)]: 0:02:25 (145)
SBY 15:56:42 [insn_addi_ch0] summary: Elapsed process time [H:MM:SS (secs)]: 0:02:25 (145)
SBY 15:56:42 [insn_addi_ch0] summary: engine_0 (smtbmc boolector) returned pass
SBY 15:56:42 [insn_addi_ch0] DONE (PASS, rc=0)
SBY 15:56:50 [insn_add_ch0] engine_0: ##   0:02:28  Status: passed
SBY 15:56:50 [insn_add_ch0] engine_0: finished (returncode=0)
SBY 15:56:50 [insn_add_ch0] engine_0: Status returned by engine: pass
SBY 15:56:50 [insn_add_ch0] summary: Elapsed clock time [H:MM:SS (secs)]: 0:02:33 (153)
SBY 15:56:50 [insn_add_ch0] summary: Elapsed process time [H:MM:SS (secs)]: 0:02:33 (153)
SBY 15:56:50 [insn_add_ch0] summary: engine_0 (smtbmc boolector) returned pass
SBY 15:56:50 [insn_add_ch0] DONE (PASS, rc=0)
SBY 15:56:51 [insn_beq_ch0] engine_0: ##   0:02:29  Status: passed
SBY 15:56:51 [insn_beq_ch0] engine_0: finished (returncode=0)
SBY 15:56:51 [insn_beq_ch0] engine_0: Status returned by engine: pass
SBY 15:56:51 [insn_beq_ch0] summary: Elapsed clock time [H:MM:SS (secs)]: 0:02:34 (154)
SBY 15:56:51 [insn_beq_ch0] summary: Elapsed process time [H:MM:SS (secs)]: 0:02:34 (154)
SBY 15:56:51 [insn_beq_ch0] summary: engine_0 (smtbmc boolector) returned pass
SBY 15:56:51 [insn_beq_ch0] DONE (PASS, rc=0)
SBY 15:56:53 [insn_bge_ch0] engine_0: ##   0:02:31  Status: passed
SBY 15:56:53 [insn_bge_ch0] engine_0: finished (returncode=0)
SBY 15:56:53 [insn_bge_ch0] engine_0: Status returned by engine: pass
SBY 15:56:53 [insn_bge_ch0] summary: Elapsed clock time [H:MM:SS (secs)]: 0:02:36 (156)
SBY 15:56:53 [insn_bge_ch0] summary: Elapsed process time [H:MM:SS (secs)]: 0:02:36 (156)
SBY 15:56:53 [insn_bge_ch0] summary: engine_0 (smtbmc boolector) returned pass
SBY 15:56:53 [insn_bge_ch0] DONE (PASS, rc=0)
SBY 15:56:56 [pc_fwd_ch0] engine_0: ##   0:02:34  Checking assertions in step 30..
SBY 15:57:02 [pc_fwd_ch0] engine_0: ##   0:02:40  Status: passed
SBY 15:57:02 [pc_fwd_ch0] engine_0: finished (returncode=0)
SBY 15:57:02 [pc_fwd_ch0] engine_0: Status returned by engine: pass
SBY 15:57:02 [pc_fwd_ch0] summary: Elapsed clock time [H:MM:SS (secs)]: 0:02:45 (165)
SBY 15:57:02 [pc_fwd_ch0] summary: Elapsed process time [H:MM:SS (secs)]: 0:02:45 (165)
SBY 15:57:02 [pc_fwd_ch0] summary: engine_0 (smtbmc boolector) returned pass
SBY 15:57:02 [pc_fwd_ch0] DONE (PASS, rc=0)
SBY 15:57:02 [causal_ch0] engine_0: ##   0:02:41  Checking assertions in step 30..
SBY 15:57:03 [causal_ch0] engine_0: ##   0:02:41  Status: passed
SBY 15:57:03 [causal_ch0] engine_0: finished (returncode=0)
SBY 15:57:03 [causal_ch0] engine_0: Status returned by engine: pass
SBY 15:57:03 [causal_ch0] summary: Elapsed clock time [H:MM:SS (secs)]: 0:02:46 (166)
SBY 15:57:03 [causal_ch0] summary: Elapsed process time [H:MM:SS (secs)]: 0:02:46 (166)
SBY 15:57:03 [causal_ch0] summary: engine_0 (smtbmc boolector) returned pass
SBY 15:57:03 [causal_ch0] DONE (PASS, rc=0)
SBY 15:57:09 [insn_bgeu_ch0] engine_0: ##   0:02:33  Status: passed
SBY 15:57:09 [insn_bgeu_ch0] engine_0: finished (returncode=0)
SBY 15:57:09 [insn_bgeu_ch0] engine_0: Status returned by engine: pass
SBY 15:57:09 [insn_bgeu_ch0] summary: Elapsed clock time [H:MM:SS (secs)]: 0:02:39 (159)
SBY 15:57:09 [insn_bgeu_ch0] summary: Elapsed process time [H:MM:SS (secs)]: 0:02:39 (159)
SBY 15:57:09 [insn_bgeu_ch0] summary: engine_0 (smtbmc boolector) returned pass
SBY 15:57:09 [insn_bgeu_ch0] DONE (PASS, rc=0)
SBY 15:57:11 [liveness_ch0] engine_0: ##   0:02:49  Checking assertions in step 30..
SBY 15:57:11 [liveness_ch0] engine_0: ##   0:02:49  Status: passed
SBY 15:57:11 [liveness_ch0] engine_0: finished (returncode=0)
SBY 15:57:11 [liveness_ch0] engine_0: Status returned by engine: pass
SBY 15:57:11 [liveness_ch0] summary: Elapsed clock time [H:MM:SS (secs)]: 0:02:54 (174)
SBY 15:57:11 [liveness_ch0] summary: Elapsed process time [H:MM:SS (secs)]: 0:02:54 (174)
SBY 15:57:11 [liveness_ch0] summary: engine_0 (smtbmc boolector) returned pass
SBY 15:57:11 [liveness_ch0] DONE (PASS, rc=0)
SBY 15:57:16 [reg_ch0] engine_0: ##   0:02:54  waiting for solver (1 minute)
SBY 15:57:39 [unique_ch0] engine_0: ##   0:03:17  Checking assertions in step 30..
SBY 15:57:39 [unique_ch0] engine_0: ##   0:03:17  Status: passed
SBY 15:57:39 [unique_ch0] engine_0: finished (returncode=0)
SBY 15:57:39 [unique_ch0] engine_0: Status returned by engine: pass
SBY 15:57:39 [unique_ch0] summary: Elapsed clock time [H:MM:SS (secs)]: 0:03:22 (202)
SBY 15:57:39 [unique_ch0] summary: Elapsed process time [H:MM:SS (secs)]: 0:03:22 (202)
SBY 15:57:39 [unique_ch0] summary: engine_0 (smtbmc boolector) returned pass
SBY 15:57:39 [unique_ch0] DONE (PASS, rc=0)
SBY 15:58:34 [pc_bwd_ch0] engine_0: ##   0:04:12  Checking assertions in step 30..
SBY 15:58:35 [pc_bwd_ch0] engine_0: ##   0:04:13  Status: passed
SBY 15:58:35 [pc_bwd_ch0] engine_0: finished (returncode=0)
SBY 15:58:35 [pc_bwd_ch0] engine_0: Status returned by engine: pass
SBY 15:58:35 [pc_bwd_ch0] summary: Elapsed clock time [H:MM:SS (secs)]: 0:04:18 (258)
SBY 15:58:35 [pc_bwd_ch0] summary: Elapsed process time [H:MM:SS (secs)]: 0:04:17 (257)
SBY 15:58:35 [pc_bwd_ch0] summary: engine_0 (smtbmc boolector) returned pass
SBY 15:58:35 [pc_bwd_ch0] DONE (PASS, rc=0)
SBY 16:01:16 [reg_ch0] engine_0: ##   0:06:54  waiting for solver (5 minutes)
SBY 16:06:16 [reg_ch0] engine_0: ##   0:11:54  waiting for solver (10 minutes)
SBY 16:11:16 [reg_ch0] engine_0: ##   0:16:54  waiting for solver (15 minutes)
SBY 16:26:16 [reg_ch0] engine_0: ##   0:31:54  waiting for solver (30 minutes)
SBY 16:39:44 [reg_ch0] engine_0: ##   0:45:22  Status: passed
SBY 16:39:44 [reg_ch0] engine_0: finished (returncode=0)
SBY 16:39:44 [reg_ch0] engine_0: Status returned by engine: pass
SBY 16:39:44 [reg_ch0] summary: Elapsed clock time [H:MM:SS (secs)]: 0:45:27 (2727)
SBY 16:39:44 [reg_ch0] summary: Elapsed process time [H:MM:SS (secs)]: 0:45:27 (2727)
SBY 16:39:44 [reg_ch0] summary: engine_0 (smtbmc boolector) returned pass
SBY 16:39:44 [reg_ch0] DONE (PASS, rc=0)
make: Leaving directory '/home/dsleung/riscv-formal/cores/picorv32/checks'