Re: [sv-bc] Errata in SV 3.1a LRM Section 18.4: inconsistent use of error and warning

Hi,

The checks performed by the static formal verification tools are usually
cycle-based.
I mean that they ignore delays, intermediate values, etc.

What some people do is to write in the case something like

test_for_unique_condition_not_true: output = 1'bx ;

and then it does not matter if it happens for a moment because in the next time
step
it gets its proper value.

Nonblocking (no hyphen, ask Cliff) assignments are good for storage element
outputs,
then are not so good for combinational logic outputs.
Just the other day, I found a bug in code someone wrote due to using nonblocking
assignments
in combinational logic. Lucky for us, our linter found it.

Shalom

Andrew MacCormack wrote:

> Dave Rich wrote:
> > There already is a way to do this:
> >
> > always @(posedge clk)
> > if (resten)
> > begin end
> > else
> > unique case (sel)
> > val1: etc...
> > endcase
>
> What I was suggesting was to make the reset and clock conditions apply to the
> unique assertion, but not to the case statement. The much beloved and
> misunderstood Verilog event model makes is easy for an always_comb unique case
> statement to get glitches in the case selector.
>
> Perhaps what we really want is that there is a defined name for the implicit
> assertion created by the unique keyword, so that $asserton/$assertoff can be
> used, this wouldn't require any syntax change.
>
> On Fri, Nov 05, 2004 at 12:15:13PM -0800, Greg Jaxon wrote:
> > The way I view "unique" is this: synthesis is going to assume that it
> > has a one-hot set of signals driving some selectors. The user would like
> > confirmation
> > that this (derived) signal set is indeed one-hot over some time intervals.
> > A simulation compiler should help him construct that assertion and test it
> > throughout
> > the relevant time period. I realize that pinning down what this means is
> > the heart of the matter, and I am personally not a bit savvy about
> > simulation,
> > so I cannot do it. What do users do now to get simulators to check their
> > "parallel case / full case" directives? Is there some bullet-proof recipe
> > for adding checks that we can standardize? Failing that, is there anything
> > close enough?
>
> A static formal check is the best way to do this. It doesn't rely on
> simulation hitting the right vector. There are already tools that do such
> checks on the full case pragma on the market and maybe even ones that check
> the SystemVerilog syntax, too. But this can be computationally expensive if
> there is a lot of state involved.
>
> If ABV is turned on in NC, it automatically creates assertions for full case
> and parallel case pragmas.
>
> I agree that it is essential that simulation and synthesis "match" for these
> keyword, otherwise we might as well stick with pragmas. This is why I think
> that a failure of unique/priority should be something more than a warning, but
> that there should be a way to eliminate false negatives.
>
> Maybe SV user's coding standards should say that case statements should only
> use variables that are driven by non-blocking assigns as selectors. Am I
> correct in thinking that this would eliminate the risk of glitches?
>
> --
> -- Andrew MacCormack andrewm@cadence.com
> -- Senior Design Engineer Phone: +44 1506 595360
> -- Cadence Design Foundry http://www.cadence.com/designfoundry
> -- Alba Campus, Livingston EH54 7HH, UK Fax: +44 1506 595959

--
Shalom Bresticker                        Shalom.Bresticker @freescale.com
Design & Verification Methodology                    Tel: +972 9  9522268
Freescale Semiconductor Israel, Ltd.                 Fax: +972 9  9522890
POB 2208, Herzlia 46120, ISRAEL                     Cell: +972 50 5441478
[ ]Freescale Internal Use Only      [ ]Freescale Confidential Proprietary