RE: [$ieee-1850] Vunit_proposal_6.0.doc

From: N.S. Subramanian <subns_at_.....>
Date: Mon Apr 28 2008 - 08:54:15 PDT
Hi Dmitry, 

My comments inlined.

thanks,
nss
 

-----Original Message-----
From: Dmitry Pidan [mailto:PIDAN1@il.ibm.com] 
Sent: Sunday, April 27, 2008 9:00 PM
To: N.S. Subramanian
Cc: ieee-1850@eda.org; owner-ieee-1850@eda.org
Subject: Re: [$ieee-1850] Vunit_proposal_6.0.doc

  Hi NSS,
  I have a few comments/questions about the proposal:
  1. Section 1, "Verification Units"
      In (b), you say "A verification task related to a design ... , at
least one of which is bound to a design module or instance"
      I am a bit confused what does it mean when unbound vunit inherits
a bound one. I can think about two different approachs, but both are
bad:
     1) Signals in the bound inherited vunit are considered to be
signals from the design according to the binding, while other signals in
the inheriting vunit are
        considered to be unbound
          This approach is bad, since it provides a way to violate
inheritance restriction about hierarchy relationship of instances.
Consider vunit A is bounded to
         u1, vunit B is not bounded and vunit C is bounded to u2.
Instances
u1 and u2 are not related - neither u2 is an instance within u1, nor u1
is an instance within
         u2. Then, B can inherit C (B is not bounded) and A can inherit
B (B is not bounded). From the transitivity of inheritance we get that A
inherits C, while A can
         not inherit C directly, since they are bounded to unconnected
instances - we have an inconsistency
     2) Inheriting vunit inherits also the binding of the inherited
vunit
           This approach is also bad, since if in the previous example B
inherits both A and C we can not determine the binding of B.
     Therefore, I think we should limit the inheritance between unbound
and bound vunit to only the possibility of an unbound vunit to be
inherited by a bound vunit. In this case, all signals in the inherited
unbounded vunit should get the binding of the closest inheriting one. If
you agree, then in
(b) a top level vunit has to be bound.

>>>>NSS: Yes, I agree that an unbound verification unit shall not
inherit a bound verification unit. However an unbound verification unit
may inherit another unbound verification unit. A bound verification unit
may inherit an unbound verification unit in which case the design
signals in the unbound verification unit will get the binding as per the
binding rules of the bound verification unit.

  2. Section 1.2, "Vpkg"
      You say "A vpkg must not contain modeling layer code".
      Didn't we agree that a vpkg must not contain overriding of
signals, but still can contain definitions of auxilliary variables? I
think auxilliary variables are very useful (counters etc.) when writing
reusable properies, since their behaviour can also rely on formal
parameters

>>>>NSS: Yes, auxiliary variables are useful and they are allowed by the
proposal. What makes you think 
        they are not allowed ? Would you like an explicit reference to
auxiliary variables ?

  3. Section 1.2, "Vpkg", Notes:
     You say: "Since a vpkg cannot be bound, either the vpkg as a whole
must be parametrized ... "
     From this statement, one can conclude that every verification unit
that is not bound must be parametrized or contain only parametric
definitions. However, we allow unbound verification units that are not
parametrized - they are just abstract. I suggest to remove "Since a vpkg
cannot be bound".

>>>>NSS: I disagree. vpkg is a special verification unit with unique
characteristics. While the generic
         verification unit rules apply to vpkg it is not true that vpkg
rules govern all verification units.

  4. Section 1.3, "Vmode"
     You say: "A default verification unit may not inherit or
instantiate other verification units of any type"
     There is a reason while vmode default may not inherit other
verification unit - since it is considered as to be explicitly inherited
by all other verification units, if
    it inherits any of them then a circular inheritance is produced,
which is disallowed. However, what is the reason not to allow
instantiation of parametrized vunits
    in vmode default?

>>>>NSS: I think we discussed and agreed to this in the SC. The primary
reason is to disallow a 
    recursive instantiation problem. Consider a vmode V1 that is
instantiated in the default Verification
    unit. Since V1 also inherits the same default verification unit, it
