From 8b3ba688453c5d279e8e7ee75c7261649ba71ebe Mon Sep 17 00:00:00 2001 From: Claire Xenia Wolf Date: Wed, 7 Jun 2023 22:05:17 +0200 Subject: [PATCH 1/6] Add aigfolds option Signed-off-by: Claire Xenia Wolf --- 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 1213fb72..48a4c2a5 100644 --- 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 index 1cb84b50..0f16fe4d 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 Date: Wed, 7 Jun 2023 22:21:06 +0200 Subject: [PATCH 2/6] Add support for "abc pdr -d" engine Signed-off-by: Claire Xenia Wolf --- 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 0f16fe4d..639a7ffd 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 From 0d6a70e1376a2735835e50819fabcbc7304f6771 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Mon, 19 Jun 2023 11:21:49 +0200 Subject: [PATCH 3/6] autotune: Fix crash on no-engine error path --- sbysrc/sby_autotune.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/sbysrc/sby_autotune.py b/sbysrc/sby_autotune.py index 771a9a01..1d6f1020 100644 --- a/sbysrc/sby_autotune.py +++ b/sbysrc/sby_autotune.py @@ -402,7 +402,7 @@ def run(self): self.build_candidates() if not self.active_candidates: - self.error("no supported engines found for the current configuration and design") + self.task.error("no supported engines found for the current configuration and design") self.log(f"testing {len(self.active_candidates)} engine configurations...") self.start_engines() From 1a4c2a57ad44ba64c048f544cbff9f9833cafa97 Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Mon, 19 Jun 2023 21:39:07 +1200 Subject: [PATCH 4/6] Add sbysrc to path during docs build --- docs/source/conf.py | 6 ++++++ docs/source/usage.rst | 2 +- 2 files changed, 7 insertions(+), 1 deletion(-) diff --git a/docs/source/conf.py b/docs/source/conf.py index ad037b89..ebebcce6 100644 --- a/docs/source/conf.py +++ b/docs/source/conf.py @@ -1,4 +1,10 @@ #!/usr/bin/env python3 +import os +import sys + +sys.path += [os.path.join(os.path.dirname(__file__), + "..", "..", "sbysrc")] + project = 'YosysHQ SBY' author = 'YosysHQ GmbH' copyright = '2023 YosysHQ GmbH' diff --git a/docs/source/usage.rst b/docs/source/usage.rst index 5a3bf797..bc8e4e98 100644 --- a/docs/source/usage.rst +++ b/docs/source/usage.rst @@ -6,6 +6,6 @@ one of the available CAD suites, it can be called as follows. Note that this in available via `sby --help`. For more information on installation, see :ref:`install-doc`. .. argparse:: - :filename: ../sbysrc/sby_cmdline.py + :module: sby_cmdline :func: parser_func :prog: sby From 28c053bd948bf74bb77a92a303e2f59a2cd80ebc Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Fri, 23 Jun 2023 10:31:17 +0200 Subject: [PATCH 5/6] smtbmc: Allow using --keep-going in cover mode See YosysHQ/yosys#3816 for the smtbmc change that made --keep-going do something in cover mode --- sbysrc/sby_engine_smtbmc.py | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/sbysrc/sby_engine_smtbmc.py b/sbysrc/sby_engine_smtbmc.py index c5f348e3..7558c094 100644 --- a/sbysrc/sby_engine_smtbmc.py +++ b/sbysrc/sby_engine_smtbmc.py @@ -69,8 +69,6 @@ def run(mode, task, engine_idx, engine): task.error("smtbmc options --basecase and --induction are exclusive.") induction_only = True elif o == "--keep-going": - if mode not in ("bmc", "prove", "prove_basecase", "prove_induction"): - task.error("smtbmc option --keep-going is only supported in bmc and prove mode.") keep_going = True elif o == "--seed": random_seed = a @@ -134,7 +132,8 @@ def run(mode, task, engine_idx, engine): if keep_going and mode != "prove_induction": smtbmc_opts.append("--keep-going") - trace_prefix += "%" + if mode != "cover": + trace_prefix += "%" if dumpsmt2: smtbmc_opts += ["--dump-smt2", trace_prefix.replace("%", "") + ".smt2"] From edbc0548afbd12fcd16d7039f80071df72b33c42 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Mon, 17 Jul 2023 15:05:54 +0200 Subject: [PATCH 6/6] Fix deadlock with parallel SBY procs each with parallel tasks When multiple SBY processes run in parallel (from a Makefile or other job-server aware tool) and each SBY process runs tasks in parallel, each with enough tasks to be limited by the total job count, it is possible for the processes to race in such a way that every SBY process's helper process is in a blocking read from the job-server but a job-token would only become available as soon as any SBY process exits. In that situation SBY doesn't actually need the job-token anymore and only previously requested it as there was opportunity for parallelism. It would immediatly return the token as soon as it is acquired. That's usually sufficient to deal with no-longer-needed-but-requested tokens, but when SBY is done, it needs to return the job-token held by the parent process ASAP which it can only do by actually exiting, so we need to interrupt the blocking read of SBY's helper process. This could be done by sending a signal to the helper process, except that Python made the decision in 3.5 to have automatic EINTR retry loops around most system calls with no opt-out. That was part of the reason to go with this specifc helper process design that avoids interrupting a blocking read in the first place. Using an exception raised from the signal handler instead might lose a token when the signal arrives after the read returns, but before the token is stored in a variable. You cannot recover from a lost token in the context of the job-server protocol, so that's not an option. (This can't happen with recent Python versions but that would depend on undocumented behavior that could plausibly change again.) Thankfully the only case where we need to interrupt the read is when SBY is about to exit and will not request any further tokens. This allows us to use a signal handler that uses dup2 to close and replace the read-from fd with one that already is at EOF, making the next retry return immediatly. (If we'd need to interrupt a read and continue running we could also do this but the fd shuffling would be more involved.) --- sbysrc/sby_jobserver.py | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/sbysrc/sby_jobserver.py b/sbysrc/sby_jobserver.py index a3501335..57d751db 100644 --- a/sbysrc/sby_jobserver.py +++ b/sbysrc/sby_jobserver.py @@ -80,7 +80,16 @@ def process_jobserver_environment(): def jobserver_helper(jobserver_read_fd, jobserver_write_fd, request_fd, response_fd): """Helper process to handle blocking jobserver pipes.""" + def handle_sigusr1(*args): + # Since Python doesn't allow user code to handle EINTR anymore, we replace the + # jobserver fd with an fd at EOF to interrupt a blocking read in a way that + # cannot lose any read data + r, w = os.pipe() + os.close(w) + os.dup2(r, jobserver_read_fd) + os.close(r) signal.signal(signal.SIGINT, signal.SIG_IGN) + signal.signal(signal.SIGUSR1, handle_sigusr1) pending = 0 while True: try: @@ -110,6 +119,8 @@ def jobserver_helper(jobserver_read_fd, jobserver_write_fd, request_fd, response except BlockingIOError: select.select([jobserver_read_fd], [], []) continue + if not token: + break pending -= 1 @@ -240,6 +251,10 @@ def atexit_blocking(self): # Closing the request pipe singals the helper that we want to exit os.close(self.request_write_fd) + # Additionally we send a signal to interrupt a blocking read within the + # helper + self.helper_process.send_signal(signal.SIGUSR1) + # The helper might have been in the process of sending us some tokens, which # we still need to return while True: