[sv-ac] feedback on the LTL proposal

The proposed operators are an excellent addition to SVA.

There seem to be two notations used for 'strong': both the keyword
'strong', used for sequences, and the angle brackets around strong
operators, e.g., <next>.  It would be nice if a single notation could be
used in each.  Note that PSL uses '!' in both cases.  Why not use that?

There also seems to be two notations for overlapping semantics - the
keyword 'with' (used with until), and the use of '=' in the operator
#=#, vs. #-#.  The '=' symbol has a precedent in '|=>' vs. '|->'
(although #-# and #=# are ugly; ##- and ##= would be better, and more
consistent with using ##0 and ##1 when the following sequence is
strong).  The keyword 'with' is understandable, but it doesn't read very
well.  Actually, it is not clear to me why ##0 and ##1 cannot be used.

What about a negated sequence?  Negation of a weak sequence should make
it strong, I believe.  (This is an issue in PSL, where "never {r}" has a
non-intuitive meaning: if {r} does not fail before the end of
simulation, then {r} will hold, and therefore "never {r}" will fail.
The right way to write this in PSL is "never {r}!".  IEEE 1850 is
considering a change in this area.)

Eventually is implicitly a strong operator - correct?  If so, the
notation seems inconsistent: always is weak, <always> is strong, but
eventually is strong (and there is no weak form).  Note that in PSL, the
corresponding operator is "eventually!".

Section 16.2.9, property p9 (and other subsequent occurrences) - why
can't you use an unbounded range with the weak next form?  Certainly you
can use an unbounded range in a weak sequence.  Why should next be
different?

Section 16.2.11, until - the inverse, "before", is often useful also.

Examples - there are four examples, three called p1, and one called p2.
The paragraph explaining them talks about properties p1, p2, p3, and p2.
Some renumbering is probably in order.

The description of property p1 can be misread - the "(not including)"
comment could be taken to mean that a must not be true when b becomes
true.  It would be better to say "The property p1 says that a remains
true in each cycle up to and including the cycle before the cycle in
which b becomes true".  Similar comments apply to other statements in
this paragraph.

=================

Formal Semantics document

F.2.3.2.7 - definition bullets 4, 5 refer to 'n-1', yet there is no n in
the LHS of the definition.  Should be 'm-1', I believe.

F.3.1 - the requirement that conditions not be dependent upon local
variables rather restricts the scope of this definition.  The formal
definition should cover the cases in which local variables are involved.

F.3.3.1 - where is the turnstile with three bars (used in the
definitions of w |= R and w |= (R|->P)) defined?  I assume this operator
means the same as in PSL formal semantics (that a word "models tightly"
a sequence R), but I don't see it defined anywhere here.

F.3.3.1 - definition of accept_on - why is it important to say (in the
first case) that no letter of w satisfies b?  Are you trying to defing
the 'endpoint' of the satisfaction, which would make it important to
know whether b was satisfied before the end of P was reached?


-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.