complete.sby

[options]
mode bmc
# aigsmt z3
depth 5

[engines]
# abc bmc3
smtbmc boolector

[script]
verilog_defines -D DEBUGNETS
verilog_defines -D RISCV_FORMAL
verilog_defines -D RISCV_FORMAL_NRET=1
verilog_defines -D RISCV_FORMAL_XLEN=32
verilog_defines -D RISCV_FORMAL_ILEN=32
# verilog_defines -D RISCV_FORMAL_COMPRESSED
# verilog_defines -D RISCV_FORMAL_ALIGNED_MEM
read_verilog -sv rvfi_macros.vh
read_verilog minlib.v
read_verilog comb_rv32.v
read_verilog -sv minrv32.v

--pycode-begin--
with open("../../riscv-formal/insns/isa_rv32i.txt") as f:
  for line in f:
    output("read_verilog -sv insn_%s.v" % line.strip())
--pycode-end--

read_verilog -sv isa_rv32i.v
read_verilog -sv complete.sv
prep -nordff -top testbench

[files]
complete.sv
../minlib.v
../comb_rv32.v
../minrv32.v
../../riscv-formal/checks/rvfi_macros.vh
../../riscv-formal/insns/isa_rv32i.v

--pycode-begin--
with open("../../riscv-formal/insns/isa_rv32i.txt") as f:
  for line in f:
    output("../../riscv-formal/insns/insn_%s.v" % line.strip())
--pycode-end--