Subject: Re: problems with current definition/document
From: Bassam Tabbara (bassam@novas.com)
Date: Tue Jul 23 2002 - 10:41:41 PDT
Thanks Tom for mentioning coverage. Indeed loosely speaking this might
be deemed as a "side-effect", although I would rather make the
distinction that this is an -action- NOT a side-effect. Might seem
trivial...let me explain.
This is not an issue of the assertion itself but rather the -interface-
(assertion access API if you will), which in this case is a trivial one
that allows you to put an action in the pass/fail, and permits you to
access design variables (alternatively, we could restrict that and allow
you to do cnt++ only if cnt is declared as a "coverage" var etc...). So
the interface is a bit permissive, of course like I say that can be
restricted if we wish ... reason why assertion access API is important.
-Bassam.
Tom Fitzpatrick wrote:
>
> Hi Cindy,
>
> > always @(posedge clk)
> > if (state==REQ)
> > @(posedge req1) assert (req2);
> > state = #1 WAIT;
>
> In this example, at posedge clk, if state == REQ, then you'll wait for
> posedge req1 and then assert that req2 is also high. Whether that is true or
> not, state will get WAIT 1 time unit later.
>
> A more accurate assertion that has a side effect, would be
>
> always @(posedge clk)
> if (state == REQ)
> assert (req1) cnt++;
> ...
>
> In this case, the counter cnt will increment each time the assertion passes.
> If cnt is used elsewhere in the design, then it's a side effect. If it's
> not, and only used by coverage, for example, then it's not. Because it could
> be extremely useful to have such a counter for coverage, we were reluctant
> to restrict what could be done in the pass (or fail) statement of an
> assertion. This particular issue is, in my opinion, best left as a lint
> check to ensure that assignments made in assertions do not adversely affect
> the behavior of the rest of the design.
>
> The basic rule is that "the design shall function identically with or
> without the assertion statement", which is why we made the assertions
> nonblocking in the first place.
>
> I agree that side effects are bad. I just don't see how to eliminate them
> from a language design standpoint and still allow useful things like
> coverage counters and such.
>
> Thanks,
> -Tom
> ------------------------------------------------------
> Tom Fitzpatrick
> Director of Technical Marketing
> Co-Design Automation, Inc.
> ------------------------------------------------------
> Email: fitz@co-design.com Mobile: (978)337-7641
> Tel: (978)448-8797 Fax: (561)594-3946
> Web: www.co-design.com
> www.superlog.org
> ------------------------------------------------------
> SUPERLOG = Faster, Smarter Verilog
> ------------------------------------------------------
>
> > -----Original Message-----
> > From: owner-assertion@server.eda.org
> > [mailto:owner-assertion@server.eda.org]On Behalf Of Cindy Eisner
> > Sent: Tuesday, July 23, 2002 6:41 AM
> > To: Bassam Tabbara
> > Cc: Adam Krolnik; assertion@server.eda.org
> > Subject: Re: problems with current definition/document
> >
> >
> >
> > bassam,
> >
> > >For the item below, please note that the assert does NOT block. Does
> > >this answer your question Cindy ? Please refer to LRM, there is an
> > >implicit "process" keyword in the form "process assert ..." i.e. a
> > >separate thread (or instance of an FSM :-)!) is created.
> >
> > ok, thanks. i missed that. the implicit process keyword seems to appear
> > only in the example at the bottom of page 46 and not in the text (although
> > the text does state that the assertion statement itself if non-blocking).
> >
> > that partially answers my question. the real question is: is there some
> > way in which an assertion can have side-effects? i'll give it
> > another try:
> >
> > always @(posedge clk)
> > if (state==REQ)
> > @(posedge req1) assert (req2);
> > state = #1 WAIT;
> >
> > is this example legal sv? the "@(posedge req1)" is now outside of the
> > assertion, so presumably does affect the assignment "state =#1
> > WAIT". if i
> > am wrong, that is good. but the question remains: is there some
> > other way
> > to cause havoc?
> >
> > regards,
> >
> > cindy.
> >
> > Cindy Eisner
> > Formal Methods Group Tel: +972-4-8296-266
> > IBM Haifa Research Laboratory Fax: +972-4-8296-114
> > Haifa 31905, Israel e-mail:
> > eisner@il.ibm.com
> >
> >
> > Bassam Tabbara <bassam@novas.com>@de.ibm.com on 22/07/2002 21:54:27
> >
> > Sent by: bassam@de.ibm.com
> >
> >
> > To: Adam Krolnik <krolnik@lsil.com>
> > cc: Cindy Eisner/Haifa/IBM@IBMIL, assertion@eda.org
> > Subject: Re: problems with current definition/document
> >
> >
> >
> > Thanks Adam, for responding to Cindy. I include a clarification on one
> > item.
> >
> > For the item below, please note that the assert does NOT block. Does
> > this answer your question Cindy ? Please refer to LRM, there is an
> > implicit "process" keyword in the form "process assert ..." i.e. a
> > separate thread (or instance of an FSM :-)!) is created.
> >
> > -Bassam.
> >
> > Adam Krolnik wrote:
> > [...]
> > > >4. the current definition seems to allow the use of assertions in such
> > a
> > > >way that the design itself is affected. for instance, consider this
> > example,
> > > >slightly modified from
> > > > page 46:
> > >
> > > > always @(posedge clk)
> > > > if (state == REQ)
> > > > b7: assert(req1)
> > > > @(posedge clk) assert(gnt)
> > > > @(posedge clk) assert(!req1);
> > > > state = #1 WAIT;
> > >
> > > > i am not sure if this is legal (and my verilog is very rusty, so
> > > > perhaps i have syntax
> > >
> > > There are certain advantages to using the temporal expression within
> > > assertions for verification codes. I have written monitors that used
> > > the temporal expressions from assertions to detect events in the
> > > hardware and send the proper data to the monitor. Another example is
> > > the use of coverage assertions that want to perform certain operations
> > > based on the event being found. Data may be collected, etc.
> > >
> > > But for hardware, you are correct, assertions are expected to have no
> > > side effects. A simulator may even choose to not implement assertion
> > > simulation if desired and this thus should have no negative effect on
> > > the proper outcome (though it may have negative effects when it comes
> > > to improper outcomes - that of taking longer to diagnose the problems.)
> > >
> > >
> > ==================================================================
> > =========
> >
-- Dr. Bassam Tabbara Technical Manager, R&DNovas Software, Inc. bassam@novas.com (408) 467-7893
This archive was generated by hypermail 2b28 : Tue Jul 23 2002 - 10:49:12 PDT