Re: [sv-bc] illegal priority if

The degenerate cases (even some that cross module boundaries) can
usually be worked out as "parallel" even if the designer does not
claim they are "unique".  The "unique" keyword exists for the benefit of
the doubtful cases.  Existing practice was to persuade synthesis
(or post process its output) to eliminate the priority logic from
a chain of selector activations.  This was done with pragmas, comments,
or scripting outside of the source code.  So both simulators
and formal verifiers were usually blindsided.

   SV exists to capture design intent.

   Here the designer is claiming something strong about
conditions in the active circuit.  This may be something that can
be formally proved by examining the whole design, or it might be true
only because of application-specific knowledge that is not represented
anywhere in the design source code!  In either case, the designer is
trying to apply this meta-knowledge to optimize the case selection.
He's specifying (potentially) non-deterministic behavior, but has
reason to think that, in practice, his design is deterministic.
The LRM asks the simulator to check, on each use, whether any evidence
contrary to his claim emerges.  This is what simulators do everywhere
else: they are used to "see if" the machine can be driven through its
paces and not outside feasible bounds of operation.  When all the
runs are done, they cannot guarantee that other runs wouldn't find
something surprising... so the nature of simulators is not really
being violated here - their expressive power just went up a notch.

We say that non-onehot uses of unique are "illegal" because, formally
speaking, they require non-deterministic simulator behavior, which
cannot be delivered.  The simulator "warns" when it must discard an
alternative simulation control flow.  Some users will promote this
to an error.  Unlike managers, who must choose one policy, a standards
body is only trying to make all interesting policies expressible in
a standard way.

   SV's hype is that it unifies test, simulation, synthesis, and
verification languages.  "Unique" is a synthesis feature
that has always been hard to shoehorn into the other points of view,
but was widely used nonetheless.  By standardizing it, the market is
challenged to do whatever can be done to integrate this too.

Like I said, as long as designers believe that a set of signals can
BE $onehot(), they will build hardware to exploit it.  SV standardized
a notation for doing this.   If you don't like this language feature,
you really need to convince users that they are trusting in a false
prophet.  I think your continuous assert( $onehot( {a,b,c} ) ) would
do a lot to surprise designers on this subject.  But I suspect that
the extra tests in unique case will be activated just as often as
the assert, and will catch nearly all the mistakes that currently
slip past when the simulator ignores synthesis directives.  I foresee net
quality increasing, but never 100% perfect.  That's life.

Greg Jaxon


Michael (Mac) McNamara wrote:
> 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