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] 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 `:` instead of `:`. 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 `` 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 ``:`` or +``~:`` 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 ``:`` 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 ``:`` or ``~:`` 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 ``~:`` 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 -``:`` or ``~:`` tag. - -The command ``sby --dumptasks `` prints the list of all tasks defined in -a given ``.sby`` file. Options section ---------------