[sv-bc] FW: Manti 1345, 1711: unique if/case

Resend. I think the server may not have accepted the original mail.

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, and is
believed to be clean.