[FIRRTL] FIRRTL needs a contract interface

[dobios]

I introduced an interface for hardware contracts to the verif dialect. This should be exposed to FIRRTL so that we can access it via Chisel. Here is an idea of what is needed:

• Modules need to be able to contain a contract region that contains the module's pre-post-conditions (as well as future invariants that might be introduces). This can also contain arbitrary hardware and reason about the module's interface. This should map to verif.contract.
• We need a way to define preconditions, probably through something like require, that maps to verif.require.
• We need a way to define postconditions, with something like ensure, that maps to verif.ensure. These should be allowed to reason about the module's outputs.

Here's an example of how I think this can be used:

public module Foo:
	input in : UInt<32>
	output out : UInt<32>

	contract:
		node prec0 = gt(in, 0)
		require prec0
		node prec1 = lt(in, 1000)
		require prec1
		node post = ;;some post-condition;;
		ensure post
		
	;; Body of the module

[dobios]

Maybe @uenoku or @fabianschuiki would have some left-over bandwidth to look into this?

[fabianschuiki]

Hey @dobios, I'm definitely going to poke at this in the near future! This is a fantastic building block to make formal verification more modular and composable.