Plumb dbg.variable anchors into SMT symbol names

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

@@ -46,9 +46,9 @@ def ExternalizeRegisters : Pass<"externalize-registers", "::mlir::ModuleOp"> {
   let summary = "Removes registers and adds corresponding input and output ports";
 
   let dependentDialects = [
-    "circt::seq::SeqDialect", "circt::hw::HWDialect"
+    "circt::debug::DebugDialect", "circt::seq::SeqDialect",
+    "circt::hw::HWDialect"
   ];
 }
 
 #endif // CIRCT_TOOLS_CIRCT_BMC_PASSES_TD
-

lib/Conversion/VerifToSMT/CMakeLists.txt

@@ -8,6 +8,7 @@ add_circt_conversion_library(CIRCTVerifToSMT
   Core
 
   LINK_LIBS PUBLIC
+  CIRCTDebug
   CIRCTHW
   CIRCTHWToSMT
   CIRCTVerif

lib/Conversion/VerifToSMT/VerifToSMT.cpp

@@ -8,6 +8,7 @@
 
 #include "circt/Conversion/VerifToSMT.h"
 #include "circt/Conversion/HWToSMT.h"
+#include "circt/Dialect/Debug/DebugOps.h"
 #include "circt/Dialect/Seq/SeqTypes.h"
 #include "circt/Dialect/Verif/VerifOps.h"
 #include "circt/Support/Namespace.h"
@@ -20,6 +21,7 @@
 #include "mlir/IR/ValueRange.h"
 #include "mlir/Pass/Pass.h"
 #include "mlir/Transforms/DialectConversion.h"
+#include "llvm/ADT/DenseMap.h"
 #include "llvm/ADT/SmallVector.h"
 
 namespace circt {
@@ -376,6 +378,22 @@ struct VerifBoundedModelCheckingOpConversion
       return success();
     }
 
+    // Collect names anchored to BMC circuit arguments via `dbg.variable` and
+    // erase the debug anchors before continuing SMT lowering.
+    SmallDenseMap<unsigned, StringAttr> debugArgNames;
+    SmallVector<debug::VariableOp> debugOpsToErase;
+    for (auto varOp : op.getCircuit().front().getOps<debug::VariableOp>()) {
+      auto arg = dyn_cast<BlockArgument>(varOp.getValue());
+      if (!arg || arg.getOwner() != &op.getCircuit().front())
+        continue;
+      if (varOp.getName().empty())
+        continue;
+      debugArgNames.try_emplace(arg.getArgNumber(), varOp.getNameAttr());
+      debugOpsToErase.push_back(varOp);
+    }
+    for (auto varOp : debugOpsToErase)
+      rewriter.eraseOp(varOp);
+
     SmallVector<Type> oldLoopInputTy(op.getLoop().getArgumentTypes());
     SmallVector<Type> oldCircuitInputTy(op.getCircuit().getArgumentTypes());
     // TODO: the init and loop regions should be able to be concrete instead of
@@ -482,13 +500,16 @@ struct VerifBoundedModelCheckingOpConversion
         }
       }
       // Give a meaningful name prefix based on the argument's role.
-      std::string name;
-      if (curIndex >= regStartIdx)
-        name = ("reg_" + Twine(curIndex - regStartIdx)).str();
-      else
-        name = ("input_" + Twine(curIndex)).str();
-      inputDecls.push_back(smt::DeclareFunOp::create(
-          rewriter, loc, newTy, rewriter.getStringAttr(name)));
+      auto name = debugArgNames.lookup(curIndex);
+      if (!name) {
+        if (curIndex >= regStartIdx)
+          name = rewriter.getStringAttr(
+              ("reg_" + Twine(curIndex - regStartIdx)).str());
+        else
+          name = rewriter.getStringAttr(("input_" + Twine(curIndex)).str());
+      }
+      inputDecls.push_back(
+          smt::DeclareFunOp::create(rewriter, loc, newTy, name));
     }
 
     auto numStateArgs = initVals.size() - initIndex;
