Re: [sv-ac] IEEE 1800 SV-AC : minutes of meeting on 10/10 2006

Hi All:

I am not tracking this discussion yet, but I have envisioned using
argument direction "output" or "inout" for specifying that a formal 
argument must be bound to an actual argument that is a local variable.

J.H.

> X-Authentication-Warning: server.eda-stds.org: majordom set sender to owner-sv-ac@eda.org using -f
> X-MIMEOLE: Produced By Microsoft Exchange V6.5
> Content-class: urn:content-classes:message
> Date: Fri, 13 Oct 2006 11:06:23 +0200
> X-MS-Has-Attach: 
> X-MS-TNEF-Correlator: 
> Thread-Topic: [sv-ac] IEEE 1800 SV-AC : minutes of meeting on 10/10 2006
> Thread-index: Acbsk50COrJUBI3iQfufOxS3GcaIZgAbe6+AADM5SDAAEENIYAAlvJpg
> From: "Miller Hillel-R53776" <r53776@freescale.com>
> Cc: "Miller Hillel-R53776" <r53776@freescale.com>
> X-MIME-Autoconverted: from quoted-printable to 8bit by server.eda-stds.org id k9D96V4Q011340
> Sender: owner-sv-ac@eda.org
> X-OriginalArrivalTime: 13 Oct 2006 09:06:58.0362 (UTC) FILETIME=[EFE8A1A0:01C6EEA6]
> 
> Ed, Dmitry
> 
> The user will still need to guess that 'lv' is a local variable given
> the sequences s2 and s1. For example he would need to pass a variable
> and not an expression. We do not have an explicit way of specifying that
> a formal parameter needs to be local.
> 
> Thanks
> Hillel
> 
> 
> -----Original Message-----
> From: Eduard Cerny [mailto:Eduard.Cerny@synopsys.com] 
> Sent: Thursday, October 12, 2006 5:03 PM
> To: Korchemny, Dmitry; Miller Hillel-R53776; Eduard Cerny; sv-ac@eda.org
> Subject: RE: [sv-ac] IEEE 1800 SV-AC : minutes of meeting on 10/10 2006
> 
> Hi Dmitry,
> 
> the form using existing rules that you have at the end would be OK, it
> seems to me 
> 
> ed 
> 
> > -----Original Message-----
> > From: Korchemny, Dmitry [mailto:dmitry.korchemny@intel.com]
> > Sent: Thursday, October 12, 2006 3:56 AM
> > To: Miller Hillel-R53776; Eduard Cerny; sv-ac@eda.org
> > Subject: RE: [sv-ac] IEEE 1800 SV-AC : minutes of meeting on 10/10 
> > 2006
> > 
> > Hi Hillel, Ed,
> > 
> > I think everything used in a sequence/property should be (implicitly) 
> > defined before its usage. I.e., it should be:
> > * a sequence/property argument
> > * a sequence local variable
> > * objects visible in sequence/property from outside (as stated in the
> > LRM: Variables used in a sequence that are not formal arguments to the
> 
> > sequence are resolved according to the scoping rules from the scope in
> 
> > which the sequence is declared.)
> > 
> > In the below example lv is not visible in p, and therefore should be 
> > forbidden.
> > 
> > I would like to understand where this example comes from.
> > 
> > If it is pure theoretic, we can just forbid such cases (the easiest 
> > solution).
> > 
> > If the goal is to divide a big sequence into parts for better 
> > modularity, the natural solution would be to allow nested sequences. 
> > In this case your example will look like:
> > 
> > property p;
> > 	int lv;
> > 
> > 	sequence s1;
> >   		(exp1, lv = exp2);
> > 	endsequence
> > 
> > 	sequence s2;
> > 		s ##1 (lv == exp3);
> > 	endsequence
> > 
> > 	s2;
> > endproperty
> > 
> > If the goal is to provide a generic solution, we need a mean to 
> > specify a type of the name of a sequence as an argument. If we assume 
> > a functional notation (I am not suggesting it as an actual sequence, 
> > just want to be precise): int -> sequence, then you example will look 
> > like:
> > 
> > sequence s1(int flv);
> >   (exp1, flv = exp2);
> > endsequence
> > 
> > sequence s2(int->sequence s);
> >   int lv;
> >   s(lv) ##1 (lv == exp3);
> > endsequence
> > 
> > property p;
> >   s2(s1);
> > endproperty
> > 
> > Explanation: sequence s2 has an argument which is a NAME of sequence 
> > having one integer argument. In property p we pass to s2 a NAME of s1,
> 
> > and not the SEQUENCE s1.
> > 
> > We should consider a type sequence proposed by Lisa not as a template 
> > of a sequence, but as a result of a sequence. We have a similar 
> > situation with functions: f(g(x)) - f takes a result of the 
> > application of a function g to its argument x, and not the function 
> > itself. If we want to APPLY a function g inside f, we should pass the 
> > NAME of the function (in C it will be a pointer to the function).
> > 
> > But again, as a user I would just rewrite your example as:
> > 
> > sequence s1(int flv);
> >   (exp1, flv = exp2);
> > endsequence
> > 
> > sequence s2(sequence s, int lv);
> >   s(lv) ##1 (lv == exp3);
> > endsequence
> > 
> > property p;
> >   int lv;
> >   s2(s1(lv));
> > endproperty
> > 
> > using existing SVA rules.
> > 
> > Thanks,
> > Dmitry
> > 
> > -----Original Message-----
> > From: owner-sv-ac@server.eda.org
> > [mailto:owner-sv-ac@server.eda.org] On Behalf Of Miller Hillel-R53776
> > Sent: Wednesday, October 11, 2006 9:31 AM
> > To: Eduard Cerny; sv-ac@server.eda.org
> > Subject: RE: [sv-ac] IEEE 1800 SV-AC : minutes of meeting on 10/10 
> > 2006
> > 
> > Ed,
> > 
> > I think the intention is not to provide formal/actual arguments of a 
> > sequence when specifying a sequence as formal type. As doron an dmitry
> 
> > said the formal argument should not include the signiture.
> > The sequence
> > type can be assigned with any legal sequence instance. So the example 
> > should reduce down to this.
> > 
> > sequence s1(int flv);
> >   (exp1, flv = exp2);
> > endsequence
> > 
> > sequence s2(sequence s); // formal arg on a formal arg?
> >   int lv;
> >   s ##1 (lv == exp3); // lv as arg??
> > endsequence
> > property p;
> >   s2(s1(lv));
> > endproperty
> > 
> > My concern in this example is that the user whom is using the sequence
> > s2 needs to be aware of s2's local variables .  If we do:
> > 
> > property p;
> >   s2(s1(lv_arg));
> > endproperty
> > 
> > Will this result in a undeclared variable error?
> > 
> > If this is the case then this use model is problematic from a language
> 
> > perspective.
> > I think it is generally expected in a modular programming framework to
> 
> > have a well defined interface as part of the code, that is, in this 
> > example one would need to specify how to use sequence s2. Not having 
> > the name of the local variable specified in the header of the sequence
> 
> > does not pack the sequence s2 well for external usage.
> > 
> > Thanks
> > Hillel
> > 
> > -----Original Message-----
> > From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of 
> > Eduard Cerny
> > Sent: Tuesday, October 10, 2006 7:44 PM
> > To: sv-ac@eda.org
> > Subject: [sv-ac] IEEE 1800 SV-AC : minutes of meeting on 10/10 2006
> > 
> > Please find attached the minutes of the SV-AC meeting earlier today. 
> > Let me know if you see any discrepancies.
> > 
> > Best regards,
> > ed
> > 
>