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