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

Hi Lisa:

> 1. the coloring needs to be reviewed. Specifically there appears to be
> very little purple and LOTS of blue. I think all of the ""local variable
> declaration" form" should be purple if you stick to the current coloring
> scheme at the beginning. There are entire sections that are blue that I
> suspect should be purple. Since new text is normally blue, I suggest
> putting 1549 dependencies in purple and keeping all 1668 additions in
> blue. Also, minimize 1549 references to de-couple this as much as
> possible, though it is likely that this will not make sense to the
> editor until 1549 is also approved.=20

Maybe the description to the editor simply needs to be changed or
clarified.

My intention was to use the variant coloring scheme only in the 
change descriptions that require the additions from 1549 in order
to locate properly the additions from 1668.  These change descriptions
are marked "consistent with 1549".  In these change descriptions, 
my intention was to differentiate the additions that are exclusive
to 1668 (currently colored purple) from the addtions that are shared
and consistent in both 1668 and 1549 (currently colored blue).

For the changes that are not marked "consistent with 1549", no
change text from 1549 appears.  Only change text for 1668 appears,
and this follows the usual coloring scheme.

We could add this elaborated explanation to the note to the editor.

Do you have a better suggestion of how to handle the coloring?

I did try to minimize the 1549 references.  I only marked the change
"consistent with 1549" when I thought the 1549 change was neede to
locate properly the additions from 1668.

1668 depends on 1549 in Annex F only, but critically.  The definition
of the push function assumes that flattening algorithm from 1549 has
already been performed.

> 1. Why did you choose to say that local variables have no initial
> default versus a default that is based on their type? Otherwise, I
> assume the local variable types are treated like types in properties and
> sequences (e.g. bit casting to the specified type)

Saying that local variables have no initial default value is, in my
opinion, consistent with the current standard.  According to 16.9,
a local variable is assigned in a sequence_match_item, and it is not
legal to reference the local variable before it has been so assigned.
One could say that the local variable gets a default initial value,
but the rule about references would mean that no reference would ever
see that default initial value.

The concept of a local variable being blocked from flowing has also
existed from the Accellera days.  Under certain circumstances a local
variable that has been assigned becomes unassigned because it does not
flow.  The LRM says that it is not legal to reference a local variable
that has become unassigned in this way until after it has again been
assigned.  This is determined statically from the structure of the
assertion.

One could take a different approach and say that local variables have
default initial values and make references to variables that are 
currently illegal return the default initial value instead.  This
could be done both for reference that precede the first assignment or
for references that follow the blocking of a variable.

Such changes could be done later in a backward-compatible way because
they are invisible with the current rules of referencing.

