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

From: Bresticker, Shalom <shalom.bresticker_at_.....>
Date: Sun Nov 11 2007 - 09:42:37 PST
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, and is
believed to be clean.
Received on Sun Nov 11 09:46:58 2007

This archive was generated by hypermail 2.1.8 : Sun Nov 11 2007 - 09:47:33 PST