Subject: Re: problems with current definition/document
From: Cindy Eisner (EISNER@il.ibm.com)
Date: Tue Jul 23 2002 - 03:41:11 PDT
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 - 03:42:15 PDT