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

avy: Fold aiger model using abc to support assumptions

Browse source
This commit is contained in:
Jannis Harder 2023-01-11 18:36:06 +01:00
parent 6398938e6a
commit f14aaa57c4
2 changed files with 17 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
sbysrc/sby_core.py
View file

@ -1146,6 +1146,18 @@ class SbyTask(SbyConfig):
return [proc] return [proc]
if model_name == "aig_fold":
proc = SbyProc(
self,
model_name,
self.model("aig"),
f"""cd {self.workdir}/model; {self.exe_paths["abc"]} -c 'read_aiger design_aiger.aig; fold; strash; write_aiger design_aiger_fold.aig'""",
logfile=open(f"{self.workdir}/model/design_aiger_fold.log", "w")
)
proc.checkretcode = True
return [proc]
self.error(f"Invalid model name: {model_name}") self.error(f"Invalid model name: {model_name}")
def model(self, model_name): def model(self, model_name):

7
sbysrc/sby_engine_aiger.py
View file

@ -31,6 +31,8 @@ def run(mode, task, engine_idx, engine):
status_2 = "UNKNOWN" status_2 = "UNKNOWN"
model_variant = ""
if solver_args[0] == "suprove": if solver_args[0] == "suprove":
if mode not in ["live", "prove"]: if mode not in ["live", "prove"]:
task.error("The aiger solver 'suprove' is only supported in live and prove modes.") task.error("The aiger solver 'suprove' is only supported in live and prove modes.")
@ -39,6 +41,7 @@ def run(mode, task, engine_idx, engine):
solver_cmd = " ".join([task.exe_paths["suprove"]] + solver_args[1:]) solver_cmd = " ".join([task.exe_paths["suprove"]] + solver_args[1:])
elif solver_args[0] == "avy": elif solver_args[0] == "avy":
model_variant = "_fold"
if mode != "prove": if mode != "prove":
task.error("The aiger solver 'avy' is only supported in prove mode.") task.error("The aiger solver 'avy' is only supported in prove mode.")
solver_cmd = " ".join([task.exe_paths["avy"], "--cex", "-"] + solver_args[1:]) solver_cmd = " ".join([task.exe_paths["avy"], "--cex", "-"] + solver_args[1:])
@ -71,8 +74,8 @@ def run(mode, task, engine_idx, engine):
proc = SbyProc( proc = SbyProc(
task, task,
f"engine_{engine_idx}", f"engine_{engine_idx}",
task.model("aig"), task.model(f"aig{model_variant}"),
f"cd {task.workdir}; {solver_cmd} model/design_aiger.aig", f"cd {task.workdir}; {solver_cmd} model/design_aiger{model_variant}.aig",
logfile=open(f"{task.workdir}/engine_{engine_idx}/logfile.txt", "w") 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"]: