[circt-bmc] Include bound in violation and success messages#10056
Open
AnmolM-777 wants to merge 1 commit intollvm:mainfrom
Open
[circt-bmc] Include bound in violation and success messages#10056AnmolM-777 wants to merge 1 commit intollvm:mainfrom
AnmolM-777 wants to merge 1 commit intollvm:mainfrom
Conversation
Previously, circt-bmc printed generic messages with no context about at which bound a violation was found. This patch includes the bound count in both the success and failure messages, making the output more informative for users debugging hardware designs.
Contributor
|
This seems to be a duplicate of #10051 |
This file contains hidden or 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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
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 improves the output messages of
circt-bmcby including the boundinformation in both violation and success cases.
Previously, the tool printed generic messages such as:
"Assertion can be violated!"
which provided no context about when the violation occurred.
With this change, the messages now include the bound value, e.g.:
"Assertion can be violated within 10 clock cycle(s)!"
"Bound reached with no violations within 10 clock cycle(s)."
This makes the output significantly more informative for users debugging
hardware designs, as they can immediately understand the depth at which
the result was obtained.
Changes:
LowerToBMC.cppTesting:
lower-to-bmc.mlirtest using llvm-litAdditional work:
I also explored adding counterexample (model) printing support in
SMTToZ3LLVM, but ran into issues related to IR insertion and lowering.
I plan to revisit this with guidance on the correct insertion point.