Skip to content

[circt-bmc] Include bound in violation and success messages #10056

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
AnmolM-777 wants to merge 1 commit into
base: main
Choose a base branch
from
+13 −11
Open

[circt-bmc] Include bound in violation and success messages #10056

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 7 additions & 5 deletions lib/Tools/circt-bmc/LowerToBMC.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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();
Expand Down
12 changes: 6 additions & 6 deletions test/Tools/circt-bmc/lower-to-bmc.mlir
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand Down Expand Up @@ -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 {
Expand Down Expand Up @@ -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
Expand Down
Loading