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

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

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

docs/examples/tags/example.log

@@ -1,3 +1,4 @@
+./gen.sh 
 $ sby --dumptasks example.sby
 task1
 task2

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 --dumptasks ${script}.sby
-$sby --dumptags $script
+$sby --dumptags ${script}.sby
-$sby --dumptags $script $task
+$sby --dumptags ${script}.sby $task
-$sby --dumpcfg $script $task
+$sby --dumpcfg ${script}.sby $task

docs/source/advanced/index.rst

@@ -0,0 +1,6 @@
+Advanced SBY usage/examples
+===========================
+
+.. toctree::
+
+   tags

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

docs/source/index.rst

@@ -22,4 +22,5 @@ formal tasks:
    verilog.rst
    verific.rst
    license.rst
+   advanced/index
 

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