[Verif] Add RefinementCheckingOp

[fzi-hielscher]

This PR adds the RefinementCheckingOp to the verif dialect. The motivation behind this operation is to be able to automatically check whether a 'target' circuit is a refinement of a 'source' circuit. This should be a small step towards performing translation validation comparable to Alive2. The operation is structurally identical to the LogicEquivalenceCheckingOp, so I factored out most of the ODS into a common CircuitRelationCheckOp. If there is no non-determinism present in the circuits, the operation is also functionally identical to LogicEquivalenceCheckingOp.

Finding a good definition of the refines relation is hard, so please just consider this as a humble first attempt. In essence, there are (at least) three factors to consider:

• Does it permit all optimizations we want to be able to do?
• Does it reject all "optimizations" we want to be illegal?
• Is it viable to perform model checking with the tools available to us?

Our current definition of logical equivalence is too restrictive for translation validation. In the presence of non-determinism it is not guaranteed that A == A, see #7025 . Stating that a circuit cannot be translated to itself is problematic.
In contrast, the RefinementCheckingOp as described here compares the sets of possible outputs for a given input. This is
potentially too permissive, as it allows a different non-deterministic value to be picked for each possible input assignment.

Note that the current specification of the undefined value in comb puts the non-determinism in the domain of functions, getting us dangerously close to second-order logic. While I think it is a good model for the likely behavior of real hardware, it is probably impractical for SMT modeling.

[uenoku]

Thank you for working on this! I think this is great extension. I have actually encountered this problem in translation validation of synthesis lowering. I end up adding verif.assume to prevent out-of-bounds access:

circt/integration_test/circt-synth/array-lec.mlir

Lines 13 to 17 in 5ee54ac

	// NOTE: If the index is out of bounds, the result value is undefined.
	// In LEC such value is lowered into unbounded SMT variable and cause
	// the LEC to fail. So just asssume that the index is in bounds.
	%inbound = comb.icmp ult %sel2, %c3_i2 : i2
	verif.assume %inbound : i1

[TaoBi22]

This looks very exciting, thanks for adding it!