From 6eb1ed39d3eb40a20c1672b5be355d4c20c090e1 Mon Sep 17 00:00:00 2001
From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com>
Date: Thu, 16 Jul 2026 11:45:14 +1200
Subject: [PATCH 01/12] Docs: Fixing double backticks

---
 docs/source/quickstart.rst | 2 +-
 docs/source/usage.rst      | 8 ++++----
 2 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/docs/source/quickstart.rst b/docs/source/quickstart.rst
index 0105dc6..f85eb9b 100644
--- a/docs/source/quickstart.rst
+++ b/docs/source/quickstart.rst
@@ -27,7 +27,7 @@ a FIFO is
 
 In hardware we can create such a construct by providing two addresses into a
 register file.  This tutorial will use an example implementation provided in
-`fifo.sv`. 
+``fifo.sv``. 
 
 First, the address generator module:  
 
diff --git a/docs/source/usage.rst b/docs/source/usage.rst
index bc8e4e9..2394ce3 100644
--- a/docs/source/usage.rst
+++ b/docs/source/usage.rst
@@ -1,9 +1,9 @@
-Using `sby`
-===========
+Using ``sby``
+=============
 
-Once SBY is installed and available on the command line as `sby`, either built from source or using
+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`.
+available via ``sby --help``.  For more information on installation, see :ref:`install-doc`.
 
 .. argparse::
     :module: sby_cmdline

From 56268b128b93347e34c55dbe1e52ec35bcb9b667 Mon Sep 17 00:00:00 2001
From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com>
Date: Thu, 16 Jul 2026 11:45:15 +1200
Subject: [PATCH 02/12] Dump active tags if a single task is given

---
 sbysrc/sby.py | 13 +++++--------
 1 file changed, 5 insertions(+), 8 deletions(-)

diff --git a/sbysrc/sby.py b/sbysrc/sby.py
index 315aa55..9177c2c 100644
--- a/sbysrc/sby.py
+++ b/sbysrc/sby.py
@@ -320,7 +320,9 @@ def read_sbyconfig(sbydata, taskname):
     if defaultlist is None:
         defaultlist = tasklist
 
-    return cfgdata, tasklist, defaultlist, sorted(list(task_tags_all))
+    return_tags = task_tags_all if taskname is None else task_tags_active
+
+    return cfgdata, tasklist, defaultlist, sorted(list(return_tags))
 
 
 sbydata = list()
@@ -368,14 +370,9 @@ if dump_files:
     print("\n".join(str(f) for f in file_set))
     sys.exit(0)
 
-if dump_tags:
-    _, _, _, tagnames = read_sbyconfig(sbydata, None)
-    for tag in tagnames:
-        print(tag)
-    sys.exit(0)
-
 if dump_tasks or dump_defaults or dump_tags:
-    _, tasks, dtasks, tags = read_sbyconfig(sbydata, None)
+    taskname = tasknames[0] if len(tasknames) == 1 else None
+    _, tasks, dtasks, tags = read_sbyconfig(sbydata, taskname)
     for name in tasks if dump_tasks else dtasks if dump_defaults else tags:
         if name is not None:
             print(name)

From c411a397de673cbe30b75de69dfcb8b630c4fa9a Mon Sep 17 00:00:00 2001
From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com>
Date: Thu, 16 Jul 2026 11:45:15 +1200
Subject: [PATCH 03/12] Docs: Clarify tasks section

Move simple tasks example into an actual `.sby` file and use `literalinclude`.
Add `gen.sh` script for generating output log (currently using checked in log file so that we don't need to deal with having sby installed for readthedocs).
Remove more complex examples.
Remove "group aliases" in favor of "tags".
Refer to `<tag>:` instead of `<taskname>:`.
Introduce `--dumptags` and tasks being assigned a tag of the same name.
Split out tags into subsection.
Move "run specific task" example call in line, and add a task (so that it shows two tasks in one)
---
 docs/examples/tags/example.log |  18 +++++
 docs/examples/tags/example.sby |   9 +++
 docs/examples/tags/gen.sh      |  28 ++++++++
 docs/source/reference.rst      | 124 ++++++++++++---------------------
 4 files changed, 98 insertions(+), 81 deletions(-)
 create mode 100644 docs/examples/tags/example.log
 create mode 100644 docs/examples/tags/example.sby
 create mode 100755 docs/examples/tags/gen.sh

diff --git a/docs/examples/tags/example.log b/docs/examples/tags/example.log
new file mode 100644
index 0000000..2a177e0
--- /dev/null
+++ b/docs/examples/tags/example.log
@@ -0,0 +1,18 @@
+$ sby --dumptasks example.sby
+task1
+task2
+task3
+$ sby --dumptags example.sby
+task1
+task2
+task3
+task_1_or_2
+task_1_or_3
+$ sby --dumptags example.sby task1
+task1
+task_1_or_2
+task_1_or_3
+$ sby --dumpcfg example.sby task1
+[options]
+mode bmc
+depth 100
diff --git a/docs/examples/tags/example.sby b/docs/examples/tags/example.sby
new file mode 100644
index 0000000..568719b
--- /dev/null
+++ b/docs/examples/tags/example.sby
@@ -0,0 +1,9 @@
+[tasks]
+task1 task_1_or_2 task_1_or_3
+task2 task_1_or_2
+task3 task_1_or_3
+
+[options]
+task_1_or_2: mode bmc
+task3: mode prove
+~task3: depth 100
diff --git a/docs/examples/tags/gen.sh b/docs/examples/tags/gen.sh
new file mode 100755
index 0000000..4064cec
--- /dev/null
+++ b/docs/examples/tags/gen.sh
@@ -0,0 +1,28 @@
+#!/usr/bin/env bash
+set -eu
+
+sby="sby"
+script="example.sby"
+task="task1"
+
+while getopts :s: opt; do
+    case "$opt" in
+        s)
+            sby=$OPTARG
+            ;;
+        *)
+            echo "Usage: $0 [-s SBY command]\n" >&2
+            exit 1
+            ;;
+    esac
+done
+
+# log our commands and output
+PS4="$ "
+exec > >(tee example.log) 2>&1
+set -x
+
+$sby --dumptasks $script
+$sby --dumptags $script
+$sby --dumptags $script $task
+$sby --dumpcfg $script $task
diff --git a/docs/source/reference.rst b/docs/source/reference.rst
index a6899e6..1a10a08 100644
--- a/docs/source/reference.rst
+++ b/docs/source/reference.rst
@@ -17,99 +17,61 @@ The optional :sby:`[tasks]` section can be used to configure multiple
 verification tasks in a single ``.sby`` file. Each line in the :sby:`[tasks]`
 section configures one task. For example:
 
-.. code-block:: sby
+.. literalinclude:: ../examples/tags/example.sby
+   :language: sby
+   :end-before: [options]
+   :caption: ``example.sby`` tasks section
+   :name: example_tasks
 
-   [tasks]
-   task1 task_1_or_2 task_1_or_3
-   task2 task_1_or_2
-   task3 task_1_or_3
+The command ``sby --dumptasks <sby_file>`` prints the list of all tasks defined
+in a given ``.sby`` file.  One or more tasks can be specified as additional
+command line arguments when calling ``sby`` on a ``.sby`` file, e.g. ``sby
+example.sby task1 task2`` will run both ``task1`` and ``task2``.  If no task is
+specified then the default behavior is to run all available tasks.
 
-Each task can be assigned additional group aliases, such as ``task_1_or_2``
-and ``task_1_or_3`` in the above example.
+.. literalinclude:: ../examples/tags/example.log
+   :language: console
+   :end-before: dumptags
+   :caption: Viewing available tasks
 
-One or more tasks can be specified as additional command line arguments when
-calling ``sby`` on a ``.sby`` file:
+Tags
+~~~~
 
-.. code-block:: text
+Each task generates a tag of the same name, and can be assigned additional tags
+that may be shared across tasks, such as ``task_1_or_2`` and ``task_1_or_3`` in
+the :ref:`example_tasks` above.  Individual lines of an ``.sby`` file can be
+enabled or disabled for certain tasks by prefixing them with ``<tag>:`` or
+``~<tag>:`` respectively:
 
-   sby example.sby task2
+.. literalinclude:: ../examples/tags/example.sby
+   :language: sby
+   :start-at: [options]
+   :caption: ``example.sby`` options section
 
-If no task is specified then all tasks in the :sby:`[tasks]` section are run.
+As with tasks, it is possible to dump all the available tags in a given ``.sby``
+file with the ``--dumptags`` option.  If a single task is provided to ``sby``,
+only the tags for that task will be listed.
 
-After the :sby:`[tasks]` section individual lines can be specified for specific
-tasks or task groups:
+.. literalinclude:: ../examples/tags/example.log
+   :language: console
+   :start-at: dumptags
+   :end-before: dumpcfg
+   :caption: Using ``--dumptags``
 
-.. code-block:: sby
+It is possible to check the pre-processed config file for a given task with the
+``--dumpcfg`` option.
 
-   [options]
-   task_1_or_2: mode bmc
-   task_1_or_2: depth 100
-   task3: mode prove
+.. literalinclude:: ../examples/tags/example.log
+   :language: console
+   :start-at: dumpcfg
+   :caption: ``example.sby`` options section when running ``task1``
 
-If the tag ``<taskname>:`` is used on a line by itself then the conditional string
-extends until the next conditional block or ``--`` on a line by itself.
+.. warning::
 
-.. code-block:: sby
+   Any ``<tag>:`` or ``~<tag>:`` lines before the :sby:`[tasks]` section will
+   not be parsed.  It is recommended to always put the :sby:`[tasks]` section
+   first.
 
-   [options]
-   task_1_or_2:
-   mode bmc
-   depth 100
-
-   task3:
-   mode prove
-   --
-
-The tag ``~<taskname>:`` can be used for a line or block that should not be used when
-the given task is active:
-
-.. code-block:: sby
-
-   [options]
-   ~task3:
-   mode bmc
-   depth 100
-
-   task3:
-   mode prove
-   --
-
-The following example demonstrates how to configure safety and liveness checks for all
-combinations of some host implementations A and B and device implementations X and Y:
-
-.. code-block:: sby
-
-   [tasks]
-   prove_hAdX prove hostA deviceX
-   prove_hBdX prove hostB deviceX
-   prove_hAdY prove hostA deviceY
-   prove_hBdY prove hostB deviceY
-   live_hAdX live hostA deviceX
-   live_hBdX live hostB deviceX
-   live_hAdY live hostA deviceY
-   live_hBdY live hostB deviceY
-
-
-   [options]
-   prove: mode prove
-   live: mode live
-
-   [engines]
-   prove: abc pdr
-   live: aiger suprove
-
-   [script]
-   hostA: read -sv hostA.v
-   hostB: read -sv hostB.v
-   deviceX: read -sv deviceX.v
-   deviceY: read -sv deviceY.v
-   ...
-
-The :sby:`[tasks]` section must appear in the ``.sby`` file before the first
-``<taskname>:`` or ``~<taskname>:`` tag.
-
-The command ``sby --dumptasks <sby_file>`` prints the list of all tasks defined in
-a given ``.sby`` file.
 
 Note that there is currently no way to specify dependencies on other tasks. For complex flows where such dependencies are needed, consider using separate ``.sby`` files, or a single file with external scripting. For an advanced example which uses tasks and external scripting to implement a multi-stage verification
 flow, see `AppNote 130: Multi-Stage Verification

