[circt-bmc] Add verif.contract support

[robert-at-pretension-io]

circt-bmc currently handles verif.formal ops (added in #9145) but not verif.contract ops. Running circt-bmc on a module containing a verif.contract fails at ConvertHWToSMT because the apply-mode hw.module produced by LowerContracts is still present when the HW dialect is marked illegal.

This patch adds contract support with two small changes:

1. circt-bmc.cpp: Add LowerContractsPass to the pipeline before LowerTests. LowerContracts splits each contract into a verif.formal check block and an apply-mode hw.module; the existing LowerTests then converts the verif.formal into an hw.module that BMC can target.
2. LowerToBMC.cpp: After absorbing the target hw.module into a verif.bmc op, erase any remaining hw.module/hw.module.extern ops. Without this, the leftover apply-mode modules cause ConvertHWToSMT to fail.

Usage: circt-bmc input.mlir --module _CheckContract_0 -b --run

The check module name is generated by LowerContracts (pattern: CheckContract).

[dobios]

This is cool! Thanks for adding support for this!

One thing I want to note is that the goal of contracts is to decouple modules from each other during verification as to enable

1. The simplification of individual BMC tasks;
2. Solving each individual task in parallel.

So correctly adding support for this would probably also require supporting running verification for each module/formal in parallel such that: if all are unsat -> success; the moment one is sat -> fail and produce witness. This should hopefully allow for much more scalability in the cases where individual modules are instantiated a bunch of times. You might also want to somehow share learned clauses across solver instances if you're taking this route, but that would be another optimization.