mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-06-09 23:53:26 +00:00
Code Activity

reflow dft docs to 80 cols

Browse source
This commit is contained in:
Emily Schmidt 2025-04-10 08:43:21 +01:00 • committed by Emily (aiju)
parent bfed96ad88
commit 19845be85c
1 changed files with 76 additions and 39 deletions
Download patch file Download diff file Expand all files Collapse all files

115
docs/source/using_yosys/more_scripting/data_flow_tracking.rst
View file

@ -1,77 +1,114 @@
Dataflow tracking Dataflow tracking
------------------- -------------------
Yosys can be used to answer questions such as "can this signal affect this other signal?" via its *dataflow tracking* support. Yosys can be used to answer questions such as "can this signal affect this other
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. signal?" via its *dataflow tracking* support. For this, four special cells,
Typically, one would then use `SBY`_ to prove assertions involving these 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 .. _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``). Ordinarily in Yosys, the state of a bit is simply ``0`` or ``1`` (or one of the
During dataflow tracking they are augmented with a set of tags. special values, ``z`` and ``x``). During dataflow tracking they are augmented
For example, the state of a bit could be ``0`` and the set of tags ``"KEY"`` and ``"OVERFLOW"``. 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. In addition to their usual operations on the logical bits, Yosys operations must
For this, tags are simply *forwarded* or *propagated* (i.e. copied) from inputs to outputs, according to the following general rule: 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: 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. #. XOR simply forwards all tags from its inputs to its output, because inputs to
#. 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 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``. #. Similarly, OR forwards tags only if the other input is ``0``.
There are two exceptions to this rule: There are two exceptions to this rule:
#. In general, propagation is only determined approximately. #. In general, propagation is only determined approximately. For example, unless
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. the ``dft_tag`` code knows about a cell, it simply assumes the worst-case
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. 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). #. 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 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. As an example use case, consider a cryptographic processor which is not supposed
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. to expose its secret keys to the outside world. We can tag all key bits with the
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. ``"KEY"`` tag and use `SBY`_ to formally verify that no external signal ever
However we can still easily detect, if e.g. an engineer forgot to remove debugging code that allows reading back key data. 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. As a different use case, we can modify all adders in the design to set the
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. ``"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 Semantics of dataflow tracking cells
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
``$set_tag`` has inputs ``A``, ``SET``, ``CLR``, an output ``Y`` and a string parameter ``TAG``. ``$set_tag`` has inputs ``A``, ``SET``, ``CLR``, an output ``Y`` and a string
The logic value of ``A`` and all tags other than the one named by the ``TAG`` parameter are simply copied to ``Y``. parameter ``TAG``. The logic value of ``A`` and all tags other than the one
If ``SET`` is ``1``, then the named tag is added to ``Y``. named by the ``TAG`` parameter are simply copied to ``Y``. If ``SET`` is ``1``,
Otherwise, if ``CLR`` is ``1``, then the named tag is removed. then the named tag is added to ``Y``. Otherwise, if ``CLR`` is ``1``, then the
Otherwise, the tag is unchanged, i.e. it is present in ``Y`` if it is present in ``A``. 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`` has an input ``A`` and an output ``Y`` and a string parameter
``$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. ``TAG``. ``$get_tag`` inspects ``A`` for the presence or absence of a tag of the
The logical value of ``A`` is completely ignored. 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. ``$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. Instead of providing a modified version of the input signal, it modifies the
The main purpose of ``$overwrite_tag`` is adding tags to signals produced within a module that cannot or should not be modified itself. 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
~~~~~~~~~~~~~~ ~~~~~~~~~~~~~~
Tag groups are an advanced feature that modify the propagation rule discussed above. Tag groups are an advanced feature that modify the propagation rule discussed
To use tag groups, simply name tags according to the schema ``"group:name"``. above. To use tag groups, simply name tags according to the schema
For example, ``"key:0"``, ``"key:a"``, ``"key:b"`` would be three tags in the ``"key"`` group. ``"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 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. For example, an AND gate will propagate a given tag on one input, if the other
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``. input is either 1 or carries a tag of the same group. So if one input is ``0,
Note that if we add an unrelated ``"overflow"`` tag to the first input, it would still not be propagated. "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.