mirror of https://github.com/llvm/circt.git
[VerifToSMT] Lower `verif.refines` to SMT (#8749)
Implement a conversion pattern for the `verif.refines` operation to the SMT dialect.
This commit is contained in:
Leon Hielscher
GitHub
parent
186dcc8b0e
commit
ab7a0a6c85
|
|
@ -222,6 +222,132 @@ struct LogicEquivalenceCheckingOpConversion
|
|||
}
|
||||
};
|
||||
|
||||
struct RefinementCheckingOpConversion
|
||||
: CircuitRelationCheckOpConversion<verif::RefinementCheckingOp> {
|
||||
using CircuitRelationCheckOpConversion<
|
||||
verif::RefinementCheckingOp>::CircuitRelationCheckOpConversion;
|
||||
|
||||
LogicalResult
|
||||
matchAndRewrite(verif::RefinementCheckingOp op, OpAdaptor adaptor,
|
||||
ConversionPatternRewriter &rewriter) const override {
|
||||
|
||||
// Find non-deterministic values (free variables) in the source circuit.
|
||||
// For now, only support quantification over 'primitive' types.
|
||||
SmallVector<Value> srcNonDetValues;
|
||||
bool canBind = true;
|
||||
for (auto ndOp : op.getFirstCircuit().getOps<smt::DeclareFunOp>()) {
|
||||
if (!isa<smt::IntType, smt::BoolType, smt::BitVectorType>(
|
||||
ndOp.getType())) {
|
||||
ndOp.emitError("Uninterpreted function of non-primitive type cannot be "
|
||||
"converted.");
|
||||
canBind = false;
|
||||
}
|
||||
srcNonDetValues.push_back(ndOp.getResult());
|
||||
}
|
||||
if (!canBind)
|
||||
return failure();
|
||||
|
||||
if (srcNonDetValues.empty()) {
|
||||
// If there is no non-determinism in the source circuit, the
|
||||
// refinement check becomes an equivalence check, which does not
|
||||
// need quantified expressions.
|
||||
auto eqOp = rewriter.create<verif::LogicEquivalenceCheckingOp>(
|
||||
op.getLoc(), op.getNumResults() != 0);
|
||||
rewriter.moveBlockBefore(&op.getFirstCircuit().front(),
|
||||
&eqOp.getFirstCircuit(),
|
||||
eqOp.getFirstCircuit().end());
|
||||
rewriter.moveBlockBefore(&op.getSecondCircuit().front(),
|
||||
&eqOp.getSecondCircuit(),
|
||||
eqOp.getSecondCircuit().end());
|
||||
rewriter.replaceOp(op, eqOp);
|
||||
return success();
|
||||
}
|
||||
|
||||
Location loc = op.getLoc();
|
||||
auto *firstOutputs = adaptor.getFirstCircuit().front().getTerminator();
|
||||
auto *secondOutputs = adaptor.getSecondCircuit().front().getTerminator();
|
||||
|
||||
auto hasNoResult = op.getNumResults() == 0;
|
||||
|
||||
if (firstOutputs->getNumOperands() == 0) {
|
||||
// Trivially equivalent
|
||||
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;
|
||||
if (hasNoResult)
|
||||
solver = rewriter.create<smt::SolverOp>(loc, TypeRange{}, ValueRange{});
|
||||
else
|
||||
solver = rewriter.create<smt::SolverOp>(loc, rewriter.getI1Type(),
|
||||
ValueRange{});
|
||||
rewriter.createBlock(&solver.getBodyRegion());
|
||||
|
||||
// Convert the block arguments of the miter bodies.
|
||||
if (failed(rewriter.convertRegionTypes(&adaptor.getFirstCircuit(),
|
||||
*typeConverter)))
|
||||
return failure();
|
||||
if (failed(rewriter.convertRegionTypes(&adaptor.getSecondCircuit(),
|
||||
*typeConverter)))
|
||||
return failure();
|
||||
|
||||
// Create the symbolic values we replace the block arguments with
|
||||
SmallVector<Value> inputs;
|
||||
for (auto arg : adaptor.getFirstCircuit().getArguments())
|
||||
inputs.push_back(rewriter.create<smt::DeclareFunOp>(loc, arg.getType()));
|
||||
|
||||
// Inline the target circuit. Free variables remain free variables.
|
||||
rewriter.mergeBlocks(&adaptor.getSecondCircuit().front(), solver.getBody(),
|
||||
inputs);
|
||||
rewriter.setInsertionPointToEnd(solver.getBody());
|
||||
|
||||
// Create the universally quantified expression containing the source
|
||||
// circuit. Free variables in the circuit's body become bound variables.
|
||||
auto forallOp = rewriter.create<smt::ForallOp>(
|
||||
op.getLoc(), TypeRange(srcNonDetValues),
|
||||
[&](OpBuilder &builder, auto, ValueRange args) -> Value {
|
||||
// Inline the source circuit
|
||||
Block *body = builder.getBlock();
|
||||
rewriter.mergeBlocks(&adaptor.getFirstCircuit().front(), body,
|
||||
inputs);
|
||||
|
||||
// Replace non-deterministic values with the quantifier's bound
|
||||
// variables
|
||||
for (auto [freeVar, boundVar] : llvm::zip(srcNonDetValues, args))
|
||||
rewriter.replaceOp(freeVar.getDefiningOp(), boundVar);
|
||||
|
||||
// Compare the output values
|
||||
rewriter.setInsertionPointToEnd(body);
|
||||
SmallVector<Value> outputsDifferent;
|
||||
createOutputsDifferentOps(firstOutputs, secondOutputs, loc, rewriter,
|
||||
outputsDifferent);
|
||||
if (outputsDifferent.size() == 1)
|
||||
return outputsDifferent[0];
|
||||
else
|
||||
return rewriter.createOrFold<smt::OrOp>(loc, outputsDifferent);
|
||||
});
|
||||
|
||||
rewriter.eraseOp(firstOutputs);
|
||||
rewriter.eraseOp(secondOutputs);
|
||||
|
||||
// Assert the quantified expression
|
||||
rewriter.setInsertionPointAfter(forallOp);
|
||||
rewriter.create<smt::AssertOp>(op.getLoc(), forallOp.getResult());
|
||||
|
||||
// Check for satisfiability and report the result back.
|
||||
replaceOpWithSatCheck(op, loc, rewriter, solver);
|
||||
return success();
|
||||
}
|
||||
};
|
||||
|
||||
/// Lower a verif::BMCOp operation to an MLIR program that performs the bounded
|
||||
/// model check
|
||||
struct VerifBoundedModelCheckingOpConversion
|
||||
|
|
@ -534,8 +660,9 @@ void circt::populateVerifToSMTConversionPatterns(TypeConverter &converter,
|
|||
Namespace &names,
|
||||
bool risingClocksOnly) {
|
||||
patterns.add<VerifAssertOpConversion, VerifAssumeOpConversion,
|
||||
LogicEquivalenceCheckingOpConversion>(converter,
|
||||
patterns.getContext());
|
||||
LogicEquivalenceCheckingOpConversion,
|
||||
RefinementCheckingOpConversion>(converter,
|
||||
patterns.getContext());
|
||||
patterns.add<VerifBoundedModelCheckingOpConversion>(
|
||||
converter, patterns.getContext(), names, risingClocksOnly);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -168,3 +168,23 @@ func.func @wrong_initial_type() -> (i1) {
|
|||
}
|
||||
func.return %bmc : i1
|
||||
}
|
||||
|
||||
// -----
|
||||
|
||||
func.func @refines_non_primitive_free_var() -> () {
|
||||
// expected-error @below {{failed to legalize operation 'verif.refines' that was explicitly marked illegal}}
|
||||
verif.refines first {
|
||||
^bb0(%arg0: !smt.bv<4>):
|
||||
// expected-error @below {{Uninterpreted function of non-primitive type cannot be converted.}}
|
||||
%nondetar = smt.declare_fun : !smt.array<[!smt.bv<4> -> !smt.bv<32>]>
|
||||
%sel = smt.array.select %nondetar[%arg0] : !smt.array<[!smt.bv<4> -> !smt.bv<32>]>
|
||||
%cc = builtin.unrealized_conversion_cast %sel : !smt.bv<32> to i32
|
||||
verif.yield %cc : i32
|
||||
} second {
|
||||
^bb0(%arg0: !smt.bv<4>):
|
||||
%const = smt.bv.constant #smt.bv<0> : !smt.bv<32>
|
||||
%cc = builtin.unrealized_conversion_cast %const : !smt.bv<32> to i32
|
||||
verif.yield %cc : i32
|
||||
}
|
||||
return
|
||||
}
|
||||
|
|
|
|||
|
|
@ -244,3 +244,214 @@ func.func @large_initial_value() -> (i1) {
|
|||
}
|
||||
func.return %bmc : i1
|
||||
}
|
||||
|
||||
// -----
|
||||
|
||||
// CHECK-LABEL: func @test_refines_noreturn
|
||||
|
||||
// CHECK: smt.solver() : () -> () {
|
||||
// CHECK: [[V0:%.+]] = smt.declare_fun : !smt.bv<32>
|
||||
// CHECK: [[V1:%.+]] = smt.distinct [[V0]], [[V0]] : !smt.bv<32>
|
||||
// CHECK: smt.assert [[V1]]
|
||||
// CHECK: smt.check sat {
|
||||
// CHECK-NEXT: } unknown {
|
||||
// CHECK-NEXT: } unsat {
|
||||
// CHECK-NEXT: }
|
||||
// CHECK-NEXT: }
|
||||
|
||||
func.func @test_refines_noreturn() -> () {
|
||||
verif.refines first {
|
||||
^bb0(%arg1: i32):
|
||||
verif.yield %arg1 : i32
|
||||
} second {
|
||||
^bb0(%arg1: i32):
|
||||
verif.yield %arg1 : i32
|
||||
}
|
||||
|
||||
// CHECK-NOT: smt.solver
|
||||
// CHECK: return
|
||||
verif.refines first {
|
||||
^bb0():
|
||||
verif.yield
|
||||
} second {
|
||||
^bb0():
|
||||
verif.yield
|
||||
}
|
||||
|
||||
return
|
||||
}
|
||||
|
||||
// -----
|
||||
|
||||
// CHECK-LABEL: func.func @test_refines_withreturn
|
||||
|
||||
// CHECK: [[RT0:%.+]] = smt.solver() : () -> i1 {
|
||||
// CHECK: [[V0:%.+]] = smt.declare_fun : !smt.bv<32>
|
||||
// CHECK: [[V1:%.+]] = smt.distinct [[V0]], [[V0]] : !smt.bv<32>
|
||||
// CHECK: smt.assert [[V1]]
|
||||
// CHECK-DAG: [[TRUE:%.+]] = arith.constant true
|
||||
// CHECK-DAG: [[FALSE:%.+]] = arith.constant false
|
||||
// CHECK: [[V2:%.+]] = smt.check sat {
|
||||
// CHECK-NEXT: smt.yield [[FALSE]]
|
||||
// CHECK-NEXT: } unknown {
|
||||
// CHECK-NEXT: smt.yield [[FALSE]]
|
||||
// CHECK-NEXT: } unsat {
|
||||
// CHECK-NEXT: smt.yield [[TRUE]]
|
||||
// CHECK-NEXT: }
|
||||
// CHECK-NEXT: smt.yield [[V2]]
|
||||
// CHECK-NEXT: }
|
||||
// CHECK: return [[RT0]] : i1
|
||||
|
||||
func.func @test_refines_withreturn() -> i1 {
|
||||
%0 = verif.refines : i1 first {
|
||||
^bb0(%arg1: i32):
|
||||
verif.yield %arg1 : i32
|
||||
} second {
|
||||
^bb0(%arg1: i32):
|
||||
verif.yield %arg1 : i32
|
||||
}
|
||||
return %0 : i1
|
||||
}
|
||||
|
||||
// -----
|
||||
|
||||
// CHECK-LABEL: func.func @test_refines_trivialreturn
|
||||
|
||||
// CHECK-NOT: smt.solver
|
||||
// CHECK: [[CST:%.+]] = arith.constant true
|
||||
// CHECK: return [[CST]] : i1
|
||||
|
||||
func.func @test_refines_trivialreturn() -> i1 {
|
||||
%0 = verif.refines : i1 first {
|
||||
^bb0():
|
||||
verif.yield
|
||||
} second {
|
||||
^bb0():
|
||||
verif.yield
|
||||
}
|
||||
return %0 : i1
|
||||
}
|
||||
|
||||
// -----
|
||||
|
||||
// Source circuit non-deterministic
|
||||
|
||||
// CHECK-LABEL: func.func @nondet_to_det
|
||||
|
||||
// CHECK: smt.solver()
|
||||
// CHECK: [[BVCST:%.+]] = smt.bv.constant #smt.bv<0> : !smt.bv<32>
|
||||
// CHECK: [[ALLQ:%.+]] = smt.forall {
|
||||
// CHECK-NEXT: ^bb0([[BVAR:%.+]]: !smt.bv<32>)
|
||||
// CHECK-NEXT: [[V0:%.+]] = smt.distinct [[BVAR]], [[BVCST]] : !smt.bv<32>
|
||||
// CHECK-NEXT: smt.yield [[V0]] : !smt.bool
|
||||
// CHECK-NEXT: }
|
||||
// CHECK-NEXT: smt.assert [[ALLQ]]
|
||||
// CHECK-NEXT: smt.check
|
||||
|
||||
|
||||
func.func @nondet_to_det() -> () {
|
||||
verif.refines first {
|
||||
^bb0():
|
||||
%nondet = smt.declare_fun : !smt.bv<32>
|
||||
%cc = builtin.unrealized_conversion_cast %nondet : !smt.bv<32> to i32
|
||||
verif.yield %cc : i32
|
||||
} second {
|
||||
^bb0():
|
||||
%const = smt.bv.constant #smt.bv<0> : !smt.bv<32>
|
||||
%cc = builtin.unrealized_conversion_cast %const : !smt.bv<32> to i32
|
||||
verif.yield %cc : i32
|
||||
}
|
||||
return
|
||||
}
|
||||
|
||||
// -----
|
||||
|
||||
// Target circuit non-deterministic
|
||||
|
||||
// CHECK-LABEL: func.func @det_to_nondet
|
||||
|
||||
// CHECK: smt.solver()
|
||||
// CHECK-DAG: [[BVCST:%.+]] = smt.bv.constant #smt.bv<0> : !smt.bv<32>
|
||||
// CHECK-DAG: [[FREEVAR:%.+]] = smt.declare_fun : !smt.bv<32>
|
||||
// CHECK: [[V0:%.+]] = smt.distinct [[BVCST]], [[FREEVAR]]
|
||||
// CHECK-NEXT: smt.assert [[V0]]
|
||||
// CHECK-NEXT: smt.check
|
||||
|
||||
func.func @det_to_nondet() -> () {
|
||||
verif.refines first {
|
||||
^bb0():
|
||||
%const = smt.bv.constant #smt.bv<0> : !smt.bv<32>
|
||||
%cc = builtin.unrealized_conversion_cast %const : !smt.bv<32> to i32
|
||||
verif.yield %cc : i32
|
||||
} second {
|
||||
^bb0():
|
||||
%nondet = smt.declare_fun : !smt.bv<32>
|
||||
%cc = builtin.unrealized_conversion_cast %nondet : !smt.bv<32> to i32
|
||||
verif.yield %cc : i32
|
||||
}
|
||||
return
|
||||
}
|
||||
// -----
|
||||
|
||||
// Both circuits non-deterministic
|
||||
|
||||
// CHECK-LABEL: func.func @nondet_to_nondet
|
||||
|
||||
// CHECK: smt.solver()
|
||||
// CHECK: [[FREEVAR:%.+]] = smt.declare_fun : !smt.bv<32>
|
||||
// CHECK: [[ALLQ:%.+]] = smt.forall {
|
||||
// CHECK-NEXT: ^bb0([[BVAR:%.+]]: !smt.bv<32>)
|
||||
// CHECK-NEXT: [[V0:%.+]] = smt.distinct [[BVAR]], [[FREEVAR]] : !smt.bv<32>
|
||||
// CHECK-NEXT: smt.yield [[V0]] : !smt.bool
|
||||
// CHECK-NEXT: }
|
||||
// CHECK-NEXT: smt.assert [[ALLQ]]
|
||||
// CHECK-NEXT: smt.check
|
||||
|
||||
func.func @nondet_to_nondet() -> () {
|
||||
verif.refines first {
|
||||
^bb0():
|
||||
%nondet = smt.declare_fun : !smt.bv<32>
|
||||
%cc = builtin.unrealized_conversion_cast %nondet : !smt.bv<32> to i32
|
||||
verif.yield %cc : i32
|
||||
} second {
|
||||
^bb0():
|
||||
%nondet = smt.declare_fun : !smt.bv<32>
|
||||
%cc = builtin.unrealized_conversion_cast %nondet : !smt.bv<32> to i32
|
||||
verif.yield %cc : i32
|
||||
}
|
||||
return
|
||||
}
|
||||
|
||||
// -----
|
||||
|
||||
// Multiple non-deterministic values in the source circuit
|
||||
|
||||
// CHECK-LABEL: func.func @multi_nondet
|
||||
// CHECK: smt.solver()
|
||||
// CHECK: [[FREEVAR:%.+]] = smt.declare_fun : !smt.bv<32>
|
||||
// CHECK: [[ALLQ:%.+]] = smt.forall {
|
||||
// CHECK-NEXT: ^bb0([[BVAR0:%.+]]: !smt.bv<32>, [[BVAR1:%.+]]: !smt.bv<32>)
|
||||
// CHECK-DAG: [[V0:%.+]] = smt.distinct [[BVAR0]], [[FREEVAR]] : !smt.bv<32>
|
||||
// CHECK-DAG: [[V1:%.+]] = smt.distinct [[BVAR1]], [[FREEVAR]] : !smt.bv<32>
|
||||
// CHECK: [[V2:%.+]] = smt.or [[V0]], [[V1]]
|
||||
// CHECK-NEXT: smt.yield [[V2]]
|
||||
// CHECK-NEXT: }
|
||||
// CHECK-NEXT: smt.assert [[ALLQ]]
|
||||
// CHECK-NEXT: smt.check
|
||||
|
||||
func.func @multi_nondet() -> () {
|
||||
verif.refines first {
|
||||
^bb0():
|
||||
%nondet0 = smt.declare_fun : !smt.bv<32>
|
||||
%cc0 = builtin.unrealized_conversion_cast %nondet0 : !smt.bv<32> to i32
|
||||
%nondet1 = smt.declare_fun : !smt.bv<32>
|
||||
%cc1 = builtin.unrealized_conversion_cast %nondet1 : !smt.bv<32> to i32
|
||||
verif.yield %cc0, %cc1 : i32, i32
|
||||
} second {
|
||||
^bb0():
|
||||
%nondet = smt.declare_fun : !smt.bv<32>
|
||||
%cc = builtin.unrealized_conversion_cast %nondet : !smt.bv<32> to i32
|
||||
verif.yield %cc, %cc : i32, i32
|
||||
}
|
||||
return
|
||||
}
|
||||
|
|
|
|||
Loading…
Reference in New Issue