From 513d0d42880af41f5aac0848c7008ed3a4ad7644 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Wed, 3 May 2023 16:56:09 +0200 Subject: [PATCH 01/12] Change Sphinx theme to "furo" --- docs/source/_templates/page.html | 43 +++++++++++++++++++++ docs/source/conf.py | 35 +++++++++++------ docs/source/requirements.txt | 2 +- docs/static/custom.css | 19 +++++++++- docs/static/yosyshq.css | 64 -------------------------------- 5 files changed, 86 insertions(+), 77 deletions(-) create mode 100644 docs/source/_templates/page.html delete mode 100644 docs/static/yosyshq.css diff --git a/docs/source/_templates/page.html b/docs/source/_templates/page.html new file mode 100644 index 0000000..de334e7 --- /dev/null +++ b/docs/source/_templates/page.html @@ -0,0 +1,43 @@ +{# + +See https://github.com/pradyunsg/furo/blob/main/src/furo/theme/furo/page.html for the original +block this is overwriting. + +The part that is customized is between the "begin of custom part" and "end of custom part" +comments below. It uses the same styles as the existing right sidebar code. + +#} +{% extends "furo/page.html" %} +{% block right_sidebar %} +
+ {# begin of custom part #} +
+ + YosysHQ + +
+
+
+ +
+
+ {# end of custom part #} + {% if not furo_hide_toc %} +
+ + {{ _("On this page") }} + +
+
+
+ {{ toc }} +
+
+ {% endif %} +
+{% endblock %} diff --git a/docs/source/conf.py b/docs/source/conf.py index 1d4cbeb..d85e198 100644 --- a/docs/source/conf.py +++ b/docs/source/conf.py @@ -1,28 +1,41 @@ #!/usr/bin/env python3 project = 'YosysHQ SBY' author = 'YosysHQ GmbH' -copyright ='2021 YosysHQ GmbH' +copyright = '2023 YosysHQ GmbH' # select HTML theme -html_theme = 'press' + +templates_path = ["_templates"] +html_theme = "furo" html_logo = '../static/logo.png' html_favicon = '../static/favico.png' -html_css_files = ['yosyshq.css', 'custom.css'] -html_sidebars = {'**': ['util/searchbox.html', 'util/sidetoc.html']} +html_css_files = ['custom.css'] # These folders are copied to the documentation's HTML output -html_static_path = ['../static', "../images"] +html_static_path = ['../static'] -# code blocks style +# code blocks style pygments_style = 'colorful' highlight_language = 'systemverilog' html_theme_options = { - 'external_links' : [ - ('YosysHQ Docs', 'https://yosyshq.readthedocs.io'), - ('Blog', 'https://blog.yosyshq.com'), - ('Website', 'https://www.yosyshq.com'), - ], + "sidebar_hide_name": True, + + "light_css_variables": { + "color-brand-primary": "#d6368f", + "color-brand-content": "#4b72b8", + "color-api-name": "#8857a3", + "color-api-pre-name": "#4b72b8", + "color-link": "#8857a3", + }, + + "dark_css_variables": { + "color-brand-primary": "#e488bb", + "color-brand-content": "#98bdff", + "color-api-name": "#8857a3", + "color-api-pre-name": "#4b72b8", + "color-link": "#be95d5", + }, } extensions = ['sphinx.ext.autosectionlabel'] diff --git a/docs/source/requirements.txt b/docs/source/requirements.txt index 954b454..a95ae18 100644 --- a/docs/source/requirements.txt +++ b/docs/source/requirements.txt @@ -1 +1 @@ -sphinx-press-theme +furo diff --git a/docs/static/custom.css b/docs/static/custom.css index 40a8c17..b23ce2d 100644 --- a/docs/static/custom.css +++ b/docs/static/custom.css @@ -1 +1,18 @@ -/* empty */ +/* Don't hide the right sidebar as we're placing our fixed links there */ +aside.no-toc { + display: block !important; +} + +/* Colorful headings */ +h1 { + color: var(--color-brand-primary); +} + +h2, h3, h4, h5, h6 { + color: var(--color-brand-content); +} + +/* Use a different color for external links */ +a.external { + color: var(--color-brand-primary) !important; +} diff --git a/docs/static/yosyshq.css b/docs/static/yosyshq.css deleted file mode 100644 index 1ceebe9..0000000 --- a/docs/static/yosyshq.css +++ /dev/null @@ -1,64 +0,0 @@ -h1, h3, p.topic-title, .content li.toctree-l1 > a { - color: #d6368f !important; -} - -h2, p.admonition-title, dt, .content li.toctree-l2 > a { - color: #4b72b8; -} - -a { - color: #8857a3; -} - -a.current, a:hover, a.external { - color: #d6368f !important; -} - -a.external:hover { - text-decoration: underline; -} - -p { - text-align: justify; -} - -.vp-sidebar a { - color: #d6368f; -} - -.vp-sidebar li li a { - color: #4b72b8; -} - -.vp-sidebar li li li a { - color: #2c3e50; - font-weight: 400; -} - -.vp-sidebar h3 { - padding-left: 1.5rem !important; -} - -.vp-sidebar ul a { - padding-left: 1.5rem !important; -} - -.vp-sidebar ul ul a { - padding-left: 3rem !important; -} - -.vp-sidebar ul ul ul a { - padding-left: 4.5rem !important; -} - -.vp-sidebar .toctree-l1.current a { - border-left: 0.5rem solid #6ecbd7; -} - -.vp-sidebar .toctree-l1 a.current { - border-left: 0.5rem solid #8857a3; -} - -.injected .rst-current-version, .injected dt { - color: #6ecbd7 !important; -} From cb968ea2bbe735eaef34245ee9c5c7b431f63ba8 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Mon, 8 May 2023 11:33:14 +0200 Subject: [PATCH 02/12] Update .readthedocs.yaml --- .readthedocs.yaml | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/.readthedocs.yaml b/.readthedocs.yaml index c42f473..b72a370 100644 --- a/.readthedocs.yaml +++ b/.readthedocs.yaml @@ -3,6 +3,11 @@ version: 2 +build: + os: ubuntu-22.04 + tools: + python: '3.11' + formats: - pdf From f49c9ebb290728f9a22943d512123e4ca2485088 Mon Sep 17 00:00:00 2001 From: Claire Xenia Wolf Date: Fri, 2 Jun 2023 13:04:45 +0200 Subject: [PATCH 03/12] Make call to "witness -rename" optional (default=on) Signed-off-by: Claire Xenia Wolf --- sbysrc/sby_core.py | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py index b27d1a5..820f6fb 100644 --- a/sbysrc/sby_core.py +++ b/sbysrc/sby_core.py @@ -1002,8 +1002,9 @@ class SbyTask(SbyConfig): print("check", file=f) # can't detect undriven wires past this point print("setundef -undriven -anyseq", file=f) print("opt -fast", file=f) - print("rename -witness", file=f) - print("opt_clean", file=f) + if self.opt_witrename: + print("rename -witness", file=f) + print("opt_clean", file=f) print(f"""write_rtlil ../model/design_prep.il""", file=f) proc = SbyProc( @@ -1233,6 +1234,8 @@ class SbyTask(SbyConfig): self.handle_bool_option("vcd_sim", False) self.handle_bool_option("fst", False) + self.handle_bool_option("witrename", True) + self.handle_str_option("smtc", None) self.handle_int_option("skip", None) self.handle_str_option("tbtop", None) From 7d60a3ba349db82f401093e767faa428dd653376 Mon Sep 17 00:00:00 2001 From: Claire Xenia Wolf Date: Sat, 3 Jun 2023 22:16:35 +0200 Subject: [PATCH 04/12] Add aigvmap and aigsyms options Signed-off-by: Claire Xenia Wolf --- sbysrc/sby_core.py | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py index 820f6fb..1213fb7 100644 --- a/sbysrc/sby_core.py +++ b/sbysrc/sby_core.py @@ -1136,7 +1136,8 @@ class SbyTask(SbyConfig): print("abc -g AND -fast", file=f) print("opt_clean", file=f) print("stat", file=f) - print("write_aiger -I -B -zinit -no-startoffset -map design_aiger.aim -ywmap design_aiger.ywa design_aiger.aig", file=f) + print(f"write_aiger -I -B -zinit -no-startoffset {'-vmap' if self.opt_aigvmap else '-map'} design_aiger.aim" + + f"{' -symbols' if self.opt_aigsyms else ''} -ywmap design_aiger.ywa design_aiger.aig", file=f) proc = SbyProc( self, @@ -1235,6 +1236,8 @@ class SbyTask(SbyConfig): self.handle_bool_option("fst", False) self.handle_bool_option("witrename", True) + self.handle_bool_option("aigvmap", False) + self.handle_bool_option("aigsyms", False) self.handle_str_option("smtc", None) self.handle_int_option("skip", None) From 8b3ba688453c5d279e8e7ee75c7261649ba71ebe Mon Sep 17 00:00:00 2001 From: Claire Xenia Wolf Date: Wed, 7 Jun 2023 22:05:17 +0200 Subject: [PATCH 05/12] 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 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 Date: Wed, 7 Jun 2023 22:21:06 +0200 Subject: [PATCH 06/12] 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 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 From 27e20fd5c31fc1638b9424841197cf24862a4d0a Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Tue, 13 Jun 2023 11:40:28 +1200 Subject: [PATCH 07/12] Add sphinx-argparse to generate usage Move parser generation into a seperate file to avoid import issues with bad python modules during docs gen. With the requirements.txt provided to readthedocs, there shouldn't need to be any other changes? Also I've never been able to run `make test` so I'm not actually sure if the changes break sby, but they shouldn't. --- docs/source/conf.py | 1 + docs/source/index.rst | 1 + docs/source/requirements.txt | 1 + docs/source/usage.rst | 11 +++++ sbysrc/sby.py | 78 ++--------------------------------- sbysrc/sby_cmdline.py | 79 ++++++++++++++++++++++++++++++++++++ 6 files changed, 96 insertions(+), 75 deletions(-) create mode 100644 docs/source/usage.rst create mode 100644 sbysrc/sby_cmdline.py diff --git a/docs/source/conf.py b/docs/source/conf.py index d85e198..ad037b8 100644 --- a/docs/source/conf.py +++ b/docs/source/conf.py @@ -39,3 +39,4 @@ html_theme_options = { } extensions = ['sphinx.ext.autosectionlabel'] +extensions += ['sphinxarg.ext'] diff --git a/docs/source/index.rst b/docs/source/index.rst index fbe43c5..ab67043 100644 --- a/docs/source/index.rst +++ b/docs/source/index.rst @@ -16,6 +16,7 @@ formal tasks: install.rst quickstart.rst + usage.rst reference.rst autotune.rst verilog.rst diff --git a/docs/source/requirements.txt b/docs/source/requirements.txt index a95ae18..0e4756e 100644 --- a/docs/source/requirements.txt +++ b/docs/source/requirements.txt @@ -1 +1,2 @@ furo +sphinx-argparse diff --git a/docs/source/usage.rst b/docs/source/usage.rst new file mode 100644 index 0000000..5a3bf79 --- /dev/null +++ b/docs/source/usage.rst @@ -0,0 +1,11 @@ +Using `sby` +=========== + +Once SBY is installed and available on the command line as `sby`, either built from source or using +one of the available CAD suites, it can be called as follows. Note that this information is also +available via `sby --help`. For more information on installation, see :ref:`install-doc`. + +.. argparse:: + :filename: ../sbysrc/sby_cmdline.py + :func: parser_func + :prog: sby diff --git a/sbysrc/sby.py b/sbysrc/sby.py index 20ae345..986fb9d 100644 --- a/sbysrc/sby.py +++ b/sbysrc/sby.py @@ -17,88 +17,16 @@ # OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. # -import argparse, json, os, sys, shutil, tempfile, re +import json, os, sys, shutil, tempfile, re ##yosys-sys-path## +from sby_cmdline import parser_func from sby_core import SbyConfig, SbyTask, SbyAbort, SbyTaskloop, process_filename, dress_message from sby_jobserver import SbyJobClient, process_jobserver_environment import time, platform, click process_jobserver_environment() # needs to be called early -class DictAction(argparse.Action): - def __call__(self, parser, namespace, values, option_string=None): - assert isinstance(getattr(namespace, self.dest), dict), f"Use ArgumentParser.set_defaults() to initialize {self.dest} to dict()" - name = option_string.lstrip(parser.prefix_chars).replace("-", "_") - getattr(namespace, self.dest)[name] = values - -parser = argparse.ArgumentParser(prog="sby", - usage="%(prog)s [options] [.sby [tasknames] | ]") -parser.set_defaults(exe_paths=dict()) - -parser.add_argument("-d", metavar="", dest="workdir", - help="set workdir name. default: or _. When there is more than one task, use --prefix instead") -parser.add_argument("--prefix", metavar="", dest="workdir_prefix", - help="set the workdir name prefix. `_` will be appended to the path for each task") -parser.add_argument("-f", action="store_true", dest="force", - help="remove workdir if it already exists") -parser.add_argument("-b", action="store_true", dest="backup", - help="backup workdir if it already exists") -parser.add_argument("-t", action="store_true", dest="tmpdir", - help="run in a temporary workdir (remove when finished)") -parser.add_argument("-T", metavar="", action="append", dest="tasknames", default=list(), - help="add taskname (useful when sby file is read from stdin)") -parser.add_argument("-E", action="store_true", dest="throw_err", - help="throw an exception (incl stack trace) for most errors") -parser.add_argument("-j", metavar="", type=int, dest="jobcount", - help="maximum number of processes to run in parallel") -parser.add_argument("--sequential", action="store_true", dest="sequential", - help="run tasks in sequence, not in parallel") - -parser.add_argument("--autotune", action="store_true", dest="autotune", - help="automatically find a well performing engine and engine configuration for each task") -parser.add_argument("--autotune-config", dest="autotune_config", - help="read an autotune configuration file (overrides the sby file's autotune options)") - -parser.add_argument("--yosys", metavar="", - action=DictAction, dest="exe_paths") -parser.add_argument("--abc", metavar="", - action=DictAction, dest="exe_paths") -parser.add_argument("--smtbmc", metavar="", - action=DictAction, dest="exe_paths") -parser.add_argument("--witness", metavar="", - action=DictAction, dest="exe_paths") -parser.add_argument("--suprove", metavar="", - action=DictAction, dest="exe_paths") -parser.add_argument("--aigbmc", metavar="", - action=DictAction, dest="exe_paths") -parser.add_argument("--avy", metavar="", - action=DictAction, dest="exe_paths") -parser.add_argument("--btormc", metavar="", - action=DictAction, dest="exe_paths") -parser.add_argument("--pono", metavar="", - action=DictAction, dest="exe_paths", - help="configure which executable to use for the respective tool") -parser.add_argument("--dumpcfg", action="store_true", dest="dump_cfg", - help="print the pre-processed configuration file") -parser.add_argument("--dumptags", action="store_true", dest="dump_tags", - help="print the list of task tags") -parser.add_argument("--dumptasks", action="store_true", dest="dump_tasks", - help="print the list of tasks") -parser.add_argument("--dumpdefaults", action="store_true", dest="dump_defaults", - help="print the list of default tasks") -parser.add_argument("--dumptaskinfo", action="store_true", dest="dump_taskinfo", - help="output a summary of tasks as JSON") -parser.add_argument("--dumpfiles", action="store_true", dest="dump_files", - help="print the list of source files") -parser.add_argument("--setup", action="store_true", dest="setupmode", - help="set up the working directory and exit") - -parser.add_argument("--init-config-file", dest="init_config_file", - help="create a default .sby config file") -parser.add_argument("sbyfile", metavar=".sby | ", nargs="?", - help=".sby file OR directory containing config.sby file") -parser.add_argument("arg_tasknames", metavar="tasknames", nargs="*", - help="tasks to run (only valid when .sby is used)") +parser = parser_func() args = parser.parse_args() diff --git a/sbysrc/sby_cmdline.py b/sbysrc/sby_cmdline.py new file mode 100644 index 0000000..a75c273 --- /dev/null +++ b/sbysrc/sby_cmdline.py @@ -0,0 +1,79 @@ +import argparse + +class DictAction(argparse.Action): + def __call__(self, parser, namespace, values, option_string=None): + assert isinstance(getattr(namespace, self.dest), dict), f"Use ArgumentParser.set_defaults() to initialize {self.dest} to dict()" + name = option_string.lstrip(parser.prefix_chars).replace("-", "_") + getattr(namespace, self.dest)[name] = values + +def parser_func(): + parser = argparse.ArgumentParser(prog="sby", + usage="%(prog)s [options] [.sby [tasknames] | ]") + parser.set_defaults(exe_paths=dict()) + + parser.add_argument("-d", metavar="", dest="workdir", + help="set workdir name. default: or _. When there is more than one task, use --prefix instead") + parser.add_argument("--prefix", metavar="", dest="workdir_prefix", + help="set the workdir name prefix. `_` will be appended to the path for each task") + parser.add_argument("-f", action="store_true", dest="force", + help="remove workdir if it already exists") + parser.add_argument("-b", action="store_true", dest="backup", + help="backup workdir if it already exists") + parser.add_argument("-t", action="store_true", dest="tmpdir", + help="run in a temporary workdir (remove when finished)") + parser.add_argument("-T", metavar="", action="append", dest="tasknames", default=list(), + help="add taskname (useful when sby file is read from stdin)") + parser.add_argument("-E", action="store_true", dest="throw_err", + help="throw an exception (incl stack trace) for most errors") + parser.add_argument("-j", metavar="", type=int, dest="jobcount", + help="maximum number of processes to run in parallel") + parser.add_argument("--sequential", action="store_true", dest="sequential", + help="run tasks in sequence, not in parallel") + + parser.add_argument("--autotune", action="store_true", dest="autotune", + help="automatically find a well performing engine and engine configuration for each task") + parser.add_argument("--autotune-config", dest="autotune_config", + help="read an autotune configuration file (overrides the sby file's autotune options)") + + parser.add_argument("--yosys", metavar="", + action=DictAction, dest="exe_paths") + parser.add_argument("--abc", metavar="", + action=DictAction, dest="exe_paths") + parser.add_argument("--smtbmc", metavar="", + action=DictAction, dest="exe_paths") + parser.add_argument("--witness", metavar="", + action=DictAction, dest="exe_paths") + parser.add_argument("--suprove", metavar="", + action=DictAction, dest="exe_paths") + parser.add_argument("--aigbmc", metavar="", + action=DictAction, dest="exe_paths") + parser.add_argument("--avy", metavar="", + action=DictAction, dest="exe_paths") + parser.add_argument("--btormc", metavar="", + action=DictAction, dest="exe_paths") + parser.add_argument("--pono", metavar="", + action=DictAction, dest="exe_paths", + help="configure which executable to use for the respective tool") + parser.add_argument("--dumpcfg", action="store_true", dest="dump_cfg", + help="print the pre-processed configuration file") + parser.add_argument("--dumptags", action="store_true", dest="dump_tags", + help="print the list of task tags") + parser.add_argument("--dumptasks", action="store_true", dest="dump_tasks", + help="print the list of tasks") + parser.add_argument("--dumpdefaults", action="store_true", dest="dump_defaults", + help="print the list of default tasks") + parser.add_argument("--dumptaskinfo", action="store_true", dest="dump_taskinfo", + help="output a summary of tasks as JSON") + parser.add_argument("--dumpfiles", action="store_true", dest="dump_files", + help="print the list of source files") + parser.add_argument("--setup", action="store_true", dest="setupmode", + help="set up the working directory and exit") + + parser.add_argument("--init-config-file", dest="init_config_file", + help="create a default .sby config file") + parser.add_argument("sbyfile", metavar=".sby | ", nargs="?", + help=".sby file OR directory containing config.sby file") + parser.add_argument("arg_tasknames", metavar="tasknames", nargs="*", + help="tasks to run (only valid when .sby is used)") + + return parser From 0d6a70e1376a2735835e50819fabcbc7304f6771 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Mon, 19 Jun 2023 11:21:49 +0200 Subject: [PATCH 08/12] 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 771a9a0..1d6f102 100644 --- a/sbysrc/sby_autotune.py +++ b/sbysrc/sby_autotune.py @@ -402,7 +402,7 @@ class SbyAutotune: 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 09/12] 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 ad037b8..ebebcce 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 5a3bf79..bc8e4e9 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 c52acf2a1fb4ac863d664f5b5f6e7cdbd4c5f7dc Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Mon, 19 Jun 2023 11:39:37 +0200 Subject: [PATCH 10/12] docs: Make sphinx-argparse work independently of sphinx's cwd --- docs/source/conf.py | 5 +++++ docs/source/usage.rst | 2 +- 2 files changed, 6 insertions(+), 1 deletion(-) diff --git a/docs/source/conf.py b/docs/source/conf.py index ad037b8..81d249c 100644 --- a/docs/source/conf.py +++ b/docs/source/conf.py @@ -1,4 +1,7 @@ #!/usr/bin/env python3 +import sys +import os + project = 'YosysHQ SBY' author = 'YosysHQ GmbH' copyright = '2023 YosysHQ GmbH' @@ -40,3 +43,5 @@ html_theme_options = { extensions = ['sphinx.ext.autosectionlabel'] extensions += ['sphinxarg.ext'] + +sys.path.append(os.path.abspath(f"{__file__}/../../../sbysrc")) diff --git a/docs/source/usage.rst b/docs/source/usage.rst index 5a3bf79..bc8e4e9 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 11/12] 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 c5f348e..7558c09 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 12/12] 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 a350133..57d751d 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 @@ class SbyJobClient: # 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: