From 19845be85c1fd2385dcfc07cdc39c2c6aae26a7f Mon Sep 17 00:00:00 2001 From: Emily Schmidt Date: Thu, 10 Apr 2025 08:43:21 +0100 Subject: [PATCH] reflow dft docs to 80 cols --- .../more_scripting/data_flow_tracking.rst | 115 ++++++++++++------ 1 file changed, 76 insertions(+), 39 deletions(-) diff --git a/docs/source/using_yosys/more_scripting/data_flow_tracking.rst b/docs/source/using_yosys/more_scripting/data_flow_tracking.rst index e0714b7e2..aa13a2e69 100644 --- a/docs/source/using_yosys/more_scripting/data_flow_tracking.rst +++ b/docs/source/using_yosys/more_scripting/data_flow_tracking.rst @@ -1,77 +1,114 @@ 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 (e.g. by a custom Yosys pass) 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. +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 (e.g. by a custom Yosys pass) 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. .. _SBY: https://yosyshq.readthedocs.io/projects/sby -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"``. +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: +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. + 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 on a given input only if the other input is ``1``. Because if one input is ``0``, the other input can never affect the output. +#. XOR simply forwards all tags from its inputs to its output, because inputs to + XOR can always affect the output. +#. AND forwards tags on a given input 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. - Further, the code also does not consider that, when a signal affects multiple inputs of a cell, the resulting simultaneous changes of the inputs can cancel each other out, for example ``A ^ A`` or ``A ^ (B ^ A)`` is independent of ``A``, but its tags would be propagated nonetheless. +#. 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. Further, the code also does + not consider that, when a signal affects multiple inputs of a cell, the + resulting simultaneous changes of the inputs can cancel each other 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. +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 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. +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``. +``$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. +``$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. +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``. +``$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. +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. + 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. \ No newline at end of file +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. \ No newline at end of file