From 2e74292d2a1d2ce401fca06e4fc5efb0b82339b4 Mon Sep 17 00:00:00 2001
From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com>
Date: Thu, 16 Jul 2026 11:45:15 +1200
Subject: [PATCH 04/12] Docs: Advanced tag use

Add complex pycode example, generating tasks and then parsing tags to select source files.  Warn against doing it, and reiterate the usefulness of `--dumptasks` and `--dumpcfg`.
Modify gen.sh for modifiable script/task and to echo how it was called (in case they need to be regenerated, which isn't a problem for the regular example/task1 but is for the complex one).
---
 docs/examples/tags/complex.log | 47 ++++++++++++++++++++++++++++++++++
 docs/examples/tags/complex.sby | 35 +++++++++++++++++++++++++
 docs/examples/tags/example.log |  1 +
 docs/examples/tags/gen.sh      | 26 ++++++++++++-------
 docs/source/advanced/index.rst |  6 +++++
 docs/source/advanced/tags.rst  | 35 +++++++++++++++++++++++++
 docs/source/index.rst          |  1 +
 docs/source/reference.rst      |  1 +
 8 files changed, 143 insertions(+), 9 deletions(-)
 create mode 100644 docs/examples/tags/complex.log
 create mode 100644 docs/examples/tags/complex.sby
 create mode 100644 docs/source/advanced/index.rst
 create mode 100644 docs/source/advanced/tags.rst

diff --git a/docs/examples/tags/complex.log b/docs/examples/tags/complex.log
new file mode 100644
index 0000000..d669f87
--- /dev/null
+++ b/docs/examples/tags/complex.log
@@ -0,0 +1,47 @@
+./gen.sh -s complex -t unbounded_hAdX
+$ sby --dumptasks complex.sby
+unbounded_hAdX
+unbounded_hAdY
+unbounded_hBdX
+unbounded_hBdY
+liveness_hAdX
+liveness_hAdY
+liveness_hBdX
+liveness_hBdY
+$ sby --dumptags complex.sby
+deviceX
+deviceY
+hostA
+hostB
+liveness
+liveness_hAdX
+liveness_hAdY
+liveness_hBdX
+liveness_hBdY
+unbounded
+unbounded_hAdX
+unbounded_hAdY
+unbounded_hBdX
+unbounded_hBdY
+$ sby --dumptags complex.sby unbounded_hAdX
+deviceX
+hostA
+unbounded
+unbounded_hAdX
+$ sby --dumpcfg complex.sby unbounded_hAdX
+[options]
+mode prove
+
+[engines]
+abc pdr
+
+[script]
+read -sv hostA.v
+read -sv deviceX.v
+read -sv unbounded.v
+prep -top unbounded
+
+[files]
+hostA.v
+deviceX.v
+unbounded.v
diff --git a/docs/examples/tags/complex.sby b/docs/examples/tags/complex.sby
new file mode 100644
index 0000000..58295ea
--- /dev/null
+++ b/docs/examples/tags/complex.sby
@@ -0,0 +1,35 @@
+[tasks]
+--pycode-begin--
+for m in ['unbounded', 'liveness']:
+    for h in ['A', 'B']:
+        for d in ['X', 'Y']:
+            output(f'{m}_h{h}d{d} {m} host{h} device{d}')
+--pycode-end--
+
+[options]
+unbounded: mode prove
+liveness: mode live
+
+[engines]
+unbounded: abc pdr
+liveness: aiger suprove
+
+[script]
+--pycode-begin--
+sources = []
+for tag in tags:
+    if tag.startswith(('host', 'device')):
+        sources.append(tag)
+        output(f'read -sv {tag}.v')
+
+if task is not None:
+    top = task.split('_')[0]
+    sources.append(top)
+    output(f'read -sv {top}.v')
+    output(f'prep -top {top}')
+
+output('')
+output('[files]')
+for source in sources:
+    output(f'{source}.v')
+--pycode-end--
diff --git a/docs/examples/tags/example.log b/docs/examples/tags/example.log
index 2a177e0..25e9ad1 100644
--- a/docs/examples/tags/example.log
+++ b/docs/examples/tags/example.log
@@ -1,3 +1,4 @@
+./gen.sh 
 $ sby --dumptasks example.sby
 task1
 task2
diff --git a/docs/examples/tags/gen.sh b/docs/examples/tags/gen.sh
index 4064cec..60c6dda 100755
--- a/docs/examples/tags/gen.sh
+++ b/docs/examples/tags/gen.sh
@@ -2,27 +2,35 @@
 set -eu
 
 sby="sby"
-script="example.sby"
+script="example"
 task="task1"
 
-while getopts :s: opt; do
+while getopts :S:s:t: opt; do
     case "$opt" in
-        s)
+        S)
             sby=$OPTARG
             ;;
