Subject: Re: [sv-ac] semantics issues
From: Surrendra Dudani (Surrendra.Dudani@synopsys.com)
Date: Thu Apr 10 2003 - 08:42:27 PDT
Hi John,
No, I'm not suggesting to get rid of *0. But, the awkward situations arise
mostly when *0 is combined with ##0. There could be good
methodology/modelling guidelines to deal with such situations, rather than
disturbing more common scenarios.
Surrendra
At 10:26 AM 4/10/2003 -0500, you wrote:
>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
> > **********************************************
**********************************************
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:43:13 PDT