RE: [sv-ac] feedback on the LTL proposal

Hi Lisa,

 

Please, see my comments below. I fixed the typos you mentioned and
uploaded the updated versions. I believe, the other comments require
further discussion.

 

Thanks,

Dmitry

 

________________________________

From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org] On
Behalf Of Lisa Piper
Sent: Tuesday, July 24, 2007 12:37 AM
To: sv-ac@server.eda-stds.org
Subject: [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?

[Korchemny, Dmitry] I would not use ! because it introduces syntactic
ambiguity: next! a may be interpreted as next !a as well. I agree with
you regarding the notation inconsistency: <next> a, but strong(a ##1 b),
I just don't have a better solution. Putting angle brackets around the
sequence instead of strong: <a ##1 b> may be confusing. I am open to
suggestions for better syntax.

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.

[Korchemny, Dmitry] I am not stuck about the notation #-#, and we can
change it to ##-. As for ##0 and ##1 there are the following subtleties
(I am illustrating everything on ##0):

*         The grammar becomes ambiguous: sequence_expr ##0 sequence_expr
and sequence_expr ##0 property_expr become undistinguishable. On the
other hand there are already such cases in SV grammar with conflicts
between sequence_expr and property_expr

*         #-# and ##0 have different semantics: A ##0 B means A #-#
strong(B). On the other hand I don't see many practical applications
that would require weak sequence after #-#.

*         For coverage purposes it is often convenient to distinguish
between the triggering condition and the rest. Even today the people are
tempted to write cover property(a |-> b ##1 c) meaning: report all
sequences b ##1 c when a happens. The right way to write this statement
is cover property(a #-# b ##1 c). Then the tool will report about
covering b ##1 c instead of reporting the coverage of the whole thing.
On the other hand in the cover statement the right operand of #-# needs
usually to be strong, and this fact needs to be expressed explicitly:
cover property(a #-# strong( b ##1 c)). Writing it weak will report the
coverage even if the clock stops ticking, The explicit strong operator
is confusing. ##0 solves this problem.

Bottom line: I see more advantages in your suggestion about using ##0
and ##1 than in ours, but all its implications have to be carefully
reviewed.

As for until with, what are the alternatives? Its advantage is that
'with' is already a keyword. We are open for other suggestions.

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.)

[Korchemny, Dmitry] Yes, this is an issue.

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!".

[Korchemny, Dmitry] The reason we defined eventually without <> is that
it does not have a weak form at all. I tend to agree with you, and use
<eventually> form.

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?

[Korchemny, Dmitry] This complicates the formal semantics description,
but it can be done. This invites introducing a weak form of eventually:
the clock is not required to tick, but if it ticks enough times, the
property shall happen,

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

[Korchemny, Dmitry] My point was to limit the operators to some
reasonable minimum. before can be derived from until and may be a part
of the library instead of belonging to the language, The reason why we
introduced until with, though it can be easily modeled using until
operator was the compilation efficiency: inverting until with gives you
<until>. Of course, nothing prevents us from adding before operator, we
can do it.

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.

[Korchemny, Dmitry] Fixed.

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.

[Korchemny, Dmitry] I rewrote these sentences.

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

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.

[Korchemny, Dmitry] Fixed

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.

[Korchemny, Dmitry] This is what is written in the original LRM, and I
didn't change this sentence. I doubt that this transformation remains
valid if the local variables allowed within the events.

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.

[Korchemny, Dmitry] This is a symbol of the tight sequence satisfaction
defined in F.3.2

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?

[Korchemny, Dmitry] This is essentially the same definition as in
disable iff: if the accepting condition never happens then accept_on
does not affect the property evaluation.


-- 
This message has been scanned for viruses and 
dangerous content by MailScanner <http://www.mailscanner.info/> , and is

believed to be clean. 

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