Hi Lisa, Please, see my answers below. I updated the proposal according to your comments and deposited it to Mantis (checkers_070923dk.pdf). Unfortunately, I cannot attach it to this mail because of its size. Thanks, Dmitry ________________________________ From: Lisa Piper [mailto:piper@cadence.com] Sent: Saturday, September 22, 2007 4:02 AM To: Korchemny, Dmitry; Thomas.Thatcher@Sun.COM Cc: sv-ac@eda-stds.org Subject: RE: [sv-ac] 1900 Checkers Hi Dmitry, I have not completed a review of this yet but I thought I'd share the comments I have so far: 1. In the objectives, there is a typo "thedescription" [Korchemny, Dmitry] Fixed. 2. In syntax 9-1, it references "four statements" but I'm not sure where this count comes from. [Korchemny, Dmitry] Fixed. Deleted "four" from the resulting version. 3. In 16.18.1 - "can be formally proved" -> can be formally proven ... [Korchemny, Dmitry] Fixed, though "proved" and "proven" may be used interchangeably (see also John's comment). 4. 16.18.2 - a. is it intentional that parameters are not allowed in the syntax? [Korchemny, Dmitry] Yes, I omitted them on purpose. I believe that checkers should be consistent with properties, and properties do not have parameters. Essentially, the last sentence is not accurate, and actually both properties and checkers do have parameters, but they have the same syntax as ports. E.g., you can pass to a property the size of its local variables, and to a checker the size of its free variable. It would be cleaner to introduce a special keyword parameter (this was also your suggestion to introduce this or similar keyword for property arguments), but I would prefer to do it in a separate proposal, common for properties and checkers. I am talking about the following syntax: checker(logic a, b, parameter int size); and similarly for properties and sequences. b. The let proposal changes concurrent_assertion _item_declaration to assertion_item_declaration [Korchemny, Dmitry] Fixed and added a note. c. Should the checker_item::= concurrent_assertion_item actually reference the procedural_assertion_statement instead. There is a definition of procedural_assertion_statement in the syntax that is not referenced. [Korchemny, Dmitry] I don't think so. Procedural assertion statements are applicable only in the procedural code, while concurrent_assertion_items are applicable outside of it. The procedural assertion statements are indeed not referenced explicitly in this proposal, but their production should be here, since it says that the checkers may be instantiated in the procedural code wherever concurrent assertions may. d. The subtitle references "Program declaration ..." instead of "Checker declaration ..." [Korchemny, Dmitry] Fixed 5. Why can't a checker be declared in compilation unit scope? In fact, the "simple checker" example seems to use compilation unit scope. [Korchemny, Dmitry] They can. See A.1.2. I also added an explicit note to the main text. 6. I think we should allow them to be declared in a package also (I know you had this as future, but not sure why) [Korchemny, Dmitry] I added this feature to the proposal, it turned out to be a small change. Moreover, it already was implicitly included in the proposal, since (concurrent_)assertion_item contains also checker declaration according to the updated BNF. I agree that the ability to be declared in a package is important for checkers. 7. "referred as checker action blocks" -> "referred to as checker action blocks" [Korchemny, Dmitry] Fixed. 8. "Connections to checker formal arguments can be created by similar means to module ports (see 16.12)" Did you mean to say property arguments. That is what 16.12 references and I think it is more appropriate, although I'm not sure how implicit connections and wildcard port names apply. What do you mean by implicit connections? It would be nice if the design and checker used the same signal names, that you would not have to type in the port list, like a PSL vunit. [Korchemny, Dmitry] I intended using wild card port names as in modules. Using port lists in checkers has its own advantages and drawbacks. The advantage is that you can make a checker generic independent from the module signals - this is a case when you use a checker as an extended library assertion. The drawback is that when you want to use a checker to verify the module (i.e., to use it as a verification unit), you have to pass arguments to it. Using wild card port list provides a partial solution to this problem. Essentially, since the checker is actually inlined into a module, nothing prevents it from using module signals as they are. The subtle point here is that it is not inlined in place of its instantiation, but at the module end. Therefore, checker may not see signals in its instantiation context, if their scope is a block, and not a module. I think this issue requires a further discussion. 9. "The supported data types for checker formal arguments are the same types as in case of properties" -> suggest "Checker formal arguments may have any data type that is legal for a property, and they are processed is a similar way (see 16.12). [Korchemny, Dmitry] Fixed. 10. "and have static lifetime" -> suggest "and are static" [Korchemny, Dmitry] Fixed. 11. "Clock and disable context are may be inherited from the scope of the checker declaration (but see 16.8.3. for usage of context value functions for passing the instantiation context to the checker)." [Korchemny, Dmitry] Lisa, what do you mean by "may be"? The intention is that they always inherit it if it exists, unless the checker redefines it. 12. I think it is going to be confusing to sometimes inherit the context from where it is defined and sometimes from where it is instantiated. I'm not sure I understand the user model for inheriting values from where the checker is defined. I don't see why checkers need to be defined in a module, program, ... [Korchemny, Dmitry] The checker inherits the context from where it is defined and never from where it is instantiated. It can query the instantiation context by means of the context value functions ($inferred_*), and use its values explicitly. The checker inherits context values from where it is defined to be consistent with modules. The checker may be defined in module, etc, when locality is required and for consistency with modules (to tell the truth, I don't think the nested module definition is widely used). On the other hand it is useful to define checker in a checker. 13. page 30 do we need to add a reserved keyword initial_check? [Korchemny, Dmitry] Done. 14. I need to go over page 8-21 again, but I did not see anything about bind. I guess I have to put the checker in a module to be able to bind to it? I could use some more up front information on the use model. I thought this was to be similar to OVL but get around the issues that result from having it conform to a module definition. But if it has to be defined in a module, then how is it used as a general library element? If I define the checker in module a, then how do I reference it from module b? I feel like I'm missing something important. [Korchemny, Dmitry] See my answer in the previous mail and my note to 5). Lisa ________________________________ From: Korchemny, Dmitry [mailto:dmitry.korchemny@intel.com] Sent: Wednesday, September 19, 2007 5:28 AM To: Lisa Piper; Thomas.Thatcher@Sun.COM Cc: sv-ac@eda-stds.org Subject: [sv-ac] 1900 Checkers Hi Lisa, Tom, I uploaded the updated version of the proposal ready for review. This proposal does not contain a description of formal semantics yet. Thanks, Dmitry --------------------------------------------------------------------- Intel Israel (74) Limited This e-mail and any attachments may contain confidential material for the sole use of the intended recipient(s). Any review or distribution by others is strictly prohibited. If you are not the intended recipient, please contact the sender and delete all copies. --------------------------------------------------------------------- Intel Israel (74) Limited This e-mail and any attachments may contain confidential material for the sole use of the intended recipient(s). Any review or distribution by others is strictly prohibited. If you are not the intended recipient, please contact the sender and delete all copies. -- This message has been scanned for viruses and dangerous content by MailScanner, and is believed to be clean.Received on Mon Sep 24 08:39:31 2007
This archive was generated by hypermail 2.1.8 : Mon Sep 24 2007 - 08:39:48 PDT