[options]
mode prove
depth 10

[engines]
smtbmc bitwuzla

[script]
read -sv defines.sv rvfi_imem_check.sv imemcheck.sv nerv.sv
prep -flatten -nordff -top testbench
chformal -early

[files]
imemcheck.sv
nerv.sv
../../checks/rvfi_macros.vh
../../checks/rvfi_imem_check.sv

[file defines.sv]
`define RISCV_FORMAL
`define RISCV_FORMAL_NRET 1
`define RISCV_FORMAL_XLEN 32
`define RISCV_FORMAL_ILEN 32
`define NERV_RVFI
`define NERV_FAIRNESS  # Required to make k-induction work
`define RISCV_FORMAL_ALIGNED_MEM
`include "rvfi_macros.vh"