From 8b3ba688453c5d279e8e7ee75c7261649ba71ebe Mon Sep 17 00:00:00 2001
From: Claire Xenia Wolf <claire@clairexen.net>
Date: Wed, 7 Jun 2023 22:05:17 +0200
Subject: [PATCH 1/2] Add aigfolds option
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
---
sbysrc/sby_core.py | 3 ++-
sbysrc/sby_engine_abc.py | 2 +-
2 files changed, 3 insertions(+), 2 deletions(-)
diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py
index 1213fb7..48a4c2a 100644
--- a/sbysrc/sby_core.py
+++ b/sbysrc/sby_core.py
@@ -1154,7 +1154,7 @@ class SbyTask(SbyConfig):
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'""",
+ f"""cd {self.workdir}/model; {self.exe_paths["abc"]} -c 'read_aiger design_aiger.aig; fold{" -s" if self.opt_aigfolds else ""}; strash; write_aiger design_aiger_fold.aig'""",
logfile=open(f"{self.workdir}/model/design_aiger_fold.log", "w")
)
proc.checkretcode = True
@@ -1236,6 +1236,7 @@ class SbyTask(SbyConfig):
self.handle_bool_option("fst", False)
self.handle_bool_option("witrename", True)
+ self.handle_bool_option("aigfolds", False)
self.handle_bool_option("aigvmap", False)
self.handle_bool_option("aigsyms", False)
diff --git a/sbysrc/sby_engine_abc.py b/sbysrc/sby_engine_abc.py
index 1cb84b5..0f16fe4 100644
--- a/sbysrc/sby_engine_abc.py
+++ b/sbysrc/sby_engine_abc.py
@@ -66,7 +66,7 @@ def run(mode, task, engine_idx, engine):
task,
f"engine_{engine_idx}",
task.model("aig"),
- f"""cd {task.workdir}; {task.exe_paths["abc"]} -c 'read_aiger model/design_aiger.aig; fold; strash; {" ".join(abc_command)}; write_cex -a engine_{engine_idx}/trace.aiw'""",
+ f"""cd {task.workdir}; {task.exe_paths["abc"]} -c 'read_aiger model/design_aiger.aig; fold{" -s" if task.opt_aigfolds else ""}; strash; {" ".join(abc_command)}; write_cex -a engine_{engine_idx}/trace.aiw'""",
logfile=open(f"{task.workdir}/engine_{engine_idx}/logfile.txt", "w")
)
proc.checkretcode = True
From f692eff845693779cb53868b4d58b3c38c0ce0b9 Mon Sep 17 00:00:00 2001
From: Claire Xenia Wolf <claire@clairexen.net>
Date: Wed, 7 Jun 2023 22:21:06 +0200
Subject: [PATCH 2/2] Add support for "abc pdr -d" engine
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
---
sbysrc/sby_engine_abc.py | 6 ++++--
1 file changed, 4 insertions(+), 2 deletions(-)
diff --git a/sbysrc/sby_engine_abc.py b/sbysrc/sby_engine_abc.py
index 0f16fe4..639a7ff 100644
--- a/sbysrc/sby_engine_abc.py
+++ b/sbysrc/sby_engine_abc.py
@@ -42,7 +42,7 @@ def run(mode, task, engine_idx, engine):
elif abc_command[0] == "pdr":
if mode != "prove":
task.error("ABC command 'pdr' is only valid in prove mode.")
- abc_command[0] += f" -v"
+ abc_command[0] += f" -v -I engine_{engine_idx}/invariants.pla"
else:
task.error(f"Invalid ABC command {abc_command[0]}.")
@@ -66,7 +66,9 @@ def run(mode, task, engine_idx, engine):
task,
f"engine_{engine_idx}",
task.model("aig"),
- f"""cd {task.workdir}; {task.exe_paths["abc"]} -c 'read_aiger model/design_aiger.aig; fold{" -s" if task.opt_aigfolds else ""}; strash; {" ".join(abc_command)}; write_cex -a engine_{engine_idx}/trace.aiw'""",
+ f"""cd {task.workdir}; {task.exe_paths["abc"]} -c 'read_aiger model/design_aiger.aig; fold{
+ " -s" if task.opt_aigfolds or (abc_command[0].startswith("pdr ") and "-d" in abc_command[1:]) else ""
+ }; strash; {" ".join(abc_command)}; write_cex -a engine_{engine_idx}/trace.aiw'""",
logfile=open(f"{task.workdir}/engine_{engine_idx}/logfile.txt", "w")
)
proc.checkretcode = True