Hi Mehdi, Neil, I hope I addressed most of your concerns at the meeting, I will summarize my answers here (see below). We will also discuss your comments at the SV-AC meeting. Thanks, Dmitry -----Original Message----- From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org] On Behalf Of Mehdi Mohtashemi Sent: Thursday, March 06, 2008 10:12 AM To: Korchemny, Dmitry Cc: sv-ec@server.eda.org; sv-ac@server.eda.org; Levy, Yossef (DT); john.havlicek@freescale.com Subject: [sv-ec] and [sv-ac] Checkers, and mantis items 2088,2089 Hi Dimitry, and SV-AC members, As you have initiated a review meeting this coming Monday, we wanted to provide a summary of the discussion that took place during our SV-EC conference call on Monday March 3 2008. Our SV-EC committee conducted an email ballot on mantis items 2088 and 2089 based on a request from SV-AC (John had sent the formal request). These mantis items did not pass during email vote as you are aware, there were many discussions on the reflector on the subject. We then had placed 2088/2089 on SV-EC meeting agenda for Monday March 3 2008 and attempted to vote on them. Below we summarize the feedback from SV-EC to SV-AC. -------------------------------------------------------------------- Mantis 2088, 2089 - from SV-AC committee At the meeting both Gordon and Arturo stated that they were now ok with the latest proposals for both of these Mantis items. The changes made by Tom addressed their concerns. Following concerns were raised: - There are concerns about checkers in general. [Korchemny, Dmitry] The usability issue is addresses in the preamble to 1900. - With respect to Checker instantiations in procedural code naming conventions (including cross-module references) [Korchemny, Dmitry] The proposal does not forbid cross-module references. Gord requested to add explicitly that the hierarchical names inside checkers are resolved in the checker declaration context only. Another restriction that should be added is that the hierarchical names referencing checker objects should not be actual arguments of a checker. forces semantics [Korchemny, Dmitry] According to the proposal the checker variable cannot be forced inside a checker (it is not allowed by its grammar). There is no limitation on forcing checker variables outside a checker, therefore their forcing is not different from the forcing of regular variables. The question is what a practical need in forcing checker variables is. It might be a better idea to disallow checker variable forcing (at all) and checker variable assignment outside the checker. is binding allowed? [Korchemny, Dmitry] Yes, it is. See subclause 22.10 in the proposal. General feeling was that the rules for all of these need definition. [Korchemny, Dmitry] See the above comments. - The assertions within checkers seem to be a new class of assertions. They are not concurrent nor immediate. [Korchemny, Dmitry] They are regular concurrent assertions. - There appear to now be 4 types of assertions. Concurrent, immediate, deferred, those inside checkers. [Korchemny, Dmitry] Only 3. See my previous comment. - It could be difficult to deal with all four. [Korchemny, Dmitry] Same. - Checkers can now have untyped formals. This creates new situations as to when certain information becomes available. [Korchemny, Dmitry] This comment needs to be clarified. - Coverage on a freevar seems to now be allowed. This type of coverage appears to be unreliable. Does the simulator just select one of the possible values? Freevars in a simulation environment are very different from a freevar in a formal tool. [Korchemny, Dmitry] I assume that the question relates to "cover property". The "cover property" with free variables will be as reliable in simulation as "assert property": if the imposed assumptions are met, both assert and cover statements with free variables are sound. If a cover point is reachable for an expression containing a free variable then it is reachable for any choice of the values for this free variable in simulation, provided it is compliant with the assumptions. Here is an illustration: free checkvar bit a; cover property (@clk a || !a); This property is covered for any a. If you substitute a by any value at any time, the cover point will still be reached. - Checkers are adding several new keywords that could clash with the names of existing variables. [Korchemny, Dmitry] As far as I can see the only problematic keyword is "free". We will discuss the alternatives. Attempt to vote on approving the proposal for Mantis 2088 failed, here is the details: Move: Arturo - approve the proposal for Mantis item 2088 Second: Steven Abstain: Gordon Ray - not against the proposal for Mantis item 2088 Steven - wants the whole group of checker proposals to be reviewed by the SV-EC as a group. Francoise - not sure how the coverage will be calculated Opposed: Cliff, Don, Heath, Dave Rich - same reason as Steven (Stu - would have also voted no if he had voting rights.) In Favor: Arturo, Neil, Mark Hartoog, David Scott 12 attendees with voting rights were on-line. Motion failed: 4-yes,4-no,4-abstains More discussion continued after the above vote was concluded. Some of the feedback from the SV-AC on questions raised on 2088 and 2089 was to look at the proposals from other SV-AC Mantis items. Some SV-EC meeting participants felt that a larger group of SV-AC mantis items should be reviewed as a group; that is a whole set of Mantis items that pertain to checkers should be reviewed as a group instead of trying to review 2088 and 2089 in isolation. Their concern is with checkers in general and not with 2088 and 2089 in particular. The following list was proposed (although there may be others): 1900, 1549, 1681, 1648, 1728, 1682, 2088, 2089 Some of the statements and concerns by attendees: There is a concern that checkers are crossing over into the rest of the language. When the proposals from the SV-AC are contained within the area of assertions, there is less of a concern. For some of the changes being made a cross-committee group would have been more appropriate. Procedural code seemed to have had created a particular concern. [Korchemny, Dmitry] See my answer to Steven. There appears to be disagreement within the SV-EC as to whether checkers are part of the procedural code or not. [Korchemny, Dmitry] The checkers may be instantiated in procedural code, but they are not part of this procedural code where they are instantiated. The checker instantiation in a procedural code is kind of "syntactic sugaring" only. Although some members are concerned that there are issues that need to be addressed but aren't sure yet. They are looking for a way to be convinced that there are no additional issues that need to be addressed. The members who voted No and abstained felt that if these issues are not addressed now they are likely to show up as a ballot issue and at that point in time there will be less flexibility in how to address them. There appears to be a concern that more of a synthesis-centric viewpoint is leading these proposals in SV-AC. In general having others review the proposals in detail would be useful. Mehdi and Neil March 5 2008 ------------------------------------------------------------------------ ------ -- This message has been scanned for viruses and dangerous content by MailScanner, and is believed to be clean. --------------------------------------------------------------------- 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 Thu Mar 13 10:05:13 2008
This archive was generated by hypermail 2.1.8 : Thu Mar 13 2008 - 10:05:45 PDT