RE: [sv-ac] review of 1731

I agree.

Dmitry

-----Original Message-----
From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org] On
Behalf Of Doron Bustan
Sent: Tuesday, March 27, 2007 5:37 PM
To: Havlicek John-r8aaau
Cc: sv-ac@server.eda-stds.org
Subject: Re: [sv-ac] review of 1731

John,

I agree with most of the definition, two comments thus

1. there is a coma mismatch - number_of_ticks is the second argument.

2. A more complete definition will add the expression2. I was thinking 
of something like:

  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 && e2) ##1 (c && e2)[=n-1]), then 
$past(e,n,e2,c)[w^j] = e[w^i].
     Otherwise, $past(e,n,e2,c)[w j] has the value x [JH:  shouldn't
this
     be the default initial value -- I thought we fixed this in Section 
17] [DB: I think that was in the
     $sample+$past+$rose... proposal that eventually was reduced to 
$sample only].
   - $past(e,,,c) \equiv $past(e,1,1,c).


Doron

John Havlicek wrote:

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

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