
[options]
mode bmc
depth 8

[engines]
smtbmc

[script]
read -sv -formal fwrisc.sv \
fwrisc_formal_tb.sv \
fwrisc_alu.sv \
fwrisc_comparator.sv \
fwrisc_dbus_if.sv \
fwrisc_regfile.sv \
fwrisc_formal_checker.sv
prep -top fwrisc_formal_tb

[files]
${FWRISC}/ve/fwrisc_formal/tb/fwrisc_formal_tb.sv
fwrisc_formal_checker.sv ${FWRISC}/ve/fwrisc_formal/tb/CHECKER.sv
fwrisc_instruction.svh ${FWRISC}/ve/fwrisc_formal/tests/INSTRUCTION.svh
${FWRISC}/ve/fwrisc_formal/tb/fwrisc_formal_opcode_defines.svh
${FWRISC}/rtl/fwrisc.sv
${FWRISC}/rtl/fwrisc_alu.sv
${FWRISC}/rtl/fwrisc_comparator.sv
${FWRISC}/rtl/fwrisc_dbus_if.sv
${FWRISC}/rtl/fwrisc_defines.vh
${FWRISC}/rtl/fwrisc_regfile.sv