RE: [sv-ac] question on goto operator (clarification)

Thanks Dmitry and John.  I think I understand it.

Lisa

-----Original Message-----
From: John Havlicek [mailto:john.havlicek@freescale.com] 
Sent: Wednesday, July 25, 2007 1:11 PM
To: dmitry.korchemny@intel.com; Lisa Piper
Cc: sv-ac@eda-stds.org
Subject: Re: [sv-ac] question on goto operator (clarification)

Hi Dmitry, Lisa:

I agree with Dmitry's characterization of the semantics of b[->0].
I don't think anything in the SV LRM currently forbids this as a 
sequence expression.

Lisa asked

> At what point can you decide it is true?=20=20

I don't think we talk about sequences being true.  We talk about
sequences matching.  b[->0] matches the emptyword.

We talk about properties being true.  The evaluation of a property
will involve testing sequence matches as subevaluations.

We do not allow a sequence that admits empty match to stand itself
as a property.  See 16.12, item a), p. 341 of Draft 3a.

I don't understand why PSL forbids b[->0] as a SERE.  Presumably, 
PSL does not forbid b[*0], which is semantically equivalent.

Dmitry, I don't understand your question about endpoints of
evaluation attempts.  We currently do not define property evaluation
on the empty word and we do not allow sequences that admit empty
match to stand as properties.  Does this clarify the situation?

J.H.

> 
> ------_=_NextPart_001_01C7CECA.406F7B04
> Content-Type: text/plain;
> 	charset="us-ascii"
> Content-Transfer-Encoding: quoted-printable
> 
> Of course, I mean the empty match of b[*0:$], not the subsequent
> matches. If it is not accounted as a match, then neither should be
> b[*0].
> 
> =20
> 
> Dmitry
> 
> =20
> 
> ________________________________
> 
> From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org]
On
> Behalf Of Korchemny, Dmitry
> Sent: Wednesday, July 25, 2007 5:31 PM
> To: Lisa Piper; sv-ac@server.eda-stds.org
> Subject: RE: [sv-ac] question on goto operator
> 
> =20
> 
> In the LRM (Annex F) it is defined as
> 
> w \tight R [*0] iff |w| =3D 0.
> 
> =20
> 
> A property b[->0] (same as b[*0]) is true regardless the value of b.
> 
> =20
> 
> If you need it to define the endpoint of the evaluation attempt, then
we
> should be aligned with the definition of the endpoints of b[*0:$]. Do
we
> have such a definition for it?
> 
> =20
> 
> Thanks,
> 
> Dmitry
> 
> =20
> 
> ________________________________
> 
> From: Lisa Piper [mailto:piper@cadence.com]=20
> Sent: Wednesday, July 25, 2007 4:58 PM
> To: Korchemny, Dmitry; sv-ac@eda-stds.org
> Subject: RE: [sv-ac] question on goto operator
> 
> =20
> 
> At what point can you decide it is true?=20=20
> 
> =20
> 
> Lisa
> 
> =20
> 
> ________________________________
> 
> From: Korchemny, Dmitry [mailto:dmitry.korchemny@intel.com]=20
> Sent: Wednesday, July 25, 2007 9:42 AM
> To: Lisa Piper; sv-ac@eda-stds.org
> Subject: RE: [sv-ac] question on goto operator
> 
> =20
> 
> Hi Lisa,
> 
> =20
> 
> Since b[->k] is (!b[*0:$] ##1 b)[*k], b[->0] should be (!b[*0:$] ##1
> b)[*0]. i.e., the same as b[*0], which matches the empty word only. It
> looks to me that there is no need to forbid this case. Of course, I
> don't think that anybody will explicitly write this, but in a
> parameterized sequence it may happen, e.g.
> 
> =20
> 
> sequence b_after_nth_a(a, b, n);
> 
>             a[->n] ##1 b;
> 
> endsequence
> 
> =20
> 
> What do you think?
> 
> =20
> 
> Thanks,
> 
> Dmitry
> 
> =20
> 
> ________________________________
> 
> From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org]
On
> Behalf Of Lisa Piper
> Sent: Wednesday, July 25, 2007 4:32 PM
> To: sv-ac@server.eda-stds.org
> Subject: [sv-ac] question on goto operator
> 
> =20
> 
> Hi all,
> 
> I have a question.  Does it make sense to have a repetition of 0 in
the
> goto operator? If so, when is it true?
> 
> =20
> 
> Ex:     b[->1]     is     (!b ##1 b)   and it is true when b=3D1,
> 
> =20
> 
> If the repetition value is 0, when is it true?  PSL has this same
> operator but it limits the repetition value to a positive number.
> 
> Lisa
> 
> 

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.