Revert "add dft_tag documentation"

This reverts commit 2443facc46.

docs/source/using_yosys/more_scripting/data_flow_tracking.rst

@@ -1,71 +0,0 @@
-Dataflow tracking
--------------------
-Yosys can be used to answer questions such as "can this signal affect this other signal?" via its *dataflow tracking* support.
-For this, four special cells, ``$get_tag``, ``$set_tag``, ``$overwrite_tag`` and ``$original_tag`` are inserted into the design and then the ``dft_tag`` is run, which converts these cells into ordinary logic.
-Typically, one would then use ``sby`` to prove assertions involving these cells.
-
-Ordinarily in Yosys, the state of a bit is simply ``0`` or ``1`` (or one of the special values, ``z`` and ``x``).
-During dataflow tracking they are augmented with a set of tags.
-For example, the state of a bit could be ``0`` and the set of tags ``"KEY"`` and ``"OVERFLOW"``.
-
-In addition to their usual operations on the logical bits, Yosys operations must now also process the status of the tags.
-For this, tags are simply *forwarded* or *propagated* (i.e. copied) from inputs to outputs, according to the following general rule:
-
-   A tag is forwarded from an input to an output if the input can affect the output, for that particular state of all other inputs.
-
-For example, XOR, AND and OR cells propagate tags as follows:
-
-#. XOR simply forwards all tags from its inputs to its output, because inputs to XOR can always affect the output.
-#. AND forwards tags only if the other input is ``1``. Because if one input is ``0``, the other input can never affect the output.
-#. Similarly, OR forwards tags only if the other input is ``0``.
-
-There are two exceptions to this rule:
-#. In general, propagation is only determined approximately.
-   For example, unless the ``dft_tag`` code knows about a cell, it simply assumes the worst-case behaviour that all inputs can affect all outputs.
-   It also does not try to determine whether the effect of a signal is cancelled out, for example ``A ^ A`` or ``A ^ (B ^ A)`` is independent of ``A``, but its tags would be propagated nonetheless.
-#. If tag groups are used, the rules are modified (see below).
-
-Because of this propagation behaviour, we can answer questions about what signals are affected by a certain signal, by injecting a tag at that point in the circuit, and observing where the tag is visible.
-
-Example use cases
-~~~~~~~~~~~~~~~~~~
-As an example use case, consider a cryptographic processor which is not supposed to expose its secret keys to the outside world.
-We can tag all key bits with the ``"KEY"`` tag and use ``sby`` to formally verify that no external signal ever carries the ``"KEY"`` tag, meaning that key information is not visible to the outside.
-As a caveat, we have to manually clear the ``"KEY"`` tag during cryptographic operations, as proving that the cryptographic operations themselves do not leak key information is beyond the ability of Yosys.
-However we can still easily detect, if e.g. an engineer forgot to remove debugging code that allows reading back key data.
-
-As a different use case, we can modify all adders in the design to set the ``"OVERFLOW"`` tag on their output bits, if the addition overflowed, and then add asserts to all flip-flop inputs and output signals that they do not carry the ``"OVERFLOW"`` tag, i.e. that the results of overflowed additions never affect system state.
-Note that in this particular example we use the ability of tag insertion to be conditional on logic, in this case the overflow condition of an adder.
-
-Semantics of dataflow tracking cells
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
-``$set_tag`` has inputs ``A``, ``SET``, ``CLR``, an output ``Y`` and a string parameter ``TAG``.
-The logic value of ``A`` and all tags other than the one named by the ``TAG`` parameter are simply copied to ``Y``.
-If ``SET`` is ``1``, then the named tag is added to ``Y``.
-Otherwise, if ``CLR`` is ``1``, then the named tag is removed.
-Otherwise, the tag is unchanged, i.e. it is present in ``Y`` if it is present in ``A``.
-
-``$get_tag`` has an input ``A`` and an output ``Y`` and a string parameter ``TAG``.
-``$get_tag`` inspects ``A`` for the presence or absence of a tag of the given name and sets ``Y`` to ``1`` if the tag is present.
-The logical value of ``A`` is completely ignored.
-
-``$overwrite_tag`` functions like ``$set_tag``, but lacks the ``Y`` output.
-Instead of providing a modified version of the input signal, it modifies the signal ``A`` "in-place", i.e. if a signal is input to ``$overwrite_tag``, that is equivalent to interposing a ``$set_tag`` between its driver and all cells it is connected to.
-The main purpose of ``$overwrite_tag`` is adding tags to signals produced within a module that cannot or should not be modified itself.
-
-``$original_tag`` functions identically to ``$get_tag``, but ignores ``$overwrite_tag``, i.e. when converting the ``$overwrite_tag`` to ``$set_tag`` as described above, it is equivalent to inserting the ``$get_tag`` *before* the ``$set_tag``.
-
-Tag groups
-~~~~~~~~~~~~~~
-Tag groups are an advanced feature that modify the propagation rule discussed above.
-To use tag groups, simply name tags according to the schema ``"group:name"``.
-For example, ``"key:0"``, ``"key:a"``, ``"key:b"`` would be three tags in the ``"key"`` group.
-
-The propagation rule is then amended by
-
-   Inputs cannot block the propagation of each other's tags for tags of the same group.
-
-For example, an AND gate will propagate a given tag on one input, if the other input is either 1 or carries a tag of the same group.
-So if one input is ``0, "key:a"`` and the other is ``0, "key:b"`` the result would be ``0, "key:a", "key:b"``, rather than simply ``0``.
-Note that if we add an unrelated ``"overflow"`` tag to the first input, it would still not be propagated.

docs/source/using_yosys/more_scripting/index.rst

@@ -12,6 +12,5 @@ More scripting
    selections
    interactive_investigation
    model_checking
-   data_flow_tracking
 
 .. troubleshooting