[circt-lec] Accept two MLIR inputs (#7450)

Practically it is very useful to verify equivalence between modules in two different MLIR files. This commit changes `inputFilename` to a list and implements a very simple module merge that moves operations in the second module to the first by resolving the symbol.

test/CMakeLists.txt

@@ -24,6 +24,7 @@ set(CIRCT_TEST_DEPENDS
   circt-capi-firtool-test
   circt-as
   circt-dis
+  circt-lec
   circt-opt
   circt-translate
   circt-reduce

test/Tools/circt-lec/merge-inputs-error.mlir

@@ -0,0 +1,14 @@
+// RUN: split-file %s %t
+// RUN: not circt-lec %t/a.mlir %t/b.mlir --c1 top_a --c2 top_not_exist 2>&1 | FileCheck %s
+
+// CHECK: module "top_not_exist" was not found in the second module
+
+//--- a.mlir
+hw.module @top_a(in %a : i8, out b : i8) {
+  hw.output %a : i8
+}
+
+//--- b.mlir
+hw.module @top_b(in %a : i8, out b : i8) {
+  hw.output %a : i8
+}

test/Tools/circt-lec/merge-inputs.mlir

@@ -0,0 +1,42 @@
+// RUN: split-file %s %t
+// RUN: circt-lec %t/a.mlir %t/b.mlir --c1 top_a --c2 top_b --emit-mlir | FileCheck %s
+
+//--- a.mlir
+hw.module @foo(in %a : i8, out b : i8) {
+  %c1_i8 = hw.constant 1 : i8
+  %add = comb.add %a, %c1_i8: i8
+  hw.output %add : i8
+}
+hw.module @top_a(in %a : i8, out b : i8) {
+  %foo.b = hw.instance "foo" @foo(a: %a: i8) -> (b: i8)
+  hw.output %foo.b : i8
+}
+
+//--- b.mlir
+hw.module @foo(in %a : i8, out b : i8) {
+  %c2_i8 = hw.constant 2 : i8
+  %add = comb.add %a, %c2_i8: i8
+  hw.output %add : i8
+}
+
+hw.module @top_b(in %a : i8, out b : i8) {
+  %foo.b = hw.instance "foo" @foo(a: %a: i8) -> (b: i8)
+  hw.output %foo.b : i8
+}
+
+// Check constants to make sure a.mlir and b.mlir are properly merged.
+// CHECK-LABEL: func.func @foo_0(%arg0: !smt.bv<8>) -> !smt.bv<8>
+// CHECK-NEXT: %c2_bv8 = smt.bv.constant #smt.bv<2>
+// CHECK-NEXT: %0 = smt.bv.add %arg0, %c2_bv8
+// CHECK-NEXT: return %0
+
+// CHECK-LABEL: func.func @foo(%arg0: !smt.bv<8>) -> !smt.bv<8>
+// CHECK-NEXT: %c1_bv8 = smt.bv.constant #smt.bv<1>
+// CHECK-NEXT: %0 = smt.bv.add %arg0, %c1_bv8
+// CHECK-NEXT: return %0
+
+// CHECK-LABEL: func.func @top_a
+// CHECK:      %[[RESULT1:.+]] = func.call @foo(%[[ARG:.+]])
+// CHECK-NEXT: %[[RESULT2:.+]] = func.call @foo_0(%[[ARG]])
+// CHECK-NEXT: %[[VAL:.+]] = smt.distinct %[[RESULT1]], %[[RESULT2]]
+// CHECK-NEXT: smt.assert %[[VAL]]

test/lit.cfg.py

@@ -60,8 +60,8 @@ tool_dirs = [
 tools = [
     'arcilator', 'circt-as', 'circt-capi-ir-test', 'circt-capi-om-test',
     'circt-capi-firrtl-test', 'circt-capi-firtool-test', 'circt-dis',
-    'circt-reduce', 'circt-translate', 'firtool', 'hlstool', 'om-linker',
-    'ibistool'
+    'circt-lec', 'circt-reduce', 'circt-translate', 'firtool', 'hlstool',
+    'om-linker', 'ibistool'
 ]
 
 if "CIRCT_OPT_CHECK_IR_ROUNDTRIP" in os.environ:

tools/circt-lec/circt-lec.cpp

@@ -71,9 +71,9 @@ static cl::opt<std::string> secondModuleName(
     cl::desc("Specify a named module for the second circuit of the comparison"),
     cl::value_desc("module name"), cl::cat(mainCategory));
 
-static cl::opt<std::string> inputFilename(cl::Positional, cl::Required,
-                                          cl::desc("<input file>"),
-                                          cl::cat(mainCategory));
+static cl::list<std::string> inputFilenames(cl::Positional, cl::OneOrMore,
+                                            cl::desc("<input files>"),
+                                            cl::cat(mainCategory));
 
 static cl::opt<std::string> outputFilename("o", cl::desc("Output filename"),
                                            cl::value_desc("filename"),
@@ -122,6 +122,65 @@ static cl::opt<OutputFormat> outputFormat(
 // Tool implementation
 //===----------------------------------------------------------------------===//
 
+// Move all operations in `src` to `dest`. Rename all symbols in `src` to avoid
+// conflict.
+static FailureOr<StringAttr> mergeModules(ModuleOp dest, ModuleOp src,
+                                          StringAttr name) {
+
+  SymbolTable destTable(dest), srcTable(src);
+  StringAttr newName = {};
+  for (auto &op : src.getOps()) {
+    if (SymbolOpInterface symbol = dyn_cast<SymbolOpInterface>(op)) {
+      auto oldSymbol = symbol.getNameAttr();
+      auto result = srcTable.renameToUnique(&op, {&destTable});
+      if (failed(result))
+        return src->emitError() << "failed to rename symbol " << oldSymbol;
+
+      if (oldSymbol == name) {
+        assert(!newName && "symbol must be unique");
+        newName = *result;
+      }
+    }
+  }
+
+  if (!newName)
+    return src->emitError()
+           << "module " << name << " was not found in the second module";
+
+  dest.getBody()->getOperations().splice(dest.getBody()->begin(),
+                                         src.getBody()->getOperations());
+  return newName;
+}
+
+// Parse one or two MLIR modules and merge it into a single module.
+static FailureOr<OwningOpRef<ModuleOp>>
+parseAndMergeModules(MLIRContext &context, TimingScope &ts) {
+  auto parserTimer = ts.nest("Parse and merge MLIR input(s)");
+
+  if (inputFilenames.size() > 2) {
+    llvm::errs() << "more than 2 files are provided!\n";
+    return failure();
+  }
+
+  auto module = parseSourceFile<ModuleOp>(inputFilenames[0], &context);
+  if (!module)
+    return failure();
+
+  if (inputFilenames.size() == 2) {
+    auto moduleOpt = parseSourceFile<ModuleOp>(inputFilenames[1], &context);
+    if (!moduleOpt)
+      return failure();
+    auto result = mergeModules(module.get(), moduleOpt.get(),
+                               StringAttr::get(&context, secondModuleName));
+    if (failed(result))
+      return failure();
+
+    secondModuleName.setValue(result->getValue().str());
+  }
+
+  return module;
+}
+
 /// This functions initializes the various components of the tool and
 /// orchestrates the work to be done.
 static LogicalResult executeLEC(MLIRContext &context) {
@@ -130,15 +189,12 @@ static LogicalResult executeLEC(MLIRContext &context) {
   applyDefaultTimingManagerCLOptions(tm);
   auto ts = tm.getRootScope();
 
-  OwningOpRef<ModuleOp> module;
-  {
-    auto parserTimer = ts.nest("Parse MLIR input");
-    // Parse the provided input files.
-    module = parseSourceFile<ModuleOp>(inputFilename, &context);
-  }
-  if (!module)
+  auto parsedModule = parseAndMergeModules(context, ts);
+  if (failed(parsedModule))
     return failure();
 
+  OwningOpRef<ModuleOp> module = std::move(parsedModule.value());
+
   // Create the output directory or output file depending on our mode.
   std::optional<std::unique_ptr<llvm::ToolOutputFile>> outputFile;
   std::string errorMessage;