Merge aed51170fb into 8f8833c617

docs/source/advanced/index.rst

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

docs/source/advanced/tags.rst

@@ -0,0 +1,136 @@
+Tasks and tags
+==============
+
+Multi-line tag sections
+-----------------------
+If ``<tag>:`` 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
+(``<tag>:``) and all lines that are conditionally disabled (``~<tag>:``).  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.

docs/source/index.rst

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

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:  
 

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 <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
+   :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 ``<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: 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 ``<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
 ---------------

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