riscv
/
OpenFPGA
mirror of https://github.com/lnis-uofu/OpenFPGA.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

Added formal verification support to fpga_flow script

This commit is contained in:
ganeshgore 2020-04-15 12:24:51 -06:00
parent 80bdb41df6
commit 7f37bf1441
1 changed files with 12 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

14
openfpga_flow/scripts/run_fpga_flow.py
View File

@ -911,13 +911,23 @@ def run_netlists_verification(exit_if_fail=True):
command = [cad_tools["iverilog_path"]] command = [cad_tools["iverilog_path"]]
command += ["-o", compiled_file] command += ["-o", compiled_file]
command += ["./SRC/%s_include_netlists.v" % fpga_define_file = "./SRC/fpga_defines.v"
args.top_module] fpga_define_file_bk = "./SRC/fpga_defines.v.bak"
shutil.copy(fpga_define_file, fpga_define_file_bk)
with open(fpga_define_file, "r") as fp:
fpga_defines = fp.readlines()
command += ["./SRC/%s_include_netlists.v" % args.top_module]
command += ["-s"] command += ["-s"]
if args.vpr_fpga_verilog_formal_verification_top_netlist: if args.vpr_fpga_verilog_formal_verification_top_netlist:
command += [tb_top_formal] command += [tb_top_formal]
else: else:
command += [tb_top_autochecked] command += [tb_top_autochecked]
with open(fpga_define_file, "w") as fp:
for eachLine in fpga_defines:
if not (("ENABLE_FORMAL_VERIFICATION" in eachLine) or
"FORMAL_SIMULATION" in eachLine):
fp.write(eachLine)
run_command("iverilog_verification", "iverilog_output.txt", command) run_command("iverilog_verification", "iverilog_output.txt", command)
vvp_command = ["vvp", compiled_file] vvp_command = ["vvp", compiled_file]