From 4fb8df56846b448ff458dbfabd16dafc588fcec6 Mon Sep 17 00:00:00 2001 From: 5iri Date: Wed, 1 Jul 2026 18:20:54 +0530 Subject: [PATCH] Add dbg.trace for BMC counterexample value tracking --- include/circt/Dialect/Debug/DebugOps.td | 17 +++++++++++++++++ lib/Conversion/SMTToZ3LLVM/LowerSMTToZ3LLVM.cpp | 16 +++++++++++++++- lib/Conversion/VerifToSMT/VerifToSMT.cpp | 17 +++++++++++++++++ test/Conversion/SMTToZ3LLVM/smt-to-z3-llvm.mlir | 3 +++ test/Conversion/VerifToSMT/bmc-debug-names.mlir | 4 +++- test/Dialect/Debug/basic.mlir | 3 ++- 6 files changed, 57 insertions(+), 3 deletions(-) diff --git a/include/circt/Dialect/Debug/DebugOps.td b/include/circt/Dialect/Debug/DebugOps.td index b8845bf8ef5d..d8f211af06cb 100644 --- a/include/circt/Dialect/Debug/DebugOps.td +++ b/include/circt/Dialect/Debug/DebugOps.td @@ -82,6 +82,23 @@ def VariableOp : DebugOp<"variable"> { }]; } +def TraceOp : DebugOp<"trace"> { + let summary = "Record a named runtime value for counterexample tracing"; + let description = [{ + Records a named value at a specific step for later counterexample + materialization. This is intended as an internal bridge from the BMC flow + to the final runtime-backed text/VCD emission path. + }]; + let arguments = (ins + I32:$step, + StrAttr:$name, + AnyType:$value + ); + let assemblyFormat = [{ + $step `,` $name `,` $value attr-dict `:` type($step) `,` type($value) + }]; +} + def ValueOp : DebugOp<"value"> { let summary = "Attach source-language metadata to a value"; diff --git a/lib/Conversion/SMTToZ3LLVM/LowerSMTToZ3LLVM.cpp b/lib/Conversion/SMTToZ3LLVM/LowerSMTToZ3LLVM.cpp index 4f8e1b9c223a..39c1d3d3c006 100644 --- a/lib/Conversion/SMTToZ3LLVM/LowerSMTToZ3LLVM.cpp +++ b/lib/Conversion/SMTToZ3LLVM/LowerSMTToZ3LLVM.cpp @@ -1282,6 +1282,18 @@ struct IntAbsOpLowering : public SMTLoweringPattern { // For now we want to ignore Debug variable and scope ops - eventually we'll // give this debug info to Z3 +/// Strip dbg.trace ops. +struct DbgTraceLowering : public OpConversionPattern { + using OpConversionPattern::OpConversionPattern; + + LogicalResult + matchAndRewrite(debug::TraceOp op, OpAdaptor adaptor, + ConversionPatternRewriter &rewriter) const final { + rewriter.eraseOp(op); + return success(); + } +}; + /// Strip dbg.variable ops. struct DbgVariableLowering : public OpConversionPattern { using OpConversionPattern::OpConversionPattern; @@ -1546,7 +1558,9 @@ void circt::populateSMTToZ3LLVMConversionPatterns( BV2IntOpLowering, QuantifierLowering, QuantifierLowering>(converter, patterns.getContext(), globals, options); - patterns.add(patterns.getContext()); + patterns.add(patterns.getContext()); + patterns.add(patterns.getContext()); + patterns.add(patterns.getContext()); } void LowerSMTToZ3LLVMPass::runOnOperation() { diff --git a/lib/Conversion/VerifToSMT/VerifToSMT.cpp b/lib/Conversion/VerifToSMT/VerifToSMT.cpp index a557ab0f0ca6..8e89a94b52b9 100644 --- a/lib/Conversion/VerifToSMT/VerifToSMT.cpp +++ b/lib/Conversion/VerifToSMT/VerifToSMT.cpp @@ -70,6 +70,20 @@ static void attachDebugVariables( } } +static void attachTraceRecords( + OpBuilder &builder, Location loc, Value step, ArrayRef originalTypes, + ValueRange values, + const llvm::SmallDenseMap &debugNames) { + for (auto [argIndex, value] : llvm::enumerate(values)) { + if (isa(originalTypes[argIndex])) + continue; + auto it = debugNames.find(argIndex); + if (it == debugNames.end()) + continue; + debug::TraceOp::create(builder, loc, step, it->second, value); + } +} + /// Lower a verif::AssertOp operation with an i1 operand to a smt::AssertOp, /// negated to check for unsatisfiability. struct VerifAssertOpConversion : OpConversionPattern { @@ -559,6 +573,9 @@ struct VerifBoundedModelCheckingOpConversion attachDebugVariables( builder, loc, oldCircuitInputTy, iterArgs.take_front(circuitFuncOp.getNumArguments()), debugNames); + attachTraceRecords( + builder, loc, i, oldCircuitInputTy, + iterArgs.take_front(circuitFuncOp.getNumArguments()), debugNames); // Drop existing assertions smt::PopOp::create(builder, loc, 1); diff --git a/test/Conversion/SMTToZ3LLVM/smt-to-z3-llvm.mlir b/test/Conversion/SMTToZ3LLVM/smt-to-z3-llvm.mlir index da7098ecb4f9..948e610869a0 100644 --- a/test/Conversion/SMTToZ3LLVM/smt-to-z3-llvm.mlir +++ b/test/Conversion/SMTToZ3LLVM/smt-to-z3-llvm.mlir @@ -391,6 +391,9 @@ func.func @test(%arg0: i32) { // CHECK: llvm.call @Z3_mk_bv2int({{%[0-9a-zA-Z_]+}}, [[BV0]], [[SIGNEDCONST]]) : (!llvm.ptr, !llvm.ptr, i1) -> !llvm.ptr smt.bv2int %c0_bv4 signed : !smt.bv<4> + // CHECK-NOT: dbg.trace + dbg.trace %arg1, "var0", %c0_bv4 : i32, !smt.bv<4> + // CHECK-NOT: dbg.variable dbg.variable "var1", %c0_bv4 : !smt.bv<4> diff --git a/test/Conversion/VerifToSMT/bmc-debug-names.mlir b/test/Conversion/VerifToSMT/bmc-debug-names.mlir index 871d77cce07f..b2a4cd10ae5b 100644 --- a/test/Conversion/VerifToSMT/bmc-debug-names.mlir +++ b/test/Conversion/VerifToSMT/bmc-debug-names.mlir @@ -5,9 +5,11 @@ // CHECK: [[REG_DECL:%.+]] = smt.declare_fun "state_q" : !smt.bv<8> // CHECK: dbg.variable "data_in", [[INPUT_DECL]] : !smt.bv<8> // CHECK: dbg.variable "state_q", [[REG_DECL]] : !smt.bv<8> -// CHECK: scf.for {{%.+}} iter_args([[CLK_ARG:%.+]] = {{%.+}}, [[INPUT_ARG:%.+]] = [[INPUT_DECL]], [[REG_ARG:%.+]] = [[REG_DECL]], {{%.+}}) +// CHECK: scf.for [[STEP:%.+]] = {{%.+}} iter_args([[CLK_ARG:%.+]] = {{%.+}}, [[INPUT_ARG:%.+]] = [[INPUT_DECL]], [[REG_ARG:%.+]] = [[REG_DECL]], {{%.+}}) // CHECK: dbg.variable "data_in", [[INPUT_ARG]] : !smt.bv<8> // CHECK: dbg.variable "state_q", [[REG_ARG]] : !smt.bv<8> +// CHECK: dbg.trace [[STEP]], "data_in", [[INPUT_ARG]] : i32, !smt.bv<8> +// CHECK: dbg.trace [[STEP]], "state_q", [[REG_ARG]] : i32, !smt.bv<8> // CHECK: [[CIRCUIT_RESULT:%.+]] = func.call @bmc_circuit{{(_[0-9]+)?}}([[CLK_ARG]], [[INPUT_ARG]], [[REG_ARG]]) : (!smt.bv<1>, !smt.bv<8>, !smt.bv<8>) -> !smt.bv<8> // CHECK-NOT: smt.declare_fun "input_1" // CHECK-NOT: smt.declare_fun "reg_0" diff --git a/test/Dialect/Debug/basic.mlir b/test/Dialect/Debug/basic.mlir index 251ff6b8255b..f03c290d1cf8 100644 --- a/test/Dialect/Debug/basic.mlir +++ b/test/Dialect/Debug/basic.mlir @@ -5,9 +5,11 @@ func.func @Foo(%arg0: i32, %arg1: index, %arg2: f64) { // CHECK-NEXT: dbg.variable "foo", %arg0 : i32 // CHECK-NEXT: dbg.variable "bar", %arg1 : index // CHECK-NEXT: dbg.variable "baz", %arg2 : f64 + // CHECK-NEXT: dbg.trace %arg0, "tracefoo", %arg2 : i32, f64 dbg.variable "foo", %arg0 : i32 dbg.variable "bar", %arg1 : index dbg.variable "baz", %arg2 : f64 + dbg.trace %arg0, "tracefoo", %arg2 : i32, f64 // CHECK-NEXT: [[TMP:%.+]] = dbg.struct {"foo": %arg0, "bar": %arg1, "baz": %arg2} : i32, index, f64 // CHECK-NEXT: dbg.variable "megafoo", [[TMP]] : !dbg.struct @@ -28,4 +30,3 @@ func.func @Foo(%arg0: i32, %arg1: index, %arg2: f64) { return } -