[circt-bmc] Add support for verif.symbolic_value

[fabianschuiki]

The circt-bmc pipeline currently doesn't support symbolic values. This feels like it might actually not be too hard to do, since we already support primary inputs. Would this be something that the externalize register pass would have to handle, such that the symbolic values become top-level inputs?

cc @TaoBi22 @maerhart

[maerhart]

Ideally, we'd have a lowering pass from verif.formal to verif.bmc which also deals with the symbolic inputs (which should be relatively easy to implement, the only thing to take care of is probably proper handling the clock signals).

But we already have the FormalToHW lowering pass which creates a module with root inputs from the symbolic values, so running that in the pipeline and then the circt-bmc pipeline by giving it the module name should already work.

[fabianschuiki]

That's an excellent idea! I forgot about FormalToHW 👍