From 7702dd44237e3ec49e319e52d7583345a3ec314a Mon Sep 17 00:00:00 2001
From: Gus Smith <guscomps@gmail.com>
Date: Thu, 16 Jul 2026 10:55:36 +1200
Subject: [PATCH] Integrate multi-stage verification docs

---
 docs/source/appnotes.rst  | 9 +++++++++
 docs/source/index.rst     | 1 +
 docs/source/reference.rst | 9 ++++++++-
 3 files changed, 18 insertions(+), 1 deletion(-)
 create mode 100644 docs/source/appnotes.rst

diff --git a/docs/source/appnotes.rst b/docs/source/appnotes.rst
new file mode 100644
index 0000000..ae675e5
--- /dev/null
+++ b/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>`_
diff --git a/docs/source/index.rst b/docs/source/index.rst
index ab67043..e40120f 100644
--- a/docs/source/index.rst
+++ b/docs/source/index.rst
@@ -21,5 +21,6 @@ formal tasks:
    autotune.rst
    verilog.rst
    verific.rst
+   appnotes.rst
    license.rst
 
diff --git a/docs/source/reference.rst b/docs/source/reference.rst
index 417a065..a6899e6 100644
--- a/docs/source/reference.rst
+++ b/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
 ---------------
 
@@ -178,7 +182,10 @@ options are:
 |                   |            | directory, even when not required to run the task.      |
 +-------------------+------------+---------------------------------------------------------+
 | ``skip_prep``     |   All      | Skip SBY's internal preparation step. Values: ``on``,   |
-|                   |            | ``off``. Default: ``off``                               |
+|                   |            | ``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>`_.      |
 +-------------------+------------+---------------------------------------------------------+
 | ``smtc``          | ``bmc``,   | Pass this ``.smtc`` file to the smtbmc engine. All      |
 |                   | ``prove``, | other engines are disabled when this option is used.    |