Subject: comments on pages 66-78
From: Adriana Maggiore (adriana.maggiore@transeda.com)
Date: Fri Oct 18 2002 - 10:34:18 PDT
page 71 - 7.2.2 Verification unit binding
Does the binding affect identifiers other than signals? That is, does it
modify property, sequence and endpoint names?
For example:
vunit V (top.i1) {
sequence S = {a;b;c};
cover S;
}
Is this equivalent to the following?
vunit V1 {
sequence top.i1.S = {top.i1.a;top.i1.b;top.i1.c};
cover top.S;
}
I raised this question some time ago; this is an extract from Cindy's
reply:
>>Can vunits in an inheritance relationship be linked to different
>>top level modules?
>>For example
>>vunit A (mod1)
>>{
>> sequence S := {x; y};
>>}
>>
>>vunit B (mod2)
>>{
>> inherit A;
>> cover {a; S; b}
>>}
>>
>>the sequence to cover would be
>> {mod2.a; mod1.x; mod1.y; mod2.b}
>>Is this allowed?
>yes and no. according to the macro expansion view of linking, vunit A
>above is equivalent to:
>
>vunit A
>{
> sequence mod1.S := (mod1.x; mod1.y};
>}
>
>and vunit B is equivalent to:
>
>vunit B
>{
> inherit A;
> cover {mod2.a; mod2.S; mod2.b};
>}
>then, you obviously don't get what you want, because you have defined
>mod1.S but used mod2.S. the solution is *not* that named properties,
>sequences, etc. don't get the prefix, because that causes all kinds of
>chicken and egg problems: an identifier in a vunit may come from the vunit
>itself, from an inherited vunit, from the default vunit, or from the design
>- how do you decide what an identifer is (i.e., whether S is a signal or a
>named sequence) if you don't know where it comes from? but where it comes
>from is exactly the problem we are trying to solve here.
>
>so, we have the no. currently, the definition does not allow you to do
>this. however, there is an easy way to get yes. it is to have an escape
>from the binding. escaping an identifier would prevent it being bound.
>then, you could escape both uses of of the identifier S above, and get what
>you want. this is the kind of minor change we were looking for in the
>current round of discussion, i think.
My suggestion is that we state clearly that the binding affects all the
identifiers.
page 73 - 7.2.4 Verification unit scoping rules
The scoping rules are defined with respect to signals. Nothing is said
about other declarations (properties, sequences and endpoints).
Can a property declaration be inherited?
Can a property be redeclared?
For example:
vunit Base {
property P = always (x -> y);
}
vunit Derived {
inherit Base;
property P = always (x until y);
assert P;
}
Is this example legal? I think it is, but we need to extend the scoping
rules to cover more than just signals.
***********************************************************************
page 75, line 5
This line says:
"The modeling layer is also used to give names to properties and other
entities
from the temporal layer."
Property, sequence and endpoint declarations are now part of the
temporal
layer.
page 75, line 20
It says :
"- named properties, SEREs and SERE endpoints"
I think it should be removed.
********************************************************************
page 76 line 23
" ... as s1.w2, s1.w2, etc." should be " ... as s1.w1, s1.w2, etc."
********************************************************************
page 77 (built-in functions)
For "rose" and "fell" we say that they are the same as "posedge"
and "negedge", respectively.
It looks like they are redundant in the Verilog flavor, so I think
that we should remove them.
"prev"
I'm not sure if I understand what "previous (latched) value of
and expression" means.
Is "prev(a & b)" legal?
"next"
I think we should show a legal usage of "next" in the example.
built-in functions and "time tick"
"prev", "next", etc. are defined in terms of time ticks as seen by
the verification tool. To me this means that if the built-in functions
are used in unclocked properties, we can expect different results
from different tools. Should the usage in unclocked properties
be discouraged?
Best regards,
Adriana
-- Adriana Maggiore TransEDA Tel: +44 (0)23 80 683523 4th floor, Black Horse House Fax: +44 (0)23 80 650805 Leigh Road, Eastleigh adriana.maggiore@transeda.com Hampshire, SO50 9FH, UK
This archive was generated by hypermail 2b28 : Fri Oct 18 2002 - 10:35:36 PDT