From 72ba57b4180aa99766094b0e6982e43db10e2917 Mon Sep 17 00:00:00 2001
From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com>
Date: Tue, 5 May 2026 14:17:24 +1200
Subject: [PATCH 1/7] 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 4297f6ed432aef9967a73f512f2f6f77e3d27ff4 Mon Sep 17 00:00:00 2001
From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com>
Date: Tue, 5 May 2026 15:18:25 +1200
Subject: [PATCH 2/7] 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 b476597edfcb805d10867eea2fb11e0f8da81299 Mon Sep 17 00:00:00 2001
From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com>
Date: Tue, 5 May 2026 16:38:18 +1200
Subject: [PATCH 3/7] 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 a50e31e..ca20870 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.
 
 Options section
 ---------------

From 1a27ba7b1b91a6383baba4e8bbfd103c3a3c2f7d Mon Sep 17 00:00:00 2001
From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com>
Date: Tue, 5 May 2026 17:50:49 +1200
Subject: [PATCH 4/7] 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 ab67043..7db0083 100644
--- a/docs/source/index.rst
+++ b/docs/source/index.rst
@@ -22,4 +22,5 @@ formal tasks:
    verilog.rst
    verific.rst
    license.rst
+   advanced/index
 
diff --git a/docs/source/reference.rst b/docs/source/reference.rst
index ca20870..2f7d58e 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 ec27ee962735ab331bdf8e3155deba81321069ec Mon Sep 17 00:00:00 2001
From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com>
Date: Tue, 5 May 2026 17:51:49 +1200
Subject: [PATCH 5/7] 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 974c2339d99f76a2344381bbd848cf70257c98ad Mon Sep 17 00:00:00 2001
From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com>
Date: Wed, 6 May 2026 09:07:32 +1200
Subject: [PATCH 6/7] 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 2f7d58e..4c0b7a4 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 aed51170fbec6e268ccb64ad2e9d7b0aaef05bb1 Mon Sep 17 00:00:00 2001
From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com>
Date: Wed, 6 May 2026 09:12:05 +1200
Subject: [PATCH 7/7] 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.