[circt-bmc] Add dbg.trace for BMC counterexample value tracking

[5iri]

This PR adds a new dbg.trace operation to record named runtime values at a specific step during BMC lowering, because dbg.variable is good for describing named values, but it does not capture the "this value at this time step" information needed for counterexample tracing.

AI Assisted by: codex:gpt-5.4(medium)

[circt-bot]

Results of circt-tests run for 4fb8df5 compared to results for 462fc74:

sv-tests

Changes in emitted diagnostics:

• -14 total change
• -3 error: no member named 'sprint' in 'm_uvm_printer_knobs'
• -3 error: value of type 'T' (aka 'uvm_sequence_base') cannot be assigned to type 'simple_seq'
• -2 error: time scale declaration must come before all other items in scope
• +2 error: unsupported construct in ClassType members: ConstraintBlock
• -1 error: unknown macro or compiler directive '`uvm_sequence_utils'
• -1 error: unknown macro or compiler directive '`uvm_sequencer_utils'
• -1 error: unknown module 'pss'
• -1 error: unknown module 'pss_wrapper'
• -1 error: unknown module 'spi_clgen'
• -1 error: unknown module 'spi_shift'
• -1 error: use of undeclared identifier 'count'
• -1 error: value of type 'T' (aka 'uvm_sequencer#(simple_item,REQ (aka simple_item))') cannot be assigned to type 'simple_sequencer'

[TaoBi22]

I'm not totally sure having this in the debug dialect is the right move when it's very specific to BMC. Maybe the verif dialect would make more sense?

[TaoBi22]

I'm not sure the motivation for this op is entirely clear to me; what's the aim for its eventual lowering?

Would the aim be to lower this op to some call that reaches out to the BMCTrace runtime with a value and a cycle number? If that's the case then I'm not sure it's completely clear to me why we need a dedicated op for this instead of building this IR directly as we build the for loop that it sits in.

[5iri]

The intended lowering is a later counterexample-materialization step that consumes dbg.trace(step, name, value) and lowers it to the BMC runtime trace path. I introduced a dedicated op to keep VerifToSMT backend-neutral instead of constructing runtime-specific IR directly in the loop body. You’re right that this isn’t clear from the current patch.

[TaoBi22]

nit: unrelated change

[5iri]

I think I split this too early. I introduced the IR marker at the pass boundary where the information is available, and added the erase pattern because SMTToZ3LLVM requires all debug ops to be legalized. But without the actual consumer, the motivation is under-explained. I’ll either fold the lowering into this PR or move the op to the follow-up where the consumer lands.