Merge 3d2d953526 into fea6e467d0

docs/examples/tags/.skip

@@ -0,0 +1,6 @@
+alt
+bad
+complex
+default
+example
+dependencies

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

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

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
+

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]
+...

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

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

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
+

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

docs/examples/tags/dependencies.mk

@@ -0,0 +1,14 @@
+.PHONY: stage_1 stage_2 stage_2_alt
+dependencies_%: dependencies.sby
+	sby -f dependencies.sby $*
+
+STAGE_1_TARGS = dependencies_stage_1
+stage_1: $(STAGE_1_TARGS)
+
+STAGE_2_TARGS = dependencies_stage_2a dependencies_stage_2b
+$(STAGE_2_TARGS): stage_1
+stage_2: $(STAGE_2_TARGS)
+
+# both tasks together
+stage_2_alt: stage_1
+	sby -f dependencies.sby stage_2a stage_2b

docs/examples/tags/dependencies.sby

@@ -0,0 +1,4 @@
+[tasks]
+stage_1
+stage_2a
+stage_2b

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

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

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

docs/source/advanced/index.rst

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

docs/source/advanced/tags.rst

@@ -0,0 +1,187 @@
+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.  If no
+``default`` tag is provided, all tasks listed in the ``[tasks]`` section will be
+used as the default.  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.
+
+
+Running tasks in parallel
+-------------------------
+
+By default, if there are multiple tasks available then SBY will attempt to run
+them in parallel.  If SBY is called by a modern version of ``make``, it will
+attempt to connect to the Make jobserver for controlling parallelism.  If no
+jobserver is available, such as when calling ``sby`` directly, the maximum
+number of parallel jobs can be set by the ``-j`` command line option:
+
+.. code-block:: shell
+
+   # Calling SBY with up to 4 parallel tasks
+   sby -j4 <jobname>.sby
+
+Task dependencies with Make
+~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+Say we have some set of tasks which can be broken into two stages, and the
+second stage shouldn't run until the first stage has completed.  In SBY we have
+no way to describe such a dependency.  Instead, we can use a Makefile for flow
+control:
+
+.. literalinclude:: /../examples/tags/dependencies.sby
+   :language: sby
+   :caption: ``docs/examples/tags/dependencies.sby``
+
+.. literalinclude:: /../examples/tags/dependencies.mk
+   :language: make
+   :caption: ``docs/examples/tags/dependencies.mk``
+   :start-after: PHONY
+   :end-before: both tasks
+
+Since each task will (by default) output to a directory called
+``<jobname>_<taskname>``, we are able to provide a single pattern rule that
+will call ``sby`` for any given ``<taskname>``.
+
+An alternative approach is to define a single rule for each stage, allowing a
+single invocation of SBY to run multiple tasks.  Remember that SBY can connect
+to the Make jobserver, so no parallelism is lost here.  This may even reduce the
+overhead of launching multiple ``sby`` processes, particularly if there are many
+tasks.
+
+.. literalinclude:: /../examples/tags/dependencies.mk
+   :language: make
+   :caption: Make rule for running both stage 2 tasks together
+   :start-after: both tasks
+
+

docs/source/index.rst

@@ -23,4 +23,5 @@ formal tasks:
    verific.rst
    appnotes.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,103 +17,68 @@ 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
-
-   [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
+   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]
-   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.
-
-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>`_.
+Note that there is currently no way to specify dependencies on other tasks. For
+complex flows where such dependencies are needed, refer to :ref:`Task
+dependencies with Make`. 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
 ---------------

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

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)

tests/Makefile

@@ -47,7 +47,8 @@ make/rules/collect.mk: make/collect_tests.py
 make/rules/test/%.mk:
 	python3 make/test_rules.py --rule $@ --source $<
 
-ifneq (help,$(MAKECMDGOALS))
+NO_COLLECT_TARGS := help clean_rules
+ifneq ($(filter-out $(NO_COLLECT_TARGS),$(MAKECMDGOALS)),)
 
 # This should run every time but only trigger anything depending on it whenever
 # the script overwrites make/rules/found_tools. This doesn't really match how
@@ -66,3 +67,7 @@ endif
 include make/rules/collect.mk
 
 endif
+
+.PHONY: clean_rules
+clean_rules:
+	@rm -rf make/rules

tests/make/collect_tests.py

@@ -40,6 +40,15 @@ def collect(path):
     ):
         return
 
+    skip_files = []
+    try:
+        with open(path / ".skip", "r") as f:
+            for line in f:
+                skip_files.append(line.rstrip())
+    except FileNotFoundError:
+        # no .skip file
+        pass
+
     checked_dirs.append(path)
     for entry in path.glob("*.sby"):
         filename = str(entry)
@@ -50,10 +59,14 @@ def collect(path):
             continue
         if entry.with_suffix(".ivy").exists():
             continue
+        if entry.stem in skip_files:
+            continue
         tests.append(entry)
     for entry in path.glob("*"):
         if entry.with_suffix(".sby").exists():
             continue
+        if entry.name.startswith("skip_"):
+            continue
         if entry.is_dir():
             collect(entry)
 

tests/staged_sim_and_verif/dependencies.mk

@@ -0,0 +1,15 @@
+skip_staged_flow_%: skip_staged_flow.sby
+	sby -f skip_staged_flow.sby $*
+	
+skip_staged_flow_stage_1: skip_staged_flow_prep
+skip_staged_flow_stage_2: skip_staged_flow_stage_1
+skip_staged_flow_stage_3_init: skip_staged_flow_stage_2
+skip_staged_flow_stage_3a_cover skip_staged_flow_stage_3b_assert: skip_staged_flow_stage_3_init
+
+.PHONY: stage_3
+stage_3: skip_staged_flow_stage_3a_cover skip_staged_flow_stage_3b_assert
+
+.PHONY: clean
+clean:
+	@rm -rf skip_staged_flow
+	@rm -rf skip_staged_flow_*