RE: [sv-bc] Mantis 1345: 10.4: "illegal" unique if/case issues

Sigh!

Again that @$!# word "any" was mis-interpeted.

Let me try again.

You wrote, 
"an implementation can evaluate in one order, and report a warning if
that evaluation produced multiple matching case items."

The LRM says that if it finds an 'illegal' interleaving, it shall issue
a warning unless it also finds a 'legal' interleaving. That is, if it
finds both a 'legal' and an 'illegal' interleaving, it is not required
to issue a warning.

My question is, why not?

If it finds (by chance or by intention) an 'illegal' ordering, why
should it not be required to issue a warning even if it happens to find
another ordering which is 'legal'?

(All uses of 'legal' and 'illegal' are in quotes because I don't agree
to the appropriateness of those terms in this context.)

Thanks,
Shalom


> -----Original Message-----
> From: Steven Sharp [mailto:sharp@cadence.com]
> Sent: Monday, February 20, 2006 11:29 PM
> To: Brad.Pierce@synopsys.com; sv-bc@eda.org; Bresticker, Shalom
> Subject: RE: [sv-bc] Mantis 1345: 10.4: "illegal" unique
> if/case issues
> 
> 
> >From: "Bresticker, Shalom" <shalom.bresticker@intel.com>
> 
> >My bad wording. What I meant was, why should a tool not be
> REQUIRED to
> >issue a warning if it finds ANY bad ordering?
> 
> If you are suggesting that the tool be required to produce a
> warning
> if there exists any bad ordering, the answer is that this is
> completely
> impractical.
> 
> The number of orderings increases as the factorial of the
> number of
> case items, which is faster than exponential.  At 16 case
> items, the
> number of orderings to be tried already exceeds 20 trillion
> (2.09E13).
> And trying each new one would require restoring the state of
> all the
> variables that might have been affected by the evaluation.
> 
> If you work through all the messy wording, what it comes down
> to is
> that an implementation can evaluate in one order, and report a
> warning
> if that evaluation produced multiple matching case items.  I
> read the
> wording carefully to make sure that it came down to that.  But
> the
> wording also allows tools to do more if they want.  A formal
> tool might
> take advantage of that.
> 
> If the lack of exhaustive checking bothers you, then don't
> write
> case item expressions that contain side effects.  They don't
> make
> much sense anyway, since unique case items are conceptually
> supposed
> to be evaluatable independently in parallel.  We could forbid
> case item
> expressions with side effects, or state that the results are
> undefined
> in that case.  But if you want to have a tool forbid such
> expressions,
> then you have to define them precisely.
> 
> Steven Sharp
> sharp@cadence.com