Merge branch 'master' into krys/scy_dev

.readthedocs.yaml

@@ -3,6 +3,11 @@
 
 version: 2
 
+build:
+    os: ubuntu-22.04
+    tools:
+        python: '3.11'
+
 formats:
   - pdf
 

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 %}
+<div class="toc-sticky toc-scroll">
+  {# begin of custom part #}
+  <div class="toc-title-container">
+    <span class="toc-title">
+      YosysHQ
+    </span>
+  </div>
+  <div class="toc-tree-container yosyshq-links" style="padding-bottom: 0">
+    <div class="toc-tree">
+      <ul>
+        <li></li>
+        <li><a class="reference external" href="https://yosyshq.readthedocs.io">Docs</a></li>
+        <li><a class="reference external" href="https://blog.yosyshq.com">Blog</a></li>
+        <li><a class="reference external" href="https://www.yosyshq.com">Website</a></li>
+      </ul>
+    </div>
+  </div>
+  {# end of custom part #}
+  {% if not furo_hide_toc %}
+  <div class="toc-title-container">
+    <span class="toc-title">
+      {{ _("On this page") }}
+    </span>
+  </div>
+  <div class="toc-tree-container">
+    <div class="toc-tree">
+      {{ toc }}
+    </div>
+  </div>
+  {% endif %}
+</div>
+{% endblock %}

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_css_files = ['custom.css']
-html_sidebars = {'**': ['util/searchbox.html', 'util/sidetoc.html']}
 
 # 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' : [
+    "sidebar_hide_name": True,
-        ('YosysHQ Docs', 'https://yosyshq.readthedocs.io'),
+
-        ('Blog', 'https://blog.yosyshq.com'),
+    "light_css_variables": {
-        ('Website', 'https://www.yosyshq.com'),
+        "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']

docs/source/index.rst

@@ -16,6 +16,7 @@ formal tasks:
 
    install.rst
    quickstart.rst
+   usage.rst
    reference.rst
    autotune.rst
    verilog.rst

docs/source/requirements.txt

@@ -1 +1,2 @@
-sphinx-press-theme
+furo
+sphinx-argparse

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

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;
+}

docs/static/yosyshq.css

@@ -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;
-}

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):
+parser = parser_func()
-    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] [<jobname>.sby [tasknames] | <dirname>]")
-parser.set_defaults(exe_paths=dict())
-
-parser.add_argument("-d", metavar="<dirname>", dest="workdir",
-        help="set workdir name. default: <jobname> or <jobname>_<taskname>. When there is more than one task, use --prefix instead")
-parser.add_argument("--prefix", metavar="<dirname>", dest="workdir_prefix",
-        help="set the workdir name prefix. `_<taskname>` 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="<taskname>", 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="<N>", 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="<path_to_executable>",
-        action=DictAction, dest="exe_paths")
-parser.add_argument("--abc", metavar="<path_to_executable>",
-        action=DictAction, dest="exe_paths")
-parser.add_argument("--smtbmc", metavar="<path_to_executable>",
-        action=DictAction, dest="exe_paths")
-parser.add_argument("--witness", metavar="<path_to_executable>",
-        action=DictAction, dest="exe_paths")
-parser.add_argument("--suprove", metavar="<path_to_executable>",
-        action=DictAction, dest="exe_paths")
-parser.add_argument("--aigbmc", metavar="<path_to_executable>",
-        action=DictAction, dest="exe_paths")
-parser.add_argument("--avy", metavar="<path_to_executable>",
-        action=DictAction, dest="exe_paths")
-parser.add_argument("--btormc", metavar="<path_to_executable>",
-        action=DictAction, dest="exe_paths")
-parser.add_argument("--pono", metavar="<path_to_executable>",
-        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="<jobname>.sby | <dirname>", 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 <jobname>.sby is used)")
 
 args = parser.parse_args()
 

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()

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] [<jobname>.sby [tasknames] | <dirname>]")
+    parser.set_defaults(exe_paths=dict())
+
+    parser.add_argument("-d", metavar="<dirname>", dest="workdir",
+            help="set workdir name. default: <jobname> or <jobname>_<taskname>. When there is more than one task, use --prefix instead")
+    parser.add_argument("--prefix", metavar="<dirname>", dest="workdir_prefix",
+            help="set the workdir name prefix. `_<taskname>` 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="<taskname>", 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="<N>", 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="<path_to_executable>",
+            action=DictAction, dest="exe_paths")
+    parser.add_argument("--abc", metavar="<path_to_executable>",
+            action=DictAction, dest="exe_paths")
+    parser.add_argument("--smtbmc", metavar="<path_to_executable>",
+            action=DictAction, dest="exe_paths")
+    parser.add_argument("--witness", metavar="<path_to_executable>",
+            action=DictAction, dest="exe_paths")
+    parser.add_argument("--suprove", metavar="<path_to_executable>",
+            action=DictAction, dest="exe_paths")
+    parser.add_argument("--aigbmc", metavar="<path_to_executable>",
+            action=DictAction, dest="exe_paths")
+    parser.add_argument("--avy", metavar="<path_to_executable>",
+            action=DictAction, dest="exe_paths")
+    parser.add_argument("--btormc", metavar="<path_to_executable>",
+            action=DictAction, dest="exe_paths")
+    parser.add_argument("--pono", metavar="<path_to_executable>",
+            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="<jobname>.sby | <dirname>", 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 <jobname>.sby is used)")
+
+    return parser

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)
+                    if self.opt_witrename:
-                    print("opt_clean", file=f)
+                        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)

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

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"]

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: