mirrors/sby
3
0
Fork 0
mirror of https://github.com/YosysHQ/sby.git synced 2025-10-30 20:42:30 +00:00
Code Activity

aigbmc: Convert aiw trace to yw trace and load that into smtbmc

Browse source 
This handles more edge cases concerning FF initialization, memories and
hierarchy.
This commit is contained in:
Jannis Harder 2022-10-20 14:31:57 +02:00
parent 6995aaef78
commit 966bdae1f6
4 changed files with 43 additions and 35 deletions
Download patch file Download diff file Expand all files Collapse all files

2
sbysrc/sby.py
View file

@ -65,6 +65,8 @@ parser.add_argument("--abc", metavar="<path_to_executable>",
action=DictAction, dest="exe_paths")
parser.add_argument("--smtbmc", metavar="<path_to_executable>",
action=DictAction, dest="exe_paths")
parser.add_argument("--witness", metavar="<path_to_executable>",
action=DictAction, dest="exe_paths")
parser.add_argument("--suprove", metavar="<path_to_executable>",
action=DictAction, dest="exe_paths")
parser.add_argument("--aigbmc", metavar="<path_to_executable>",

1
sbysrc/sby_core.py
View file

@ -614,6 +614,7 @@ class SbyTask(SbyConfig):
"yosys": os.getenv("YOSYS", yosys_program_prefix + "yosys"),
"abc": os.getenv("ABC", yosys_program_prefix + "yosys-abc"),
"smtbmc": os.getenv("SMTBMC", yosys_program_prefix + "yosys-smtbmc"),
"witness": os.getenv("WITNESS", yosys_program_prefix + "yosys-witness"),
"suprove": os.getenv("SUPROVE", "suprove"),
"aigbmc": os.getenv("AIGBMC", "aigbmc"),
"avy": os.getenv("AVY", "avy"),

25
sbysrc/sby_engine_abc.py
View file

@ -90,19 +90,26 @@ def run(mode, task, engine_idx, engine):
if proc_status == "FAIL" and task.opt_aigsmt != "none":
trace_prefix = f"engine_{engine_idx}/trace"
dump_flags = f"--dump-vcd {trace_prefix}.vcd " if task.opt_vcd else ""
dump_flags += f"--dump-yw {trace_prefix}.yw --dump-vlogtb {trace_prefix}_tb.v --dump-smtc {trace_prefix}.smtc"
smtbmc_opts = []
smtbmc_opts += ["-s", task.opt_aigsmt]
if task.opt_tbtop is not None:
smtbmc_opts += ["--vlogtb-top", task.opt_tbtop]
smtbmc_opts += ["--noprogress", f"--append {task.opt_append}"]
if task.opt_vcd:
smtbmc_opts += [f"--dump-vcd {trace_prefix}.vcd"]
smtbmc_opts += [f"--dump-yw {trace_prefix}.yw", f"--dump-vlogtb {trace_prefix}_tb.v", f"--dump-smtc {trace_prefix}.smtc"]
witness_proc = SbyProc(
task, f"engine_{engine_idx}", [],
f"cd {task.workdir}; {task.exe_paths['witness']} aiw2yw engine_{engine_idx}/trace.aiw model/design_aiger.ywa engine_{engine_idx}/trace.yw",
)
proc2 = SbyProc(
task,
f"engine_{engine_idx}",
task.model("smt2"),
("cd {}; {} -s {}{} --noprogress --append {} {dump_flags} --aig model/design_aiger.aim:engine_{i}/trace.aiw --aig-noheader model/design_smt2.smt2").format
(task.workdir, task.exe_paths["smtbmc"], task.opt_aigsmt,
"" if task.opt_tbtop is None else f" --vlogtb-top {task.opt_tbtop}",
task.opt_append,
dump_flags=dump_flags,
i=engine_idx),
[*task.model("smt2"), witness_proc],
f"cd {task.workdir}; {task.exe_paths['smtbmc']} {' '.join(smtbmc_opts)} --yw engine_{engine_idx}/trace.yw model/design_smt2.smt2",
logfile=open(f"{task.workdir}/engine_{engine_idx}/logfile2.txt", "w")
)

50
sbysrc/sby_engine_aiger.py
View file

@ -106,34 +106,32 @@ def run(mode, task, engine_idx, engine):
if proc_status == "FAIL" and task.opt_aigsmt != "none":
if produced_cex:
trace_prefix = f"engine_{engine_idx}/trace"
dump_flags = f"--dump-vcd {trace_prefix}.vcd " if task.opt_vcd else ""
dump_flags += f"--dump-yw {trace_prefix}.yw --dump-vlogtb {trace_prefix}_tb.v --dump-smtc {trace_prefix}.smtc"
smtbmc_opts = []
if mode == "live":
proc2 = SbyProc(
task,
f"engine_{engine_idx}",
task.model("smt2"),
("cd {}; {} -g -s {}{} --noprogress {dump_flags} --aig model/design_aiger.aim:engine_{i}/trace.aiw model/design_smt2.smt2").format
(task.workdir, task.exe_paths["smtbmc"], task.opt_aigsmt,
"" if task.opt_tbtop is None else f" --vlogtb-top {task.opt_tbtop}",
dump_flags=dump_flags,
i=engine_idx),
logfile=open(f"{task.workdir}/engine_{engine_idx}/logfile2.txt", "w")
)
else:
proc2 = SbyProc(
task,
f"engine_{engine_idx}",
task.model("smt2"),
("cd {}; {} -s {}{} --noprogress --append {} {dump_flags} --aig model/design_aiger.aim:engine_{i}/trace.aiw model/design_smt2.smt2").format
(task.workdir, task.exe_paths["smtbmc"], task.opt_aigsmt,
"" if task.opt_tbtop is None else f" --vlogtb-top {task.opt_tbtop}",
task.opt_append,
dump_flags=dump_flags,
i=engine_idx),
logfile=open(f"{task.workdir}/engine_{engine_idx}/logfile2.txt", "w")
)
smtbmc_opts += ["-g"]
smtbmc_opts += ["-s", task.opt_aigsmt]
if task.opt_tbtop is not None:
smtbmc_opts += ["--vlogtb-top", task.opt_tbtop]
smtbmc_opts += ["--noprogress"]
if mode != "live":
smtbmc_opts += [f"--append {task.opt_append}"]
if task.opt_vcd:
smtbmc_opts += [f"--dump-vcd {trace_prefix}.vcd"]
smtbmc_opts += [f"--dump-yw {trace_prefix}.yw", f"--dump-vlogtb {trace_prefix}_tb.v", f"--dump-smtc {trace_prefix}.smtc"]
witness_proc = SbyProc(
task, f"engine_{engine_idx}", [],
f"cd {task.workdir}; {task.exe_paths['witness']} aiw2yw engine_{engine_idx}/trace.aiw model/design_aiger.ywa engine_{engine_idx}/trace.yw",
)
proc2 = SbyProc(
task,
f"engine_{engine_idx}",
[*task.model("smt2"), witness_proc],
f"cd {task.workdir}; {task.exe_paths['smtbmc']} {' '.join(smtbmc_opts)} --yw engine_{engine_idx}/trace.yw model/design_smt2.smt2",
logfile=open(f"{task.workdir}/engine_{engine_idx}/logfile2.txt", "w")
)
proc2_status = None