diff --git a/include/circt/Dialect/Verif/Passes.td b/include/circt/Dialect/Verif/Passes.td index 6d70a83cfef9..33c05ad25bb5 100644 --- a/include/circt/Dialect/Verif/Passes.td +++ b/include/circt/Dialect/Verif/Passes.td @@ -132,7 +132,7 @@ def LowerContractsPass : Pass<"lower-contracts", "mlir::ModuleOp"> { def LowerSymbolicValuesPass : Pass<"verif-lower-symbolic-values", "mlir::ModuleOp"> { - let summary = "Lower symbolic values to blackbox instances or wires"; + let summary = "Lower symbolic values to blackbox instances, wires, or inputs"; let description = [{ Converts `verif.symbolic_value` ops into one of the following representations that formal tools can work with: @@ -142,6 +142,8 @@ def LowerSymbolicValuesPass : Pass<"verif-lower-symbolic-values", outputs. - Wire declarations marked with `(* anyseq *)`, which Yosys treats like a top-level input port. + - Input ports on the containing `hw.module`, for downstream lowerings that + already model module inputs as unconstrained values. }]; let options = [ Option< diff --git a/include/circt/Dialect/Verif/VerifPasses.h b/include/circt/Dialect/Verif/VerifPasses.h index 53dc0a9387df..2cc59b0be13a 100644 --- a/include/circt/Dialect/Verif/VerifPasses.h +++ b/include/circt/Dialect/Verif/VerifPasses.h @@ -31,6 +31,8 @@ enum class SymbolicValueLowering { ExtModule, /// Lower to wire declarations with a `(* anyseq *)` attribute. Yosys, + /// Lower to input ports on the containing `hw.module`. + HWInput, }; /// Construct the command line options to pick one of the symbolic value @@ -40,7 +42,9 @@ static inline llvm::cl::ValuesClass symbolicValueLoweringCLValues() { clEnumValN(SymbolicValueLowering::ExtModule, "extmodule", "Lower to instances of an external module"), clEnumValN(SymbolicValueLowering::Yosys, "yosys", - "Lower to `(* anyseq *)` wire declarations")); + "Lower to `(* anyseq *)` wire declarations"), + clEnumValN(SymbolicValueLowering::HWInput, "hw-input", + "Lower to input ports on the containing `hw.module`")); } #define GEN_PASS_DECL diff --git a/lib/Dialect/Verif/Transforms/LowerSymbolicValues.cpp b/lib/Dialect/Verif/Transforms/LowerSymbolicValues.cpp index 649ac22a456e..344059d0fb7d 100644 --- a/lib/Dialect/Verif/Transforms/LowerSymbolicValues.cpp +++ b/lib/Dialect/Verif/Transforms/LowerSymbolicValues.cpp @@ -9,6 +9,7 @@ #include "circt/Dialect/SV/SVOps.h" #include "circt/Dialect/Verif/VerifOps.h" #include "circt/Dialect/Verif/VerifPasses.h" +#include "llvm/ADT/DenseSet.h" using namespace circt; using namespace mlir; @@ -29,6 +30,7 @@ struct LowerSymbolicValuesPass void runOnOperation() override; LogicalResult lowerToExtModule(); void lowerToAnySeqWire(); + LogicalResult lowerToHWInputs(); }; } // namespace @@ -41,6 +43,10 @@ void LowerSymbolicValuesPass::runOnOperation() { case SymbolicValueLowering::Yosys: lowerToAnySeqWire(); break; + case SymbolicValueLowering::HWInput: + if (failed(lowerToHWInputs())) + signalPassFailure(); + break; } } @@ -113,3 +119,50 @@ void LowerSymbolicValuesPass::lowerToAnySeqWire() { op.erase(); }); } + +/// Replace `SymbolicValueOp`s in `hw.module` bodies with input ports. +LogicalResult LowerSymbolicValuesPass::lowerToHWInputs() { + auto module = getOperation(); + DenseSet referencedModules; + module.walk([&](InstanceOp op) { + referencedModules.insert(op.getReferencedModuleNameAttr()); + }); + + auto result = module.walk([&](SymbolicValueOp op) -> WalkResult { + if (!op->getParentOfType()) + return op.emitError() + << "cannot lower symbolic value to hw.module input outside of an " + "hw.module"; + return WalkResult::advance(); + }); + if (result.wasInterrupted()) + return failure(); + + for (auto hwModule : module.getOps()) { + SmallVector symbolicValues; + hwModule.walk([&](SymbolicValueOp op) { symbolicValues.push_back(op); }); + if (symbolicValues.empty()) + continue; + + if (referencedModules.contains(hwModule.getModuleNameAttr())) { + hwModule.emitError() + << "cannot lower symbolic values in instantiated module '" + << hwModule.getModuleName() + << "' to HW inputs; run the 'hw-input' lowering strategy after " + "flattening modules"; + return failure(); + } + + for (auto symbolicValue : symbolicValues) { + auto [name, arg] = hwModule.insertInput( + hwModule.getNumInputPorts(), + StringAttr::get(module.getContext(), "symbolic_value"), + symbolicValue.getType()); + (void)name; + symbolicValue.getResult().replaceAllUsesWith(arg); + symbolicValue.erase(); + } + } + + return success(); +} diff --git a/test/Dialect/Verif/lower-symbolic-values-errors.mlir b/test/Dialect/Verif/lower-symbolic-values-errors.mlir index f6eda4b17ff0..a3d000409487 100644 --- a/test/Dialect/Verif/lower-symbolic-values-errors.mlir +++ b/test/Dialect/Verif/lower-symbolic-values-errors.mlir @@ -1,6 +1,31 @@ -// RUN: circt-opt --verif-lower-symbolic-values=mode=extmodule --split-input-file --verify-diagnostics %s +// RUN: split-file %s %t +// RUN: circt-opt --verif-lower-symbolic-values=mode=extmodule --verify-diagnostics %t/extmodule.mlir +// RUN: circt-opt --verif-lower-symbolic-values=mode=hw-input --verify-diagnostics %t/hw-input-instantiated.mlir +// RUN: circt-opt --verif-lower-symbolic-values=mode=hw-input --verify-diagnostics %t/hw-input-formal.mlir + +//--- extmodule.mlir hw.module @Foo() { // expected-error @below {{symbolic value bit width unknown}} verif.symbolic_value : !hw.string } + +//--- hw-input-instantiated.mlir + +hw.module @Top(out y : i8) { + %0 = hw.instance "m" @Instantiated() -> (y: i8) + hw.output %0 : i8 +} + +// expected-error @+1 {{cannot lower symbolic values in instantiated module 'Instantiated' to HW inputs; run the 'hw-input' lowering strategy after flattening modules}} +hw.module @Instantiated(out y : i8) { + %0 = verif.symbolic_value : i8 + hw.output %0 : i8 +} + +//--- hw-input-formal.mlir + +verif.formal @Formal {} { + // expected-error @below {{cannot lower symbolic value to hw.module input outside of an hw.module}} + verif.symbolic_value : i8 +} diff --git a/test/Dialect/Verif/lower-symbolic-values.mlir b/test/Dialect/Verif/lower-symbolic-values.mlir index 85ef37c4c88e..ae7308566fb3 100644 --- a/test/Dialect/Verif/lower-symbolic-values.mlir +++ b/test/Dialect/Verif/lower-symbolic-values.mlir @@ -1,5 +1,6 @@ // RUN: circt-opt --verif-lower-symbolic-values=mode=extmodule %s | FileCheck --check-prefixes=CHECK,CHECK-EXTMODULE %s // RUN: circt-opt --verif-lower-symbolic-values=mode=yosys %s | FileCheck --check-prefixes=CHECK,CHECK-YOSYS %s +// RUN: circt-opt --verif-lower-symbolic-values=mode=hw-input %s | FileCheck --check-prefix=CHECK-HW-INPUT %s // CHECK-LABEL: hw.module @Foo hw.module @Foo() { @@ -44,3 +45,12 @@ hw.module @Foo() { // CHECK-EXTMODULE: hw.module.extern @circt.symbolic_value.12 // CHECK-EXTMODULE-SAME: verilogName = "circt_symbolic_value" + +// CHECK-HW-INPUT-LABEL: hw.module @HWInput( +// CHECK-HW-INPUT-SAME: in %[[SYM:.+]] : i8, out {{.*}} : i8) +// CHECK-HW-INPUT-NEXT: hw.output %[[SYM]] : i8 +// CHECK-HW-INPUT-NEXT: } +hw.module @HWInput(out y : i8) { + %0 = verif.symbolic_value : i8 + hw.output %0 : i8 +} diff --git a/test/Tools/circt-bmc/contract.mlir b/test/Tools/circt-bmc/contract.mlir new file mode 100644 index 000000000000..8a1e9c38fcf1 --- /dev/null +++ b/test/Tools/circt-bmc/contract.mlir @@ -0,0 +1,41 @@ +// RUN: circt-opt %s --lower-contracts | circt-bmc - -b 1 --module Caller_CheckContract_0 --emit-mlir -o - | FileCheck %s + +// CHECK-NOT: verif.symbolic_value +// CHECK-LABEL: func.func @Callee( +// CHECK-SAME: %[[CALLEE_INPUT:.+]]: !smt.bv<8>, %[[CALLEE_RESULT:.+]]: !smt.bv<8> +// CHECK: %[[CALLEE_EQ:.+]] = smt.eq %[[CALLEE_RESULT]], %[[CALLEE_INPUT]] : !smt.bv<8> +// CHECK: %[[CALLEE_ITE:.+]] = smt.ite %[[CALLEE_EQ]], +// CHECK: %[[CALLEE_ASSUME:.+]] = smt.eq %[[CALLEE_ITE]], +// CHECK: smt.assert %[[CALLEE_ASSUME]] +hw.module @Callee(in %a : i8, out y : i8) { + %0 = verif.contract %a : i8 { + %1 = comb.icmp eq %0, %a : i8 + verif.ensure %1 : i1 + } + hw.output %0 : i8 +} + +// CHECK-NOT: func.func @Caller( +// CHECK-LABEL: func.func @Caller_CheckContract_0() +// CHECK: smt.solver +hw.module @Caller(in %a : i8, out y : i8) { + %0 = hw.instance "callee" @Callee(a: %a: i8) -> (y: i8) + %1 = verif.contract %0 : i8 { + %2 = comb.icmp eq %1, %a : i8 + verif.ensure %2 : i1 + } + hw.output %1 : i8 +} + +// CHECK-LABEL: func.func @bmc_circuit( +// CHECK-SAME: %[[INPUT:.+]]: !smt.bv<8>, %[[RESULT:.+]]: !smt.bv<8>) +// CHECK: %[[ASSUME_EQ:.+]] = smt.eq %[[RESULT]], %[[INPUT]] : !smt.bv<8> +// CHECK: %[[ASSUME_ITE:.+]] = smt.ite %[[ASSUME_EQ]], +// CHECK: %[[ASSUME:.+]] = smt.eq %[[ASSUME_ITE]], +// CHECK: smt.assert %[[ASSUME]] +// CHECK: %[[ASSERT_EQ:.+]] = smt.eq %[[RESULT]], %[[INPUT]] : !smt.bv<8> +// CHECK: %[[ASSERT_ITE:.+]] = smt.ite %[[ASSERT_EQ]], +// CHECK: %[[ASSERT:.+]] = smt.eq %[[ASSERT_ITE]], +// CHECK: %[[VIOLATED:.+]] = smt.not %[[ASSERT]] +// CHECK: smt.assert %[[VIOLATED]] +// CHECK-NOT: verif.symbolic_value diff --git a/tools/circt-bmc/circt-bmc.cpp b/tools/circt-bmc/circt-bmc.cpp index aadfb08d86c5..562315ec362f 100644 --- a/tools/circt-bmc/circt-bmc.cpp +++ b/tools/circt-bmc/circt-bmc.cpp @@ -27,6 +27,7 @@ #include "circt/Dialect/OM/OMPasses.h" #include "circt/Dialect/Seq/SeqDialect.h" #include "circt/Dialect/Verif/VerifDialect.h" +#include "circt/Dialect/Verif/VerifOps.h" #include "circt/Dialect/Verif/VerifPasses.h" #include "circt/Support/Passes.h" #include "circt/Support/Version.h" @@ -42,6 +43,7 @@ #include "mlir/IR/Diagnostics.h" #include "mlir/IR/OwningOpRef.h" #include "mlir/IR/PatternMatch.h" +#include "mlir/IR/SymbolTable.h" #include "mlir/Parser/Parser.h" #include "mlir/Pass/PassManager.h" #include "mlir/Support/FileUtilities.h" @@ -50,6 +52,7 @@ #include "mlir/Target/LLVMIR/Dialect/LLVMIR/LLVMToLLVMIRTranslation.h" #include "mlir/Target/LLVMIR/Export.h" #include "mlir/Transforms/Passes.h" +#include "llvm/ADT/SmallVector.h" #include "llvm/IR/Module.h" #include "llvm/Support/CommandLine.h" #include "llvm/Support/Error.h" @@ -163,6 +166,49 @@ static cl::opt outputFormat( // Tool implementation //===----------------------------------------------------------------------===// +static void collectTopLevelSymbolDeps(Operation *op, Operation *topLevel, + SymbolTable &symbolTable, + DenseSet &liveOps) { + SmallVector worklist{op}; + while (!worklist.empty()) { + auto *current = worklist.pop_back_val(); + if (!liveOps.insert(current).second) + continue; + + auto symbolUses = SymbolTable::getSymbolUses(current); + if (!symbolUses) + continue; + + for (auto &use : *symbolUses) { + auto symbolRef = dyn_cast(use.getSymbolRef()); + if (!symbolRef) + continue; + auto *symbol = symbolTable.lookup(symbolRef.getValue()); + if (!symbol || symbol->getParentOp() != topLevel) + continue; + worklist.push_back(symbol); + } + } +} + +static void isolateFormalTest(ModuleOp module) { + if (moduleName.empty()) + return; + + auto formalOp = module.lookupSymbol(moduleName); + if (!formalOp) + return; + + SymbolTable symbolTable(module); + DenseSet liveOps; + collectTopLevelSymbolDeps(formalOp, module, symbolTable, liveOps); + + for (auto &op : llvm::make_early_inc_range(module.getBody()->getOperations())) + if (!liveOps.contains(&op) && + isa(op)) + op.erase(); +} + /// This function initializes the various components of the tool and /// orchestrates the work to be done. static LogicalResult executeBMC(MLIRContext &context) { @@ -180,6 +226,8 @@ static LogicalResult executeBMC(MLIRContext &context) { if (!module) return failure(); + isolateFormalTest(*module); + // Create the output directory or output file depending on our mode. std::optional> outputFile; std::string errorMessage; @@ -210,6 +258,8 @@ static LogicalResult executeBMC(MLIRContext &context) { // builtin.module options.inlinePublic = true; pm.addPass(hw::createFlattenModules(options)); + pm.addPass(verif::createLowerSymbolicValuesPass( + {verif::SymbolicValueLowering::HWInput})); } pm.addNestedPass(createLowerLTLToCorePass()); pm.addNestedPass(verif::createCombineAssertLikePass());