Add sensitivity analysis to replace unsound onehot optimization
- Dominant language
- C++
- Stars
- 1.9k
- Forks
- 283
- Avg merge
- 2d 10h
- Merged PRs (30d)
- 135
Description
The following optimization is unsound and is being removed: https://github.com/google/xls/blob/24046e424af962efd2b151d383cb9e01071bc1c8/xls/passes/bdd_simplification_pass.cc#L327
Reasoning:
The transformation tries to determine if the most-significant bit of a one-hot output can affect the value of some other node and if not zero out the msb. It does this by making two different assumptions:
(1) assume the output of the one-hot is 0.
(2) assume the output of the one-hot is 1000...0.
And then checking if these assumptions both imply an identical value V for some other node X. If so, then most-significant bit of the one-hot is zero'd out via slicing and concat with zero. Fundamentally, what this is trying to imply is that the output of node X is not sensitive to the msb of the one-hot. However, this does not follow. For example in the following code, X produces the same value if the one-hot value is 0000 or 1000, but the value of X is sensitive to the msb of the onehot:
onehot: bits[4] = onehot(input)
X: bits[1] = !onehot[3] & onehot[2]
The transformation would replace the value of X with 0. However, an input value of 100 produces an X value of one.
A correct way of handling this is to add a sensitivity analysis to the query engine. Something like:
bool QueryEngine::IsSensitiveTo(BitLocation a, BitLocation b)
Returns true if the bit 'b' can be affected by the value of bit 'a'. This information can be extracted from a BDD. Each bit B in the XLS graph has a corresponding node in the BDD, and by traversing the BDD you can find all other bits which are inputs to the B's boolean expression. Special handling will be required for our saturating BDD which creates new nodes for overly complex expressions, but something reasonable can likely be worked out.
Contributor guide
Assessment
This issue has not been assessed yet.