From e391299f6927ee4b5406e771784817218b062f48 Mon Sep 17 00:00:00 2001 From: AnmolM-777 Date: Fri, 27 Mar 2026 02:27:57 +0530 Subject: [PATCH] [circt-bmc] Include bound in violation and success messages Previously, circt-bmc printed generic messages with no context about at which bound a violation was found. This patch includes the bound count in both the success and failure messages, making the output more informative for users debugging hardware designs. --- lib/Tools/circt-bmc/LowerToBMC.cpp | 12 +++++++----- test/Tools/circt-bmc/lower-to-bmc.mlir | 12 ++++++------ 2 files changed, 13 insertions(+), 11 deletions(-) diff --git a/lib/Tools/circt-bmc/LowerToBMC.cpp b/lib/Tools/circt-bmc/LowerToBMC.cpp index c4379076c9a1..21919bc23d68 100644 --- a/lib/Tools/circt-bmc/LowerToBMC.cpp +++ b/lib/Tools/circt-bmc/LowerToBMC.cpp @@ -209,11 +209,13 @@ void LowerToBMCPass::runOnOperation() { LLVM::AddressOfOp::create(builder, loc, global)->getResult(0)); }; - auto successStrAddr = - createUniqueStringGlobal("Bound reached with no violations!\n"); - auto failureStrAddr = - createUniqueStringGlobal("Assertion can be violated!\n"); - +auto successStrAddr = createUniqueStringGlobal( + "Bound reached with no violations within " + std::to_string(bound) + + " clock cycle(s).\n"); + auto failureStrAddr = createUniqueStringGlobal( + "Assertion can be violated within " + std::to_string(bound) + + " clock cycle(s)!\n"); + if (failed(successStrAddr) || failed(failureStrAddr)) { moduleOp->emitOpError("could not create result message strings"); return signalPassFailure(); diff --git a/test/Tools/circt-bmc/lower-to-bmc.mlir b/test/Tools/circt-bmc/lower-to-bmc.mlir index a17ed950e29c..c49bd286c3e4 100644 --- a/test/Tools/circt-bmc/lower-to-bmc.mlir +++ b/test/Tools/circt-bmc/lower-to-bmc.mlir @@ -17,8 +17,8 @@ // CHECK: llvm.call @printf([[SEL]]) // CHECK: return // CHECK: } -// CHECK: llvm.mlir.global private constant [[SSTR]]("Bound reached with no violations!\0A\00") {addr_space = 0 : i32} -// CHECK: llvm.mlir.global private constant [[FSTR]]("Assertion can be violated!\0A\00") {addr_space = 0 : i32} +// CHECK: llvm.mlir.global private constant [[SSTR]]("Bound reached with no violations within 10 clock cycle(s).\0A\00") {addr_space = 0 : i32} +// CHECK: llvm.mlir.global private constant [[FSTR]]("Assertion can be violated within 10 clock cycle(s)!\0A\00") {addr_space = 0 : i32} // RUN: circt-opt --lower-to-bmc="top-module=comb bound=10 ignore-asserts-until=3" %s | FileCheck %s --check-prefix=CHECKIGNOREUNTIL // CHECKIGNOREUNTIL: {{%.+}} = verif.bmc bound 20 num_regs 0 initial_values [] attributes {ignore_asserts_until = 6 : i32} init { @@ -58,8 +58,8 @@ hw.module @comb(in %in0: i32, in %in1: i32, out out: i32) attributes {num_regs = // CHECK1: llvm.call @printf([[SEL]]) // CHECK1: return // CHECK1: } -// CHECK1: llvm.mlir.global private constant [[SSTR]]("Bound reached with no violations!\0A\00") {addr_space = 0 : i32} -// CHECK1: llvm.mlir.global private constant [[FSTR]]("Assertion can be violated!\0A\00") {addr_space = 0 : i32} +// CHECK1: llvm.mlir.global private constant [[SSTR]]("Bound reached with no violations within 10 clock cycle(s).\0A\00") {addr_space = 0 : i32} +// CHECK1: llvm.mlir.global private constant [[FSTR]]("Assertion can be violated within 10 clock cycle(s)!\0A\00") {addr_space = 0 : i32} // RUN: circt-opt --lower-to-bmc="top-module=seq bound=10 rising-clocks-only=true" %s | FileCheck %s --check-prefix=CHECKRISING // CHECKRISING: [[BMC:%.+]] = verif.bmc bound 10 num_regs 1 initial_values [unit] init { @@ -105,8 +105,8 @@ hw.module @seq(in %clk : !seq.clock, in %in0 : i32, in %in1 : i32, in %reg_state // CHECK2: llvm.call @printf([[SEL]]) // CHECK2: return // CHECK2: } -// CHECK2: llvm.mlir.global private constant [[SSTR]]("Bound reached with no violations!\0A\00") {addr_space = 0 : i32} -// CHECK2: llvm.mlir.global private constant [[FSTR]]("Assertion can be violated!\0A\00") {addr_space = 0 : i32} +// CHECK2: llvm.mlir.global private constant [[SSTR]]("Bound reached with no violations within 10 clock cycle(s).\0A\00") {addr_space = 0 : i32} +// CHECK2: llvm.mlir.global private constant [[FSTR]]("Assertion can be violated within 10 clock cycle(s)!\0A\00") {addr_space = 0 : i32} hw.module @nondominance(in %clk : !seq.clock, in %in0 : i32, in %in1 : i32, in %reg_state : i32, out out : i32, out reg_input : i32) attributes {num_regs = 1 : i32, initial_values = [unit]} { %0 = comb.icmp eq %1, %in0 : i32 %1 = comb.add %in0, %in1 : i32