Plumb dbg.variable anchors into SMT symbol names

[5iri]

This PR improves BMC traceability by propagating dbg.variable anchors into VerifToSMT symbol names.

• Emit dbg.variable anchors in externalize-registers for non-clock module inputs.
• Add/extend regression tests for both anchor emission and name propagation.

For example,

func.func @bmc_debug_anchors_to_names() -> i1 {
  %bmc = verif.bmc bound 2 num_regs 1 initial_values [unit]                                                 init {
    %c0_i1 = hw.constant 0 : i1
    %clk = seq.to_clock %c0_i1
    verif.yield %clk : !seq.clock                                                                           }
  loop {
  ^bb0(%clk: !seq.clock):
    %fromClock = seq.from_clock %clk                                                                          %c-1_i1 = hw.constant -1 : i1
    %nclk = comb.xor %fromClock, %c-1_i1 : i1
    %toClock = seq.to_clock %nclk
    verif.yield %toClock : !seq.clock                                                                       }
  circuit {
  ^bb0(%clk: !seq.clock, %data: i8, %state: i8):
    dbg.variable "port_data", %data : i8                                                                      dbg.variable "state_data", %state : i8
    %true = hw.constant true
    verif.assert %true : i1
    verif.yield %data, %state : i8, i8
  }
  return %bmc : i1
}

can produce

module {
  func.func @bmc_debug_anchors_to_names() -> i1 {
    %0 = smt.solver() : () -> i1 {
      %1 = func.call @bmc_init() : () -> !smt.bv<1>
      smt.push 1
      %port_data = smt.declare_fun "port_data" : !smt.bv<8>
      %state_data = smt.declare_fun "state_data" : !smt.bv<8>
      %c0_i32 = arith.constant 0 : i32
      %c1_i32 = arith.constant 1 : i32
      %c2_i32 = arith.constant 2 : i32
      %false = arith.constant false
      %true = arith.constant true
      %2:4 = scf.for %arg0 = %c0_i32 to %c2_i32 step %c1_i32 iter_args(%arg1 = %1, %arg2 = %port_data, %arg3 = %state_data, %arg4 = %false) -> (!smt.bv<1>, !smt.bv<8>, !smt.bv<8>, i1)  : i32 {
        smt.pop 1
        smt.push 1
        %4:2 = func.call @bmc_circuit(%arg1, %arg2, %arg3) : (!smt.bv<1>, !smt.bv<8>, !smt.bv<8>) -> (!smt.bv<8>, !smt.bv<8>)
        %5 = smt.check sat {
          smt.yield %true : i1
        } unknown {
          smt.yield %true : i1
        } unsat {
          smt.yield %false : i1
        } -> i1
        %6 = arith.ori %5, %arg4 : i1
        %7 = func.call @bmc_loop(%arg1) : (!smt.bv<1>) -> !smt.bv<1>
        %port_data_0 = smt.declare_fun "port_data" : !smt.bv<8>
        %8 = smt.bv.not %arg1 : !smt.bv<1>
        %9 = smt.bv.and %8, %7 : !smt.bv<1>
        %c-1_bv1 = smt.bv.constant #smt.bv<-1> : !smt.bv<1>
        %10 = smt.eq %9, %c-1_bv1 : !smt.bv<1>
        %11 = smt.ite %10, %4#1, %arg3 : !smt.bv<8>
        scf.yield %7, %port_data_0, %11, %6 : !smt.bv<1>, !smt.bv<8>, !smt.bv<8>, i1
      }
      %3 = arith.xori %2#3, %true : i1
      smt.yield %3 : i1
    }
    return %0 : i1
  }
  func.func @bmc_init() -> !smt.bv<1> {
    %false = hw.constant false
    %0 = seq.to_clock %false
    %1 = builtin.unrealized_conversion_cast %0 : !seq.clock to !smt.bv<1>
    return %1 : !smt.bv<1>
  }                                                                                                         func.func @bmc_loop(%arg0: !smt.bv<1>) -> !smt.bv<1> {
    %0 = builtin.unrealized_conversion_cast %arg0 : !smt.bv<1> to !seq.clock
    %1 = seq.from_clock %0
    %true = hw.constant true
    %2 = comb.xor %1, %true : i1
    %3 = seq.to_clock %2                                                                                      %4 = builtin.unrealized_conversion_cast %3 : !seq.clock to !smt.bv<1>
    return %4 : !smt.bv<1>
  }
  func.func @bmc_circuit(%arg0: !smt.bv<1>, %arg1: !smt.bv<8>, %arg2: !smt.bv<8>) -> (!smt.bv<8>, !smt.bv<8>) {
    %true = hw.constant true                                                                                  %0 = builtin.unrealized_conversion_cast %true : i1 to !smt.bv<1>
    %c-1_bv1 = smt.bv.constant #smt.bv<-1> : !smt.bv<1>
    %1 = smt.eq %0, %c-1_bv1 : !smt.bv<1>
    %2 = smt.not %1
    smt.assert %2
    return %arg1, %arg2 : !smt.bv<8>, !smt.bv<8>                                                            }
}

Key part of the output:

%port_data = smt.declare_fun "port_data" : !smt.bv<8>

%state_data = smt.declare_fun "state_data" : !smt.bv<8>

So the debug anchors are being consumed correctly, and SMT symbols use meaningful names (port_data,state_data) instead of only input_N/reg_N.

[5iri]

@TaoBi22 would love your thoughts on this implementation!

[TaoBi22]

Thanks for looking into this @5iri! A couple of preliminary comments below - I think the main question is whether it makes sense to do this in ExternalizeRegisters or in a separate pass (more discussion of that in the comment directly)

[TaoBi22]

It would be nice to check a bit more of the IR here to make sure that the right names are being given to the right functions

[TaoBi22]

What's the reasoning behind doing this in ExternalizeRegisters? It seems quite distinct from the existing function of the pass, it might be sensible to put this in a separate pass (which it would be nice to split into a different PR from the VerifToSMT changes)

[5iri]

Yes! I think yes it is sensible to put this in a seperate pass, like materialize-debug-anchors. I was more focused on getting to produce the correct dbg.variable anchors without extra plumbing.

That said, I am happy to split this into a dedicated pass and then a follow up PR where VerifToSMT consumes those anchors.

I can rework this so ExternalizeRegisters stays focused and the pipeline composes the two passes explicitly.

[TaoBi22]

nit: if you use llvm::make_early_inc_range you should be able to do this in the loop directly