+        s)
+            script=$OPTARG
+            ;;
+        t)
+            task=$OPTARG
+            ;;
         *)
-            echo "Usage: $0 [-s SBY command]\n" >&2
+            echo "Usage: $0 [-s SBY command] [-s .sby file] [-t task]\n" >&2
             exit 1
             ;;
     esac
 done
 
+
 # log our commands and output
+echo "$0 $@" > ${script}.log
 PS4="$ "
-exec > >(tee example.log) 2>&1
+exec > >(tee -a ${script}.log) 2>&1
 set -x
 
-$sby --dumptasks $script
-$sby --dumptags $script
-$sby --dumptags $script $task
-$sby --dumpcfg $script $task
+$sby --dumptasks ${script}.sby
+$sby --dumptags ${script}.sby
+$sby --dumptags ${script}.sby $task
+$sby --dumpcfg ${script}.sby $task
diff --git a/docs/source/advanced/index.rst b/docs/source/advanced/index.rst
new file mode 100644
index 0000000..c10df58
--- /dev/null
+++ b/docs/source/advanced/index.rst
@@ -0,0 +1,6 @@
+Advanced SBY usage/examples
+===========================
+
+.. toctree::
+
+   tags
diff --git a/docs/source/advanced/tags.rst b/docs/source/advanced/tags.rst
new file mode 100644
index 0000000..2665827
--- /dev/null
+++ b/docs/source/advanced/tags.rst
@@ -0,0 +1,35 @@
+Tasks and tags
+==============
+
+Complex pycode blocks
+---------------------
+The following example demonstrates how to configure safety and liveness checks
+for all combinations of host and device implementations.  Note that the ``task``
+variable is set to a value of ``None`` when initially parsing the ``.sby`` file,
+so it is important to check ``if task is not None`` to avoid the
+``AttributeError`` when trying to use string methods on it.
+
+.. literalinclude:: /../examples/tags/complex.sby
+   :language: sby
+   :caption: ``docs/examples/tags/complex.sby``
+
+.. warning::
+
+   Including section headings in pycode blocks like this is a quick way to make
+   your ``.sby`` file very difficult to follow and is generally not recommended.
+   However since it is not possible to share variables between pycode sections,
+   in cases such as this it does simplify adding new host/device implementations
+   while avoiding duplication of the tag parsing.
+
+When working with complex ``.sby`` files like this, it is very helpful to use
+``--dumptasks`` and ``--dumpcfg`` to confirm things are being pre-processed as
+expected.
+
+.. literalinclude:: /../examples/tags/complex.log
+   :language: console
+   :start-at: dumptasks
+   :end-before: dumptags
+
+.. literalinclude:: /../examples/tags/complex.log
+   :language: console
+   :start-at: dumpcfg
diff --git a/docs/source/index.rst b/docs/source/index.rst
index e40120f..bc699ee 100644
--- a/docs/source/index.rst
+++ b/docs/source/index.rst
@@ -23,4 +23,5 @@ formal tasks:
    verific.rst
    appnotes.rst
    license.rst
