[Verif] LowerContractsPass

[leonardt]

• Adds pass to convert hw modules containing contracts into verif.formal tests with contracts inlined
  • ensure -> assert, require -> assume
• Adds tests for multiplier, carry save compressor, and shift left

[maerhart]

Since you are only matching on modules, you can also just have a for loop iterating over the modules, which would be a bit more efficient.

[maerhart]

This file contains tests that are great as integration tests, but for regression tests we want to check the corner cases and keep the tests small (they don't have to do something that makes sense from a design implementation/logics perspective). For example, there's no test of a module with more than one contract inside, with zero contracts inside. Deleting the module also only works because you have no other module instantiating it.

[fabianschuiki]

Really cool! 🥳

Instead of converting modules to verif.formal ops directly, it would be great to create a separate verif.formal op for each verif.contract op in the design. You could for example do a mlirModule.walk([&](ContractOp op){ ... }) to find all contract ops in the design. Each could then go into its own verif.formal op. You could do a depth-first traversal starting at the contract and traversing its operands until you hit primary module inputs, and clone all ops that you encounter into the verif.formal op. There's a handy IRMapper that you can pass to Operation::clone that will automatically update operands for you 🙂.

If a contract has another contract somewhere in its fan-in cone of operands, we should be able to just assume that that other contract holds by directly inlining it. Maybe there's an interleaving of steps that would do all of this, something like:

1. Collect all verif.contract ops into a worklist.
2. Replace uses of contract results with the contract body.
3. Outline all of the contracts into dedicated verif.formal ops, cloning all ops in their fan-in cone into the formal op.

I think that would get you the inlining of contracts everywhere, except for the one formal test that checks a contract, where we would check the actual design in the module against the contract body.