Add abstract pass for formal verification
#4894
Open
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
…state, -init temporarily gutted
In the past we had the occasional bug due to some place not handling all 4 combinations of upto/downto and zero/nonzero start_offset correctly.
This fixes the offsets_to_abstract collection in abstract_state so that it now works the same way as in abstract_value which was already correct.
Also improves -enable and -enablen command line handling
Print the port bit instead of the arbitrary representative sigbit to identify the target of the abstraction operation.
widlarizer
force-pushed
the
emil/abstract
branch
from
d3b3f6b to
925c617
Compare
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
This PR adds a new
abstractpass to allow reducing and never increasing the constraints on a circuit's behavior in a formal verification setting. This pass allows removinginitattributes (-init) and multiplexing arbitrary wires (-valuemode) or flip flop internal states (-statemode). It is intended to be used with narrow selections. Debug logs explain which changes are triggered by which selected objects.abstract -valueto work on module inputs, not just cell outputs