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