Subject: Re: problems with current definition/document
From: Bassam Tabbara (bassam@novas.com)
Date: Tue Jul 23 2002 - 10:28:35 PDT
There shouldn't be any side-effects since it's non-blocking (no
assignments/no force ... either). Of course, -any statement- (assert or
otherwise) will inherit and be affected by the context it is in (what is
"outside" of it as you state)... In general block level asserts would be
"inserted" in the right context. If on the other hand you want to
specify a complex assertion (of a behavior implicit in the design say
for example) you can always have an always block island to freely
describe the assertion (preconditions and all).
-Bassam.
Cindy Eisner wrote:
>
> 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:30:43 PDT