RE: [sv-bc] illegal priority if

>From: "Michael \(Mac\) McNamara" <mcnamara@cadence.com>

>Perhaps, then, the unique if construct is reduced to primarily being a
>directive to a formal verification tool, and the simulator mostly
>ignores it, except for pointing out cases where the order it picked
>results in !onehot.

Yes, though I don't consider it that much of a reduction.  If the
simulator has been "reduced" to only catching problems in 99.9% of
design styles (those that don't have an order dependency), I wouldn't
call that "mostly ignoring it".

Note that the capabilities of a simulator are already less than a
formal tool in a much more significant way.  A simulator can only
verify the uniqueness property for the particular set of stimulus
that has been applied.  If the tester has missed the input combination
that violates uniqueness, the simulator won't point out the problem.
A formal tool can try to prove uniqueness for all possible inputs.

The fact that a simulator will only check uniqueness for the set of
inputs simulated is a more significant limitation than the fact that
it also only checks it for a particular evaluation order (which will
be irrelevant for most coding styles).


>Note that it is possible to detect situations using regular dataflow
>analysis of just the module,  where the various conditional terms are
>mutually exclusive, or precisely the same, and hence know that there is
>no possibility for other than onehot or allhot.

It is also possible to detect some situations where there is an order
dependency in the evaluation.  I think it would be reasonable to allow
a tool to declare a violation of uniqueness in that case, even if it
couldn't result in two conditions being true with any evaluation order.
It is a violation of the intent to specify parallel logic.  However, it
is not reasonable to require a tool to detect order dependencies, only
to allow it.


Steven Sharp
sharp@cadence.com