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

Hi Hillel,

I think John's proposal addresses your issue.

Thanks,
Dmitry

-----Original Message-----
From: Miller Hillel-R53776 [mailto:r53776@freescale.com] 
Sent: Friday, October 13, 2006 11:06 AM
To: Eduard Cerny; Korchemny, Dmitry; sv-ac@eda.org
Cc: Miller Hillel-R53776
Subject: RE: [sv-ac] IEEE 1800 SV-AC : minutes of meeting on 10/10 2006

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
>