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

>From: "Bresticker, Shalom" <shalom.bresticker@intel.com>

>[Shalom] And in unique 'if'. I admit I don't understand all the
>discussion about interleaving orderings in that I don't think it makes a
>difference in any normal case. Is there any such case which is not
>pathological?

Except for the issue in Mantis item 1304, which is just plain wrong,
I would call all the cases where interleaving order matters pathological.
They could all be considered illegal, without losing anything useful.

>I would be happy with deleting all the discussion about
>various orderings from the LRM and even be willing to have the LRM
>specify evaluation in top-down order.

I wouldn't have any problem with that.  Has anyone else implemented
it with a different evaluation order?

I can see the possibility of someone optimizing case statements for
efficient table lookup in a way that effectively alters the evaluation
order.  I can't actually think of any way of doing it in the presence
of the kinds of expressions that could have side effects, but maybe
somebody else could.

Note that specifying top-down isn't enough.  That still leaves open
the question of whether you can short-circuit the evaluation of
multiple case item expressions attached to a single case item as soon
as one of them is true.  Once you know one of them is true, you don't
need to check the rest to know that the item is selected, or to do the
uniqueness check.  But if a later one has a side-effect, then it could
make a difference whether you evaluate it or not.

And then there is the question of whether you can stop evaluating
as soon as you have determined that a warning will be produced, or
whether you need to keep evaluating all the case items.


>What is much more relevant than interleaving ordering, I think, is the
>problem of input constraints. In many cases, uniqueness is a result of
>constraints on the set of legal input combinations and sequences to the
>module. The module is designed according to the assumptions on the input
>constraints. When you give such a module to synthesis, for example, with
>a parallel_case directive ("unique"), you are telling the tool, "You
>cannot know that these combinations are mutually exclusive, but I know
>they are, and I want you to assume that. It is my responsibility to
>ensure that that assumption is fulfilled." How are tools going to react
>to uniqueness assertions in such situations? 

If I understand your question, I think that the answer is that the LRM
specifies the language semantics, which means the behavior of simulation
tools.  It requires such tools to check the 'assertion'.

A formal tool may be attempting to prove the assertion, or assuming it as
an external constraint while it proves other local properties.  Synthesis
will presumably assume the constraint.  Neither of these is really in
the scope of the LRM.


Steven Sharp
sharp@cadence.com