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

Hi John,

but that does not restrict to a variable in general, would be specific
to properties/sequences?

ed 

> -----Original Message-----
> From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On 
> Behalf Of John Havlicek
> Sent: Friday, October 13, 2006 7:18 AM
> To: sv-ac@eda.org
> Subject: 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
> > > 
> > 
>