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
>