+   advanced/index
 
diff --git a/docs/source/reference.rst b/docs/source/reference.rst
index 1a10a08..786fa49 100644
--- a/docs/source/reference.rst
+++ b/docs/source/reference.rst
@@ -31,6 +31,7 @@ specified then the default behavior is to run all available tasks.
 
 .. literalinclude:: ../examples/tags/example.log
    :language: console
+   :start-at: dumptasks
    :end-before: dumptags
    :caption: Viewing available tasks
 

From 6f212c47a45880503f6a8bf8bb02325a094f71ba Mon Sep 17 00:00:00 2001
From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com>
Date: Thu, 16 Jul 2026 11:45:16 +1200
Subject: [PATCH 05/12] Docs: Multi-line tag sections

---
 docs/examples/tags/bad.log    | 20 ++++++++++++++++++++
 docs/examples/tags/bad.sby    | 15 +++++++++++++++
 docs/source/advanced/tags.rst | 33 +++++++++++++++++++++++++++++++++
 3 files changed, 68 insertions(+)
 create mode 100644 docs/examples/tags/bad.log
 create mode 100644 docs/examples/tags/bad.sby

diff --git a/docs/examples/tags/bad.log b/docs/examples/tags/bad.log
new file mode 100644
index 0000000..26ddb04
--- /dev/null
+++ b/docs/examples/tags/bad.log
@@ -0,0 +1,20 @@
+./gen.sh -s bad
+$ sby --dumptasks bad.sby
+task1
+task2
+task3
+$ sby --dumptags bad.sby
+task1
+task2
+task3
+task_1_or_2
+task_1_or_3
+$ sby --dumptags bad.sby task1
+task1
+task_1_or_2
+task_1_or_3
+$ sby --dumpcfg bad.sby task1
+[options]
+mode bmc
+depth 100
+
diff --git a/docs/examples/tags/bad.sby b/docs/examples/tags/bad.sby
new file mode 100644
index 0000000..aa795c8
--- /dev/null
+++ b/docs/examples/tags/bad.sby
@@ -0,0 +1,15 @@
+[tasks]
+task1 task_1_or_2 task_1_or_3
+task2 task_1_or_2
+task3 task_1_or_3
+
+[options]
+task_1_or_2:
+mode bmc
+depth 100
+
+task3:
+mode prove
+
+[engines]
+...
diff --git a/docs/source/advanced/tags.rst b/docs/source/advanced/tags.rst
index 2665827..fcefa04 100644
--- a/docs/source/advanced/tags.rst
+++ b/docs/source/advanced/tags.rst
@@ -1,6 +1,39 @@
 Tasks and tags
 ==============
 
+Multi-line tag sections
+-----------------------
+If ``<tag>:`` is used on a line by itself then the conditional string
+extends until ``--`` is found on a line by itself.
+
+.. code-block:: sby
+
+   [options]
+   task_1_or_2:
+   mode bmc
+   depth 100
+   --
+
+   task3:
+   mode prove
+   --
+
+If the closing ``--`` line is ommitted, the current conditional block will
+extend until the next conditional block.  However it is recommended to always
+include the closing ``--`` line to avoid inadvertently making the rest of the
+file conditional.
+
+.. literalinclude:: /../examples/tags/bad.sby
+   :language: sby
+   :start-at: [options]
+   :caption: ``bad.sby``
+
+.. literalinclude:: /../examples/tags/bad.log
+   :language: console
+   :start-at: dumpcfg
+   :caption: ``[engines]`` section is only enabled for ``task3``
+
+
 Complex pycode blocks
 ---------------------
 The following example demonstrates how to configure safety and liveness checks

From a31f3706ecae0ef487ee3b063e54749b3535471d Mon Sep 17 00:00:00 2001
From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com>
Date: Thu, 16 Jul 2026 11:45:16 +1200
Subject: [PATCH 06/12] Docs: Add default tasks and alt tag assignment

Demonstrate `--dumpcfg` sans task in the complex code example (and how the empty task impacts tag matching).
---
 docs/examples/tags/bad.log     | 11 +++++++++
 docs/examples/tags/complex.log | 29 +++++++++++++++++++++++
 docs/examples/tags/complex.sby |  4 ++--
 docs/examples/tags/default.log | 27 +++++++++++++++++++++
 docs/examples/tags/default.sby |  6 +++++
 docs/examples/tags/example.log | 12 ++++++++++
 docs/examples/tags/gen.sh      |  2 ++
 docs/source/advanced/tags.rst  | 43 +++++++++++++++++++++++++++++++++-
 docs/source/reference.rst      |  2 +-
 9 files changed, 132 insertions(+), 4 deletions(-)
 create mode 100644 docs/examples/tags/default.log
 create mode 100644 docs/examples/tags/default.sby

diff --git a/docs/examples/tags/bad.log b/docs/examples/tags/bad.log
index 26ddb04..57b5776 100644
--- a/docs/examples/tags/bad.log
+++ b/docs/examples/tags/bad.log
@@ -13,6 +13,17 @@ $ sby --dumptags bad.sby task1
 task1
 task_1_or_2
 task_1_or_3
