[Verif] LowerContractsPass #7870
Conversation
leonardt
commented
Nov 21, 2024
leonardt
commented
- Adds pass to convert hw modules containing contracts into verif.formal tests with contracts inlined
- ensure -> assert, require -> assume
- Adds tests for multiplier, carry save compressor, and shift left
| // SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception | ||
| //===----------------------------------------------------------------------===// |
There was a problem hiding this comment.
| // SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception | |
| //===----------------------------------------------------------------------===// | |
| // SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception | |
| // | |
| //===----------------------------------------------------------------------===// |
| //===----------------------------------------------------------------------===// | ||
| #include "circt/Dialect/Verif/VerifOps.h" |
There was a problem hiding this comment.
| //===----------------------------------------------------------------------===// | |
| #include "circt/Dialect/Verif/VerifOps.h" | |
| //===----------------------------------------------------------------------===// | |
| #include "circt/Dialect/Verif/VerifOps.h" |
| LogicalResult matchAndRewrite(HWModuleOp op, | ||
| PatternRewriter &rewriter) const override { | ||
| auto formalOp = rewriter.create<verif::FormalOp>( | ||
| op.getLoc(), op.getNameAttr(), rewriter.getDictionaryAttr({})); |
There was a problem hiding this comment.
What if there's no verif.contract op in the module? In that case we want to just leave the module as-is, right? Because the top-level of the test is already wrapped in a verif.formal and just arbitrarily splitting out this module and proving it separately won't work.
| auto formalOp = rewriter.create<verif::FormalOp>( | ||
| op.getLoc(), op.getNameAttr(), rewriter.getDictionaryAttr({})); | ||
|
|
||
| // Clone module body into fomal op body |
There was a problem hiding this comment.
| // Clone module body into fomal op body | |
| // Clone module body into formal op body |
| replaceContractOp<RequireOp, AssumeOp>(rewriter, contractBlock); | ||
|
|
||
| // Inline body | ||
| rewriter.inlineBlockBefore(&contractOp.getBody().front(), |
There was a problem hiding this comment.
| rewriter.inlineBlockBefore(&contractOp.getBody().front(), | |
| rewriter.inlineBlockBefore(contractBlock, |
| &formalOp.getBody().front(), | ||
| formalOp.getBody().front().end()); |
There was a problem hiding this comment.
| &formalOp.getBody().front(), | |
| formalOp.getBody().front().end()); | |
| bodyBlock, | |
| bodyBlock->end()); |
| rewriter.eraseOp(contractOp); | ||
| } | ||
|
|
||
| rewriter.eraseOp(op); |
There was a problem hiding this comment.
You cannot just delete the module here, instead you want to apply the contracts (i.e., assume they hold to simplify the body of the module).
| patterns.add<HWOpRewritePattern>(patterns.getContext()); | ||
|
|
||
| if (failed(applyPatternsAndFoldGreedily(getOperation(), std::move(patterns)))) | ||
| signalPassFailure(); |
There was a problem hiding this comment.
Since you are only matching on modules, you can also just have a for loop iterating over the modules, which would be a bit more efficient.
There was a problem hiding this comment.
This file contains tests that are great as integration tests, but for regression tests we want to check the corner cases and keep the tests small (they don't have to do something that makes sense from a design implementation/logics perspective). For example, there's no test of a module with more than one contract inside, with zero contracts inside. Deleting the module also only works because you have no other module instantiating it.
