RE: [sv-bc] illegal priority if

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.

The formal tool processing the same code can use nearly infinite time
and seek a witness path for a set of inputs that would result in
!onehot.

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.. Degenerate examples
include:

unique if (a) f_a();
else if (!a) f_b();

or that we are definately not onehot:

unique if(a) f_a();
else if (a) f_b();

Michael McNamara
mcnamara@cadence.com
408-914-6808 work
408-348-7025 cell


-----Original Message-----
From: Steven Sharp [mailto:sharp] 
Sent: Friday, January 13, 2006 2:58 PM
To: Francoise Martinolle; Brad.Pierce@synopsys.com; sv-bc@eda.org;
Michael (Mac) McNamara
Subject: RE: [sv-bc] illegal priority if


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

>Greg is right that it is only crazy cases where there is any order
dependent 
effect in any case; but the corollary to that is the slow down would
only be 
experienced in those crazy cases, and *gosh* those are the ones I want
to spend 
simulation time on!

This assumes that the simulator can statically detect those crazy cases,
so that it doesn't slow down in other cases.  If it could reliably
detect
those crazy cases, then we could make it illegal to have this kind of
order dependency, and the problem would go away.  But I don't think this
is practical to detect in the general case.  We could put restrictions
in
that would prevent it from happening, but people might not be happy with
those restrictions.

And as far as being willing to spend extra simulation time on those
cases:
we are talking about spending exponential amounts of time.  So I doubt
you
really want to spend the simulation time on it in extreme cases.  If the
sun has burned out before you get your results back, they won't do you
much good.

BTW, defining a required evaluation order would avoid differences
between simulators and give predictable results.  However, it doesn't
really solve the issue between simulators and synthesizers.  Yes, the
synthesizer knows the order the simulator used.  But if the synthesizer
is required to follow that order, then I think it defeats the purpose
of "unique".  As I understand it, "unique" was supposed to mean pretty
much the same thing as "parallel_case".  It tells the synthesis tool
that it can evaluate these things in parallel.  If it has to evaluate
them sequentially to match side effects, then the purpose has been
defeated.

Note that any unique if/case that has an order dependency has inherently
violated this intent of unique, by not being computable in parallel.  So
it could be considered an illegal unique if/case.  The problem is how
are
you going to detect this kind of order dependency in the general case?

Steven Sharp
sharp@cadence.com