[Verif] Lowering from verif.formal to verif.bmc

[dobios]

The current formal test interface can be picked up by the btor2 back-end, but not the circt-bmc backend. It would be nice to look into whether or not this conversion is possible and if not, what information is missing in verif.formal to enable it?

That way, both back-ends could benefit from the modularity offered by the hardware contracts.

[dobios]

Maybe @TaoBi22 could look into this if time permits?

[TaoBi22]

I'll take a look into this at some point, no promises on timescale though!