mirrors/sby
3
0
Fork 0
mirror of https://github.com/YosysHQ/sby.git synced 2026-01-18 10:18:59 +00:00
Code Activity

Fix rIC3 BMC command

Browse source
This commit is contained in:
Yuheng Su 2025-11-27 10:09:53 +08:00
parent cc84339b37
commit 3e906f8317
1 changed files with 9 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

10
sbysrc/sby_engine_aiger.py
View file

@ -53,7 +53,15 @@ def run(mode, task, engine_idx, engine):
if mode == "prove":
solver_cmd = " ".join([task.exe_paths["rIC3"], "--witness"] + solver_args[1:])
if mode == "bmc":
solver_cmd = " ".join([task.exe_paths["rIC3"], "--bmc-max-k {}".format(task.opt_depth - 1), "-e bmc", "-v 0", "--witness"] + solver_args[1:])
solver_cmd = " ".join(
[
task.exe_paths["rIC3"],
"-e bmc",
"--end {}".format(task.opt_depth - 1),
"--witness",
]
+ solver_args[1:]
)
status_2 = "PASS" # rIC3 outputs status 2 when BMC passes
elif solver_args[0] == "aigbmc":