complete.sby

[options]
mode bmc
aigsmt z3
depth 20

[engines]
abc bmc3

[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 -sv picorv32.v

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

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

[files]
complete.sv
../../../picorv32/picorv32.v
../../checks/rvfi_macros.vh
../../insns/isa_rv32ic.v

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