> 2. It is not clear to me when local variable declaration assignments
> occur. It states that the Preponed value of that timestep is used. In
> the example shown, is this the Preponed value relative to clk1 and clk2
> for the two copies of the local variable? But exactly when is the
> assignment made? For example, what happens if I say:
> 
> 	property p;
> 	logic v =3D e1;
> 	(@(posedge clk1) (1, v =3D e2) ##0 (a =3D=3D v)[*1:$] |-> b)
> 	and
> 	(@(posedge clk2) (1, v =3D e3) ##0 c[*1:$] |-> d =3D=3D v)
> 	;
> 	endproperty

The proposal says:

   If there are two or more distinct semantic leading clocks for an
   instance of a named property, then a separate copy of the local
   variable shall be created for each semantic leading clock. For each
   copy of the local variable, the declaration assignment shall be
   performed at the earliest tick of the corresponding semantic
   leading clock that is at or after the beginning of the evaluation
   attempt, and that copy of the local variable shall be used in the
   evaluation of the subproperty associated with the corresponding
   semantic leading clock.

There is an example property similar to the one you have shown and
an explanation of the timesteps.  

For the subproperty with semantic leading clock posedge clk1, the
declaration assignment "v = e1" is performed in the timestep that is
the the earliest tick of posedge clk1 that is at or after the
beginning of the evaluation attempt of the property p.  The Preponed 
value of e1 in this timestep is used.

Similarly, for the subproperty with semantic leading clock posedge
clk1, the declaration assignment "v = e1" is performed in the timestep
that is the the earliest tick of posedge clk1 that is at or after the
beginning of the evaluation attempt of the property p.  The Preponed 
value of e2 in this timestep is used.

In your example, however, the declaration assignment will never
observed.  This is because the explicit assignments "v = e2" in the
first subproperty overwrite the value written in the declaration
assignment in the same timestep that the declaration assignment is
performed.  Similarly for "v = e3" in the second subproperty.  

This behavior is clear from the description in Annex F, because the
local variable declaration assignments are added before any
assignments appearing in sequence_match_items.

Let me know if you think adjustments to the proposal text need to be
made.

J.H.

> X-MimeOLE: Produced By Microsoft Exchange V6.5
> Content-class: urn:content-classes:message
> Date: Thu, 20 Sep 2007 13:52:50 -0400
> X-MS-Has-Attach: 
> X-MS-TNEF-Correlator: 
> Thread-Topic: [sv-ac] call to vote on Mantis 1668
> Thread-Index: Acf5yEix7Y8DQXZ8Q6WUgFjarH9MHwB3Gifg
> From: "Lisa Piper" <piper@cadence.com>
> Cc: <sv-ac@eda.org>
> X-Received: By mx-sanjose2.Cadence.COM as l8KHnIIk017255 at Thu Sep 20 10:49:19 2007
> X-OriginalArrivalTime: 20 Sep 2007 17:52:37.0478 (UTC) FILETIME=[07F65060:01C7FBAF]
> 
> Hi John,
> 
> I have some questions:
> 
> 1668-formal-semantics.pdf:
> 1. the coloring needs to be reviewed. Specifically there appears to be
> very little purple and LOTS of blue. I think all of the ""local variable
> declaration" form" should be purple if you stick to the current coloring
> scheme at the beginning. There are entire sections that are blue that I
> suspect should be purple. Since new text is normally blue, I suggest
> putting 1549 dependencies in purple and keeping all 1668 additions in
> blue. Also, minimize 1549 references to de-couple this as much as
> possible, though it is likely that this will not make sense to the
> editor until 1549 is also approved.=20
> 
> 1668-2007-09-03.pdf:
> 1. Why did you choose to say that local variables have no initial
> default versus a default that is based on their type? Otherwise, I
> assume the local variable types are treated like types in properties and
> sequences (e.g. bit casting to the specified type)
> 
> 2. It is not clear to me when local variable declaration assignments
> occur. It states that the Preponed value of that timestep is used. In
> the example shown, is this the Preponed value relative to clk1 and clk2
> for the two copies of the local variable? But exactly when is the
> assignment made? For example, what happens if I say:
> 
> 	property p;
> 	logic v =3D e1;
> 	(@(posedge clk1) (1, v =3D e2) ##0 (a =3D=3D v)[*1:$] |-> b)
> 	and
> 	(@(posedge clk2) (1, v =3D e3) ##0 c[*1:$] |-> d =3D=3D v)
> 	;
> 	endproperty
> 
> Lisa
> 
> -----Original Message-----
> From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of John
> Havlicek
> Sent: Monday, September 17, 2007 9:10 PM
> To: sv-ac@eda-stds.org
> Subject: [sv-ac] call to vote on Mantis 1668
> 
> Hi Folks:
> 
> This is the call to vote on Mantis 1668, as discussed in
> our last meeting.
> 
> The documents that are being voted on are 1668-2007-09-03.pdf
> and 1668-formal-semantics.pdf on Mantis.
> 
> Please vote if you are eligible.  See the details below.
> 
> Best regards,
> 
> J.H.
> 
> ------------------------------------------------------------------------
> --------------
> 
> Ballot on Mantis 1668=20
> 
> - Called on 2007-09-17, final ballots due by 2007-09-24 T 23:59-07:00.
> 
> 
>  v[xxxxxx-xxxxxxxxxxxxxxxxxxxxxxxx-xx] Doron Bustan (Intel)
>  v[xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx-x] Eduard Cerny (Synopsys)    =20
>  n[-------x-xxx---------x-x-xxx-x---x] Surrendra Dudani (Synopsys)
>  v[-xxxxxxxxx-xx-xxxxx-xxx-xxx-------] Yaniv Fais (Freescale)
>  t[xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx] John Havlicek (Freescale - Chair)
>  v[xxxxxxxxxxxxxxxxrxxxxxxxxxxxxx-xxx] Dmitry Korchemny (Intel -
> Co-Chair)
>  v[-xxx-x--xx--xxxxx----------xx-xxxx] Manisha Kulshrestha (Mentor
> Graphics)
>  n[---------------xxxxx-------x-xx-x-] Jiang Long (Mentor Graphics)
>  n[-------x--xxx.....................] Joseph Lu (Altera)
>  v[xxxx..............................] Johan Martensson (Jasper)
>  n[------------x--x-xx--xx-xxxxxxx-x-] Hillel Miller (Freescale)
>  v[xxxxxxxxxxxxxxx-xxxxxxxx-xxxxxxxxx] Lisa Piper (Cadence)
>  v[xxxxxx-x-xxxxx-x..................] Erik Seligman (Intel)
>  n[--------xxxx-----xxxx-xx----------] Tej Singh (Mentor Graphics)
>  v[--xxxxxxxx-xxxxxxxxxxxxxxxxxxxxxxx] Bassam Tabbara (Synopsys)
>  v[xxxxxxxx-xxxxxxxxxx...............] Tom Thatcher (Sun Microsystems)
>    |---------------------------------- attendance on 2007-09-11
>  |------------------------------------ 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.