Description of the override transparency property needed for decomposition

In the SVTV decomposition methodology, we expect to be able to override the values of certain internal signals of a design in order to reason about fanout logic of those signals without including the fanin logic. In order to then compose these theorems with theorems about other decompositions of the design, we need to know that if we overrode those signals with the same values they would have anyway, then we get the same outputs. This is called the override transparency property. Here we explain that property more formally.

Override transparency is a property of an expression or set of expressions
with respect to (1) a set of *overridekeys* (a set of internal signals
that may be overridden) and (2) a substitution (svex-alist) giving the driving
expressions for those internal signals if those expressions evaluate the same
on environments that agree in a certain sense with respect to those variables.
(When discussing override-transparency of an FSM, we use the FSM's value
substitution for the driving expressions; an FSM is then override-transparent
on a set of keys if its value substitution and nextstate substitution are both
override-transparent with respect to those keys and the value substitution.) A
set of expressions is override-transparent if the expressions evaluate to the
same values on any two environments which are consistent on all override values
and agree strictly on all other variables. This notion of consistency on
overridden values essentially says that environment

To formalize this more completely we need a few definitions.

Each variable has an override property, which may be

Before we compose the local assignments for each signal of the circuit to
obtain the full update functions of all signals, we insert override muxes on
some or all internal signals, replacing each use of such signals with a bitwise
if-then-else expression:

We can now define the override consistency condition between environments.
In ACL2 this predicate is named

Environments *override-consistent* with respect to override signals

- Values of non-override variables and override test/value variables not in
S are equal in the two environments: $\backslash mathrm\{env\}\_1[s]\; =\; \backslash mathrm\{env\}\_2[s]$ $s\; \backslash notin\; S\; \backslash Rightarrow\; \backslash mathrm\{env\}\_1[s\_t]\; =\; \backslash mathrm\{env\}\_2[s\_t]$ $s\; \backslash notin\; S\; \backslash Rightarrow\; \backslash mathrm\{env\}\_1[s\_v]\; =\; \backslash mathrm\{env\}\_2[s\_v]$ - All signal bits overridden in
\mathrm{env}_2 are also overridden in\mathrm{env}_1 : $\backslash mathrm\{env\}\_2[s\_t][i]\; =\; 1\; \backslash Rightarrow\; \backslash mathrm\{env\}\_1[s\_t][i]\; =\; 1$ - Signal bits overridden in both environments are overridden to the same value: $\backslash mathrm\{env\}\_2[s\_t][i]\; =\; 1\; \backslash Rightarrow\; \backslash mathrm\{env\}\_1[s\_v][i]\; =\; \backslash mathrm\{env\}\_2[s\_v][i]$
- Signal bits overridden in
\mathrm{env}_1 and not\mathrm{env}_2 are overridden there to the corresponding bit of the evaluation with\mathrm{env}_2 of that signal's binding in\sigma : $\backslash mathrm\{env\}\_1[s\_t][i]\; =\; 1\; \backslash wedge\; \backslash mathrm\{env\}\_2[s\_t][i]\; \backslash neq\; 1\; \backslash Rightarrow\; \backslash mathrm\{env\}\_1[s\_v][i]\; =\; \backslash textrm\{Ev\}(\backslash sigma[s],\backslash mathrm\{env\}\_2)[i]$

Finally, we can now define the override transparency property of expressions, expression lists, and substitutions. This is parametrized on the same set of variables and substitution as in the override consistency of environments, and simply says that for any two environments that satisfy the override consistency condition, the evaluations of that expression/expression list/substitution on those two environments are equal.