[LTL] Add repeat and until operators

[liuyic00]

Add repeat and until operators to LTL dialect.

This PR is separated from #6712.

[dobios]

Thank you so much for these additions, there are really useful !!
I left a few comments mostly about the wording of things (I want to avoid having ambiguous documentation for LTL because it is already subtle enough as is ^^"). Feel free to ping me when you've updated things!

[dobios]

This is really tricky to encode when expressed this way (inverse liveness of an inverse property) using anything outside of actual SVA, so I'm a bit skeptical about including it here. Also the default is always when you don't specify anything, so it is in theory implemented, you just can't specify it explicitly because it is always implicit.

[liuyic00]

Here I mean the operator is not implemented. We can't write something like p |-> always q for now.
As for not s_eventually not p, maybe we can just leave it here until we have the plan to implement or encode always.

[dobios]

It's a question of semantic meaning, i.e. p |-> always q and always p |-> q are semantically equivalent, but p |-> eventually q and eventually p |-> q are not. This is one of the annoying subtleties of the always so in practice leaving it as the default will make it easier to encode. I'm just afraid that telling people to encode it as the negated liveness of a negated property will make it impossible to encode as anything other than a vendor-specific implementation of SVA. The end goal here is to have something that we can implement in open-source simulation, rather than relying on things that require weird heuristics to implement. This is just my opinion, but I think this particular sentence will lead to a lot of trouble in the future.

[liuyic00]

It's a mistake I use p |-> because |-> in SVA only allows a sequence on the left side. However, we can consider the |-> as the logical implacation in this conversation.
p |-> always q means if p is true, then q needs to be always true for the reset of the time. But (always p) |-> q means if p is always true, then q needs be true. Or always (p |-> q) means every time p is true, then q needs to be true. They don't seem equivalent.

It's precisely because simulation that I don't think we need to worry about this liveness. In simulation, it dosen't actually check if the property eventually holds on the infinite trace, but only evaluates the property based on the existing simulation trace. Please let me know if I have a misunderstanding about what we want the simulation do with the properties.

[dobios]

It would be a lot clearer if you had one //CHECK per line, i.e.

// Check: assert property (a[*0]);
%r0 = ltl.repeat %a, 0, 0 : i1
verif.assert %r0 : !ltl.sequence

// CHECK: assert property (a[*4]);
....

[liuyic00]

Here is written in the same way as the code above, to keep all the tests about repeat in one code block.

[dobios]

It's more of a question of not propagating bad habits

[liuyic00]

I think they are both okay as long as they are consistent in the context. What does @fabianschuiki think about this? I could modify both here and previous codes.

[dobios]

This is great! Thank you so much for doing this, apart from a couple of minor comments (that I would greatly appreciate you take into account) LGTM!

[dobios]

I would suggest removing this paragraph (see previous comment)

[dobios]

Let's try avoiding bad testing habits, even if for some reason they were used earlier, other tests in CIRCT usually do a line-by-line check

[SpriteOvO]

LGTM. Thanks for your work! Waiting for CI to pass then we merge.