Hi NSS, 2. Section 1.2, "Vpkg" >>>>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 ? I think, the statement "A vpkg must not contain modeling layer code" explicitly says that there is no ability to define auxilliary variables in vpkg, since every code that does not fail under boolean, temporal, or verification layer is modeling layer, including definition of auxilliary variables. I suggest to change this restriction to "A vpkg must not override signals" 4. Section 1.3, "Vmode" >>>>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. I see your point. This causes me to think that the problem is even deeper that I thought and we may discuss it in the subcommitee meeting. Consider some collection of parametrized vunits that implements commonly used checks. If this collection is used in the particular verification environment, then by the current proposal every vunit in this collection will inherit a vmode default of this specific verification environment, which I don't think will be an intention of the user and may break the original semantics of the vunits in the collection. I think we should somehow address this problem. One possible way can be a definition that vmode default is inherited only by bounded verification units. What do you think? 5. Section 2, "Verification units instantiation" >>> NSS: If you think it adds value, we could do this. (your answer about cross-language semantics for instantiation) I mentioned this just because for inheritance and binding it is said explicitly that vunits/entities of different language/flavors can be connected. I think for a consistency we should say this also for an instantiation. 7. Section 4, "Verification unit inheritance", example of valid use models: >>>NSS: Isn't the bidirectional property addressed by the wordings in the restrictions section itself ? I think we should say explicitly in the examples that they are correct in both ways (also replacing X and Y), otherwise the example is confusing since it gives an impression of one way only. 8. Section 9.3, "Direct and indirect name references", Restrictions: The first restriction is "A vunit may not be both inherited and instantiated in any given vunit" >>> NSS: Which section would you like this to be moved to ? I think restrictions in Section 1 "Verification Units" is a more appropriate place for it. >>>>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. Do we need at all vunit that can be both inherited and instantiated? My understanding is that vunit either does not contain parameters list and then this vunit should be only inherited or contains parameters list (which can be empty) and then this vunit should be only instantiated. 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> Dmitry Pidan/Haifa/IBM@IBMIL cc 28/04/08 18:54 <ieee-1850@eda.org>, <owner-ieee-1850@eda.org> Subject RE: [$ieee-1850] Vunit_proposal_6.0.doc 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 Tue Apr 29 06:26:05 2008
This archive was generated by hypermail 2.1.8 : Tue Apr 29 2008 - 06:26:16 PDT