mirrors/sby
3
0
Fork 0
mirror of https://github.com/YosysHQ/sby.git synced 2025-04-23 05:15:30 +00:00
Code Activity

Support rIC3 as backend

Browse source 
Signed-off-by: Yuheng Su <gipsyh.icu@gmail.com>
This commit is contained in:
Yuheng Su 2024-12-16 11:02:45 +00:00
parent 26b387466d
commit daf4e4cb39
6 changed files with 19 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
sbysrc/sby_cmdline.py
View file

@ -49,6 +49,8 @@ def parser_func(release_version='unknown SBY version'):
action=DictAction, dest="exe_paths")
parser.add_argument("--avy", metavar="<path_to_executable>",
action=DictAction, dest="exe_paths")
parser.add_argument("--rIC3", metavar="<path_to_executable>",
action=DictAction, dest="exe_paths")
parser.add_argument("--btormc", metavar="<path_to_executable>",
action=DictAction, dest="exe_paths")
parser.add_argument("--pono", metavar="<path_to_executable>",

1
sbysrc/sby_core.py
View file

@ -849,6 +849,7 @@ class SbyTask(SbyConfig):
"suprove": os.getenv("SUPROVE", "suprove"),
"aigbmc": os.getenv("AIGBMC", "aigbmc"),
"avy": os.getenv("AVY", "avy"),
"rIC3": os.getenv("RIC3", "rIC3"),
"btormc": os.getenv("BTORMC", "btormc"),
"pono": os.getenv("PONO", "pono"),
"imctk-eqy-engine": os.getenv("IMCTK_EQY_ENGINE", "imctk-eqy-engine"),

7
sbysrc/sby_engine_aiger.py
View file

@ -46,6 +46,11 @@ def run(mode, task, engine_idx, engine):
if mode != "prove":
task.error("The aiger solver 'avy' is only supported in prove mode.")
solver_cmd = " ".join([task.exe_paths["avy"], "--cex", "-"] + solver_args[1:])
elif solver_args[0] == "rIC3":
if mode != "prove":
task.error("The aiger solver 'rIC3' is only supported in prove mode.")
solver_cmd = " ".join([task.exe_paths["rIC3"], "-v0", "--sby"] + solver_args[1:])
elif solver_args[0] == "aigbmc":
if mode != "bmc":
@ -87,7 +92,7 @@ def run(mode, task, engine_idx, engine):
f"cd {task.workdir}; {solver_cmd} model/design_aiger{model_variant}.aig",
logfile=open(f"{task.workdir}/engine_{engine_idx}/logfile.txt", "w")
)
if solver_args[0] not in ["avy"]:
if solver_args[0] not in ["avy", "rIC3"]:
proc.checkretcode = True
proc_status = None