Subject: Re: [sv-ac] comments on lrm
From: Cindy Eisner (EISNER@il.ibm.com)
Date: Thu Jan 30 2003 - 06:54:50 PST
all,
i strongly agree with all of john's comments. in addition, i have a few
others. see below.
regards,
cindy.
-------------------------------------------------------------------------------------------------------------------------
1. section 11.4, p. 45: i propose that we cancel the unary delay
expressions, and keep only the binary. justification: as per john's
observation that
s ;[m] ([n]t) is equivalent to s ;[m+n] t
having two kinds of delay expression that are so close in syntax and in
meaning is extremely confusing. having only one kind would greatly improve
readability.
2. section 11.6.11, p. 61: i assume that the explanation "the end point
of a sequence is reached whenever there is a match on its expression" is
also intended to imply that the starting point of the match is not
relevant. if so, this should be said explicitly, and the example should
discuss this as well.
3. section 11.7, p. 61: i do not understand how a declared boolean
expression is different from a restricted type of function. perhaps a
keyword indicating the relation to functions would be better.
4. section 11.10, p. 64: i do not understand what it means to "cover" a
property, as opposed to a sequence. for instance, consider the following
property:
property p1 = accept (foo) @(clk) a => (b;c;d);
now, suppose that the sequence (a&&b;c;d) never occurs during any test, but
sequence (a&&b;c;foo) does occur. is the property covered or not?
according to the text in this section, it seems that it is - because the
property is successful at every cycle. another example without "accept" is
as follows:
property p2 = @(clk) e => (f;g;h);
suppose that "e" never occurs. according to the text in this section, the
property is covered.
i would prefer "cover" to be applicable to a sequence rather than to a
property, which is what i think the intuitive notion of coverage is about.
5. sections 11.10.1, 11.10.2, p. 65: it is not clear to me whether the
same rules are intended to apply to directives as well. the placement of
directives should be explained in more detail.
-------------------------------------------------------------------------------------------------------------------------
Cindy Eisner
Formal Methods Group Tel: +972-4-8296-266
IBM Haifa Research Laboratory Fax: +972-4-8296-114
Haifa 31905, Israel e-mail:
eisner@il.ibm.com
John Havlicek <john.havlicek@motorola.com>@eda.org on 30/01/2003 06:34:31
Please respond to john.havlicek@motorola.com
Sent by: owner-sv-ac@eda.org
To: sv-ac@eda.org
cc:
Subject: [sv-ac] comments on lrm
Dear SV-AC:
Below are some comments on the lrm.
Best regards,
John H.
========================================
1. In 11.6.8, I have serious concern about the semantics of the
sequence implication operator, "(s1 => s2)". This sequence does
not define a language of finite words in the usual sense because
the context of a word affects whether there is a match. As a
specific example, consider
((a;true*[0:inf];b) => (true;c))
where a, b, c are independent booleans. This sequence
matches from time 0 to 0 in the following waveform
time 0 1 2
--------------
a 1 0 0
b 0 0 0
c 0 0 0
But the sequence no longer matches from time 0 to 0 if I
extend the waveform to
time 0 1 2 3
-----------------
a 1 0 0 0
b 0 0 0 1
c 0 0 0 0
Once we have such a sequence building operator, the sequence
semantics has the following poor property: given a sequence s
that matches a finite word w, it may not be the case that s
matches w viewed as a prefix of ww'.
I see this context sensitivity as highly undesirable for
usability. I also think that making the sequence implication
a sequence building operator will cause problems merging with
PSL, in which the sequence implication operators yield properties,
not sequences.
I think that the sequence implication should be a property
building operator, not a sequence building operator.
2. I have some reservations about the way delays have turned out.
I see nothing broken here, but users must be careful always
to treat ";" without a range as ";[1]" when moving the
delay indexes about. Once this is understood, then the
following "algebra" all seems to work out:
s ;[m] ([n]t) is equivalent to s ;[m+n] t
is equivalent to s ;[0] ([m+n] t)
is equivalent to s ; ([m+n-1] t)
3. In 11.6.4, I prefer the keyword "intersect" to "congruent" because
"intersect"is motivated from language intersection. If we define
L(s) to be the set of finite words that are matched by sequence s,
then we should have
L(s intersect t) = L(s) intersect L(t)
4. In 11.6.9, I suggest
b throughout s
rather than either
b until s
or
throughout b within s
The last does not read well. The danger of using "b until s" for
this operator is that it will clash with the usual meaning of
promotion of a sequence to a property: if w is a word, then s
holds as a property at time i provided there exists j >= i such that
s matches the sub-word of w from i to j.
This archive was generated by hypermail 2b28 : Thu Jan 30 2003 - 06:52:21 PST