RE: [sv-ac] call to vote on 1668

Hi John,

Please, see my comments below.

Thanks,
Dmitry

-----Original Message-----
From: John Havlicek [mailto:john.havlicek@freescale.com] 
Sent: Thursday, March 01, 2007 3:07 PM
To: Korchemny, Dmitry
Cc: john.havlicek@freescale.com; sv-ac@eda-stds.org
Subject: Re: [sv-ac] call to vote on 1668

Hi Dmitry:

I don't really see this as an inconsistency.  Sequences and properties
are different kinds of things, and we have different satisfaction
relations for the two.

In fact, our neutral satisfaction relation for properties is not
currently defined on empty words.  The definition can be extended to
include empty words, and I expect it eventually will be.  It was with
that vision that I thought we ought to have the two cases for
rewriting the semantics of a property with local variables with
declaration assignments.

[Korchemny, Dmitry] Yes, indeed, I noticed that

w |= R iff there exists 0 <= j < |w| so that w^{0, j} \tight R,
therefore if sequence can be satisfied by an empty word, the
property-sequence cannot (though I don't know why).

Also,
w |= disable iff (b) P iff either w |= P or there exists 0 < k < |w| so
that w^k |= b and w^{0, k-1} \top ^ \omega |= P. Here, w^{0, -1} denotes
the empty word. 

Therefore a property cannot be satisfied by an empty word. So, what kind
of definition extension of satisfiability relation on empty words do you
expect? 

My intention has been to place as few restrictions as possible, but
when we don't have a good solution I prefer to make things illegal
and leave the possibility of relaxing the restriction later if we
can come up with a good definition.

So I am willing to modify the proposal to say that local variable
declaration assignments are illegal in the declaration of a named
property whose body property expression is a sequence expression that 
admits an empty match.

Would this satisfy you?

[Korchemny, Dmitry] Yes, I agree with this approach.

We could have only one rewrite rule, say the one with "|->", but 
in that case I would like to leave a reminder that this will become
broken if we extend the semantics to define property satisfaction on
the empty word.

[Korchemny, Dmitry] In your original proposal you reserved "|->" for
properties satisfied by the empty word. Could you, please, elaborate?

Would this satisfy you?

[Korchemny, Dmitry] I don't think we should mention in the LRM that the
definition will change when the semantics changes.

I don't think "disable iff" should be considered in these
restrictions.  We have changed our language concerning "disable iff"
to say that an attempt that is terminated by the "disable iff"
condition is called "disabled", not "passing" or "failing".  According
to the Draft 1 revisions to Annex E, the "disable iff" condition is
relevant to the disposition of one of the satisfaction relations only
in the case of a non-empty word.  (Technically, we are only talking
about non-empty words in that context, as I pointed out above, but I
mean if you read the conditions imagining the possibility that the
word be empty.)

Do you agree?  Does this satisfy you?

[Korchemny, Dmitry] If accepton operator is introduced then all these
issues (if they exist) become relevant again. I think that the
definition should be robust relative to such changes.

Best regards,

John H.


> X-ExtLoop1: 1
> X-IronPort-AV: i="4.14,233,1170662400"; 
>    d="scan'208"; a="202668077:sNHT44372447"
> X-MimeOLE: Produced By Microsoft Exchange V6.5
> Content-class: urn:content-classes:message
> Date: Thu, 1 Mar 2007 07:29:33 +0200
> X-MS-Has-Attach: 
> X-MS-TNEF-Correlator: 
> Thread-Topic: [sv-ac] call to vote on 1668
> Thread-Index: AcdanekCnESOe8PDST2yrOXleY+mtwBIPl6Q
> From: "Korchemny, Dmitry" <dmitry.korchemny@intel.com>
> X-OriginalArrivalTime: 01 Mar 2007 05:29:36.0362 (UTC)
FILETIME=[99B09CA0:01C75BC2]
> 
> Hi John,
> 
> I reread your proposal again and found the following inconsistency: it
> is illegal to initialize variables in sequences matching an empty word
> 
> sequence s;
>     bit v =3D 0;
>     a[*0:$] ##1 v[*0:1];
> endsequence
> 
> but it is legal to initialize variables in properties matching an
empty
> word:
> 
> property  s;
>     bit v =3D 0;
>     a[*0:$] ##1 v[*0:1];
> endproperty
> 
> Though in the latter case we guarantee that it won't be used as a
> sequence, the distinction is vague. Also it is desirable to have the
> same rewriting rules for all properties.
> 
> Is it correct that the properties satisfied by empty words are exactly
> the sequences satisfied by empty words (with optional disable iff) and
> the properties having the form disable iff (1) P? If so, why not to
> disallow them as well?
> 
> Another question:
> 
> How can one decide whether the property 'disable iff (b) a' is
satisfied
> by an empty word? If b has a value of 1 it is, otherwise, it is not.
> 
> What do you think?
> 
> Thanks,
> Dmitry
> 
> -----Original Message-----
> From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org]
On
> Behalf Of John Havlicek
> Sent: Tuesday, February 27, 2007 8:32 PM
> To: sv-ac@server.eda-stds.org
> Subject: [sv-ac] call to vote on 1668
> 
> All:
> 
> Since our last meeting there has been no further discussion
> or suggestion of changes to 1668.  I am therefore calling for
> an email vote on this item.  See below for the details and
> eligibility.
> 
> Please remember that 80% participation is expected in order
> to retain voting eligibility.
> 
> Best regards,
> 
> John H.
> 
> ---------------------------------------------------------------------
> 
> Ballot on Mantis 1668=20
> 
> - Called on 2007-02-27, final ballots due by 23:59 PST on 2007-03-06.
> 
> 
>  v[xxxxxxxxxxxxxxx-xx] Doron Bustan (Freescale)
>  v[xxxxxxxxxxxxxxxx-x] Eduard Cerny (Synopsys)=09
>  n[-----x-x-xxx-x---x] Surrendra Dudani (Synopsys)
>  v[xxx-xxx-xxx-------] Yaniv Fais (Freescale)
>  t[xxxxxxxxxxxxxxxxxx] John Havlicek (Freescale - Chair)
>  v[rxxxxxxxxxxxxx-xxx] Dmitry Korchemny (Intel - Co-Chair)
>  n[x----------xx-xxxx] Manisha Kulshrestha (Mentor Graphics)
>  v[xxxx-------x-xx-x-] Jiang Long (Mentor Graphics)
>  v[-xx--xx-xxxxxxx-x-] Hillel Miller (Freescale)
>  v[xxxxxxxx-xxxxxxxxx] Lisa Piper (Cadence)
>  v[-xxxx-xx----------] Tej Singh (Mentor Graphics)
>  v[xxxxxxxxxxxxxxxxxx] Bassam Tabbara (Synopsys)
>  v[xxx...............] Tom Thatcher (Sun Microsystems)
>    |------------------ attendance on 2007-02-20
>  |-------------------- voting eligibility for this ballot
> |--------------------- email ballots received
> 
> 
> 	Legend:
> 		x =3D attended
> 		- =3D missed
> 		r =3D represented
> 		. =3D not yet a member
> 		v =3D valid voter (2 out of last 3)
> 		n =3D not valid voter
>                 t =3D chair eligible to vote only to make or break a
tie
> 
> 
> 
> --=20
> This message has been scanned for viruses and
> dangerous content by MailScanner, and is
> believed to be clean.

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