Subject: Re: [sv-ac] semantics issues
From: John Havlicek (john.havlicek@motorola.com)
Date: Thu Apr 10 2003 - 08:26:33 PDT
Hi Surrendra:
I hope you are not suggesting we get rid of *0. It will
make me case-split all my sequences.
John H.
> X-Sender: dudani@us04.synopsys.com
> Date: Thu, 10 Apr 2003 11:02:28 -0400
> From: Surrendra Dudani<Surrendra.Dudani@synopsys.com>
> Sender: owner-sv-ac@eda.org
> Precedence: bulk
>
> 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:27:13 PDT