Re: [sv-bc] illegal priority if

Mac,

    I am also sorry that this language feature cannot offer more certainty
than it does, but I don't think the situation is as grim as you portray.
To begin with, simulation can only detect errors in the handling of the
the test patterns that are actually simulated.  So we have lots of
"illegal" things that go undetected everyday right now, with V2K.  Every
source of non-determinacy sets up a similar predicament.

Illegal RTL is still worth defining (and exorcising) even if not every
tool or every run of one tool detects it - precisely because code that
permits too many interpretations is not sound, portable "design".
If your simulator misses uniqueness violations too often, you may need a more
scrupulous simulator.  The alternative is for the LRM to require that N
distinct evaluation orders satisfy uniqueness for some N>1.  This just
drives up the average cost of simulating unique cases until everyone
stops using them.  Even asking for 1 full inspection (which is what the
LRM tries to require) is causing moans and groans - despite everyone's
hunch that doing this will catch >80% of problematic codes.
In some ideal world, all SV implementations behave exactly
the same, but less-ideal states are nearly as valuable.  Until we
can prescribe an ideal way to unequivocally detect $onehot it seems
wise to just ask the marketplace to do its best.

General relativity and quantum uncertainty might ultimately prevent a
set of signals from being $onehot in every frame of reference!  If that
ever stops designers from believing in unique case, they will vote it
out of the LRM.

"Unique" may be a bad solution, but if it's worth doing; it's even worth
doing badly.  If it's /really/ worth doing, someone will figure out
how to do it /really/ well.

The synthesis engines aren't going to lose any sleep trying to guess
how the simulator made a bus be $onehot: they will synthesize
onehot branching and the gate-level simulation might or might not
deliver a confirming result.  Formal verifiers aren't likely to
adopt "simulation semantics" here - they can state and test the formal
assertion of onehotness without appealing to evaluation order at all.
In this sense they will probably become the highest arbiters of
"legal vs illegal" RTL - if the problems are tractable.  When they aren't,
the simulator checks are your only hope.


Greg Jaxon


Michael (Mac) McNamara wrote:
> I see where one might interpreter the words in the standard that way.  
> 
> However, it would be much better if your language was used rather than the convoluted construction we have today!
> 
> Taking the spec to mean precisely they way you have clarified it, there are still issues:
> 
> The first sentence: "A unique if shall be illegal if, for any such interleaving of evaluation and use of the conditions, more than one condition is true. " unequivocally defines a class of unique ifs which are "illegal"
> 
> The second sentence : "For an illegal unique if, an implementation shall be required to issue a warning, unless it can demonstrate a legal interleaving so that no more than one condition is
> true." differentiates between those illegal if's for which there is a discovered path that does not result in a contradiction with the "unique", and those for which there is no such path (at all, or such that happened to be discovered) and has the effect of the later to be something that requires a warning, but the former do not require a warning.  This is like the rule in Ice Hockey: If the umpire didn't see it, there is no penalty.  [Must the simulator actually demonstrate the legal order of evaluation, perhaps under a verbose switch??]
> 
> I am imagining that the committee worded it this way so as to create the smallest burden on the simulator implementer: pick an order, evaluate the terms, and if more than one are true, issue a warning. Don't bother considering other orders of evaluation.
> 
> However, this does result in a disservice to the synthesis implementer: there is no way for the synthesis programmer to know what order was chosen by the simulator programmer, and hence to generate gates which match the results simulated by the simulator. 
> 
> Moreover, this becomes yet another place where two simulators could give different results for the same design & stimulus, and yet both be standard compliant.
> 
> 
> 
> Michael McNamara
> mcnamara@cadence.com
> 408-914-6808 work
> 408-348-7025 cell
> 
> 
> -----Original Message-----
> From: owner-sv-bc@eda.org [mailto:owner-sv-bc@eda.org] On Behalf Of Brad Pierce
> Sent: Thursday, January 12, 2006 1:58 PM
> To: sv-bc@eda.org
> Subject: Re: [sv-bc] illegal priority if
> 
> No, the tool is required to try it one way.  If there is no uniqueness violation, then it doesn't warn.  If there is a uniqueness violation, it warns.
> 
> -- Brad
> 
> -----Original Message-----
> From: Michael (Mac) McNamara [mailto:mcnamara@cadence.com] 
> Sent: Thursday, January 12, 2006 1:47 PM
> To: Brad Pierce; sv-bc@eda.org
> Subject: RE: [sv-bc] illegal priority if
> 
> But is this leniency useful?
> 
> Doesn't it imply the synthesis must also implement the leniency in gates somehow?
> 
> Doesn't it require the simulator to evaluate as many possible orders of evaluation until a
> order is discovered which results in a unique evaluation is obtained, while doing so in a back tracking, non side-effect manner (the condition functions can't call $display, any global variables must be restored, no processes can be scheduled basd on these speculative evaluations)
> 
> Bottom line: who wants this leniency? Do you want to put it in your design tools? Do users want such logic in their silicon?
> 
> Michael McNamara
> mcnamara@cadence.com
> 408-914-6808 work
> 408-348-7025 cell
> 
> 
> -----Original Message-----
> From: owner-sv-bc@eda.org [mailto:owner-sv-bc@eda.org] On Behalf Of Brad Pierce
> Sent: Thursday, January 12, 2006 1:14 PM
> To: sv-bc@eda.org
> Subject: Re: [sv-bc] illegal priority if
> 
> It means that if the tool finds such a sequence, then a warning is not required.  So the tool is not required to prove whether the unique if is legal, but the tool is required to do some due diligence.
> 
> -- Brad
> 
> -----Original Message-----
> From: owner-sv-bc@eda.org [mailto:owner-sv-bc@eda.org] On Behalf Of francoise martinolle
> Sent: Thursday, January 12, 2006 10:49 AM
> To: 'Bresticker, Shalom'; sv-bc@eda.org
> Subject: RE: [sv-bc] illegal priority if
> 
>  
> I do not understand what it means "interleaving evaluation and *use* of the
> conditions".
> Also what is the meaning of the sentence "unless it can demonstrate a legal
> interleaving so that no more than 
> one condition is true"?
> Does it mean that if I found 1 sequence of evaluation of each condition in
> the branches that
> does not make more than one condition true, the unique if is correct?
> 
> -----Original Message-----
> From: owner-sv-bc@eda.org [mailto:owner-sv-bc@eda.org] On Behalf Of
> Bresticker, Shalom
> Sent: Thursday, January 12, 2006 8:20 AM
> To: sv-bc@eda.org
> Subject: [sv-bc] illegal priority if
> 
> Question:
> 
> 1800 10.4 says, 
> 
> "A unique if shall be illegal if, for any such interleaving of evaluation
> and use of the conditions, more than one condition is true. For an illegal
> unique if, an implementation shall be required to issue a warning, unless it
> can demonstrate a legal interleaving so that no more than one condition is
> true."
> 
> What is the meaning of this "illegality"?
> 
> Generally, "illegal" means a fatal compile-time error or something similar.
> Is that really the meaning here? Or is the meaning simply that a warning (or
> error, for strict people) message needs to be issued? 
> 
> I hope my question is clear.
> 
> Thanks,
> Shalom
> 
> 
> Shalom Bresticker
> Intel Jerusalem LAD DA
> +972 2 589-6852
> +972 54 721-1033
> I don't represent Intel 
> 
> 
> 
> 
> 
> 
>