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

Hi Manisha:

I thought I had taken care of this already.

For example, the proposal says 

   . If the declaration assignments are in a named property with body
     property expression P and the instance of P is satisfied by the
     empty word, then P is replaced by (1, v1 = e1, ..., vk = ek) |-> (P) 
     before the substitution of actual arguments.

My intention is that "P" refers to the body property expression only.

In the syntax, the body of a property declaration is a property_spec,
which can have an optional clocking event and an optional "disable
iff" before the obligatory property expression.  When I said "body
property expression" my intention was that we do not include the 
"disable iff" in "P" here.

Is this still unclear?  How would you reword it to make it clearer?

Best regards,

John H.
 

> X-MimeOLE: Produced By Microsoft Exchange V6.5
> Content-class: urn:content-classes:message
> Date: Thu, 1 Mar 2007 09:29:21 -0800
> X-MS-Has-Attach: 
> X-MS-TNEF-Correlator: 
> Thread-Topic: [sv-ac] call to vote on 1668
> Thread-Index: AcdcApTMAoWMk3VoSXKNifZWoKBNJAAJJEYq
> From: "Kulshrestha, Manisha" <Manisha_Kulshrestha@mentor.com>
> Cc: <john.havlicek@freescale.com>, <sv-ac@eda-stds.org>
> X-OriginalArrivalTime: 01 Mar 2007 17:32:12.0360 (UTC) FILETIME=[8BE0E480:01C75C27]
> 
> This is a multi-part message in MIME format.
> 
> ------_=_NextPart_001_01C75C27.8B6D96B9
> Content-Type: text/plain;
> 	charset="iso-8859-1"
> Content-Transfer-Encoding: quoted-printable
> 
> John,
> 
> I was just wondering if it will be better to consider the case of =
> properties with disable iff in the formal semantics separaterly as we do =
> not allow embedded disable iffs. Currently the proposal says that =
> initializations are like this:
>  (1, initializations) |-> P=20
> 
> Now if P has disable iff, then it becomes equivalent to having nested =
> disable iff.
> 
> Manisha
> 
> 
> -----Original Message-----
> From: owner-sv-ac@server.eda.org on behalf of John Havlicek
> Sent: Thu 3/1/2007 5:06 AM
> To: dmitry.korchemny@intel.com
> Cc: john.havlicek@freescale.com; sv-ac@server.eda-stds.org
> Subject: Re: [sv-ac] call to vote on 1668
> =20
> 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.
> 
> 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=20
> admits an empty match.
> 
> Would this satisfy you?
> 
> We could have only one rewrite rule, say the one with "|->", but=20
> 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.
> 
> Would this satisfy you?
> 
> 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?
> 
> Best regards,
> 
> John H.
> 
> 
> > X-ExtLoop1: 1
> > X-IronPort-AV: i=3D"4.14,233,1170662400";=20
> >    d=3D"scan'208"; a=3D"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:=20
> > X-MS-TNEF-Correlator:=20
> > 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=3D[99B09CA0:01C75BC2]
> >=20
> > Hi John,
> >=20
> > I reread your proposal again and found the following inconsistency: it
> > is illegal to initialize variables in sequences matching an empty word
> >=20
> > sequence s;
> >     bit v =3D3D 0;
> >     a[*0:$] ##1 v[*0:1];
> > endsequence
> >=20
> > but it is legal to initialize variables in properties matching an =
> empty
> > word:
> >=20
> > property  s;
> >     bit v =3D3D 0;
> >     a[*0:$] ##1 v[*0:1];
> > endproperty
> >=20
> > 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.
> >=20
> > 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?
> >=20
> > Another question:
> >=20
> > 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.
> >=20
> > What do you think?
> >=20
> > Thanks,
> > Dmitry
> >=20

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