add dft_tag documentation

docs/source/using_yosys/more_scripting/data_flow_tracking.rst

@@ -0,0 +1,71 @@
+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,5 +12,6 @@ More scripting
    selections
    interactive_investigation
    model_checking
+   data_flow_tracking
 
 .. troubleshooting