terapines
/
circt
mirror of https://github.com/llvm/circt.git
2
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

[VerifToSMT] Fix lowering of no output, no result LEC op (#8763)

This commit is contained in:
Leon Hielscher 2025-07-22 18:16:17 +02:00 committed by GitHub
parent f0ec28ac16
commit e80a67d30d
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
2 changed files with 17 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

13
lib/Conversion/VerifToSMT/VerifToSMT.cpp
View File

@ -150,18 +150,23 @@ struct LogicEquivalenceCheckingOpConversion
auto *firstOutputs = adaptor.getFirstCircuit().front().getTerminator();
auto *secondOutputs = adaptor.getSecondCircuit().front().getTerminator();
auto hasNoResult = op.getNumResults() == 0;
if (firstOutputs->getNumOperands() == 0) {
// Trivially equivalent
Value trueVal =
rewriter.create<arith::ConstantOp>(loc, rewriter.getBoolAttr(true));
rewriter.replaceOp(op, trueVal);
if (hasNoResult) {
rewriter.eraseOp(op);
} else {
Value trueVal =
rewriter.create<arith::ConstantOp>(loc, rewriter.getBoolAttr(true));
rewriter.replaceOp(op, trueVal);
}
return success();
}
// Solver will only return a result when it is used to check the returned
// value.
smt::SolverOp solver;
auto hasNoResult = op.getNumResults() == 0;
if (hasNoResult)
solver = rewriter.create<smt::SolverOp>(loc, TypeRange{}, ValueRange{});
else

8
test/Conversion/VerifToSMT/verif-to-smt.mlir
View File

@ -83,6 +83,14 @@ func.func @test_lec(%arg0: !smt.bv<1>) -> (i1, i1, i1) {
verif.yield
}
verif.lec first {
^bb0(%arg1: i32):
verif.yield
} second {
^bb0(%arg1: i32):
verif.yield
}
verif.lec first {
^bb0(%arg1: i32):
verif.yield %arg1 : i32