+$ sby --dumpdefaults bad.sby
+task1
+task2
+task3
+$ sby --dumpcfg bad.sby
+[tasks]
+task1 task_1_or_2 task_1_or_3
+task2 task_1_or_2
+task3 task_1_or_3
+
+[options]
 $ sby --dumpcfg bad.sby task1
 [options]
 mode bmc
diff --git a/docs/examples/tags/complex.log b/docs/examples/tags/complex.log
index d669f87..d9baad5 100644
--- a/docs/examples/tags/complex.log
+++ b/docs/examples/tags/complex.log
@@ -28,6 +28,35 @@ deviceX
 hostA
 unbounded
 unbounded_hAdX
+$ sby --dumpdefaults complex.sby
+unbounded_hAdX
+unbounded_hAdY
+unbounded_hBdX
+unbounded_hBdY
+liveness_hAdX
+liveness_hAdY
+liveness_hBdX
+liveness_hBdY
+$ sby --dumpcfg complex.sby
+[tasks]
+unbounded_hAdX unbounded hostA deviceX
+unbounded_hAdY unbounded hostA deviceY
+unbounded_hBdX unbounded hostB deviceX
+unbounded_hBdY unbounded hostB deviceY
+liveness_hAdX liveness hostA deviceX
+liveness_hAdY liveness hostA deviceY
+liveness_hBdX liveness hostB deviceX
+liveness_hBdY liveness hostB deviceY
+
+[options]
+
+[engines]
+abc pdr
+aiger suprove
+
+[script]
+
+[files]
 $ sby --dumpcfg complex.sby unbounded_hAdX
 [options]
 mode prove
diff --git a/docs/examples/tags/complex.sby b/docs/examples/tags/complex.sby
index 58295ea..f155b7b 100644
--- a/docs/examples/tags/complex.sby
+++ b/docs/examples/tags/complex.sby
@@ -11,8 +11,8 @@ unbounded: mode prove
 liveness: mode live
 
 [engines]
-unbounded: abc pdr
-liveness: aiger suprove
+~liveness: abc pdr
+~unbounded: aiger suprove
 
 [script]
 --pycode-begin--
diff --git a/docs/examples/tags/default.log b/docs/examples/tags/default.log
new file mode 100644
index 0000000..5761655
--- /dev/null
+++ b/docs/examples/tags/default.log
@@ -0,0 +1,27 @@
+./gen.sh -s default
+$ sby --dumptasks default.sby
+task1
+task2
+task3
+$ sby --dumptags default.sby
+task1
+task2
+task3
+task_1_or_2
+task_1_or_3
+$ sby --dumptags default.sby task1
+task1
+task_1_or_2
+task_1_or_3
+$ sby --dumpdefaults default.sby
+task2
+task3
+$ sby --dumpcfg default.sby
+[tasks]
+task1 task_1_or_3 task_1_or_2
+task2 task_1_or_2
+task3 task_1_or_3
+
+task2 task3 : default
+$ sby --dumpcfg default.sby task1
+
diff --git a/docs/examples/tags/default.sby b/docs/examples/tags/default.sby
new file mode 100644
index 0000000..03c61f7
--- /dev/null
+++ b/docs/examples/tags/default.sby
@@ -0,0 +1,6 @@
+[tasks]
+task1 task_1_or_3 task_1_or_2
+task2 task_1_or_2
+task3 task_1_or_3
+
+task2 task3 : default
diff --git a/docs/examples/tags/example.log b/docs/examples/tags/example.log
index 25e9ad1..d11acbb 100644
--- a/docs/examples/tags/example.log
+++ b/docs/examples/tags/example.log
@@ -13,6 +13,18 @@ $ sby --dumptags example.sby task1
 task1
 task_1_or_2
 task_1_or_3
+$ sby --dumpdefaults example.sby
+task1
+task2
+task3
+$ sby --dumpcfg example.sby
+[tasks]
+task1 task_1_or_2 task_1_or_3
+task2 task_1_or_2
+task3 task_1_or_3
+
+[options]
+depth 100
 $ sby --dumpcfg example.sby task1
 [options]
 mode bmc
diff --git a/docs/examples/tags/gen.sh b/docs/examples/tags/gen.sh
index 60c6dda..05d8112 100755
--- a/docs/examples/tags/gen.sh
+++ b/docs/examples/tags/gen.sh
@@ -33,4 +33,6 @@ set -x
 $sby --dumptasks ${script}.sby
 $sby --dumptags ${script}.sby
 $sby --dumptags ${script}.sby $task
+$sby --dumpdefaults ${script}.sby
+$sby --dumpcfg ${script}.sby
 $sby --dumpcfg ${script}.sby $task
diff --git a/docs/source/advanced/tags.rst b/docs/source/advanced/tags.rst
index fcefa04..4681270 100644
--- a/docs/source/advanced/tags.rst
+++ b/docs/source/advanced/tags.rst
@@ -31,9 +31,47 @@ file conditional.
 .. literalinclude:: /../examples/tags/bad.log
    :language: console
    :start-at: dumpcfg
+   :end-before: dumpcfg
    :caption: ``[engines]`` section is only enabled for ``task3``
 
 
+Alternative tag assignment
+--------------------------
+
+An alternative tag assignment method is provided which uses the colon (``:``)
+character to separate tasks and tags.  With this method it is possible to assign
+a group of tags to multiple tasks at the same time.
+
+.. code-block:: sby
+
+   [tasks]
+   task1
+   task2
+   task3
+
+   task1 task2 : deep bounded
+
+
+Default tasks
+-------------
+
+A special tag, ``default``, is provided for controlling which tasks should be
+run when no specific tasks are provided.  The ``--dumpdefaults`` option is
+provided for getting the list of default tasks for a given ``.sby`` file.  Note
+that ``default`` does *not* get added to the list of tags, and should not be
+used for controlling conditional lines.
+
+.. literalinclude:: /../examples/tags/default.sby
+   :language: sby
+   :caption: ``default.sby`` tasks section
+
+.. literalinclude:: /../examples/tags/default.log
+   :language: console
+   :start-at: dumpdefaults
+   :end-before: dumpcfg
+   :caption: Using ``--dumpdefaults``
+
+
 Complex pycode blocks
 ---------------------
 The following example demonstrates how to configure safety and liveness checks
