[circt-bmc] Preserve signal names before lowering

[ankit-cybertron]

This patch adds dbg.scope and dbg.variable ops in LowerToBMC to preserve hardware signal names before
hwModule->erase() discards them.

This is needed to support counter-example generation -- without preserving names here, there is no way to produce human-readable waveform output when the solver finds a violation.

[TaoBi22]

Thanks for looking at this! Could we add a test or two in test/Tools/circt-bmc/ to make sure this is working properly?

[ankit-cybertron]

Thanks for looking at this! Could we add a test or two in test/Tools/circt-bmc/ to make sure this is working properly?

Thanks for the review! Added 2 tests in test/Tools/circt-bmc/lower-to-bmc-debug.mlir -- one for a simple passthrough module and one for a module with a computed output -- to verify that dbg.scope and dbg.variable ops are correctly emitted for all ports. But I'm not sure if these tests cover everything we have here

[TaoBi22]

Thanks! This is looking good modulo some comments below.

While I think landing this makes sense for now as a first step, I wonder if the best way to handle module hierarchy would actually be to add another pass to the circt-bmc pipeline that adds the dbg.variable ops to every module. Then these changes in LowerToBMC could just be to make sure those ops get carried across (not even sure that wouldn't just happen automatically). Not a blocker on this, just a thought!

[ankit-cybertron]

Thanks! This is looking good modulo some comments below.

While I think landing this makes sense for now as a first step, I wonder if the best way to handle module hierarchy would actually be to add another pass to the circt-bmc pipeline that adds the dbg.variable ops to every module. Then these changes in LowerToBMC could just be to make sure those ops get carried across (not even sure that wouldn't just happen automatically). Not a blocker on this, just a thought!

That sounds like a really interesting direction -- I can definitely try exploring that as well. Not sure if something like this will work for circt-bmc at this stage, but happy to look into it

[TaoBi22]

Thanks! LGTM modulo a couple of nits - let me know if you need me to hit merge once these are addressed.

[TaoBi22]

Ah looks like the CI is failing on this - we probably need some kind of placeholder to discard dbg ops for now further down the pipeline.

[ankit-cybertron]

Ah looks like the CI is failing on this - we probably need some kind of placeholder to discard dbg ops for now further down the pipeline.

Added mlir::createStripDebugInfoPass() after createLowerToBMC in circt-bmc.cpp to discard debug ops before SMT lowering, and registered DebugDialect in the tool's dialect registry. That should fix the CI failure!

[ankit-cybertron]

Thanks! LGTM modulo a couple of nits - let me know if you need me to hit merge once these are addressed.

Thanks! All nits and comments addressed. Yes, please, if we could merge once CI goes green

[TaoBi22]

@ankit-cybertron the CI is still failing here (debug is a CIRCT dialect, so MLIR upstream infra won't strip it, that pass just strips location tracking information) - I'd recommend running ninja check-circt-integration to check this locally so you don't have to wait for me to approve your CI runs.

I've opened #10102 to discard the debug ops - once that's landed I think this PR should be green. If you could remove those last changes (from the commit where you add the StripDebugInfo pass), then I'll rerun the CI after #10102 lands and merge if green.

[ankit-cybertron]

Ahh😅 thanks for pointing that out and sorry for the confusion. I assumed that approach would work
I’ll revert those changes and wait for #10102 to land.

[TaoBi22]

Thanks @ankit-cybertron! If you could just rebase this on main then we should have green CI

[ankit-cybertron]

CI is still failing with a runner communication error, I successfully ran ninja check-circt-integration locally , not sure what's causing this.

[TaoBi22]

CI is still failing with a runner communication error, I successfully ran ninja check-circt-integration locally , not sure what's causing this.

I relaunched it and it ran through fine, so I'll hit merge. Thanks for the contribution! 🎉

[ankit-cybertron]

Thanks for helping through the PR, really appreciate your guidance on the code and structure. Happy to contribute! I’ll also look into your idea of adding another pass to add dbg.variable ops across module