[circt-bmc] Preserve signal names before lowering

include/circt/Tools/circt-bmc/Passes.td

@@ -38,7 +38,8 @@ def LowerToBMC : Pass<"lower-to-bmc", "::mlir::ModuleOp"> {
 
   let dependentDialects = [
     "mlir::func::FuncDialect", "mlir::LLVM::LLVMDialect",
-    "circt::verif::VerifDialect", "circt::comb::CombDialect"
+    "circt::verif::VerifDialect", "circt::comb::CombDialect",
+    "circt::debug::DebugDialect"
   ];
 }
 

lib/Tools/circt-bmc/CMakeLists.txt

@@ -10,6 +10,7 @@ add_circt_library(CIRCTBMCTransforms
   CIRCTSeq
   CIRCTComb
   CIRCTVerif
+  CIRCTDebug
 
   MLIRFuncDialect
   MLIRIR

lib/Tools/circt-bmc/LowerToBMC.cpp

@@ -7,6 +7,7 @@
 //===----------------------------------------------------------------------===//
 
 #include "circt/Dialect/Comb/CombOps.h"
+#include "circt/Dialect/Debug/DebugOps.h"
 #include "circt/Dialect/HW/HWOps.h"
 #include "circt/Dialect/HW/HWTypes.h"
 #include "circt/Dialect/Seq/SeqOps.h"
@@ -86,6 +87,16 @@ void LowerToBMCPass::runOnOperation() {
                                         builder.getFunctionType({}, {}));
   builder.createBlock(&entryFunc.getBody());
 
+  // Save module name and port info before the module is erased
+  auto *hwOutput = hwModule.getBody().front().getTerminator();
+  SmallVector<std::pair<StringAttr, Value>> namedPorts;
+  for (auto &port : hwModule.getPortList()) {
+    Value portValue = port.isInput()
+                          ? hwModule.getBody().front().getArgument(port.argNum)
+                          : hwOutput->getOperand(port.argNum);
+    namedPorts.push_back({builder.getStringAttr(port.getName()), portValue});
+  }
+
   {
     OpBuilder::InsertionGuard guard(builder);
     auto *terminator = hwModule.getBody().front().getTerminator();
@@ -187,9 +198,24 @@ void LowerToBMCPass::runOnOperation() {
       verif::YieldOp::create(builder, loc, ValueRange{});
     }
   }
+  auto moduleName = hwModule.getNameAttr();
   bmcOp.getCircuit().takeBody(hwModule.getBody());
   hwModule->erase();
 
+  // signal names for counter-example generation.
+  {
+    OpBuilder::InsertionGuard guard(builder);
+    auto &circuitBlock = bmcOp.getCircuit().front();
+    builder.setInsertionPoint(circuitBlock.getTerminator());
+    auto scope = debug::ScopeOp::create(
+        builder, loc, moduleName.getValue(),
+        // TODO: Hierarchy support would require walking parent InstanceOps,
+        // but LowerToBMC operates on a single top-level module with no
+        // instance context available at this point.
+        moduleName, nullptr);
+    for (auto &[name, value] : namedPorts)
+      debug::VariableOp::create(builder, loc, name, value, scope);
+  }
   // Define global string constants to print on success/failure
   auto createUniqueStringGlobal = [&](StringRef str) -> FailureOr<Value> {
     Location loc = moduleOp.getLoc();

test/Tools/circt-bmc/lower-to-bmc-debug.mlir

@@ -0,0 +1,23 @@
+// RUN: circt-opt --lower-to-bmc="top-module=Simple bound=1" %s | FileCheck %s --check-prefix=SIMPLE
+// RUN: circt-opt --lower-to-bmc="top-module=Passthrough bound=2" %s | FileCheck %s --check-prefix=PASSTHROUGH
+
+// SIMPLE: ^bb0([[IN:%.+]]: i8):
+// SIMPLE: [[SCOPE:%.+]] = dbg.scope "Simple", "Simple"
+// SIMPLE-DAG: dbg.variable "in", [[IN]] scope [[SCOPE]] : i8
+// SIMPLE-DAG: dbg.variable "out", [[IN]] scope [[SCOPE]] : i8
+
+hw.module @Simple(in %in: i8, out out: i8) attributes {num_regs = 0 : i32, initial_values = []} {
+  hw.output %in : i8
+}
+
+// PASSTHROUGH: ^bb0([[A:%.+]]: i4, [[B:%.+]]: i4):
+// PASSTHROUGH: [[SUM:%.+]] = comb.add [[A]], [[B]] : i4
+// PASSTHROUGH: [[SCOPE:%.+]] = dbg.scope "Passthrough", "Passthrough"
+// PASSTHROUGH-DAG: dbg.variable "a", [[A]] scope [[SCOPE]] : i4
+// PASSTHROUGH-DAG: dbg.variable "b", [[B]] scope [[SCOPE]] : i4
+// PASSTHROUGH-DAG: dbg.variable "sum", [[SUM]] scope [[SCOPE]] : i4
+
+hw.module @Passthrough(in %a: i4, in %b: i4, out sum: i4) attributes {num_regs = 0 : i32, initial_values = []} {
+  %0 = comb.add %a, %b : i4
+  hw.output %0 : i4
+}