[Verif] Introduce a clocked assertion verif.clocked_assert

[dobios]

The current structure of the verif dialect requires the use of ltl.clock to associate a clock to an assertion (which is required). This means that a use-def analysis is required everytime we want to work with verif.assert, which leads to the sv.assert operation being used in most lowerings to Core dialects.

As suggested by @fabianschuiki , I propose that we add a verif.clocked_assert(clock, prop) that would be the canonicalization of verif.assert(ltl.clock(clock, prop)). This would make it easier to use move away from sv dialect ops in the core representations.

[fabianschuiki]

You'd probably want to flip the canonicalization around: canonicalize verif.assert(ltl.clock(clock, prop)) to verif.clocked_assert(clock, prop), in order to allow passes to only work with verif.clocked_assert.

[maerhart]

I assume the verif.clocked_assert will also verify that no (other) ltl.clock operation is present in the use-def chain of the prop operand?

[fabianschuiki]

That's an excellent point. I like the idea of having clocked_assert enforce that the operand itself contains no clocking or enable/disable information. The regular assert could then have a canonicalizer which pulls single unambiguous clocking and enable/disable signals up into a clocked_assert where possible.