@@ -56,7 +94,10 @@ so it is important to check ``if task is not None`` to avoid the
 
 When working with complex ``.sby`` files like this, it is very helpful to use
 ``--dumptasks`` and ``--dumpcfg`` to confirm things are being pre-processed as
-expected.
+expected.  Note that when ``--dumpcfg`` is called without any tasks, the
+generated config does not include any lines that are conditionally enabled
+(``<tag>:``) and all lines that are conditionally disabled (``~<tag>:``).  The
+``[tasks]`` section is also only included when called without any tasks.
 
 .. literalinclude:: /../examples/tags/complex.log
    :language: console
diff --git a/docs/source/reference.rst b/docs/source/reference.rst
index 786fa49..e66ba87 100644
--- a/docs/source/reference.rst
+++ b/docs/source/reference.rst
@@ -56,7 +56,7 @@ only the tags for that task will be listed.
 .. literalinclude:: ../examples/tags/example.log
    :language: console
    :start-at: dumptags
-   :end-before: dumpcfg
+   :end-before: dumpdefaults
    :caption: Using ``--dumptags``
 
 It is possible to check the pre-processed config file for a given task with the

From 948a2caacb4342bc9107113c0c96f5417070ff91 Mon Sep 17 00:00:00 2001
From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com>
Date: Thu, 16 Jul 2026 11:45:16 +1200
Subject: [PATCH 07/12] Docs: regex tag matching

This feels cursed.
---
 docs/examples/tags/alt.log    | 42 +++++++++++++++++++++++++++++++++++
 docs/examples/tags/alt.sby    | 38 +++++++++++++++++++++++++++++++
 docs/source/advanced/tags.rst | 27 ++++++++++++++++++++++
 3 files changed, 107 insertions(+)
 create mode 100644 docs/examples/tags/alt.log
 create mode 100644 docs/examples/tags/alt.sby

diff --git a/docs/examples/tags/alt.log b/docs/examples/tags/alt.log
new file mode 100644
index 0000000..34c8e12
--- /dev/null
+++ b/docs/examples/tags/alt.log
@@ -0,0 +1,42 @@
+./gen.sh -s alt -t unbounded_hAdX
+$ sby --dumptasks alt.sby
+$ sby --dumptags alt.sby
+known
+liveness
+unbounded
+$ sby --dumptags alt.sby unbounded_hAdX
+\w+_h[AB]d[XY]
+known
+unbounded
+unbounded_h.d.
+$ sby --dumpdefaults alt.sby
+$ sby --dumpcfg alt.sby
+[tasks]
+unbounded_h.d. : unbounded
+liveness_h.d. : liveness
+\w+_h[AB]d[XY] : known
+
+[options]
+
+[engines]
+abc pdr
+aiger suprove
+
+[script]
+
+[files]
+$ sby --dumpcfg alt.sby unbounded_hAdX
+[options]
+mode prove
+
+[engines]
+abc pdr
+
+[script]
+read -sv A.v X.v unbounded.v
+prep -top unbounded
+
+[files]
+unbounded.v
+hostA.v
+deviceX.v
diff --git a/docs/examples/tags/alt.sby b/docs/examples/tags/alt.sby
new file mode 100644
index 0000000..6633c00
--- /dev/null
+++ b/docs/examples/tags/alt.sby
@@ -0,0 +1,38 @@
+[tasks]
+unbounded_h.d. : unbounded
+liveness_h.d. : liveness
+\w+_h[AB]d[XY] : known
+
+[options]
+unbounded: mode prove
+liveness: mode live
+
+[engines]
+~liveness: abc pdr
+~unbounded: aiger suprove
+
+[script]
+--pycode-begin--
+m = re.fullmatch(r'(unbounded|liveness)_h(.)d(.)', task or '')
+if m:
+    top, h, d = m.groups()
+    output(f'read -sv {h}.v {d}.v {top}.v')
+    output(f'prep -top {top}')
+else:
+    assert task is None, f'Invalid task {task!r}'
+--pycode-end--
+
+[files]
+--pycode-begin--
+m = re.fullmatch(r'(\w+)_h(\w)d(\w)', task or '')
+if m:
+    assert 'known' in tags, f'Unknown host/device {task!r}'
+    top, h, d = m.groups()
+    sources = [
+        f"{top}.v",
+        f"host{h}.v",
+        f"device{d}.v",
+    ]
+    for source in sources:
+        output(source)
+--pycode-end--
diff --git a/docs/source/advanced/tags.rst b/docs/source/advanced/tags.rst
index 4681270..c133ebc 100644
--- a/docs/source/advanced/tags.rst
+++ b/docs/source/advanced/tags.rst
@@ -107,3 +107,30 @@ generated config does not include any lines that are conditionally enabled
 .. literalinclude:: /../examples/tags/complex.log
    :language: console
    :start-at: dumpcfg
+
+A better way
+~~~~~~~~~~~~
+
+For this particular example, a better approach might be the following:
+
+.. literalinclude:: /../examples/tags/alt.sby
+   :language: sby
+
+This uses regex string matching on the task name, allowing any task to be
+provided in the ``sby`` call that matches at least one task.  This allows for
+all of the same calls, e.g. ``sby alt.sby unbounded_hAdX``, but there are no
+longer any default tasks, so calling ``sby alt.sby`` is no longer valid.
+
+.. warning::
+
+   So long as the provided task matches *any* regex task then SBY will recognize
+   it as valid, opening up the potential for downstream issues where a partially
+   recognized task name is not fully configured.  Extreme care should be taken
+   when using multiple regex tasks.
+
+We use the tag ``known`` here to validate that the host/device implementations
+are valid. This isn't strictly necessary, but it does mean that we can provide
+an error message if an unknown host/device is used, and demonstrates that care
+must be taken when using regex matching.  e.g. without the ``assert task is
+None`` line, a task of ``witness_hAdX`` would provide an error message about
+``mode`` being unset, which may not be immediately obvious as to why that is.

