Subject: [sv-ac] comments on lrm
From: John Havlicek (john.havlicek@motorola.com)
Date: Wed Jan 29 2003 - 20:34:31 PST
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 : Wed Jan 29 2003 - 20:35:16 PST