@@ -601,9 +622,12 @@ struct VerifBoundedModelCheckingOpConversion
             if (isa<seq::ClockType>(oldTy)) {
               newDecls.push_back(loopVals[loopIndex++]);
             } else {
-              auto name = ("input_" + Twine(inputIdx)).str();
-              newDecls.push_back(smt::DeclareFunOp::create(
-                  builder, loc, newTy, builder.getStringAttr(name)));
+              auto name = debugArgNames.lookup(inputIdx);
+              if (!name)
+                name =
+                    builder.getStringAttr(("input_" + Twine(inputIdx)).str());
+              newDecls.push_back(
+                  smt::DeclareFunOp::create(builder, loc, newTy, name));
             }
           }
 

lib/Tools/circt-bmc/CMakeLists.txt

@@ -6,6 +6,7 @@ add_circt_library(CIRCTBMCTransforms
   CIRCTBMCTransformsIncGen
 
   LINK_LIBS PUBLIC
+  CIRCTDebug
   CIRCTHW
   CIRCTSeq
   CIRCTComb

lib/Tools/circt-bmc/ExternalizeRegisters.cpp

@@ -7,6 +7,7 @@
 //===----------------------------------------------------------------------===//
 
 #include "circt/Dialect/Comb/CombOps.h"
+#include "circt/Dialect/Debug/DebugOps.h"
 #include "circt/Dialect/HW/HWInstanceGraph.h"
 #include "circt/Dialect/HW/HWOps.h"
 #include "circt/Dialect/Seq/SeqOps.h"
@@ -51,6 +52,8 @@ struct ExternalizeRegistersPass
   DenseMap<StringAttr, SmallVector<StringAttr>> addedOutputNames;
   DenseMap<StringAttr, SmallVector<Attribute>> initialValues;
 
+  void materializeDebugVariables(HWModuleOp module);
+
   LogicalResult externalizeReg(HWModuleOp module, Operation *op, Twine regName,
                                Value clock, Attribute initState, Value reset,
                                bool isAsync, Value resetValue, Value next);
@@ -204,7 +207,48 @@ void ExternalizeRegistersPass::runOnOperation() {
       module->setAttr("initial_values",
                       ArrayAttr::get(&getContext(),
                                      initialValues[module.getSymNameAttr()]));
+      materializeDebugVariables(module);
+    }
+  }
+}
+
+void ExternalizeRegistersPass::materializeDebugVariables(HWModuleOp module) {
+  auto *body = module.getBodyBlock();
+  DenseSet<Value> trackedValues;
+  for (auto varOp : body->getOps<debug::VariableOp>())
+    trackedValues.insert(varOp.getValue());
+
+  DenseSet<StringAttr> outputPortNames;
+  for (auto &port : module.getPortList())
+    if (port.isOutput())
+      outputPortNames.insert(port.name);
+
+  OpBuilder builder = OpBuilder::atBlockBegin(body);
+  StringRef stateSuffix = "_state";
+  for (auto &port : module.getPortList()) {
+    if (port.isOutput())
+      continue;
+    if (isa<seq::ClockType>(port.type))
+      continue;
+    if (!port.name || port.name.getValue().empty())
+      continue;
+
+    auto value = body->getArgument(port.argNum);
+    if (!trackedValues.insert(value).second)
+      continue;
+
+    StringAttr debugName = port.name;
+    auto portName = port.name.getValue();
+    if (portName.ends_with(stateSuffix)) {
+      auto baseName = portName.drop_back(stateSuffix.size());
+      auto nextNameAttr =
+          builder.getStringAttr((Twine(baseName) + "_next").str());
+      if (outputPortNames.contains(nextNameAttr))
+        debugName = builder.getStringAttr(baseName);
     }
+
+    debug::VariableOp::create(builder, value.getLoc(), debugName, value,
+                              /*scope=*/Value{});
   }
 }
 

