Re: [sv-ac] 1668-formal-semantics.pdf

Hi Dmitry:

O.k., I'll make the symbols disjoint.  Greek letter should work.

J.H.

> X-ExtLoop1: 1
> X-IronPort-AV: E=Sophos;i="4.19,289,1183359600"; 
>    d="scan'208";a="265922294"
> X-MimeOLE: Produced By Microsoft Exchange V6.5
> Content-class: urn:content-classes:message
> Date: Tue, 21 Aug 2007 16:27:41 +0300
> X-MS-Has-Attach: 
> X-MS-TNEF-Correlator: 
> Thread-Topic: [sv-ac] 1668-formal-semantics.pdf
> Thread-Index: Acfj9dyfzhbFSdkATp6hJV4l9d48LwAACuZg
> From: "Korchemny, Dmitry" <dmitry.korchemny@intel.com>
> Cc: <sv-ac@eda-stds.org>
> X-OriginalArrivalTime: 21 Aug 2007 13:28:24.0221 (UTC) FILETIME=[264AC4D0:01C7E3F7]
> 
> Hi John,
> 
> Then Clause F.2.2 has to be modified, since it explicitly states that
> "In F.2.3 the following notational conventions will be used:...", and
> your proposal belongs to Clause F.2.3. It is always better to use a
> unified notation throughout the whole Annex F.
> 
> Thanks,
> Dmitry
> 
> -----Original Message-----
> From: John Havlicek [mailto:john.havlicek@freescale.com]=20
> Sent: Tuesday, August 21, 2007 4:19 PM
> To: Korchemny, Dmitry
> Cc: john.havlicek@freescale.com; sv-ac@eda-stds.org
> Subject: Re: [sv-ac] 1668-formal-semantics.pdf
> 
> Hi Dmitry:
> 
> I don't think that it should be necessary to replicate
> the definitions for each of the possible letters (p,q,r,s,t,u).
> 
> I had tried to define the terms, but I guess I failed to do this
> for admits_empty.
> 
> Maybe it is better to define all terms at the beginning of the=20
> subclause.  I could add a paragaraph at the very beginning that says=20
> something like
> 
>   Throughtout this subclause, r denotes a sequence (clocked or
>   unclocked); p denotes a property (clocked or unclocked, top-level or
>   not); t denotes a type; v denotes a local variable name; b, c, and d=20
>   denote boolean expressions; e denotes an expression.  Subscripts may=20
>   also be added to these symbols.
> 
> I could then get rid of the q's and use p_1, p_2 rather than p, q.
> 
> Would this be satisfactory?
> 
> J.H.
> 
> 
> > X-ExtLoop1: 1
> > X-IronPort-AV: E=3DSophos;i=3D"4.19,289,1183359600";=20
> >    d=3D"scan'208";a=3D"281753854"
> > X-MimeOLE: Produced By Microsoft Exchange V6.5
> > Content-class: urn:content-classes:message
> > Date: Tue, 21 Aug 2007 15:38:03 +0300
> > X-MS-Has-Attach:=20
> > X-MS-TNEF-Correlator:=20
> > Thread-Topic: [sv-ac] 1668-formal-semantics.pdf
> > Thread-Index: AcfjHl+F88ELQEZ3TFa7vaZx+6n9pQA0XhZg
> > From: "Korchemny, Dmitry" <dmitry.korchemny@intel.com>
> > X-OriginalArrivalTime: 21 Aug 2007 12:38:25.0782 (UTC)
> FILETIME=3D[2B154960:01C7E3F0]
> >=20
> > Hi John,
> >=20
> > I have one minor comment: you are using r to dente clocked sequences
> and
> > p and q to denote clocked properties while the notation requires using
> S
> > in the former case, and Q in the latter.
> >=20
> > Thanks,
> > Dmitry
> >=20
> > -----Original Message-----
> > From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org]
> On
> > Behalf Of John Havlicek
> > Sent: Monday, August 20, 2007 2:33 PM
> > To: sv-ac@server.eda-stds.org
> > Subject: [sv-ac] 1668-formal-semantics.pdf
> >=20
> > Hi Folks:
> >=20
> > Since I've regained the ability to attach things,
> > 1668-formal-semantics.pdf is attached.
> >=20
> > J.H.
> >=20
> > --=3D20
> > 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.