Subject: RE: [sv-ac] semantics issues
From: Erich Marschner (erichm@cadence.com)
Date: Thu Apr 10 2003 - 07:14:36 PDT
Roy,
I agree with you that fusion should have lower precedence than concatenation, and that this implies the need for different operators rather than using ## for both.
Regards,
Erich
-------------------------------------------
Erich Marschner, Cadence Design Systems
Senior Architect, Advanced Verification
Phone: +1 410 750 6995 Email: erichm@cadence.com
Vmail: +1 410 872 4369 Email: erichm@comcast.net
| -----Original Message-----
| From: Armoni, Roy [mailto:roy.armoni@intel.com]
| Sent: Thursday, April 10, 2003 1:55 AM
| To: sv-ac@eda.org
| Subject: RE: [sv-ac] semantics issues
|
|
| Hi John,
|
| I would like to support your proposal for the definition of within.
|
| For the second issue that you raise regarding fusion, I am
| not sure that
| right associativity is significantly better than left.
| Consider a property
| such as
|
| assert (req ##1 !ack[*0:3] ##0 retry[*2]) |-> !ack[*2]
|
| IMHO, such examples show that fusion is different than
| concatenation, and
| should have lower precedence. If the proposed syntax
| prevents the parser
| from recognizing fusion and giving it lower precedence, then
| we should
| probably give special syntax for fusion.
|
| What do you think?
|
| Regards,
| Roy
|
|
| -----Original Message-----
| From: John Havlicek [mailto:john.havlicek@motorola.com]
| Sent: Thursday, April 10, 2003 5:50 AM
| To: sv-ac@eda.org
| Subject: [sv-ac] semantics issues
|
|
| All:
|
| > Will tune expansion to align with semantic defintion:
| > (1 [*0:$](sequence_expr1) ##[0:$] 1 ) intersect sequence_expr2
| > Detailed discussion of matching of empty words and whether
| the overlapping
| > concatentation absorbs the empty word. It has been
| defined that it does,
| but
| > John sees an associativity. John will own this as part of
| semantics
| effort.
|
| In my opinion, the semantics of within should be defined as follows:
|
| sequence_expr1 within sequence_expr2
|
| means
|
| (1[*0:$] ##1 sequence_expr1 ##1 1[*0:$]) intersect sequence_expr2
|
| This is the way it is defined in the semantics document we
| are finishing
| up.
|
| Note that for any sequence expression S, the following are
| equivalent:
|
| 1. (1[*0] ##1 S)
| 2. (S ##1 1[*0])
| 3. S
|
| This is the usual way non-overlapping concatenation interacts with
| a regular expression matching the empty word.
|
| In my opinion, we should not use the "##0" operator in the definition
| of within. "##0" can match only if both its operands match non-empty
| words. This is because "##0" requires the last letter of
| the lhs word
| to overlap with the first letter of the rhs word, so, a
| fortiori, both
| words must have at least one letter. Thus,
|
| (1[*0:$] ##0 S ##0 1[*0:$]) intersect T
|
| is equivalent to
|
| (1[*1:$] ##0 (1 and S) ##0 1[*1:$]) intersect T
|
| which forbids S, hence T, from matching empty.
|
|
| Regarding association of "##0" and "##1", note that
|
| (R ##0 S) ##1 T
|
| is equivalent to
|
| ((1 and R) ##0 (1 and S)) ##1 T
|
| Both R and S must match non-empty words to get a match. On the
| other hand,
|
| R ##0 (S ##1 T)
|
| is equivalent to
|
| (1 and R) ##0 (1 and (S ##1 T))
|
| Here R must match non-empty, but only the concatenation S ##1 T,
| rather than S specifically, must match non-empty. To show this
| difference more concretely, if I write
|
| a ##0 b[*0:$] ##1 c
|
| and rely on left-association of operators ##0 and ##1 at the
| same precedence, what I get is equivalent to
|
| a ##0 b[*1:$] ##1 c
|
| and this is not equivalent to
|
| a ##0 (b[*0:$] ##1 c)
|
| It has been suggested to me that pushing the precedence of
| ##0 lower than ##m m > 0 is problematic for parsing.
|
| Perhaps we should consider changing the associativity for
| concatenation from left to right. What is the PSL convention
| for associativity?
|
| Best regards,
|
| John Havlicek
|
|
|
This archive was generated by hypermail 2b28 : Thu Apr 10 2003 - 07:16:01 PDT