Subject: RE: [sv-ac] semantics issues
From: Surrendra Dudani (Surrendra.Dudani@synopsys.com)
Date: Thu Apr 10 2003 - 08:02:28 PDT
Hi All,
I think using *0 is confusing and the user has to be aware of all the
possibilities. In reality, most problems can be solved simply by using
disjunction, rather than *0. Introducing a different precedence and
new syntax for ##0 will create more confusion than solve these situations.
For example,
>assert (req ##1 !ack[*0:3] ##0 retry[*2]) |-> !ack[*2])
can be written as (although I'm not sure of the intention here)
assert ((req ##1 retry[*2]) or (req ##1 !ack[*1:3] ##0 retry[*2]) |->
!ack[*2]);
For the cases where *0 is combined with ##0, one can create a solution
using parenthesis or, as I said, by conjunction.
Surrendra
At 08:55 AM 4/10/2003 +0300, Armoni, Roy wrote:
>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
**********************************************
Surrendra A. Dudani
Synopsys, Inc.
377 Simarano Drive, Suite 300
Marlboro, MA 01752
Tel: 508-263-8072
Fax: 508-263-8123
email: Surrendra.Dudani@synopsys.com
**********************************************
This archive was generated by hypermail 2b28 : Thu Apr 10 2003 - 08:03:24 PDT