[LTL] Add fundamental operators

[liuyic00]

This PR aims to add fundamental operators into LTL dialect, namely until, next and repeat, to complete expressive power according to #6618 .

The current plan is:

• Add ltl.until for properties.
• Reuse ltl.delay as next operator on property. Inspired by ltl.or can be applied to both sequences and properties.
• Add ltl.repeat for sequences.

The document for the LTL dialect has been updated. I will add code implementation later.

Please let me know if you have any advice.

[liuyic00]

Thanks for the review. I fixed some of the problems you pointed out and left comments above regarding the parts I am not sure about.

I am wondering though, for things such as indefinite repetition or delays, how do you plan on implementing that? Is this just being planned as something that is directly mapped to SV and not actually lowered to synthesizable hardware?

The current plan is to directly map the properties to SVA. However, if synthesizable hardware is used for emulation to replace the simulation with SVA, indefinite repetition and delays can be implemented by an automaton with loops, considering that the sequence expresses a regular expression.

[dobios]

Thanks for the review. I fixed some of the problems you pointed out and left comments above regarding the parts I am not sure about.

I am wondering though, for things such as indefinite repetition or delays, how do you plan on implementing that? Is this just being planned as something that is directly mapped to SV and not actually lowered to synthesizable hardware?

The current plan is to directly map the properties to SVA. However, if synthesizable hardware is used for emulation to replace the simulation with SVA, indefinite repetition and delays can be implemented by an automaton with loops, considering that the sequence expresses a regular expression.

My issue was more in how you would like to do this in the always case, where synthesizing the automata requires creating multiple copies of them for each cycle in your delays and repetitions. So in theory if you have a variable length repetition that can go to infinity, then implementing this in an assert always requires an infinite amount of registers. So either this can be something that is special cased out or maybe we need to figure out some approximation if we are given the max simulation time ahead of compilation. I might just be overthinking this, but I ran into this problem when testing out my first ideas for implementing the variable delays. They also mention this issue in the BlueSpec Verilog SVA implementation paper from way back in 2005, where they just chose not to support it.

[liuyic00]

I added ltl.repeat, ltl.until and reused ltl.delay in LTL, FIRRTL and ExportVerilog.

Using ltl.delay on properties allows ltl.delay to express nexttime[n] and bounded weak eventually:

LTL dialect and SVA:

ltl.delay p, 0    == eventually p
ltl.delay p, n    == nexttime[n] eventually p
ltl.delay p, n, 0 == nexttime[n] p
ltl.delay p, n, m == eventually[n:n+m] p
                  == nexttime[n] eventually[0:m] p

UPDATE: eventually p (weak unbounded eventually) is not part of SVA and is meaningless because it always true.

We can also express all versions of bounded always and eventually.

SVA on the left and SVA or LTL dailect on the right:

always p        == not s_eventually not p
always[m:n] p   == not s_eventually[m:n] not p 
always[m:$] p   == not s_eventually[m:$] not p
s_always[m:n] p == not eventually[m:n] not p

s_eventually p      == ltl.eventually p                                         -> OK
s_eventually[m:n] p == (not nexttime[n] false) and (eventually[m:n] p)
s_eventually[m:$] p == (not nexttime[m] false) and (nexttime[m] s_eventually p)
eventually[m:n] p   == ltl.delay p, m, n-m                                      -> OK

nexttime[m] p   == ltl.delay p, m, 0                                            -> OK
s_nexttime[m] p == not nexttime[m] not p

// (not nexttime[n] false) holds if there is 0 to n clock cycle.

I think this kind of implementation has some problems. If "we'll want to have that always/globally quantifier eventually", maybe we will have bounded eventually at the same time, considering the symmetry between always and eventually. The function will be duplicated when using ltl.delay to express bounded weak eventually. Another problem is we do not have an operator to cast a sequence or boolean expression to a property. I think this would be useful for clarifying where the property is. For example, avoiding nexttime ##1 s be folded to ltl.delay s, 2, 0. I tried to add a CastToProp operation, but it is not suitable because the existing code doesn't seem to solve the problem this way. We already have ltl.delay i, 0, 0 to cast boolean expression to sequence, and LTLAnyPropertyType worked like implicit type conversion.

Therefore, maybe we should not reuse ltl.dealy. Add a next[n] for property like in SVA will be batter:

ltl.next s, 0 could be used as cast to property. Bounded always and eventually could be implemented with one parameter:

SVA on the left and possible LTL dailict on the right:

always p        == always[*] p
always[m:n] p   == next[m] always[n-m] p
always[m:$] p   == next[m] always[*] p
s_always[m:n] p == (next[m] always[n-m] p) and (not next[n] false)
                == strong(next[m] strong(always[n-m] p))           // or use `strong(...)` and `weak(...)` operator
                == next['s', m] always['s', n-m] p                 // or add 'strong' and 'weak' as parameter

s_eventually p      == eventually[*] p // here is strong eventually
s_eventually[m:n] p == (next[m] eventually[n-m] p) and (not next[n] false)
s_eventually[m:$] p == (next[m] eventually[*] p) and (not next[m] false)
eventually[m:n] p   == next[m] ((eventually[n-m] p) or (next[n-m] false))

nexttime[m] p   == next[m] p
s_nexttime[m] p == not next[m] not p

I mentioned bounded operators here because I believe they will influence how we implement the next operator. However, they should be discussed and added in another pull request.

My issue was more in how you would like to do this in the always case, where synthesizing the automata requires creating multiple copies of them for each cycle in your delays and repetitions. ...

This is indeed a problem that I didn't consider thoroughly.

[liuyic00]

I have added repeat, until and next (without reusing delay). These should be good enough for review and passing CI. I changed the plan from reusing delay because the "weak unbounded eventually" introduced by ltl.delay %p, 0 is unnecessary redundancy.

I think it's preferable to distinguish between sequences and properties rather than explaining them all through LTL. Particularly, sequences express some semantics that LTL cannot capture, and sequences evaluate differently on the left and right sides of |->.

[sequencer]

I'm not so sure I'm a good person to review the LTL implementation in CIRCT, may I request review from @fabianschuiki, I think he was the original design to this dialect. For implementations in chisel, I'm happy to review after this is merged.

[liuyic00]

NextOp and DelayOp are similar. I tried using DelayOp on both properties and sequences before. You can see this branch or previous comments.

There are two reasons I gave up this plan. The "weak unbounded eventually" or "weak unbounded next" introduced by ltl.delay %p, n (work on a property) is unnecessary redundancy, as it always evaluates to true. This redundancy will mislead the semantics of this operation and cause trouble when processing the expressions. Another reason is ltl.delay %p, n, m represents eventually[n:n+m] p in SVA. Considering that we are likely to add "bounded always" in some way in the future, it will be strange for "bounded eventually" to be merged into "next", where "always" and "eventually" are two very symmetrical operations.

ltl.dealy %s, n or ##[n:$] s is acceptable because we evaluate the sequence differently when we treat it as a sequence or a property. ##[n:$] s is like strong when finding a match on the trace at left side of |-> as a sequence, but is like weak when we determining if the trace meets it as a property. ("strong" and "weak" are not used to discrube operations inside of sequences in SVA.)

[liuyic00]

I have written a longer plan for adding operators here, which may be more convincing about NextOp.

[sequencer]

Any update on this PR? hopefully it won't be stall. :)

[liuyic00]

The repeat and until are adding in #6989. next/delayProp needs further discussion.