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.