Merge 043920d6e1 into f57802a166

docs/source/appnotes.rst

@@ -0,0 +1,9 @@
+Application Notes
+=================
+
+Formal Basics and Methods
+--------------------------
+
+- `109 Property Checking with SVA <https://yosyshq.readthedocs.io/projects/ap109>`_
+- `120 Weak precondition cover and witness for SVA properties <https://yosyshq.readthedocs.io/projects/ap120>`_
+- `130 Multi-Stage Verification <https://yosyshq.readthedocs.io/projects/ap130>`_

docs/source/index.rst

@@ -21,5 +21,6 @@ formal tasks:
    autotune.rst
    verilog.rst
    verific.rst
+   appnotes.rst
    license.rst
 

docs/source/reference.rst

@@ -111,6 +111,10 @@ The :sby:`[tasks]` section must appear in the ``.sby`` file before the first
 The command ``sby --dumptasks <sby_file>`` prints the list of all tasks defined in
 a given ``.sby`` file.
 
+Note that there is currently no way to specify dependencies on other tasks. For complex flows where such dependencies are needed, consider using separate ``.sby`` files, or a single file with external scripting. For an advanced example which uses tasks and external scripting to implement a multi-stage verification
+flow, see `AppNote 130: Multi-Stage Verification
+<https://yosyshq.readthedocs.io/projects/ap130>`_.
+
 Options section
 ---------------
 
@@ -204,6 +208,13 @@ options are:
 | ``cover_assert``  | ``cover``  | Check for assertion properties during ``cover`` mode.   |
 |                   |            | Values: ``on``, ``off``. Default: ``off``               |
 +-------------------+------------+---------------------------------------------------------+
+| ``skip_prep``     |   All      | Skip SBY's internal preparation step. Values: ``on``,   |
+|                   |            | ``off``. Default: ``off``. For an example of how it can |
+|                   |            | be useful to disable the preparation step in complex    |
+|                   |            | flows, see `AppNote 130:                                |
+|                   |            | Multi-Stage Verification                                |
+|                   |            | <https://yosyshq.readthedocs.io/projects/ap130>`_.      |
++-------------------+------------+---------------------------------------------------------+
 
 Cancelledby section
 -------------------