From 6a71a74ed8bbc060440a79b19a47d4d038411b30 Mon Sep 17 00:00:00 2001
From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com>
Date: Thu, 16 Jul 2026 11:45:17 +1200
Subject: [PATCH 08/12] tests: Add clean_rules target

Calling `make clean` can fail if a test folder has been collected but the source no longer exists. `make clean_rules` bypasses this by skipping the `include make/rules/collect.mk` in the same way as `make help`.
---
 tests/Makefile | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/tests/Makefile b/tests/Makefile
index 6063a01..cc20b30 100644
--- a/tests/Makefile
+++ b/tests/Makefile
@@ -47,7 +47,8 @@ make/rules/collect.mk: make/collect_tests.py
 make/rules/test/%.mk:
 	python3 make/test_rules.py --rule $@ --source $<
 
-ifneq (help,$(MAKECMDGOALS))
+NO_COLLECT_TARGS := help clean_rules
+ifneq ($(filter-out $(NO_COLLECT_TARGS),$(MAKECMDGOALS)),)
 
 # This should run every time but only trigger anything depending on it whenever
 # the script overwrites make/rules/found_tools. This doesn't really match how
@@ -66,3 +67,7 @@ endif
 include make/rules/collect.mk
 
 endif
+
+.PHONY: clean_rules
+clean_rules:
+	@rm -rf make/rules

From 62cd0028a0016948699eee3fd4f68face613ca9d Mon Sep 17 00:00:00 2001
From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com>
Date: Thu, 16 Jul 2026 11:45:17 +1200
Subject: [PATCH 09/12] tests: Don't collect folders that start with skip_

---
 tests/make/collect_tests.py | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/tests/make/collect_tests.py b/tests/make/collect_tests.py
index 1f9b2c9..9ac0df0 100644
--- a/tests/make/collect_tests.py
+++ b/tests/make/collect_tests.py
@@ -54,6 +54,8 @@ def collect(path):
     for entry in path.glob("*"):
         if entry.with_suffix(".sby").exists():
             continue
+        if entry.name.startswith("skip_"):
+            continue
         if entry.is_dir():
             collect(entry)
 

From 0bfda866870b9aafeb11cbd69fed08b15eb58d9a Mon Sep 17 00:00:00 2001
From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com>
Date: Thu, 16 Jul 2026 11:45:17 +1200
Subject: [PATCH 10/12] tests: Support .skip file

SBY entires in a file named `.skip` are ignored from the current directory during collection.
Useful for when you want to skip a file, but don't want to use the `skip_` prefix, such as when it's a docs example.
---
 tests/make/collect_tests.py | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/tests/make/collect_tests.py b/tests/make/collect_tests.py
index 9ac0df0..1416732 100644
--- a/tests/make/collect_tests.py
+++ b/tests/make/collect_tests.py
@@ -40,6 +40,15 @@ def collect(path):
     ):
         return
 
+    skip_files = []
+    try:
+        with open(path / ".skip", "r") as f:
+            for line in f:
+                skip_files.append(line.rstrip())
+    except FileNotFoundError:
+        # no .skip file
+        pass
+
     checked_dirs.append(path)
     for entry in path.glob("*.sby"):
         filename = str(entry)
@@ -50,6 +59,8 @@ def collect(path):
             continue
         if entry.with_suffix(".ivy").exists():
             continue
+        if entry.stem in skip_files:
+            continue
         tests.append(entry)
     for entry in path.glob("*"):
         if entry.with_suffix(".sby").exists():

From 138d39159eaff464b12f6eb8184ec3a9e3368e19 Mon Sep 17 00:00:00 2001
From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com>
Date: Thu, 16 Jul 2026 11:45:18 +1200
Subject: [PATCH 11/12] docs/examples/tags: Don't run in CI

They're not fully formed SBY files, so we don't want to try running them.
---
 docs/examples/tags/.skip | 5 +++++
 1 file changed, 5 insertions(+)
 create mode 100644 docs/examples/tags/.skip

diff --git a/docs/examples/tags/.skip b/docs/examples/tags/.skip
new file mode 100644
index 0000000..5057937
--- /dev/null
+++ b/docs/examples/tags/.skip
@@ -0,0 +1,5 @@
+alt
+bad
+complex
+default
+example

From 3d2d953526757d0926ea4dc788467f4b9f0de2a3 Mon Sep 17 00:00:00 2001
From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com>
Date: Thu, 16 Jul 2026 15:12:10 +1200
Subject: [PATCH 12/12] Docs: Running tasks in parallel

Also using make for dependency management/ordering.
Includes `tests/stage_sim_and_verif/dependencies.mk` file because I was using that to check my make logic (and the docs example is once again incomplete sby).
---
 docs/examples/tags/.skip                   |  1 +
 docs/examples/tags/dependencies.mk         | 14 ++++++
 docs/examples/tags/dependencies.sby        |  4 ++
 docs/source/advanced/tags.rst              | 57 ++++++++++++++++++++--
 docs/source/reference.rst                  |  8 +--
 tests/staged_sim_and_verif/dependencies.mk | 15 ++++++
 6 files changed, 93 insertions(+), 6 deletions(-)
 create mode 100644 docs/examples/tags/dependencies.mk
 create mode 100644 docs/examples/tags/dependencies.sby
 create mode 100644 tests/staged_sim_and_verif/dependencies.mk

diff --git a/docs/examples/tags/.skip b/docs/examples/tags/.skip
index 5057937..8bc8ee6 100644
--- a/docs/examples/tags/.skip
+++ b/docs/examples/tags/.skip
@@ -3,3 +3,4 @@ bad
 complex
 default
 example
