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/examples/tags/bad.log b/docs/examples/tags/bad.log new file mode 100644 index 0000000..57b5776 --- /dev/null +++ b/docs/examples/tags/bad.log @@ -0,0 +1,31 @@ +./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 --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 +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/examples/tags/complex.log b/docs/examples/tags/complex.log new file mode 100644 index 0000000..d9baad5 --- /dev/null +++ b/docs/examples/tags/complex.log @@ -0,0 +1,76 @@ +./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 --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 + +[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..f155b7b --- /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] +~liveness: abc pdr +~unbounded: 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/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 new file mode 100644 index 0000000..d11acbb --- /dev/null +++ b/docs/examples/tags/example.log @@ -0,0 +1,31 @@ +./gen.sh +$ 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 --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 +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..05d8112 --- /dev/null +++ b/docs/examples/tags/gen.sh @@ -0,0 +1,38 @@ +#!/usr/bin/env bash +set -eu + +sby="sby" +script="example" +task="task1" + +while getopts :S:s:t: opt; do + case "$opt" in + S) + sby=$OPTARG + ;; + s) + script=$OPTARG + ;; + t) + task=$OPTARG + ;; + *) + 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 -a ${script}.log) 2>&1 +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/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..c133ebc --- /dev/null +++ b/docs/source/advanced/tags.rst @@ -0,0 +1,136 @@ +Tasks and tags +============== + +Multi-line tag sections +----------------------- +If ``:`` 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 + :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 +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. Note that when ``--dumpcfg`` is called without any tasks, the +generated config does not include any lines that are conditionally enabled +(``:``) and all lines that are conditionally disabled (``~:``). The +``[tasks]`` section is also only included when called without any tasks. + +.. literalinclude:: /../examples/tags/complex.log + :language: console + :start-at: dumptasks + :end-before: dumptags + +.. 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. 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/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/reference.rst b/docs/source/reference.rst index a50e31e..4c0b7a4 100644 --- a/docs/source/reference.rst +++ b/docs/source/reference.rst @@ -17,99 +17,62 @@ 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 + :start-at: dumptasks + :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: dumpdefaults + :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 --------------- 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 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)