share: add -pattern-limit to limit analysis effort #4904
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
The
share
pass uses SAT to find cells with same observability with regards to inputs of cells other than$mux
. First, it expresses the observability conditions as basically a logical function over the S inputs of$mux
cells infind_cell_activation_patterns
by traversing contiguous$mux
regions. This function is stored per cell as a sum of products inactivation_patterns_cache[cell]
. In some unfortunately shaped designs, the count of these products increases exponentially with the length of a chain of divering-converging muxes. This PR adds a user-configurable limit to how many "patterns" can be stored per cell. When this limit is exceeded, the cell is assumed to be always "active" in the sense that some of its input bits are always observable by outputs or cells other than multiplexers. This is always safe to do so as it can only inhibit merging cells. This limit is set to 1000 by default.To test, you can observe the linear rise of memory usage beyond any reasonable bounds when running
yosys -p "verific -sv slow-share.sv; prep; share"
on the following:While this reproducer uses kind of a lot of wire bits, it is a completely reasonable design pattern. Pre-share statistics:
share
is used fromsynth
commands