+dependencies
diff --git a/docs/examples/tags/dependencies.mk b/docs/examples/tags/dependencies.mk
new file mode 100644
index 0000000..b117799
--- /dev/null
+++ b/docs/examples/tags/dependencies.mk
@@ -0,0 +1,14 @@
+.PHONY: stage_1 stage_2 stage_2_alt
+dependencies_%: dependencies.sby
+	sby -f dependencies.sby $*
+
+STAGE_1_TARGS = dependencies_stage_1
+stage_1: $(STAGE_1_TARGS)
+
+STAGE_2_TARGS = dependencies_stage_2a dependencies_stage_2b
+$(STAGE_2_TARGS): stage_1
+stage_2: $(STAGE_2_TARGS)
+
+# both tasks together
+stage_2_alt: stage_1
+	sby -f dependencies.sby stage_2a stage_2b
diff --git a/docs/examples/tags/dependencies.sby b/docs/examples/tags/dependencies.sby
new file mode 100644
index 0000000..1eb500a
--- /dev/null
+++ b/docs/examples/tags/dependencies.sby
@@ -0,0 +1,4 @@
+[tasks]
+stage_1
+stage_2a
+stage_2b
diff --git a/docs/source/advanced/tags.rst b/docs/source/advanced/tags.rst
index c133ebc..4c458e1 100644
--- a/docs/source/advanced/tags.rst
+++ b/docs/source/advanced/tags.rst
@@ -57,9 +57,10 @@ Default tasks
 
 A special tag, ``default``, is provided for controlling which tasks should be
 run when no specific tasks are provided.  The ``--dumpdefaults`` option is
-provided for getting the list of default tasks for a given ``.sby`` file.  Note
-that ``default`` does *not* get added to the list of tags, and should not be
-used for controlling conditional lines.
+provided for getting the list of default tasks for a given ``.sby`` file.  If no
+``default`` tag is provided, all tasks listed in the ``[tasks]`` section will be
+used as the default.  Note that ``default`` does *not* get added to the list of
+tags, and should not be used for controlling conditional lines.
 
 .. literalinclude:: /../examples/tags/default.sby
    :language: sby
@@ -134,3 +135,53 @@ an error message if an unknown host/device is used, and demonstrates that care
 must be taken when using regex matching.  e.g. without the ``assert task is
 None`` line, a task of ``witness_hAdX`` would provide an error message about
 ``mode`` being unset, which may not be immediately obvious as to why that is.
+
+
+Running tasks in parallel
+-------------------------
+
+By default, if there are multiple tasks available then SBY will attempt to run
+them in parallel.  If SBY is called by a modern version of ``make``, it will
+attempt to connect to the Make jobserver for controlling parallelism.  If no
+jobserver is available, such as when calling ``sby`` directly, the maximum
+number of parallel jobs can be set by the ``-j`` command line option:
+
+.. code-block:: shell
+
+   # Calling SBY with up to 4 parallel tasks
+   sby -j4 <jobname>.sby
+
+Task dependencies with Make
+~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+Say we have some set of tasks which can be broken into two stages, and the
+second stage shouldn't run until the first stage has completed.  In SBY we have
+no way to describe such a dependency.  Instead, we can use a Makefile for flow
+control:
+
+.. literalinclude:: /../examples/tags/dependencies.sby
+   :language: sby
+   :caption: ``docs/examples/tags/dependencies.sby``
+
+.. literalinclude:: /../examples/tags/dependencies.mk
+   :language: make
+   :caption: ``docs/examples/tags/dependencies.mk``
+   :start-after: PHONY
+   :end-before: both tasks
+
+Since each task will (by default) output to a directory called
+``<jobname>_<taskname>``, we are able to provide a single pattern rule that
+will call ``sby`` for any given ``<taskname>``.
+
+An alternative approach is to define a single rule for each stage, allowing a
+single invocation of SBY to run multiple tasks.  Remember that SBY can connect
+to the Make jobserver, so no parallelism is lost here.  This may even reduce the
+overhead of launching multiple ``sby`` processes, particularly if there are many
+tasks.
+
+.. literalinclude:: /../examples/tags/dependencies.mk
+   :language: make
+   :caption: Make rule for running both stage 2 tasks together
+   :start-after: both tasks
+
+
diff --git a/docs/source/reference.rst b/docs/source/reference.rst
index e66ba87..91767f6 100644
--- a/docs/source/reference.rst
+++ b/docs/source/reference.rst
@@ -74,9 +74,11 @@ It is possible to check the pre-processed config file for a given task with the
    first.
 
 
-Note that there is currently no way to specify dependencies on other tasks. For complex flows where such dependencies are needed, consider using separate ``.sby`` files, or a single file with external scripting. For an advanced example which uses tasks and external scripting to implement a multi-stage verification
-flow, see `AppNote 130: Multi-Stage Verification
-<https://yosyshq.readthedocs.io/projects/ap130>`_.
+Note that there is currently no way to specify dependencies on other tasks. For
+complex flows where such dependencies are needed, refer to :ref:`Task
+dependencies with Make`. For an advanced example which uses tasks and external
+scripting to implement a multi-stage verification flow, see `AppNote 130:
+Multi-Stage Verification <https://yosyshq.readthedocs.io/projects/ap130>`_.
 
 Options section
 ---------------
diff --git a/tests/staged_sim_and_verif/dependencies.mk b/tests/staged_sim_and_verif/dependencies.mk
new file mode 100644
index 0000000..8633fa8
--- /dev/null
+++ b/tests/staged_sim_and_verif/dependencies.mk
@@ -0,0 +1,15 @@
+skip_staged_flow_%: skip_staged_flow.sby
+	sby -f skip_staged_flow.sby $*
+	
+skip_staged_flow_stage_1: skip_staged_flow_prep
+skip_staged_flow_stage_2: skip_staged_flow_stage_1
+skip_staged_flow_stage_3_init: skip_staged_flow_stage_2
+skip_staged_flow_stage_3a_cover skip_staged_flow_stage_3b_assert: skip_staged_flow_stage_3_init
+
+.PHONY: stage_3
+stage_3: skip_staged_flow_stage_3a_cover skip_staged_flow_stage_3b_assert
+
+.PHONY: clean
+clean:
+	@rm -rf skip_staged_flow
+	@rm -rf skip_staged_flow_*