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

On Mon, Nov 08, 2004 at 01:07:06PM +0200, Shalom Bresticker wrote:
> The checks performed by the static formal verification tools are usually
> cycle-based.
> I mean that they ignore delays, intermediate values, etc.

Exactly.

> 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.

Writing in explicitly non-unique

> 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.

Indeed, I've read Cliff's papers on the assigns. What I was looking for was a
way to avoid glitches. What is required is a way to make sure all the bits of
the selector change at the same time, if at all. VHDL's event model would do
this automcatically, but how can you get Verilog to do it? You could defer
the uniqueness check to the "Observed" stage of the event queue, so it was
only run on the last value of the case statement selector. Would that work?

>
> 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
>
>

-- 
-- 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