Hi, I have attached a draft (not yet complete) of a proposal to Mantis 1345, which I think addresses the issues I have mentioned, according to approach 6A, which is the more conservative change, being closer to the current LRM. Please review and feed back. The proposal would have to be expanded to cover unique-if as well. Thanks, Shalom ________________________________ From: owner-sv-bc@server.eda.org [mailto:owner-sv-bc@server.eda.org] On Behalf Of Bresticker, Shalom Sent: Sunday, November 11, 2007 7:43 PM To: sv-bc@server.eda.org Subject: RE: [sv-bc] FW: Manti 1345, 1711: unique if/case Hi, Regarding Item 6 below, please indicate whether you prefer option A or option B. Thanks, Shalom ________________________________ From: Bresticker, Shalom Sent: Wednesday, November 07, 2007 10:42 AM To: sv-bc@server.eda.org Subject: Manti 1345, 1711: unique if/case Hi, I've been reviewing the discussions about unique if/case. I have not finished, but I'd like to present what I have so far: 1. The current language is unclear as to whether a tool needs to check different evaluation and comparison orders of case_item expressions, in order to actively look for an order which causes a unique violation/non-violation. It seems to be agreed that the intent was that a tool may choose any order it likes, but it need choose only one, and then the result is whatever it is. The tool need not examine other orders, though it may. (Remember that the LRM only defines simulation semantics. Synthesis or formal property checking tools may choose to work differently, in order to better achieve their purposes.) The language should be rewritten to make that clear. In any case, all the discussion about evaluation and comparison orders seems to be relevant only if any of the case_item expressions have side-effects. (Except that a tool which reports the details of a uniqueness violation might report different locations of the violation, i.e., which case_item expressions, for different orders.) Probably all the simulators evaluate and compare all the non-constant case_item expressions in order anyway (the constant ones can be pre-calculated), if for no other reason than that a plain case and a priority case have to work that way anyway. More on that below. 1A. What if case_items contain multiple expressions? May a tool evaluate an expression of one case_item, jump to an expression of a different case_item, then go back to a second expression of the first case_item? It seems permitted, though probably nobody does it. 2. The LRM says in 1800-2005, "To implement this requirement, an implementation can continue the evaluation of conditions after a first true condition has been found and even after the execution of the statement associated with the first true condition. However, the statements associated with any additional true conditions shall not be executed." Then several people jumped out of their seats and cried, "Gevald!" (in Yiddish), and said that must not be done. So we filed Mantis 1304 to change the LRM so that it will not say that case_item expressions can be evaluated after the execution of the first matching statement. However, in my opinion, the new language, which changed "even after" to "before" is still ambiguous, because it still says that an implementation "can continue ...". "can" implies a capability or an option, but not a requirement. That leaves open the interpretation that one could do otherwise and continue the evaluations after the execution of the first matching statement. I would like to reword that statement to be even clearer. 3. The LRM is ambiguous as to whether the tool must or may continue evaluating additional case_item expressions after finding a uniqueness violation. I suggest that the LRM permit, though not require, stopping after finding a violation. 4. Related is whether a tool is required to report all case_items which match in a uniqueness violation or it can just report the first. I don't think a tool should be required to report all of them. Actually, the LRM does not even require the tool to report the first duplicate case_item. A tool could simply report that a uniqueness violation occurred at time N in design element M (instance name) at line P. That would be enough to allow the user to start debug. I don't think the LRM needs to specify the content of the warning more than it already does. 5. Related is in the case where a case_item contains multiple expressions, whether a tool is required to evaluate the other case_item expressions in the same case_item if the first expression causes a uniqueness violation. I think the answer should be no. Similarly, if a case_item expression is the first match to the case_expression, must the tool evaluate the other case_item expressions in the case_item? Here too, I think the answer should be no. Here too, it is important only for side-effects. 6. Side-effects: Unique is not intended for use with side-effects. In my view, someone who tries it deserves whatever he gets, and probably deserves worse than that. For simplicity, I'd like to suggest one of the following: A. Keep the statement that the case_item expressions can be evaluated and compared in any order, with the statements about optional short-circuiting. If a case_item expression has a side-effect, the side-effect occurs when the expression is evaluated, so no book-keeping needed. Add a statement that if case_item expressions contain side-effects, then because the order is not specified and short-circuiting may or may not occur, it is not determinate which side-effects will occur, and the results may therefore be unexpected and/or undesirable. B. Specify the order of evaluation and comparison to be like that of plain and priority cases, in order of appearance (see also Mantis 1041), except that in unique case, evaluations and comparisons continue after the first match until the end of the case or until a uniqueness violation is found. (Evaluations might still continue even after a violation is found.) Side-effects occur as the case_item expressions are evaluated. Short-circuiting can still occur. Again, without side effects, the order does not matter, so we can arbitrarily decide on the order. Another advantage of this is for debug. Suppose case_items 1, 2, and 3 all match the case_expression in a uniqueness violation. I'd expect the tool to report that there is a multiple match in items 1 and 2 or in items 1, 2, and 3. I'd be surprised if the tool reported that 2 and 3 match without reporting 1, but that could happen if the tool can choose any order. 7. I already mentioned in Mantis 1345 that I dislike the terms "legal" and "illegal" with respect to unique, but that is a separate issue. 8. Most of this applies to unique if as well as to unique case. Disagreements, violent or otherwise? What else does this leave open? Thanks, Shalom Shalom Bresticker Intel Jerusalem LAD DA +972 2 589-6582 +972 54 721-1033 --------------------------------------------------------------------- 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 <http://www.mailscanner.info/> , 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 <http://www.mailscanner.info/> , 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.
This archive was generated by hypermail 2.1.8 : Wed Nov 14 2007 - 02:47:47 PST