sees an instance of itself in itself,creating
    a recursion. 

  5. Section 2, "Verification units instantiation"
      Shouldn't we add here a note about cross-language semantics for
instantiating/instantiated vunits written using different flavors, like
you do for inheritance and binding?

   >>> NSS: If you think it adds value, we could do this.

  6. Section 4, "Verification unit inheritance"
      If you agree to what I proposed about inheritance relationship
between bound and unbound verification units, then in the restrictions
the following restriction should be added: "an unbound verification unit
can inherit only unbound verification unit"

>>>>> NSS: I agree.

  7. Section 4, "Verification unit inheritance", example of valid use
models:
     - Is it correct that for every use model a reverse version is also
valid if the original one is valid and invalid if the original one is
invalid, i.e. if in the example we replace X and Y the valid and invalid
use models remain the same? If yes, we should mention it.

       >>>NSS: Isn't the bidirectional property addressed by the
wordings in the restrictions section itself ?
       
     - The last invalid example is no more invalid because the
restriction on binding to modules was relaxed.

       >>>> NSS:  Yes, my bad. I will fix this.
  8. Section 9.3, "Direct and indirect name references", Restrictions:
     The first restriction is "A vunit may not be both inherited or
instantiated in any given vunit" 

>>> NSS: I think the wording in the proposal is "...both inherited and
instantiated...."
      a. Why is this restriction appear in this section?

>>> NSS: Which section would you like this to be moved to ?

      b. This restrictions seems to be not exact since it can be
understood from it that a vunit can be at the same time instantiated in
one vunit and inherited in another one, which is not correct. I think it
will be better to say: "A vunit can be either inherited or instantiated,
but not both".

>>>>NSS: A vunit with parameters cannot be inherited because the
association for formals to actuals
does not happen in inheritance. It can only be instantiated. But
otherwise a vunit without parameters may be both instantiated and
inherited. I propose that we only mention that vunits with explicit
parameters cannot be
inherited. I agree that this restriction can be relaxed. 

      c. Since only parameterized vunit can be instantiated (vunit with
empty parameters list is still a parametrized one), and only
non-parametrized vunit can be instantiated, do we need this restriction?

   Regards,
   Dmitry


Dmitry Pidan
Formal Verification Group
IBM Haifa Research Lab.
Lotus Notes: Dmitry Pidan/Haifa/IBM@IBMIL
E-mail: pidan1@il.ibm.com
Phone: 972-4-8296036



 

             "N.S.

             Subramanian"

             <subns@cadence.co
To 
             m>                        <ieee-1850@server.eda.org>

             Sent by:
cc 
             owner-ieee-1850@s

             erver.eda.org
Subject 
                                       [$ieee-1850]
Vunit_proposal_6.0.doc 
 

             23/04/08 17:03

 

 

 

 





 <<Vunit_proposal_6.0.doc>>
Hi SC,

Please find attached version 6.0 of the vunit proposal.

This revision addresses the following.
   a) Dmitry concerns on transitive closure of inherited vunits.
   b) Cindly's concerns on inheritance restrictions when binding
        of vunits to modules versus instances.
   c) Sitvanit's comments on pending items (mail dated 3/24)

The following is not addressed in not addressed by this revision.
  a) Verification task
           - Cadence does not agree to Cindy's proposal here.
              A separate email will discuss that.
  b) abstract keyword
           - After Dmitry's email we feel that the abstract keyword is
             redundant. It does not break backward compatibility
            as the current LRM only mentions that tools are free to
choose
            the binding of unbound vunits, not that they are bound to
            the top module of the design hierarchy.

Please review and send your comments. We can discuss the same in the
issues SC on 4/28.

thanks and regards,
nss



--
This message has been scanned for viruses and dangerous content by
MailScanner, and is believed to be clean.

[attachment "Vunit_proposal_6.0.doc" deleted by Dmitry Pidan/Haifa/IBM]


-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.
Received on Mon Apr 28 08:56:10 2008

This archive was generated by hypermail 2.1.8 : Mon Apr 28 2008 - 08:56:14 PDT