mirrors/sby
3
0
Fork 0
mirror of https://github.com/YosysHQ/sby.git synced 2026-05-09 14:02:23 +00:00
Code Activity

Docs: Clarify tasks section

Browse source 
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)
This commit is contained in:
Krystine Sherwin 2026-05-05 16:38:18 +12:00
parent 4297f6ed43
commit b476597edf
No known key found for this signature in database
4 changed files with 98 additions and 81 deletions
Download patch file Download diff file Expand all files Collapse all files

18
docs/examples/tags/example.log Normal file
View file

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

9
docs/examples/tags/example.sby Normal file
View file

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

28
docs/examples/tags/gen.sh Executable file
View file

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

124
docs/source/reference.rst
View file

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