test/Conversion/VerifToSMT/verif-to-smt.mlir

@@ -457,3 +457,37 @@ func.func @multi_nondet() -> () {
   }
   return
 }
+
+// -----
+
+// CHECK-LABEL: func.func @bmc_debug_anchors_to_names() -> i1 {
+// CHECK:         smt.declare_fun "port_data" : !smt.bv<8>
+// CHECK:         smt.declare_fun "state_data" : !smt.bv<8>
+// CHECK:         smt.declare_fun "port_data" : !smt.bv<8>
+// CHECK-NOT:     dbg.variable
+
+func.func @bmc_debug_anchors_to_names() -> i1 {
+  %bmc = verif.bmc bound 2 num_regs 1 initial_values [unit]
+  init {
+    %c0_i1 = hw.constant 0 : i1
+    %clk = seq.to_clock %c0_i1
+    verif.yield %clk : !seq.clock
+  }
+  loop {
+  ^bb0(%clk: !seq.clock):
+    %fromClock = seq.from_clock %clk
+    %c-1_i1 = hw.constant -1 : i1
+    %nclk = comb.xor %fromClock, %c-1_i1 : i1
+    %toClock = seq.to_clock %nclk
+    verif.yield %toClock : !seq.clock
+  }
+  circuit {
+  ^bb0(%clk: !seq.clock, %data: i8, %state: i8):
+    dbg.variable "port_data", %data : i8
+    dbg.variable "state_data", %state : i8
+    %true = hw.constant true
+    verif.assert %true : i1
+    verif.yield %data, %state : i8, i8
+  }
+  return %bmc : i1
+}

test/Tools/circt-bmc/externalize-registers.mlir

@@ -39,6 +39,10 @@ hw.module @two_reg(in %clk: !seq.clock, in %in0: i32, in %in1: i32, out out: i32
 }
 
 // CHECK:  hw.module @named_regs(in [[CLK:%.+]] : !seq.clock, in [[IN0:%.+]] : i32, in [[IN1:%.+]] : i32, in %firstreg_state : i32, in %secondreg_state : i32, out {{.+}} : i32, out {{.+}} : i32, out {{.+}} : i32) attributes {initial_values = [unit, unit], num_regs = 2 : i32} {
+// CHECK:    dbg.variable "in0", [[IN0]] : i32
+// CHECK:    dbg.variable "in1", [[IN1]] : i32
+// CHECK:    dbg.variable "firstreg", %firstreg_state : i32
+// CHECK:    dbg.variable "secondreg", %secondreg_state : i32
 // CHECK:    [[ADD:%.+]] = comb.add [[IN0]], [[IN1]]
 // CHECK:    hw.output %secondreg_state, [[ADD]], %firstreg_state
 // CHECK:  }

tools/circt-bmc/CMakeLists.txt

@@ -15,6 +15,7 @@ target_link_libraries(circt-bmc
   CIRCTBMCTransforms
   CIRCTComb
   CIRCTCombToSMT
+  CIRCTDebug
   CIRCTEmitTransforms
   CIRCTHW
   CIRCTHWToSMT

tools/circt-bmc/circt-bmc.cpp

@@ -16,6 +16,7 @@
 #include "circt/Conversion/SMTToZ3LLVM.h"
 #include "circt/Conversion/VerifToSMT.h"
 #include "circt/Dialect/Comb/CombDialect.h"
+#include "circt/Dialect/Debug/DebugDialect.h"
 #include "circt/Dialect/Emit/EmitDialect.h"
 #include "circt/Dialect/Emit/EmitPasses.h"
 #include "circt/Dialect/HW/HWDialect.h"
@@ -360,6 +361,7 @@ int main(int argc, char **argv) {
   // clang-format off
   registry.insert<
     circt::comb::CombDialect,
+    circt::debug::DebugDialect,
     circt::emit::EmitDialect,
     circt::hw::HWDialect,
     circt::om::OMDialect,