[circt-bmc] Include bound in violation and success messages#10051
Open
AnmolM-777 wants to merge 1 commit intollvm:mainfrom
Open
[circt-bmc] Include bound in violation and success messages#10051AnmolM-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.
TaoBi22
reviewed
Mar 27, 2026
Contributor
TaoBi22
left a comment
TaoBi22
left a comment
There was a problem hiding this comment.
Hi @AnmolM-777, thanks for taking a look at this. I think this change could be slightly misleading in its current form - a user could reasonably expect that the message indicates that the assertions were first violated after the given number of cycles (whereas the output will obviously actually just be the maximal bound). Not the end of the world, but given the only information we're feeding back to the user is a command line argument they provided themselves anyway, I wonder if it's worth the tradeoff? Happy to discuss if you have a use-case for this though!
Comment on lines
+212
to
+217
| auto successStrAddr = createUniqueStringGlobal( | ||
| "Bound reached with no violations within " + std::to_string(bound) + | ||
| " clock cycle(s).\n"); | ||
| auto failureStrAddr = createUniqueStringGlobal( | ||
| "Assertion can be violated within " + std::to_string(bound) + | ||
| " clock cycle(s)!\n"); |
Contributor
There was a problem hiding this comment.
This probably needs corresponding integration tests changed too.
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 patch improves the user-facing output of circt-bmc by including
the bound count in both the success and failure messages.
Previously:
"Assertion can be violated!"
"Bound reached with no violations!"
Now:
"Assertion can be violated within 10 clock cycle(s)!"
"Bound reached with no violations within 10 clock cycle(s)."
This makes the output more informative for users debugging hardware
designs, as they immediately know the bound at which the check was run.
This is part of the GSoC 2026 project: "Generate Counter Examples for
Bounded Model Checks in CIRCT".
I am a GSoC applicant working on the counterexample feature and this is my first contribution, would love to make any changes or improvements given the chance !