RE: [sv-ac] review of 1731

Hi John,

I definitely agree with your comments (I am also accepting Doron's
suggestion), and will update the proposal accordingly.

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, March 27, 2007 2:33 PM
To: sv-ac@server.eda-stds.org
Subject: [sv-ac] review of 1731

Hi Dmitry & All:

I had an action item to review 1731.

The proposal itself is very short.  There is nothing wrong with
the text changes described, but the proposal is not complete.

As Dmitry suggested, we will need to change the definition in 
Annex E (I use draft1 as my reference).  I also believe that
it will be good to add some more language to Section 17 to describe
more precisely what happens when the clock of $past is not
the same as the prevailing clock in the context where the reference
to $past is made.

Dmitry:  note that we already changed "[->n-1]" to "[->n]" in Annex E.
I guess that your proposed definition is the following:

   E.4.2 Past
   
   w denotes a nonempty finite or infinite word over \Sigma, and j
denotes
   an integer so that 0 <= j < |w|.
   - Let n >= 1. If there exist 0 <= i < j so that 
     w^{i,j},{},{} \tight (c ##1 c [->n]), then 
     $past(e, n, c)[w^j] = e[w^i]. Otherwise, $past(e, n, c)[w j] 
     has the value x.
   - $past(e) \equiv $past(e,1) .

But this is broken.  We cannot use c ##1 c[->n] and get what we want.
The c ##1 c[->n] form was to force us to the alignment point with the 
assertion clock (that used to be required to be the same as the $past
clock) where the reference to $past is made.  This goes too far if 
we want to be able to make references to $past in the context a clock
different from c.

The following looks better to me, but I haven't had time to check it
carefully:

   E.4.2 Past
   
   w denotes a nonempty finite or infinite word over \Sigma, and j
denotes
   an integer so that 0 <= j < |w|.
   - Let n >= 1. If there exist 0 <= i < j so that 
     w^{i,j-1},{},{} \tight (c ##1 c[=n-1]), then $past(e,,n,c)[w^j] =
e[w^i]. 
     Otherwise, $past(e,,n,c)[w j] has the value x [JH:  shouldn't this
     be the default initial value -- I thought we fixed this in Section
17].
   - $past(e,,,c) \equiv $past(e,,1,c).

The key difference is that 

   w^{i,j} \tight (c ##1 c[->n])

in your version is changed to

   w^{i,j-1} \tight (c ##1 c[=n-1])

in my version.  Do you agree?

I added some commas to try to make the form of $past match what is in
Annex A.  Also, I think we already changed Section 17 to say that when
$past references too far back, we get default initial value, not just
x.  I haven't found that mantis item -- does anyone remember it?

At this point I have not checked whether my proposed definition above
leads to semantic discontinuities -- hopefully it does not.

J.H.


> X-ExtLoop1: 1
> X-IronPort-AV: i="4.14,289,1170662400"; 
>    d="scan'208"; a="196978010:sNHT43278508"
> X-MimeOLE: Produced By Microsoft Exchange V6.5
> Content-class: urn:content-classes:message
> Date: Thu, 15 Mar 2007 17:36:24 +0200
> X-MS-Has-Attach: 
> X-MS-TNEF-Correlator: 
> Thread-Topic: [sv-ac] 1731
> thread-index: Acdm+Z+D8rYGPSSXRJOVHRttACzSnAAGb4NA
> From: "Korchemny, Dmitry" <dmitry.korchemny@intel.com>
> Cc: <sv-ac@eda-stds.org>
> X-OriginalArrivalTime: 15 Mar 2007 15:36:32.0343 (UTC)
FILETIME=[B516D670:01C76717]
> 
> Hi John,
> 
> I think that the semantic definition of $past requires some trivial
> rewriting to deal with this enhancement.
> 
> Here is the current definition:
> 
> E.4.2 Past
> 
> w denotes a nonempty finite or infinite word over \Sigma, and j
denotes
> an integer so that 0 <=3D j < |w|.
> - Let n >=3D 1. If there exist 0 <=3D i < j so that w^{i, j} , {}, {}
=
> \tight
> (c ##1 c [->n - 1]), then @(c)$past(e, n)[w^j] =3D e[w^i]. Otherwise,
> @(c)$past(e, n)[w j] has the value x.
> - $past(e) =3D=3D $past(e,1) .
> 
> This definition does not deal with the full syntax of $past, but
always
> assumes that the clock is implicit. We can rewrite $past definition
with
> an explicit clock: $past(e, n, clk) and make the context inference
pure
> syntactic, so that the semantic definition does not deal with the
clock
> propagation for $past. Then we will have:
> 
> E.4.2 Past
> 
> w denotes a nonempty finite or infinite word over \Sigma, and j
denotes
> an integer so that 0 <=3D j < |w|.
> - Let n >=3D 1. If there exist 0 <=3D i < j so that w^{i, j} , {}, {}
=
> \tight
> (c ##1 c [->n - 1]), then $past(e, n, c)[w^j] =3D e[w^i]. Otherwise,
> $past(e, n, c)[w j] has the value x.
> - $past(e) =3D=3D $past(e,1) .
> 
> This definition actually means that clock of $past is independent of
the
> property clock, and that $past is evaluated according its own clock. I
> cannot see any semantic discontinuity here, never mind what the clock
> patterns are.
> 
> 1698 may formalize the simulation semantics of $past, but whatever
> decision is taken for 1698, it won't affect the consistency of the
clock
> changes in $past described in this item.
> =20
> Thanks,
> Dmitry
> 

-- 
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.