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 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..e18817c 100644 --- a/docs/source/conf.py +++ b/docs/source/conf.py @@ -1,28 +1,47 @@ #!/usr/bin/env python3 +import sys +import os + +sys.path.append(os.path.abspath(f"{__file__}/../../../sbysrc")) + 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'] +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 954b454..0e4756e 100644 --- a/docs/source/requirements.txt +++ b/docs/source/requirements.txt @@ -1 +1,2 @@ -sphinx-press-theme +furo +sphinx-argparse diff --git a/docs/source/usage.rst b/docs/source/usage.rst new file mode 100644 index 0000000..bc8e4e9 --- /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:: + :module: sby_cmdline + :func: parser_func + :prog: sby 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; -} 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_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() 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 diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py index bd62317..ecd901c 100644 --- a/sbysrc/sby_core.py +++ b/sbysrc/sby_core.py @@ -1003,8 +1003,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( @@ -1136,7 +1137,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, @@ -1153,7 +1155,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 @@ -1234,6 +1236,11 @@ class SbyTask(SbyConfig): self.handle_bool_option("vcd_sim", False) 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) + self.handle_str_option("smtc", None) self.handle_int_option("skip", None) self.handle_str_option("tbtop", None) diff --git a/sbysrc/sby_engine_abc.py b/sbysrc/sby_engine_abc.py index 1cb84b5..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; 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 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"] 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: