Onehot-rewriting
Conservatively rewrite 4v-sexprs by assuming some variables
are one-hot.
Introduction
Sometimes you know that certain inputs to a module are supposed to be
one-hot. Using this information, it may be possible to simplify the sexprs
produced during esim runs. For example, if we know that the variables
A1 and A2 are one-hot, we might like to rewrite a sexpr like:
(ITE A1 (AND A2 FOO) BAR)
Here, we can "see" that A2 has to be false in the true-branch since
to get there we must have that A1 is true. Accordingly, we would like to
replace the sexpr with something like:
(AND (NOT A1) BAR)
This sort of rewriting may occasionally help to avoid combinational loops
that are only broken when the inputs are truly one-hot, e.g., notice how the
variable FOO has dropped out of the expression above.
The Basic Transformation
Our main function for onehot rewriting is 4v-onehot-rw-sexpr. Given
a list of variables A1...AN that we think are one-hot, and an s-expression
SEXPR to rewrite, it basically constructs:
(ITE* ONEHOT-P SEXPR' (X))
Where:
- ONEHOT-P is constructed by 4vs-onehot and evaluates to
T when the A1...N are one-hot, and
- SEXPR' is formed
from SEXPR by assuming A1...N are indeed one-hot; see 4v-onehot-sexpr-prime for details.
We prove this conservatively approximates SEXPR, but keep in mind that
this approximation is not an equivalent term! For instance, the
rewritten expression will always produce X if it turns out that the inputs
were not really one-hot. Accordingly, you should only use this rewrite when
you are really are certain the variables will be one-hot.
The Alist Transformation
Our main use for onehot rewriting is in simplifiers for esim-simplify-update-fns, where the goal is to rewrite a whole alist binding
names to sexprs.
Our main function for this is 4v-onehot-rw-sexpr-alist, which
takes the list of one-hot variables and the alist to rewrite as arguments.
This function is reasonably clever: it avoids changing sexprs that don't
mention any of the onehot variables, and it has some other performance
optimizations that are geared toward reusing memoized results across
sexprs.
Subtopics
- 4v-onehot-sexpr-list-prime
- Efficiently reduce a list of sexprs under the assumption that some
variables are one-hot.
- 4v-onehot-sexpr-prime
- (4v-onehot-sexpr-prime vars sexpr) rewrites sexpr under the
assumption that vars are one-hot.
- 4v-onehot-rw-sexpr-alist-aux
- Apply one-hot rewriting to a sexpr-alist.
- 4v-onehot-rw-sexpr-alist
- Apply onehot-rewriting to a sexpr alist.
- 4v-onehot-rw-sexpr
- Apply onehot-rewriting to a single s-expression.
- 4vs-onehot
- (4vs-onehot sexprs) constructs an s-expression that is T when the
members of X are one-hot.
- 4vs-ite*-list-dumb
- (4vs-ite*-list-dumb c as bs) produces a list of sexprs, basically
(4V-ITE* C Ai Bi) for the corresponding elements of AS and BS.
- 4v-onehot-filter
- Filter a sexpr-alist to avoid unnecessary onehot-rewriting.
- 4v-onehot-list-p
- (4v-onehot-list-p x) determines if a list of 4vps has
exactly one member that is T while the rest are F.
