[circt-bmc] handle 'verif.formal' / 'verif.contract' op in module

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<

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

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<StringAttr> referencedModules;
+  module.walk([&](InstanceOp op) {
+    referencedModules.insert(op.getReferencedModuleNameAttr());
+  });
+
+  auto result = module.walk([&](SymbolicValueOp op) -> WalkResult {
+    if (!op->getParentOfType<HWModuleOp>())
+      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<HWModuleOp>()) {
+    SmallVector<SymbolicValueOp> 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();
+}

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
+}

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<WIDTH: i32>
 // 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
+}

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

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> outputFormat(
 // Tool implementation
 //===----------------------------------------------------------------------===//
 
+static void collectTopLevelSymbolDeps(Operation *op, Operation *topLevel,
+                                      SymbolTable &symbolTable,
+                                      DenseSet<Operation *> &liveOps) {
+  SmallVector<Operation *> 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<FlatSymbolRefAttr>(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<verif::FormalOp>(moduleName);
+  if (!formalOp)
+    return;
+
+  SymbolTable symbolTable(module);
+  DenseSet<Operation *> liveOps;
+  collectTopLevelSymbolDeps(formalOp, module, symbolTable, liveOps);
+
+  for (auto &op : llvm::make_early_inc_range(module.getBody()->getOperations()))
+    if (!liveOps.contains(&op) &&
+        isa<hw::HWModuleOp, verif::FormalOp, verif::SimulationOp>(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<std::unique_ptr<llvm::ToolOutputFile>> 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<hw::HWModuleOp>(createLowerLTLToCorePass());
   pm.addNestedPass<hw::HWModuleOp>(verif::createCombineAssertLikePass());