From ea6e5b3c48c44ea17470803d21c4c8b83a09ace9 Mon Sep 17 00:00:00 2001 From: Emily Schmidt Date: Thu, 10 Apr 2025 08:23:07 +0100 Subject: [PATCH] add changes to dft docs suggested by Krystine --- .../using_yosys/more_scripting/data_flow_tracking.rst | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 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 e13dfac7d..0bf5e567c 100644 --- a/docs/source/using_yosys/more_scripting/data_flow_tracking.rst +++ b/docs/source/using_yosys/more_scripting/data_flow_tracking.rst @@ -1,8 +1,11 @@ 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. +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 docs`_ to prove assertions involving these cells. + +.. _SBY docs: 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. @@ -20,6 +23,7 @@ For example, XOR, AND and OR cells propagate tags as follows: #. 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. @@ -29,6 +33,7 @@ Because of this propagation behaviour, we can answer questions about what signal 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. @@ -58,6 +63,7 @@ The main purpose of ``$overwrite_tag`` is adding tags to signals produced within 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.