Merge pull request #240 from YosysHQ/claire/aigfolds

Add "pdr -d" engine support (and aigfolds config option)
YosysHQ · Jun 28, 2023 · fbbbab2 · fbbbab2
2 parents 4d1ac01 + f692eff
commit fbbbab2
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 3 deletions.
diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py
@@ -1154,7 +1154,7 @@ def instance_hierarchy_error_callback(retcode):
                 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 @@ def handle_non_engine_options(self):
         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
@@ -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; 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