From 0bdaccceb5a3ed66a48a8358873aab3d539da752 Mon Sep 17 00:00:00 2001 From: Bea Healy Date: Fri, 13 Sep 2024 13:09:36 +0100 Subject: [PATCH 01/11] Add BMC to SMT lowering Co-authored-by: Martin Erhart --- include/circt/Conversion/Passes.td | 7 +- include/circt/Conversion/VerifToSMT.h | 4 +- lib/Conversion/HWToSMT/CMakeLists.txt | 1 + lib/Conversion/HWToSMT/HWToSMT.cpp | 24 +- lib/Conversion/VerifToSMT/CMakeLists.txt | 1 + lib/Conversion/VerifToSMT/VerifToSMT.cpp | 293 ++++++++++++++++++- test/Conversion/VerifToSMT/verif-to-smt.mlir | 102 ++++++- 7 files changed, 419 insertions(+), 13 deletions(-) diff --git a/include/circt/Conversion/Passes.td b/include/circt/Conversion/Passes.td index 6eb67b865093..791c998bfd32 100644 --- a/include/circt/Conversion/Passes.td +++ b/include/circt/Conversion/Passes.td @@ -699,7 +699,12 @@ def ConvertHWToSMT : Pass<"convert-hw-to-smt", "mlir::ModuleOp"> { def ConvertVerifToSMT : Pass<"convert-verif-to-smt", "mlir::ModuleOp"> { let summary = "Convert Verif ops to SMT ops"; - let dependentDialects = ["smt::SMTDialect", "mlir::arith::ArithDialect"]; + let dependentDialects = [ + "smt::SMTDialect", + "mlir::arith::ArithDialect", + "mlir::scf::SCFDialect", + "mlir::func::FuncDialect" + ]; } //===----------------------------------------------------------------------===// diff --git a/include/circt/Conversion/VerifToSMT.h b/include/circt/Conversion/VerifToSMT.h index a72a709a3a99..51806233b278 100644 --- a/include/circt/Conversion/VerifToSMT.h +++ b/include/circt/Conversion/VerifToSMT.h @@ -13,13 +13,15 @@ #include namespace circt { +class Namespace; #define GEN_PASS_DECL_CONVERTVERIFTOSMT #include "circt/Conversion/Passes.h.inc" /// Get the Verif to SMT conversion patterns. void populateVerifToSMTConversionPatterns(TypeConverter &converter, - RewritePatternSet &patterns); + RewritePatternSet &patterns, + Namespace &names); } // namespace circt diff --git a/lib/Conversion/HWToSMT/CMakeLists.txt b/lib/Conversion/HWToSMT/CMakeLists.txt index d4b67509376f..fdd114cf39f3 100644 --- a/lib/Conversion/HWToSMT/CMakeLists.txt +++ b/lib/Conversion/HWToSMT/CMakeLists.txt @@ -10,6 +10,7 @@ add_circt_conversion_library(CIRCTHWToSMT LINK_LIBS PUBLIC CIRCTHW CIRCTSMT + CIRCTSeq MLIRFuncDialect MLIRTransforms MLIRTransformUtils diff --git a/lib/Conversion/HWToSMT/HWToSMT.cpp b/lib/Conversion/HWToSMT/HWToSMT.cpp index 919078a91276..04f18493985b 100644 --- a/lib/Conversion/HWToSMT/HWToSMT.cpp +++ b/lib/Conversion/HWToSMT/HWToSMT.cpp @@ -9,6 +9,7 @@ #include "circt/Conversion/HWToSMT.h" #include "circt/Dialect/HW/HWOps.h" #include "circt/Dialect/SMT/SMTOps.h" +#include "circt/Dialect/Seq/SeqOps.h" #include "mlir/Analysis/TopologicalSortUtils.h" #include "mlir/Dialect/Func/IR/FuncOps.h" #include "mlir/Pass/Pass.h" @@ -92,6 +93,20 @@ struct InstanceOpConversion : OpConversionPattern { } }; +/// Remove redundant (seq::FromClock and seq::ToClock) ops. +template +struct ReplaceWithInput : OpConversionPattern { + using OpConversionPattern::OpConversionPattern; + using OpAdaptor = typename OpTy::Adaptor; + + LogicalResult + matchAndRewrite(OpTy op, OpAdaptor adaptor, + ConversionPatternRewriter &rewriter) const override { + rewriter.replaceOp(op, adaptor.getOperands()); + return success(); + } +}; + } // namespace //===----------------------------------------------------------------------===// @@ -118,6 +133,9 @@ void circt::populateHWToSMTTypeConverter(TypeConverter &converter) { return std::nullopt; return smt::BitVectorType::get(type.getContext(), type.getWidth()); }); + converter.addConversion([](seq::ClockType type) -> std::optional { + return smt::BitVectorType::get(type.getContext(), 1); + }); // Default target materialization to convert from illegal types to legal // types, e.g., at the boundary of an inlined child block. @@ -200,12 +218,16 @@ void circt::populateHWToSMTTypeConverter(TypeConverter &converter) { void circt::populateHWToSMTConversionPatterns(TypeConverter &converter, RewritePatternSet &patterns) { patterns.add(converter, patterns.getContext()); + InstanceOpConversion, ReplaceWithInput, + ReplaceWithInput>(converter, + patterns.getContext()); } void ConvertHWToSMTPass::runOnOperation() { ConversionTarget target(getContext()); target.addIllegalDialect(); + target.addIllegalOp(); + target.addIllegalOp(); target.addLegalDialect(); target.addLegalDialect(); diff --git a/lib/Conversion/VerifToSMT/CMakeLists.txt b/lib/Conversion/VerifToSMT/CMakeLists.txt index 84351314b07c..c108d401c320 100644 --- a/lib/Conversion/VerifToSMT/CMakeLists.txt +++ b/lib/Conversion/VerifToSMT/CMakeLists.txt @@ -13,6 +13,7 @@ add_circt_conversion_library(CIRCTVerifToSMT CIRCTSMT CIRCTVerif MLIRArithDialect + MLIRSCFDialect MLIRTransforms MLIRTransformUtils MLIRReconcileUnrealizedCasts diff --git a/lib/Conversion/VerifToSMT/VerifToSMT.cpp b/lib/Conversion/VerifToSMT/VerifToSMT.cpp index a8ca67df1d51..021a72ef3bbf 100644 --- a/lib/Conversion/VerifToSMT/VerifToSMT.cpp +++ b/lib/Conversion/VerifToSMT/VerifToSMT.cpp @@ -9,12 +9,17 @@ #include "circt/Conversion/VerifToSMT.h" #include "circt/Conversion/HWToSMT.h" #include "circt/Dialect/SMT/SMTOps.h" +#include "circt/Dialect/Seq/SeqTypes.h" #include "circt/Dialect/Verif/VerifOps.h" +#include "circt/Support/Namespace.h" #include "mlir/Conversion/ReconcileUnrealizedCasts/ReconcileUnrealizedCasts.h" #include "mlir/Dialect/Arith/IR/Arith.h" +#include "mlir/Dialect/Func/IR/FuncOps.h" +#include "mlir/Dialect/SCF/IR/SCF.h" +#include "mlir/IR/ValueRange.h" #include "mlir/Pass/Pass.h" #include "mlir/Transforms/DialectConversion.h" -#include "mlir/Transforms/GreedyPatternRewriteDriver.h" +#include "llvm/ADT/SmallVector.h" namespace circt { #define GEN_PASS_DEF_CONVERTVERIFTOSMT @@ -30,7 +35,8 @@ using namespace hw; //===----------------------------------------------------------------------===// namespace { -/// Lower a verif::AssertOp operation with an i1 operand to a smt::AssertOp. +/// Lower a verif::AssertOp operation with an i1 operand to a smt::AssertOp, +/// negated to check for unsatisfiability. struct VerifAssertOpConversion : OpConversionPattern { using OpConversionPattern::OpConversionPattern; @@ -40,11 +46,74 @@ struct VerifAssertOpConversion : OpConversionPattern { Value cond = typeConverter->materializeTargetConversion( rewriter, op.getLoc(), smt::BoolType::get(getContext()), adaptor.getProperty()); + Value notCond = rewriter.create(op.getLoc(), cond); + rewriter.replaceOpWithNewOp(op, notCond); + return success(); + } +}; + +/// Lower a verif::AssumeOp operation with an i1 operand to a smt::AssertOp +struct VerifAssumeOpConversion : OpConversionPattern { + using OpConversionPattern::OpConversionPattern; + + LogicalResult + matchAndRewrite(verif::AssumeOp op, OpAdaptor adaptor, + ConversionPatternRewriter &rewriter) const override { + Value cond = typeConverter->materializeTargetConversion( + rewriter, op.getLoc(), smt::BoolType::get(getContext()), + adaptor.getProperty()); rewriter.replaceOpWithNewOp(op, cond); return success(); } }; +// Fail to convert unsupported verif ops to avoid silent failure +struct VerifCoverOpConversion : OpConversionPattern { + using OpConversionPattern::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 { + using OpConversionPattern::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 { + using OpConversionPattern::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 { + using OpConversionPattern::OpConversionPattern; + + LogicalResult + matchAndRewrite(verif::ClockedAssumeOp op, OpAdaptor adaptor, + ConversionPatternRewriter &rewriter) const override { + return op.emitError( + "Conversion of ClockedAssumeOps to SMT not yet supported"); + }; +}; + /// Lower a verif::LecOp operation to a miter circuit encoded in SMT. /// More information on miter circuits can be found, e.g., in this paper: /// Brand, D., 1993, November. Verification of large synthesized designs. In @@ -146,6 +215,204 @@ struct LogicEquivalenceCheckingOpConversion } }; +/// Lower a verif::BMCOp operation to an MLIR program that performs the bounded +/// model check +struct VerifBoundedModelCheckingOpConversion + : OpConversionPattern { + using OpConversionPattern::OpConversionPattern; + + VerifBoundedModelCheckingOpConversion(TypeConverter &converter, + MLIRContext *context, Namespace &names) + : OpConversionPattern(converter, context), names(names) {} + + LogicalResult + matchAndRewrite(verif::BoundedModelCheckingOp op, OpAdaptor adaptor, + ConversionPatternRewriter &rewriter) const override { + Location loc = op.getLoc(); + SmallVector oldLoopInputTy(op.getLoop().getArgumentTypes()); + SmallVector oldCircuitInputTy(op.getCircuit().getArgumentTypes()); + SmallVector loopInputTy, circuitInputTy, initOutputTy, loopOutputTy, + circuitOutputTy; + if (failed(typeConverter->convertTypes(oldLoopInputTy, loopInputTy))) + return failure(); + if (failed(typeConverter->convertTypes(oldCircuitInputTy, circuitInputTy))) + return failure(); + if (failed(typeConverter->convertTypes( + op.getInit().front().back().getOperandTypes(), initOutputTy))) + return failure(); + // loop and init should have same output types + loopOutputTy = initOutputTy; + if (failed(typeConverter->convertTypes( + op.getCircuit().front().back().getOperandTypes(), circuitOutputTy))) + return failure(); + if (failed(rewriter.convertRegionTypes(&op.getInit(), *typeConverter))) + return failure(); + if (failed(rewriter.convertRegionTypes(&op.getLoop(), *typeConverter))) + return failure(); + if (failed(rewriter.convertRegionTypes(&op.getCircuit(), *typeConverter))) + return failure(); + + unsigned numRegs = + cast(op->getAttr("num_regs")).getValue().getZExtValue(); + + auto initFuncTy = rewriter.getFunctionType({}, initOutputTy); + auto loopFuncTy = rewriter.getFunctionType(loopInputTy, loopOutputTy); + auto circuitFuncTy = + rewriter.getFunctionType(circuitInputTy, circuitOutputTy); + + func::FuncOp initFuncOp, loopFuncOp, circuitFuncOp; + + { + OpBuilder::InsertionGuard guard(rewriter); + rewriter.setInsertionPointToEnd( + op->getParentOfType().getBody()); + initFuncOp = rewriter.create(loc, names.newName("bmc_init"), + initFuncTy); + rewriter.inlineRegionBefore(op.getInit(), initFuncOp.getFunctionBody(), + initFuncOp.end()); + loopFuncOp = rewriter.create(loc, names.newName("bmc_loop"), + loopFuncTy); + rewriter.inlineRegionBefore(op.getLoop(), loopFuncOp.getFunctionBody(), + loopFuncOp.end()); + circuitFuncOp = rewriter.create( + loc, names.newName("bmc_circuit"), circuitFuncTy); + rewriter.inlineRegionBefore(op.getCircuit(), + circuitFuncOp.getFunctionBody(), + circuitFuncOp.end()); + auto funcOps = {&initFuncOp, &loopFuncOp, &circuitFuncOp}; + auto outputTys = {initOutputTy, loopOutputTy, circuitOutputTy}; + for (auto [funcOp, outputTy] : llvm::zip(funcOps, outputTys)) { + auto operands = funcOp->getBody().front().back().getOperands(); + rewriter.eraseOp(&funcOp->getFunctionBody().front().back()); + rewriter.setInsertionPointToEnd(&funcOp->getBody().front()); + SmallVector toReturn; + for (unsigned i = 0; i < outputTy.size(); ++i) + toReturn.push_back(typeConverter->materializeTargetConversion( + rewriter, loc, outputTy[i], operands[i])); + rewriter.create(loc, toReturn); + } + } + + auto solver = + rewriter.create(loc, rewriter.getI1Type(), ValueRange{}); + rewriter.createBlock(&solver.getBodyRegion()); + + // Call init func to get initial clock values + ValueRange initVals = + rewriter.create(loc, initFuncOp)->getResults(); + + // InputDecls order should be + // + // Get list of clock indexes in circuit args + size_t initIndex = 0, curIndex = 0; + SmallVector inputDecls; + SmallVector clockIndexes; + for (auto [oldTy, newTy] : + llvm::zip(oldCircuitInputTy, circuitInputTy)) { + if (isa(oldTy)) { + inputDecls.push_back(initVals[initIndex++]); + clockIndexes.push_back(curIndex); + } + else + inputDecls.push_back(rewriter.create(loc, newTy)); + curIndex++; + } + + auto numStateArgs = initVals.size() - initIndex; + // Add the rest of the init vals (state args) + for (; initIndex < initVals.size(); ++initIndex) + inputDecls.push_back(initVals[initIndex]); + + Value lowerBound = + rewriter.create(loc, rewriter.getI32IntegerAttr(0)); + Value step = + rewriter.create(loc, rewriter.getI32IntegerAttr(1)); + Value upperBound = + rewriter.create(loc, adaptor.getBoundAttr()); + Value constFalse = + rewriter.create(loc, rewriter.getBoolAttr(false)); + Value constTrue = + rewriter.create(loc, rewriter.getBoolAttr(true)); + inputDecls.push_back(constFalse); // wasViolated? + + // TODO: swapping to a whileOp here would allow early exit once the property + // is violated + // Perform model check up to the provided bound + auto forOp = rewriter.create( + loc, lowerBound, upperBound, step, inputDecls, + [&](OpBuilder &builder, Location loc, Value i, ValueRange iterArgs) { + // Execute the circuit + ValueRange circuitCallOuts = + builder + .create( + loc, circuitFuncOp, + iterArgs.take_front(circuitFuncOp.getNumArguments())) + ->getResults(); + auto checkOp = + rewriter.create(loc, builder.getI1Type()); + { + OpBuilder::InsertionGuard guard(builder); + builder.createBlock(&checkOp.getSatRegion()); + builder.create(loc, constTrue); + builder.createBlock(&checkOp.getUnknownRegion()); + builder.create(loc, constTrue); + builder.createBlock(&checkOp.getUnsatRegion()); + builder.create(loc, constFalse); + } + + Value violated = builder.create( + loc, checkOp.getResult(0), iterArgs.back()); + + SmallVector newDecls; + + // Call loop func to update clock & state arg values + SmallVector loopCallInputs; + // Get all clock inputs to module + // for (auto arg : + // iterArgs.take_front(circuitFuncOp.getNumArguments())) { + // } + for (auto index: clockIndexes) { + loopCallInputs.push_back(iterArgs[index]); + } + for (auto stateArg: iterArgs.drop_back().take_back(numStateArgs)) { + loopCallInputs.push_back(stateArg); + } + ValueRange loopVals = + builder + .create(loc, loopFuncOp, loopCallInputs) + ->getResults(); + + size_t loopIndex = 0; + for (auto [oldTy, newTy] : + llvm::zip(TypeRange(oldCircuitInputTy).drop_back(numRegs), + TypeRange(circuitInputTy).drop_back(numRegs))) { + if (isa(oldTy)) + newDecls.push_back(loopVals[loopIndex++]); + else + newDecls.push_back(builder.create(loc, newTy)); + } + newDecls.append( + SmallVector(circuitCallOuts.take_back(numRegs))); + + // Add the rest of the loop state args + for (; loopIndex < loopVals.size(); ++loopIndex) + newDecls.push_back(loopVals[loopIndex]); + + newDecls.push_back(violated); + + builder.create(loc, newDecls); + }); + + Value res = rewriter.create(loc, forOp->getResults().back(), + constTrue); + rewriter.create(loc, res); + rewriter.replaceOp(op, solver.getResults()); + return success(); + } + + Namespace &names; +}; + } // namespace //===----------------------------------------------------------------------===// @@ -160,21 +427,33 @@ struct ConvertVerifToSMTPass } // namespace void circt::populateVerifToSMTConversionPatterns(TypeConverter &converter, - RewritePatternSet &patterns) { - patterns.add( - converter, patterns.getContext()); + RewritePatternSet &patterns, + Namespace &names) { + patterns.add(converter, + patterns.getContext()); + patterns.add( + converter, patterns.getContext(), names); } void ConvertVerifToSMTPass::runOnOperation() { ConversionTarget target(getContext()); target.addIllegalDialect(); - target.addLegalDialect(); + target.addLegalDialect(); target.addLegalOp(); RewritePatternSet patterns(&getContext()); TypeConverter converter; populateHWToSMTTypeConverter(converter); - populateVerifToSMTConversionPatterns(converter, patterns); + + SymbolCache symCache; + symCache.addDefinitions(getOperation()); + Namespace names; + names.add(symCache); + populateVerifToSMTConversionPatterns(converter, patterns, names); if (failed(mlir::applyPartialConversion(getOperation(), target, std::move(patterns)))) diff --git a/test/Conversion/VerifToSMT/verif-to-smt.mlir b/test/Conversion/VerifToSMT/verif-to-smt.mlir index 92b828b23c9e..e5c13b8a82e8 100644 --- a/test/Conversion/VerifToSMT/verif-to-smt.mlir +++ b/test/Conversion/VerifToSMT/verif-to-smt.mlir @@ -1,12 +1,13 @@ // RUN: circt-opt %s --convert-verif-to-smt --reconcile-unrealized-casts -allow-unregistered-dialect | FileCheck %s -// CHECK-LABEL: func @test +// CHECK-LABEL: func @test_lec // CHECK-SAME: ([[ARG0:%.+]]: !smt.bv<1>) -func.func @test(%arg0: !smt.bv<1>) -> (i1, i1, i1) { +func.func @test_lec(%arg0: !smt.bv<1>) -> (i1, i1, i1) { %0 = builtin.unrealized_conversion_cast %arg0 : !smt.bv<1> to i1 // CHECK: [[C0:%.+]] = smt.bv.constant #smt.bv<-1> : !smt.bv<1> // CHECK: [[V0:%.+]] = smt.eq %arg0, [[C0]] : !smt.bv<1> - // CHECK: smt.assert [[V0]] + // CHECK: [[V1:%.+]] = smt.not [[V0]] + // CHECK: smt.assert [[V1]] verif.assert %0 : i1 // CHECK: [[EQ:%.+]] = smt.solver() : () -> i1 @@ -60,3 +61,98 @@ func.func @test(%arg0: !smt.bv<1>) -> (i1, i1, i1) { // CHECK: return [[EQ]], [[EQ2]], %true return %1, %2, %3 : i1, i1, i1 } + +// CHECK-LABEL: func.func @test_bmc() -> i1 { +// CHECK: [[BMC:%.+]] = smt.solver +// CHECK: [[INIT:%.+]]:2 = func.call @bmc_init() +// CHECK: [[F0:%.+]] = smt.declare_fun : !smt.bv<32> +// CHECK: [[F1:%.+]] = smt.declare_fun : !smt.bv<32> +// CHECK: [[C0_I32:%.+]] = arith.constant 0 : i32 +// CHECK: [[C1_I32:%.+]] = arith.constant 1 : i32 +// CHECK: [[C10_I32:%.+]] = arith.constant 10 : i32 +// CHECK: [[FALSE:%.+]] = arith.constant false +// CHECK: [[TRUE:%.+]] = arith.constant true +// CHECK: [[FOR:%.+]]:5 = scf.for [[ARG0:%.+]] = [[C0_I32]] to [[C10_I32]] step [[C1_I32]] iter_args([[ARG1:%.+]] = [[INIT]]#0, [[ARG2:%.+]] = [[F0]], [[ARG3:%.+]] = [[F1]], [[ARG4:%.+]] = [[INIT]]#1, [[ARG5:%.+]] = [[FALSE]]) +// CHECK: [[CIRCUIT:%.+]]:2 = func.call @bmc_circuit([[ARG1]], [[ARG2]], [[ARG3]]) +// CHECK: [[SMTCHECK:%.+]] = smt.check sat { +// CHECK: smt.yield [[TRUE]] +// CHECK: } unknown { +// CHECK: smt.yield [[TRUE]] +// CHECK: } unsat { +// CHECK: smt.yield [[FALSE]] +// CHECK: } +// CHECK: [[ORI:%.+]] = arith.ori [[SMTCHECK]], [[ARG5]] +// CHECK: [[LOOP:%.+]]:2 = func.call @bmc_loop([[ARG1]], [[ARG4]]) +// CHECK: [[F2:%.+]] = smt.declare_fun : !smt.bv<32> +// CHECK: scf.yield [[LOOP]]#0, [[F2]], [[CIRCUIT]]#1, [[LOOP]]#1, [[ORI]] +// CHECK: } +// CHECK: [[XORI:%.+]] = arith.xori [[FOR]]#4, [[TRUE]] +// CHECK: smt.yield [[XORI]] +// CHECK: } +// CHECK: return [[BMC]] +// CHECK: } +// CHECK-LABEL: func.func @bmc_init() -> (!smt.bv<1>, !smt.bv<1>) { +// CHECK: [[FALSE:%.+]] = hw.constant false +// CHECK: [[TOCLOCK:%.+]] = seq.to_clock %false +// CHECK: [[C0:%.+]] = builtin.unrealized_conversion_cast [[TOCLOCK]] : !seq.clock to !smt.bv<1> +// CHECK: [[C1:%.+]] = builtin.unrealized_conversion_cast [[FALSE]] : i1 to !smt.bv<1> +// CHECK: return [[C0]], [[C1]] +// CHECK: } +// CHECK: func.func @bmc_loop([[ARGO:%.+]]: !smt.bv<1>, [[ARG1:%.+]]: !smt.bv<1>) +// CHECK: [[C2:%.+]] = builtin.unrealized_conversion_cast [[ARG1]] : !smt.bv<1> to i1 +// CHECK: [[C3:%.+]] = builtin.unrealized_conversion_cast [[ARG0]] : !smt.bv<1> to !seq.clock +// CHECK: [[FROMCLOCK:%.+]] = seq.from_clock [[C3]] +// CHECK: [[TRUE]] = hw.constant true +// CHECK: [[NCLOCK:%.+]] = comb.xor [[FROMCLOCK]], [[TRUE]] +// CHECK: [[NARG:%.+]] = comb.xor [[C2]], [[TRUE]] +// CHECK: [[TOCLOCK:%.+]] = seq.to_clock [[NCLOCK]] +// CHECK: [[C4:%.+]] = builtin.unrealized_conversion_cast [[TOCLOCK]] : !seq.clock to !smt.bv<1> +// CHECK: [[C5:%.+]] = builtin.unrealized_conversion_cast [[NARG]] : i1 to !smt.bv<1> +// CHECK: return [[C4]], [[C5]] +// CHECK: } +// CHECK: func.func @bmc_circuit([[ARGO:%.+]]: !smt.bv<1>, [[ARG1:%.+]]: !smt.bv<32>, [[ARG2:%.+]]: !smt.bv<32>) +// CHECK: [[C6:%.+]] = builtin.unrealized_conversion_cast [[ARG2]] : !smt.bv<32> to i32 +// CHECK: [[C7:%.+]] = builtin.unrealized_conversion_cast [[ARG1]] : !smt.bv<32> to i32 +// CHECK: [[CN1_I32:%.+]] = hw.constant -1 : i32 +// CHECK: [[ADD:%.+]] = comb.add [[C7]], [[C6]] +// CHECK: [[XOR:%.+]] = comb.xor [[C6]], [[CN1_I32]] +// CHECK: [[FALSE:%.+]] = hw.constant false +// CHECK: [[C8:%.+]] = builtin.unrealized_conversion_cast [[FALSE]] : i1 to !smt.bv<1> +// CHECK: [[CN1_BV:%.+]] = smt.bv.constant #smt.bv<-1> : !smt.bv<1> +// CHECK: [[EQ:%.+]] = smt.eq [[C8]], [[CN1_BV]] +// CHECK: [[NOT:%.+]] = smt.not [[EQ]] +// CHECK: smt.assert [[NOT]] +// CHECK: [[C9:%.+]] = builtin.unrealized_conversion_cast [[XOR]] : i32 to !smt.bv<32> +// CHECK: [[C10:%.+]] = builtin.unrealized_conversion_cast [[ADD]] : i32 to !smt.bv<32> +// CHECK: return [[C9]], [[C10]] +// CHECK: } + +func.func @test_bmc() -> (i1) { + %bmc = verif.bmc bound 10 num_regs 1 + init { + %c0_i1 = hw.constant 0 : i1 + %clk = seq.to_clock %c0_i1 + verif.yield %clk, %c0_i1 : !seq.clock, i1 + } + loop { + ^bb0(%clk: !seq.clock, %stateArg: i1): + %from_clock = seq.from_clock %clk + %c-1_i1 = hw.constant -1 : i1 + %neg_clock = comb.xor %from_clock, %c-1_i1 : i1 + %newStateArg = comb.xor %stateArg, %c-1_i1 : i1 + %newclk = seq.to_clock %neg_clock + verif.yield %newclk, %newStateArg : !seq.clock, i1 + } + circuit { + ^bb0(%clk: !seq.clock, %arg0: i32, %state0: i32): + %c-1_i32 = hw.constant -1 : i32 + %0 = comb.add %arg0, %state0 : i32 + // %state0 is the result of a seq.compreg taking %0 as input + %2 = comb.xor %state0, %c-1_i32 : i32 + %false = hw.constant false + // Arbitrary assertion so op verifies + verif.assert %false : i1 + verif.yield %2, %0 : i32, i32 + } + func.return %bmc : i1 +} From 80736fce3928eb56f4fd1c8a56f6cb803971cc93 Mon Sep 17 00:00:00 2001 From: Bea Healy Date: Mon, 16 Sep 2024 16:59:13 +0100 Subject: [PATCH 02/11] Format & clean-up --- lib/Conversion/VerifToSMT/VerifToSMT.cpp | 38 ++++++++++++------------ 1 file changed, 19 insertions(+), 19 deletions(-) diff --git a/lib/Conversion/VerifToSMT/VerifToSMT.cpp b/lib/Conversion/VerifToSMT/VerifToSMT.cpp index 021a72ef3bbf..989586904cd8 100644 --- a/lib/Conversion/VerifToSMT/VerifToSMT.cpp +++ b/lib/Conversion/VerifToSMT/VerifToSMT.cpp @@ -231,7 +231,10 @@ struct VerifBoundedModelCheckingOpConversion Location loc = op.getLoc(); SmallVector oldLoopInputTy(op.getLoop().getArgumentTypes()); SmallVector oldCircuitInputTy(op.getCircuit().getArgumentTypes()); - SmallVector loopInputTy, circuitInputTy, initOutputTy, loopOutputTy, + // TODO: the init and loop regions should be able to be concrete instead of + // symbolic which is probably preferable - just need to convert back and + // forth + SmallVector loopInputTy, circuitInputTy, initOutputTy, circuitOutputTy; if (failed(typeConverter->convertTypes(oldLoopInputTy, loopInputTy))) return failure(); @@ -240,8 +243,6 @@ struct VerifBoundedModelCheckingOpConversion if (failed(typeConverter->convertTypes( op.getInit().front().back().getOperandTypes(), initOutputTy))) return failure(); - // loop and init should have same output types - loopOutputTy = initOutputTy; if (failed(typeConverter->convertTypes( op.getCircuit().front().back().getOperandTypes(), circuitOutputTy))) return failure(); @@ -256,7 +257,9 @@ struct VerifBoundedModelCheckingOpConversion cast(op->getAttr("num_regs")).getValue().getZExtValue(); auto initFuncTy = rewriter.getFunctionType({}, initOutputTy); - auto loopFuncTy = rewriter.getFunctionType(loopInputTy, loopOutputTy); + // Loop and init output types are necessarily the same, so just use init + // output types + auto loopFuncTy = rewriter.getFunctionType(loopInputTy, initOutputTy); auto circuitFuncTy = rewriter.getFunctionType(circuitInputTy, circuitOutputTy); @@ -280,7 +283,8 @@ struct VerifBoundedModelCheckingOpConversion circuitFuncOp.getFunctionBody(), circuitFuncOp.end()); auto funcOps = {&initFuncOp, &loopFuncOp, &circuitFuncOp}; - auto outputTys = {initOutputTy, loopOutputTy, circuitOutputTy}; + // initOutputTy is the same as loop output types + auto outputTys = {initOutputTy, initOutputTy, circuitOutputTy}; for (auto [funcOp, outputTy] : llvm::zip(funcOps, outputTys)) { auto operands = funcOp->getBody().front().back().getOperands(); rewriter.eraseOp(&funcOp->getFunctionBody().front().back()); @@ -307,14 +311,13 @@ struct VerifBoundedModelCheckingOpConversion size_t initIndex = 0, curIndex = 0; SmallVector inputDecls; SmallVector clockIndexes; - for (auto [oldTy, newTy] : - llvm::zip(oldCircuitInputTy, circuitInputTy)) { + for (auto [oldTy, newTy] : llvm::zip(oldCircuitInputTy, circuitInputTy)) { if (isa(oldTy)) { inputDecls.push_back(initVals[initIndex++]); clockIndexes.push_back(curIndex); - } - else + } else { inputDecls.push_back(rewriter.create(loc, newTy)); + } curIndex++; } @@ -363,26 +366,23 @@ struct VerifBoundedModelCheckingOpConversion Value violated = builder.create( loc, checkOp.getResult(0), iterArgs.back()); - SmallVector newDecls; - // Call loop func to update clock & state arg values SmallVector loopCallInputs; - // Get all clock inputs to module - // for (auto arg : - // iterArgs.take_front(circuitFuncOp.getNumArguments())) { - // } - for (auto index: clockIndexes) { + // Fetch clock values to feed to loop + for (auto index : clockIndexes) { loopCallInputs.push_back(iterArgs[index]); } - for (auto stateArg: iterArgs.drop_back().take_back(numStateArgs)) { + // Fetch state args to feed to loop + for (auto stateArg : iterArgs.drop_back().take_back(numStateArgs)) { loopCallInputs.push_back(stateArg); } ValueRange loopVals = - builder - .create(loc, loopFuncOp, loopCallInputs) + builder.create(loc, loopFuncOp, loopCallInputs) ->getResults(); size_t loopIndex = 0; + // Collect decls to yield at end of iteration + SmallVector newDecls; for (auto [oldTy, newTy] : llvm::zip(TypeRange(oldCircuitInputTy).drop_back(numRegs), TypeRange(circuitInputTy).drop_back(numRegs))) { From 8353a4bad39cae849c911cb818b0aaf2d38cd384 Mon Sep 17 00:00:00 2001 From: Bea Healy Date: Mon, 16 Sep 2024 17:07:13 +0100 Subject: [PATCH 03/11] Remove now-unnecessary assert --- test/Conversion/VerifToSMT/verif-to-smt.mlir | 9 --------- 1 file changed, 9 deletions(-) diff --git a/test/Conversion/VerifToSMT/verif-to-smt.mlir b/test/Conversion/VerifToSMT/verif-to-smt.mlir index e5c13b8a82e8..7d1f23c9ceea 100644 --- a/test/Conversion/VerifToSMT/verif-to-smt.mlir +++ b/test/Conversion/VerifToSMT/verif-to-smt.mlir @@ -116,12 +116,6 @@ func.func @test_lec(%arg0: !smt.bv<1>) -> (i1, i1, i1) { // CHECK: [[CN1_I32:%.+]] = hw.constant -1 : i32 // CHECK: [[ADD:%.+]] = comb.add [[C7]], [[C6]] // CHECK: [[XOR:%.+]] = comb.xor [[C6]], [[CN1_I32]] -// CHECK: [[FALSE:%.+]] = hw.constant false -// CHECK: [[C8:%.+]] = builtin.unrealized_conversion_cast [[FALSE]] : i1 to !smt.bv<1> -// CHECK: [[CN1_BV:%.+]] = smt.bv.constant #smt.bv<-1> : !smt.bv<1> -// CHECK: [[EQ:%.+]] = smt.eq [[C8]], [[CN1_BV]] -// CHECK: [[NOT:%.+]] = smt.not [[EQ]] -// CHECK: smt.assert [[NOT]] // CHECK: [[C9:%.+]] = builtin.unrealized_conversion_cast [[XOR]] : i32 to !smt.bv<32> // CHECK: [[C10:%.+]] = builtin.unrealized_conversion_cast [[ADD]] : i32 to !smt.bv<32> // CHECK: return [[C9]], [[C10]] @@ -149,9 +143,6 @@ func.func @test_bmc() -> (i1) { %0 = comb.add %arg0, %state0 : i32 // %state0 is the result of a seq.compreg taking %0 as input %2 = comb.xor %state0, %c-1_i32 : i32 - %false = hw.constant false - // Arbitrary assertion so op verifies - verif.assert %false : i1 verif.yield %2, %0 : i32, i32 } func.return %bmc : i1 From 8a8f9120d4465a3f4f190b2614a31fd676568b03 Mon Sep 17 00:00:00 2001 From: Bea Healy Date: Mon, 16 Sep 2024 17:29:03 +0100 Subject: [PATCH 04/11] Drop error conversions --- lib/Conversion/VerifToSMT/VerifToSMT.cpp | 49 ------------------------ 1 file changed, 49 deletions(-) diff --git a/lib/Conversion/VerifToSMT/VerifToSMT.cpp b/lib/Conversion/VerifToSMT/VerifToSMT.cpp index 989586904cd8..ffc1655476b1 100644 --- a/lib/Conversion/VerifToSMT/VerifToSMT.cpp +++ b/lib/Conversion/VerifToSMT/VerifToSMT.cpp @@ -67,53 +67,6 @@ struct VerifAssumeOpConversion : OpConversionPattern { } }; -// Fail to convert unsupported verif ops to avoid silent failure -struct VerifCoverOpConversion : OpConversionPattern { - using OpConversionPattern::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 { - using OpConversionPattern::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 { - using OpConversionPattern::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 { - using OpConversionPattern::OpConversionPattern; - - LogicalResult - matchAndRewrite(verif::ClockedAssumeOp op, OpAdaptor adaptor, - ConversionPatternRewriter &rewriter) const override { - return op.emitError( - "Conversion of ClockedAssumeOps to SMT not yet supported"); - }; -}; - /// Lower a verif::LecOp operation to a miter circuit encoded in SMT. /// More information on miter circuits can be found, e.g., in this paper: /// Brand, D., 1993, November. Verification of large synthesized designs. In @@ -430,8 +383,6 @@ void circt::populateVerifToSMTConversionPatterns(TypeConverter &converter, RewritePatternSet &patterns, Namespace &names) { patterns.add(converter, patterns.getContext()); patterns.add( From 1d0dcec5777d806fdb700862fe51b730596ba189 Mon Sep 17 00:00:00 2001 From: Bea Healy Date: Tue, 17 Sep 2024 11:11:29 +0100 Subject: [PATCH 05/11] Address nits & add missing Func dialect dep --- lib/Conversion/VerifToSMT/CMakeLists.txt | 1 + lib/Conversion/VerifToSMT/VerifToSMT.cpp | 13 ++++++------- 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/lib/Conversion/VerifToSMT/CMakeLists.txt b/lib/Conversion/VerifToSMT/CMakeLists.txt index c108d401c320..135c906ff0ad 100644 --- a/lib/Conversion/VerifToSMT/CMakeLists.txt +++ b/lib/Conversion/VerifToSMT/CMakeLists.txt @@ -13,6 +13,7 @@ add_circt_conversion_library(CIRCTVerifToSMT CIRCTSMT CIRCTVerif MLIRArithDialect + MLIRFuncDialect MLIRSCFDialect MLIRTransforms MLIRTransformUtils diff --git a/lib/Conversion/VerifToSMT/VerifToSMT.cpp b/lib/Conversion/VerifToSMT/VerifToSMT.cpp index ffc1655476b1..867da9899d0c 100644 --- a/lib/Conversion/VerifToSMT/VerifToSMT.cpp +++ b/lib/Conversion/VerifToSMT/VerifToSMT.cpp @@ -261,17 +261,18 @@ struct VerifBoundedModelCheckingOpConversion // InputDecls order should be // // Get list of clock indexes in circuit args - size_t initIndex = 0, curIndex = 0; + size_t initIndex = 0; SmallVector inputDecls; SmallVector clockIndexes; - for (auto [oldTy, newTy] : llvm::zip(oldCircuitInputTy, circuitInputTy)) { + for (auto [curIndex, types] : + llvm::enumerate(llvm::zip(oldCircuitInputTy, circuitInputTy))) { + auto [oldTy, newTy] = types; if (isa(oldTy)) { inputDecls.push_back(initVals[initIndex++]); clockIndexes.push_back(curIndex); } else { inputDecls.push_back(rewriter.create(loc, newTy)); } - curIndex++; } auto numStateArgs = initVals.size() - initIndex; @@ -322,13 +323,11 @@ struct VerifBoundedModelCheckingOpConversion // Call loop func to update clock & state arg values SmallVector loopCallInputs; // Fetch clock values to feed to loop - for (auto index : clockIndexes) { + for (auto index : clockIndexes) loopCallInputs.push_back(iterArgs[index]); - } // Fetch state args to feed to loop - for (auto stateArg : iterArgs.drop_back().take_back(numStateArgs)) { + for (auto stateArg : iterArgs.drop_back().take_back(numStateArgs)) loopCallInputs.push_back(stateArg); - } ValueRange loopVals = builder.create(loc, loopFuncOp, loopCallInputs) ->getResults(); From ef796faadfbdf32a3b4f52062715e891986785eb Mon Sep 17 00:00:00 2001 From: Bea Healy Date: Tue, 17 Sep 2024 13:39:16 +0100 Subject: [PATCH 06/11] Add lowering tests for assert & assume ops --- test/Conversion/VerifToSMT/verif-to-smt.mlir | 25 ++++++++++++++++++++ 1 file changed, 25 insertions(+) diff --git a/test/Conversion/VerifToSMT/verif-to-smt.mlir b/test/Conversion/VerifToSMT/verif-to-smt.mlir index 7d1f23c9ceea..754de7800e15 100644 --- a/test/Conversion/VerifToSMT/verif-to-smt.mlir +++ b/test/Conversion/VerifToSMT/verif-to-smt.mlir @@ -1,5 +1,30 @@ // RUN: circt-opt %s --convert-verif-to-smt --reconcile-unrealized-casts -allow-unregistered-dialect | FileCheck %s +// CHECK: func.func @lower_assert([[ARG0:%.+]]: i1) +// CHECK: [[CAST:%.+]] = builtin.unrealized_conversion_cast [[ARG0]] : i1 to !smt.bv<1> +// CHECK: [[Cn1_BV:%.+]] = smt.bv.constant #smt.bv<-1> +// CHECK: [[EQ:%.+]] = smt.eq [[CAST]], [[Cn1_BV]] +// CHECK: [[NEQ:%.+]] = smt.not [[EQ]] +// CHECK: smt.assert [[NEQ]] +// CHECK: return + +func.func @lower_assert(%arg0: i1) { + verif.assert %arg0 : i1 + return +} + +// CHECK: func.func @lower_assume([[ARG0:%.+]]: i1) +// CHECK: [[CAST:%.+]] = builtin.unrealized_conversion_cast [[ARG0]] : i1 to !smt.bv<1> +// CHECK: [[Cn1_BV:%.+]] = smt.bv.constant #smt.bv<-1> +// CHECK: [[EQ:%.+]] = smt.eq [[CAST]], [[Cn1_BV]] +// CHECK: smt.assert [[EQ]] +// CHECK: return + +func.func @lower_assume(%arg0: i1) { + verif.assume %arg0 : i1 + return +} + // CHECK-LABEL: func @test_lec // CHECK-SAME: ([[ARG0:%.+]]: !smt.bv<1>) func.func @test_lec(%arg0: !smt.bv<1>) -> (i1, i1, i1) { From b6740f8cfe75d00f7fd7940023cc13f9931dd8d0 Mon Sep 17 00:00:00 2001 From: Bea Healy Date: Tue, 17 Sep 2024 17:34:12 +0100 Subject: [PATCH 07/11] Error on multiple assertions --- lib/Conversion/VerifToSMT/VerifToSMT.cpp | 27 ++++++++ .../VerifToSMT/verif-to-smt-errors.mlir | 65 +++++++++++++++++++ 2 files changed, 92 insertions(+) diff --git a/lib/Conversion/VerifToSMT/VerifToSMT.cpp b/lib/Conversion/VerifToSMT/VerifToSMT.cpp index 867da9899d0c..a3ce3030d6c0 100644 --- a/lib/Conversion/VerifToSMT/VerifToSMT.cpp +++ b/lib/Conversion/VerifToSMT/VerifToSMT.cpp @@ -181,6 +181,33 @@ struct VerifBoundedModelCheckingOpConversion LogicalResult matchAndRewrite(verif::BoundedModelCheckingOp op, OpAdaptor adaptor, ConversionPatternRewriter &rewriter) const override { + // Check there is exactly one assertion + auto topAssertions = op.getCircuit().getOps(); + int numAssertions = + std::distance(topAssertions.begin(), topAssertions.end()); + SymbolTable symbolTable(op->getParentOfType()); + SmallVector worklist; + for (auto instance : op.getCircuit().getOps()) { + worklist.push_back(symbolTable.lookup(instance.getModuleName())); + } + // TODO: probably negligible compared to actual model checking time but + // cacheing the assertion count of modules would speed this up + for (auto *module : worklist) { + auto moduleAssertions = module->getRegion(0).getOps(); + numAssertions += + std::distance(moduleAssertions.begin(), moduleAssertions.end()); + if (numAssertions > 1) + break; + for (auto instance : module->getBlock()->getOps()) { + worklist.push_back(symbolTable.lookup(instance.getModuleName())); + } + } + if (numAssertions > 1) { + return op->emitError("designs with multiple assertions are not yet " + "correctly handled - instead, you can assert the " + "conjunction of your assertions"); + } + Location loc = op.getLoc(); SmallVector oldLoopInputTy(op.getLoop().getArgumentTypes()); SmallVector oldCircuitInputTy(op.getCircuit().getArgumentTypes()); diff --git a/test/Conversion/VerifToSMT/verif-to-smt-errors.mlir b/test/Conversion/VerifToSMT/verif-to-smt-errors.mlir index 709b531a0acb..5ce3da97b885 100644 --- a/test/Conversion/VerifToSMT/verif-to-smt-errors.mlir +++ b/test/Conversion/VerifToSMT/verif-to-smt-errors.mlir @@ -15,3 +15,68 @@ func.func @assert_with_unsupported_property_type(%arg0: !smt.bv<1>) { verif.assert %0 : !ltl.property return } + +// ----- + +func.func @multiple_assertions_bmc() -> (i1) { + // expected-error @below {{designs with multiple assertions are not yet correctly handled - instead, you can assert the conjunction of your assertions}} + // expected-error @below {{failed to legalize operation 'verif.bmc' that was explicitly marked illegal}} + %bmc = verif.bmc bound 10 num_regs 1 + init {} + loop {} + circuit { + ^bb0(%arg0: i32, %arg1: i32): + %c1_i32 = hw.constant 1 : i32 + %cond1 = comb.icmp ugt %arg0, %c1_i32 : i32 + verif.assert %cond1 : i1 + %cond2 = comb.icmp ugt %arg1, %c1_i32 : i32 + verif.assert %cond2 : i1 + %sum = comb.add %arg0, %arg1 : i32 + verif.yield %sum : i32 + } + func.return %bmc : i1 +} + +// ----- + +func.func @multiple_asserting_modules_bmc() -> (i1) { + // expected-error @below {{designs with multiple assertions are not yet correctly handled - instead, you can assert the conjunction of your assertions}} + // expected-error @below {{failed to legalize operation 'verif.bmc' that was explicitly marked illegal}} + %bmc = verif.bmc bound 10 num_regs 1 + init {} + loop {} + circuit { + ^bb0(%arg0: i32, %arg1: i1, %arg2: i1): + hw.instance "" @OneAssertion(x: %arg1: i1) -> () + hw.instance "" @OneAssertion(x: %arg2: i1) -> () + %sum = comb.add %arg0, %arg0 : i32 + verif.yield %sum : i32 + } + func.return %bmc : i1 +} + +hw.module @OneAssertion(in %x: i1) { + verif.assert %x : i1 +} + +// ----- + +func.func @multiple_nested_assertions() -> (i1) { + // expected-error @below {{designs with multiple assertions are not yet correctly handled - instead, you can assert the conjunction of your assertions}} + // expected-error @below {{failed to legalize operation 'verif.bmc' that was explicitly marked illegal}} + %bmc = verif.bmc bound 10 num_regs 1 + init {} + loop {} + circuit { + ^bb0(%arg0: i32, %arg1: i1, %arg2: i1): + hw.instance "" @TwoAssertions(x: %arg1: i1, y: %arg2: i1) -> () + %sum = comb.add %arg0, %arg0 : i32 + verif.yield %sum : i32 + } + func.return %bmc : i1 +} + +hw.module @TwoAssertions(in %x: i1, in %y: i1) { + verif.assert %x : i1 + verif.assert %y : i1 +} From 7fdbe4029b7b40343516bc9d69e874e66297c447 Mon Sep 17 00:00:00 2001 From: Bea Healy Date: Mon, 23 Sep 2024 12:53:56 +0100 Subject: [PATCH 08/11] Drop unnecessary zip & braces --- lib/Conversion/VerifToSMT/VerifToSMT.cpp | 26 +++++++++++------------- 1 file changed, 12 insertions(+), 14 deletions(-) diff --git a/lib/Conversion/VerifToSMT/VerifToSMT.cpp b/lib/Conversion/VerifToSMT/VerifToSMT.cpp index a3ce3030d6c0..4c4f66fc2caf 100644 --- a/lib/Conversion/VerifToSMT/VerifToSMT.cpp +++ b/lib/Conversion/VerifToSMT/VerifToSMT.cpp @@ -182,14 +182,15 @@ struct VerifBoundedModelCheckingOpConversion matchAndRewrite(verif::BoundedModelCheckingOp op, OpAdaptor adaptor, ConversionPatternRewriter &rewriter) const override { // Check there is exactly one assertion - auto topAssertions = op.getCircuit().getOps(); - int numAssertions = - std::distance(topAssertions.begin(), topAssertions.end()); - SymbolTable symbolTable(op->getParentOfType()); SmallVector worklist; - for (auto instance : op.getCircuit().getOps()) { - worklist.push_back(symbolTable.lookup(instance.getModuleName())); - } + SymbolTable symbolTable(op->getParentOfType()); + int numAssertions = 0; + op.walk([&](Operation *curOp) { + if (isa(curOp)) + numAssertions++; + if (auto inst = dyn_cast(curOp)) + worklist.push_back(symbolTable.lookup(inst.getModuleName())); + }); // TODO: probably negligible compared to actual model checking time but // cacheing the assertion count of modules would speed this up for (auto *module : worklist) { @@ -198,15 +199,13 @@ struct VerifBoundedModelCheckingOpConversion std::distance(moduleAssertions.begin(), moduleAssertions.end()); if (numAssertions > 1) break; - for (auto instance : module->getBlock()->getOps()) { + for (auto instance : module->getBlock()->getOps()) worklist.push_back(symbolTable.lookup(instance.getModuleName())); - } } - if (numAssertions > 1) { + if (numAssertions > 1) return op->emitError("designs with multiple assertions are not yet " "correctly handled - instead, you can assert the " "conjunction of your assertions"); - } Location loc = op.getLoc(); SmallVector oldLoopInputTy(op.getLoop().getArgumentTypes()); @@ -291,9 +290,8 @@ struct VerifBoundedModelCheckingOpConversion size_t initIndex = 0; SmallVector inputDecls; SmallVector clockIndexes; - for (auto [curIndex, types] : - llvm::enumerate(llvm::zip(oldCircuitInputTy, circuitInputTy))) { - auto [oldTy, newTy] = types; + for (auto [curIndex, oldTy, newTy] : + llvm::enumerate(oldCircuitInputTy, circuitInputTy)) { if (isa(oldTy)) { inputDecls.push_back(initVals[initIndex++]); clockIndexes.push_back(curIndex); From 3fe3e64b1274b573dd1711c55375c300eab6fb95 Mon Sep 17 00:00:00 2001 From: Bea Healy Date: Mon, 23 Sep 2024 13:22:55 +0100 Subject: [PATCH 09/11] Instantiate SymbolTable in runOnOperation --- include/circt/Conversion/VerifToSMT.h | 3 ++- lib/Conversion/VerifToSMT/VerifToSMT.cpp | 28 ++++++++++++++---------- 2 files changed, 19 insertions(+), 12 deletions(-) diff --git a/include/circt/Conversion/VerifToSMT.h b/include/circt/Conversion/VerifToSMT.h index 51806233b278..d83c1c0c9e7b 100644 --- a/include/circt/Conversion/VerifToSMT.h +++ b/include/circt/Conversion/VerifToSMT.h @@ -21,7 +21,8 @@ class Namespace; /// Get the Verif to SMT conversion patterns. void populateVerifToSMTConversionPatterns(TypeConverter &converter, RewritePatternSet &patterns, - Namespace &names); + Namespace &names, + SymbolTable &symbolTable); } // namespace circt diff --git a/lib/Conversion/VerifToSMT/VerifToSMT.cpp b/lib/Conversion/VerifToSMT/VerifToSMT.cpp index 4c4f66fc2caf..f3882f0ee5cf 100644 --- a/lib/Conversion/VerifToSMT/VerifToSMT.cpp +++ b/lib/Conversion/VerifToSMT/VerifToSMT.cpp @@ -175,15 +175,16 @@ struct VerifBoundedModelCheckingOpConversion using OpConversionPattern::OpConversionPattern; VerifBoundedModelCheckingOpConversion(TypeConverter &converter, - MLIRContext *context, Namespace &names) - : OpConversionPattern(converter, context), names(names) {} + MLIRContext *context, Namespace &names, + SymbolTable &symbolTable) + : OpConversionPattern(converter, context), names(names), + symbolTable(symbolTable) {} LogicalResult matchAndRewrite(verif::BoundedModelCheckingOp op, OpAdaptor adaptor, ConversionPatternRewriter &rewriter) const override { // Check there is exactly one assertion SmallVector worklist; - SymbolTable symbolTable(op->getParentOfType()); int numAssertions = 0; op.walk([&](Operation *curOp) { if (isa(curOp)) @@ -194,13 +195,14 @@ struct VerifBoundedModelCheckingOpConversion // TODO: probably negligible compared to actual model checking time but // cacheing the assertion count of modules would speed this up for (auto *module : worklist) { - auto moduleAssertions = module->getRegion(0).getOps(); - numAssertions += - std::distance(moduleAssertions.begin(), moduleAssertions.end()); + module->walk([&](Operation *curOp) { + if (isa(curOp)) + numAssertions++; + if (auto inst = dyn_cast(curOp)) + worklist.push_back(symbolTable.lookup(inst.getModuleName())); + }); if (numAssertions > 1) break; - for (auto instance : module->getBlock()->getOps()) - worklist.push_back(symbolTable.lookup(instance.getModuleName())); } if (numAssertions > 1) return op->emitError("designs with multiple assertions are not yet " @@ -388,6 +390,7 @@ struct VerifBoundedModelCheckingOpConversion } Namespace &names; + SymbolTable &symbolTable; }; } // namespace @@ -405,12 +408,13 @@ struct ConvertVerifToSMTPass void circt::populateVerifToSMTConversionPatterns(TypeConverter &converter, RewritePatternSet &patterns, - Namespace &names) { + Namespace &names, + SymbolTable &symbolTable) { patterns.add(converter, patterns.getContext()); patterns.add( - converter, patterns.getContext(), names); + converter, patterns.getContext(), names, symbolTable); } void ConvertVerifToSMTPass::runOnOperation() { @@ -428,7 +432,9 @@ void ConvertVerifToSMTPass::runOnOperation() { symCache.addDefinitions(getOperation()); Namespace names; names.add(symCache); - populateVerifToSMTConversionPatterns(converter, patterns, names); + SymbolTable symbolTable(getOperation()); + + populateVerifToSMTConversionPatterns(converter, patterns, names, symbolTable); if (failed(mlir::applyPartialConversion(getOperation(), target, std::move(patterns)))) From f6e32a2890eebe2518c26149fcff8657466b8fc4 Mon Sep 17 00:00:00 2001 From: Bea Healy Date: Mon, 23 Sep 2024 15:14:21 +0100 Subject: [PATCH 10/11] Check assertion count outside pattern, update error message & add test --- include/circt/Conversion/VerifToSMT.h | 3 +- lib/Conversion/VerifToSMT/VerifToSMT.cpp | 79 ++++++++++--------- .../VerifToSMT/verif-to-smt-errors.mlir | 24 ++++-- 3 files changed, 62 insertions(+), 44 deletions(-) diff --git a/include/circt/Conversion/VerifToSMT.h b/include/circt/Conversion/VerifToSMT.h index d83c1c0c9e7b..51806233b278 100644 --- a/include/circt/Conversion/VerifToSMT.h +++ b/include/circt/Conversion/VerifToSMT.h @@ -21,8 +21,7 @@ class Namespace; /// Get the Verif to SMT conversion patterns. void populateVerifToSMTConversionPatterns(TypeConverter &converter, RewritePatternSet &patterns, - Namespace &names, - SymbolTable &symbolTable); + Namespace &names); } // namespace circt diff --git a/lib/Conversion/VerifToSMT/VerifToSMT.cpp b/lib/Conversion/VerifToSMT/VerifToSMT.cpp index f3882f0ee5cf..b54a64dfed75 100644 --- a/lib/Conversion/VerifToSMT/VerifToSMT.cpp +++ b/lib/Conversion/VerifToSMT/VerifToSMT.cpp @@ -175,40 +175,12 @@ struct VerifBoundedModelCheckingOpConversion using OpConversionPattern::OpConversionPattern; VerifBoundedModelCheckingOpConversion(TypeConverter &converter, - MLIRContext *context, Namespace &names, - SymbolTable &symbolTable) - : OpConversionPattern(converter, context), names(names), - symbolTable(symbolTable) {} + MLIRContext *context, Namespace &names) + : OpConversionPattern(converter, context), names(names) {} LogicalResult matchAndRewrite(verif::BoundedModelCheckingOp op, OpAdaptor adaptor, ConversionPatternRewriter &rewriter) const override { - // Check there is exactly one assertion - SmallVector worklist; - int numAssertions = 0; - op.walk([&](Operation *curOp) { - if (isa(curOp)) - numAssertions++; - if (auto inst = dyn_cast(curOp)) - worklist.push_back(symbolTable.lookup(inst.getModuleName())); - }); - // TODO: probably negligible compared to actual model checking time but - // cacheing the assertion count of modules would speed this up - for (auto *module : worklist) { - module->walk([&](Operation *curOp) { - if (isa(curOp)) - numAssertions++; - if (auto inst = dyn_cast(curOp)) - worklist.push_back(symbolTable.lookup(inst.getModuleName())); - }); - if (numAssertions > 1) - break; - } - if (numAssertions > 1) - return op->emitError("designs with multiple assertions are not yet " - "correctly handled - instead, you can assert the " - "conjunction of your assertions"); - Location loc = op.getLoc(); SmallVector oldLoopInputTy(op.getLoop().getArgumentTypes()); SmallVector oldCircuitInputTy(op.getCircuit().getArgumentTypes()); @@ -390,7 +362,6 @@ struct VerifBoundedModelCheckingOpConversion } Namespace &names; - SymbolTable &symbolTable; }; } // namespace @@ -408,13 +379,12 @@ struct ConvertVerifToSMTPass void circt::populateVerifToSMTConversionPatterns(TypeConverter &converter, RewritePatternSet &patterns, - Namespace &names, - SymbolTable &symbolTable) { + Namespace &names) { patterns.add(converter, patterns.getContext()); patterns.add( - converter, patterns.getContext(), names, symbolTable); + converter, patterns.getContext(), names); } void ConvertVerifToSMTPass::runOnOperation() { @@ -424,6 +394,44 @@ void ConvertVerifToSMTPass::runOnOperation() { func::FuncDialect>(); target.addLegalOp(); + // Check BMC ops contain only one assertion (done outside pattern to avoid + // issues with whether assertions are/aren't lowered yet) + SymbolTable symbolTable(getOperation()); + getOperation().walk( + [&](Operation *op) { // Check there is exactly one assertion + if (isa(op)) { + SmallVector worklist; + int numAssertions = 0; + op->walk([&](Operation *curOp) { + if (isa(curOp)) + numAssertions++; + if (auto inst = dyn_cast(curOp)) + worklist.push_back(symbolTable.lookup(inst.getModuleName())); + }); + // TODO: probably negligible compared to actual model checking time + // but cacheing the assertion count of modules would speed this up + while (!worklist.empty()) { + auto *module = worklist.pop_back_val(); + module->walk([&](Operation *curOp) { + if (isa(curOp)) + numAssertions++; + if (auto inst = dyn_cast(curOp)) + worklist.push_back(symbolTable.lookup(inst.getModuleName())); + }); + if (numAssertions > 1) + break; + } + if (numAssertions > 1) { + op->emitError( + "bounded model checking problems with multiple assertions are " + "not yet " + "correctly handled - instead, you can assert the " + "conjunction of your assertions"); + signalPassFailure(); + } + } + }); + RewritePatternSet patterns(&getContext()); TypeConverter converter; populateHWToSMTTypeConverter(converter); @@ -432,9 +440,8 @@ void ConvertVerifToSMTPass::runOnOperation() { symCache.addDefinitions(getOperation()); Namespace names; names.add(symCache); - SymbolTable symbolTable(getOperation()); - populateVerifToSMTConversionPatterns(converter, patterns, names, symbolTable); + populateVerifToSMTConversionPatterns(converter, patterns, names); if (failed(mlir::applyPartialConversion(getOperation(), target, std::move(patterns)))) diff --git a/test/Conversion/VerifToSMT/verif-to-smt-errors.mlir b/test/Conversion/VerifToSMT/verif-to-smt-errors.mlir index 5ce3da97b885..bc8e99c2030c 100644 --- a/test/Conversion/VerifToSMT/verif-to-smt-errors.mlir +++ b/test/Conversion/VerifToSMT/verif-to-smt-errors.mlir @@ -19,8 +19,7 @@ func.func @assert_with_unsupported_property_type(%arg0: !smt.bv<1>) { // ----- func.func @multiple_assertions_bmc() -> (i1) { - // expected-error @below {{designs with multiple assertions are not yet correctly handled - instead, you can assert the conjunction of your assertions}} - // expected-error @below {{failed to legalize operation 'verif.bmc' that was explicitly marked illegal}} + // expected-error @below {{bounded model checking problems with multiple assertions are not yet correctly handled - instead, you can assert the conjunction of your assertions}} %bmc = verif.bmc bound 10 num_regs 1 init {} loop {} @@ -40,8 +39,7 @@ func.func @multiple_assertions_bmc() -> (i1) { // ----- func.func @multiple_asserting_modules_bmc() -> (i1) { - // expected-error @below {{designs with multiple assertions are not yet correctly handled - instead, you can assert the conjunction of your assertions}} - // expected-error @below {{failed to legalize operation 'verif.bmc' that was explicitly marked illegal}} + // expected-error @below {{bounded model checking problems with multiple assertions are not yet correctly handled - instead, you can assert the conjunction of your assertions}} %bmc = verif.bmc bound 10 num_regs 1 init {} loop {} @@ -55,6 +53,21 @@ func.func @multiple_asserting_modules_bmc() -> (i1) { func.return %bmc : i1 } +func.func @two_separated_assertions() -> (i1) { + // expected-error @below {{bounded model checking problems with multiple assertions are not yet correctly handled - instead, you can assert the conjunction of your assertions}} + %bmc = verif.bmc bound 10 num_regs 1 + init {} + loop {} + circuit { + ^bb0(%arg0: i32, %arg1: i1, %arg2: i1): + hw.instance "" @OneAssertion(x: %arg1: i1) -> () + verif.assert %arg2 : i1 + %sum = comb.add %arg0, %arg0 : i32 + verif.yield %sum : i32 + } + func.return %bmc : i1 +} + hw.module @OneAssertion(in %x: i1) { verif.assert %x : i1 } @@ -62,8 +75,7 @@ hw.module @OneAssertion(in %x: i1) { // ----- func.func @multiple_nested_assertions() -> (i1) { - // expected-error @below {{designs with multiple assertions are not yet correctly handled - instead, you can assert the conjunction of your assertions}} - // expected-error @below {{failed to legalize operation 'verif.bmc' that was explicitly marked illegal}} + // expected-error @below {{bounded model checking problems with multiple assertions are not yet correctly handled - instead, you can assert the conjunction of your assertions}} %bmc = verif.bmc bound 10 num_regs 1 init {} loop {} From 2af0484fca203466e4ea05c0f85a19dab4145591 Mon Sep 17 00:00:00 2001 From: Bea Healy Date: Tue, 24 Sep 2024 17:07:00 +0100 Subject: [PATCH 11/11] Add assertion check early pass exit --- lib/Conversion/VerifToSMT/VerifToSMT.cpp | 8 +++++--- test/Conversion/VerifToSMT/verif-to-smt-errors.mlir | 6 ++++++ 2 files changed, 11 insertions(+), 3 deletions(-) diff --git a/lib/Conversion/VerifToSMT/VerifToSMT.cpp b/lib/Conversion/VerifToSMT/VerifToSMT.cpp index b54a64dfed75..57ef512d1f2d 100644 --- a/lib/Conversion/VerifToSMT/VerifToSMT.cpp +++ b/lib/Conversion/VerifToSMT/VerifToSMT.cpp @@ -397,7 +397,7 @@ void ConvertVerifToSMTPass::runOnOperation() { // Check BMC ops contain only one assertion (done outside pattern to avoid // issues with whether assertions are/aren't lowered yet) SymbolTable symbolTable(getOperation()); - getOperation().walk( + WalkResult assertionCheck = getOperation().walk( [&](Operation *op) { // Check there is exactly one assertion if (isa(op)) { SmallVector worklist; @@ -427,11 +427,13 @@ void ConvertVerifToSMTPass::runOnOperation() { "not yet " "correctly handled - instead, you can assert the " "conjunction of your assertions"); - signalPassFailure(); + return WalkResult::interrupt(); } } + return WalkResult::advance(); }); - + if (assertionCheck.wasInterrupted()) + return signalPassFailure(); RewritePatternSet patterns(&getContext()); TypeConverter converter; populateHWToSMTTypeConverter(converter); diff --git a/test/Conversion/VerifToSMT/verif-to-smt-errors.mlir b/test/Conversion/VerifToSMT/verif-to-smt-errors.mlir index bc8e99c2030c..dad326befb6c 100644 --- a/test/Conversion/VerifToSMT/verif-to-smt-errors.mlir +++ b/test/Conversion/VerifToSMT/verif-to-smt-errors.mlir @@ -53,6 +53,12 @@ func.func @multiple_asserting_modules_bmc() -> (i1) { func.return %bmc : i1 } +hw.module @OneAssertion(in %x: i1) { + verif.assert %x : i1 +} + +// ----- + func.func @two_separated_assertions() -> (i1) { // expected-error @below {{bounded model checking problems with multiple assertions are not yet correctly handled - instead, you can assert the conjunction of your assertions}} %bmc = verif.bmc bound 10 num_regs 1