[Verif][circt-bmc] Add verif.bmc op and circt-bmc tool
#7259
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
TaoBi22
commented
Jul 2, 2024
Comment on lines
+69
to
+115
| // Fail to convert unsupported verif ops to avoid silent failure | ||
| struct VerifCoverOpConversion : OpConversionPattern<verif::CoverOp> { | ||
| using OpConversionPattern<verif::CoverOp>::OpConversionPattern; | ||
|
|
||
| LogicalResult | ||
| matchAndRewrite(verif::CoverOp op, OpAdaptor adaptor, | ||
| ConversionPatternRewriter &rewriter) const override { | ||
| return op.emitError("Conversion of CoverOps to SMT not yet supported"); | ||
| }; | ||
| }; | ||
|
|
||
| struct VerifClockedAssertOpConversion | ||
| : OpConversionPattern<verif::ClockedAssertOp> { | ||
| using OpConversionPattern<verif::ClockedAssertOp>::OpConversionPattern; | ||
|
|
||
| LogicalResult | ||
| matchAndRewrite(verif::ClockedAssertOp op, OpAdaptor adaptor, | ||
| ConversionPatternRewriter &rewriter) const override { | ||
| return op.emitError( | ||
| "Conversion of ClockedAssertOps to SMT not yet supported"); | ||
| }; | ||
| }; | ||
|
|
||
| struct VerifClockedCoverOpConversion | ||
| : OpConversionPattern<verif::ClockedCoverOp> { | ||
| using OpConversionPattern<verif::ClockedCoverOp>::OpConversionPattern; | ||
|
|
||
| LogicalResult | ||
| matchAndRewrite(verif::ClockedCoverOp op, OpAdaptor adaptor, | ||
| ConversionPatternRewriter &rewriter) const override { | ||
| return op.emitError( | ||
| "Conversion of ClockedCoverOps to SMT not yet supported"); | ||
| }; | ||
| }; | ||
|
|
||
| struct VerifClockedAssumeOpConversion | ||
| : OpConversionPattern<verif::ClockedAssumeOp> { | ||
| using OpConversionPattern<verif::ClockedAssumeOp>::OpConversionPattern; | ||
|
|
||
| LogicalResult | ||
| matchAndRewrite(verif::ClockedAssumeOp op, OpAdaptor adaptor, | ||
| ConversionPatternRewriter &rewriter) const override { | ||
| return op.emitError( | ||
| "Conversion of ClockedAssumeOps to SMT not yet supported"); | ||
| }; | ||
| }; | ||
|
|
There was a problem hiding this comment.
Not totally sure if this is necessary, but my thinking is that without these patterns the errors produced will likely be pretty opaque to someone not familiar with CIRCT/MLIR internals, which maybe isn't ideal for this tool.
|
Can this be split up into
|
That should be fine, thanks for the suggestion! |
|
New op PR now up at #7263 |
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 (based on an initial draft by @maerhart, thanks!) introduces a bounded model checking tool based on the SMT dialect, similar to the updated circt-lec tool.
To achieve this, a BMC op is added to the verif dialect - in order to support multiple clocks in the near future, this has init and loop regions that allow the manipulation of clocks to be specified (e.g. so that specific interleavings can be explored). These regions are allowed some extra state arguments, as is likely necessary for specifying clock interleavings (e.g. to say which clock's turn it is to be toggled next).
Sorry for the big diff!