llvm/circt

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

dobios opened this issue · 2 comments

dobios commented

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 commented

Maybe @TaoBi22 could look into this if time permits?

TaoBi22 commented

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

  • 🎉1
  • 🚀1