Subject: Re: problems with current definition/document
From: Cindy Eisner (EISNER@il.ibm.com)
Date: Wed Jul 24 2002 - 04:30:31 PDT
bassam,
>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)...
ok. this is what was bothering me about that latest example. but i see
that it is not a problem of assertions per se.
thanks,
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 23/07/2002 20:28:35
Sent by: bassam@de.ibm.com
To: Cindy Eisner/Haifa/IBM@IBMIL
cc: Adam Krolnik <krolnik@lsil.com>, assertion@eda.org
Subject: Re: problems with current definition/document
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 : Wed Jul 24 2002 - 04:31:00 PDT