[Verif] Add clocked Assert Assume Cover ops

[dobios]

This PR is in response to #6982 and adds clocked versions of assert, assume, cover.
What still needs to be done:

• Update ExportVerilog
• Add Verifier that checks that we have exactly one disable and clock.
• Add tests

[dobios]

@uenoku @fabianschuiki I moved the verification into a dedicated pass, now the question is: when should this pass be called? Just before emission? At the end of the hw pass pipeline?

[fabianschuiki]

when should this pass be called? Just before emission? At the end of the hw pass pipeline?

I would run this pass at least just before ExportVerilog, or before any pass that wants to rely on the invariant that clocked asserts contain no ltl.clock ops in the property/sequence that they're checking.

[uenoku]

Thank you for iterating on this! Separating verification into a pass makes sense to me.

@uenoku @fabianschuiki I moved the verification into a dedicated pass, now the question is: when should this pass be called? Just before emission? At the end of the hw pass pipeline?

I think we want to verify after IR constructed so probably after LowerToHW would be good place. It also makes sense to verify before ExportVerilog.

[fabianschuiki]

LGTM! Just a few nits on stray changes that you may want to revert/restore. Love the tests!