From 957d19b60d7f60bf2eee99436c78524b13e8e743 Mon Sep 17 00:00:00 2001 From: 5iri Date: Thu, 16 Apr 2026 17:07:07 +0530 Subject: [PATCH 1/2] Plumb dbg.variable anchors into SMT symbol names --- include/circt/Tools/circt-bmc/Passes.td | 4 +- lib/Conversion/VerifToSMT/VerifToSMT.cpp | 44 ++++++++++++++----- lib/Tools/circt-bmc/CMakeLists.txt | 1 + lib/Tools/circt-bmc/ExternalizeRegisters.cpp | 44 +++++++++++++++++++ test/Conversion/VerifToSMT/verif-to-smt.mlir | 34 ++++++++++++++ .../circt-bmc/externalize-registers.mlir | 4 ++ tools/circt-bmc/CMakeLists.txt | 1 + tools/circt-bmc/circt-bmc.cpp | 2 + 8 files changed, 122 insertions(+), 12 deletions(-) diff --git a/include/circt/Tools/circt-bmc/Passes.td b/include/circt/Tools/circt-bmc/Passes.td index 9f2878beb3d1..6e1e684bc520 100644 --- a/include/circt/Tools/circt-bmc/Passes.td +++ b/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 - diff --git a/lib/Conversion/VerifToSMT/VerifToSMT.cpp b/lib/Conversion/VerifToSMT/VerifToSMT.cpp index 0f6f415b7f80..faf1a5a9587c 100644 --- a/lib/Conversion/VerifToSMT/VerifToSMT.cpp +++ b/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 debugArgNames; + SmallVector debugOpsToErase; + for (auto varOp : op.getCircuit().front().getOps()) { + auto arg = dyn_cast(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 oldLoopInputTy(op.getLoop().getArgumentTypes()); SmallVector 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(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)); } } diff --git a/lib/Tools/circt-bmc/CMakeLists.txt b/lib/Tools/circt-bmc/CMakeLists.txt index 8181bb016781..df5e8dcca271 100644 --- a/lib/Tools/circt-bmc/CMakeLists.txt +++ b/lib/Tools/circt-bmc/CMakeLists.txt @@ -6,6 +6,7 @@ add_circt_library(CIRCTBMCTransforms CIRCTBMCTransformsIncGen LINK_LIBS PUBLIC + CIRCTDebug CIRCTHW CIRCTSeq CIRCTComb diff --git a/lib/Tools/circt-bmc/ExternalizeRegisters.cpp b/lib/Tools/circt-bmc/ExternalizeRegisters.cpp index a67f53ae0eda..7deaa3a3661f 100644 --- a/lib/Tools/circt-bmc/ExternalizeRegisters.cpp +++ b/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> addedOutputNames; DenseMap> 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 trackedValues; + for (auto varOp : body->getOps()) + trackedValues.insert(varOp.getValue()); + + DenseSet 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(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{}); } } diff --git a/test/Conversion/VerifToSMT/verif-to-smt.mlir b/test/Conversion/VerifToSMT/verif-to-smt.mlir index 0221e6cb5920..4d6eb3a44e40 100644 --- a/test/Conversion/VerifToSMT/verif-to-smt.mlir +++ b/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 +} diff --git a/test/Tools/circt-bmc/externalize-registers.mlir b/test/Tools/circt-bmc/externalize-registers.mlir index 445edbfed2c6..0eea193be7be 100644 --- a/test/Tools/circt-bmc/externalize-registers.mlir +++ b/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: } diff --git a/tools/circt-bmc/CMakeLists.txt b/tools/circt-bmc/CMakeLists.txt index 2a65075e82c4..6385b4a6094c 100644 --- a/tools/circt-bmc/CMakeLists.txt +++ b/tools/circt-bmc/CMakeLists.txt @@ -15,6 +15,7 @@ target_link_libraries(circt-bmc CIRCTBMCTransforms CIRCTComb CIRCTCombToSMT + CIRCTDebug CIRCTEmitTransforms CIRCTHW CIRCTHWToSMT diff --git a/tools/circt-bmc/circt-bmc.cpp b/tools/circt-bmc/circt-bmc.cpp index 459a8621aa0a..cee6042bd4f3 100644 --- a/tools/circt-bmc/circt-bmc.cpp +++ b/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, From c2b5cea4cced6b1d28a64403c1eb8fec4f59715e Mon Sep 17 00:00:00 2001 From: 5iri Date: Thu, 16 Apr 2026 18:18:34 +0530 Subject: [PATCH 2/2] missed CIRCTDebug in CMakeLists.txt --- lib/Conversion/VerifToSMT/CMakeLists.txt | 1 + 1 file changed, 1 insertion(+) diff --git a/lib/Conversion/VerifToSMT/CMakeLists.txt b/lib/Conversion/VerifToSMT/CMakeLists.txt index 4d923bc70261..abce00f9b758 100644 --- a/lib/Conversion/VerifToSMT/CMakeLists.txt +++ b/lib/Conversion/VerifToSMT/CMakeLists.txt @@ -8,6 +8,7 @@ add_circt_conversion_library(CIRCTVerifToSMT Core LINK_LIBS PUBLIC + CIRCTDebug CIRCTHW CIRCTHWToSMT CIRCTVerif