Subject: RE: problems with current definition/document
From: Cindy Eisner (EISNER@il.ibm.com)
Date: Tue Jul 23 2002 - 06:53:26 PDT
tom,
>> 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.
i don't understand this (as i said before, my verilog is very very rusty).
the assertion is non-blocking, but the @(posedge req1) comes *before* the
assertion, so it seems to me that it blocks. going by the "process"
example on page 46, the above becomes
always @(posedge clk)
if (state==REQ)
@(posedge req1) assert(req2) process;
state =#1 WAIT;
why does this not delay the assignment "state =#1 WAIT"?
>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.
i agree. in fact, this could be enforced by the language (see below).
>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.
that is a good rule. i'm still concerned slightly that there is a way for
assertions to affect the design through delays despite the fact that they
are non-blocking, as in my example above.
>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.
isn't it enough that the language enforce a distinction between assertion
signals/variables and design signals/variables? for instance, if you
assign to a signal or variable within an assertion, then the only thing you
are allowed to do to it outside of an assertion is print its value. you
could make this more explicit by defining a new type which can only be used
within assertions or print statements (and the converse - all the other
types can be used but not assigned to from within an assertion).
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
"Tom Fitzpatrick" <fitz@co-design.com> on 23/07/2002 16:23:19
To: Cindy Eisner/Haifa/IBM@IBMIL, "Bassam Tabbara" <bassam@novas.com>
cc: "Adam Krolnik" <krolnik@lsil.com>, <assertion@eda.org>
Subject: RE: problems with current definition/document
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&D
>
> Novas Software, Inc.
> bassam@novas.com
> (408) 467-7893
>
>
>
>
This archive was generated by hypermail 2b28 : Tue Jul 23 2002 - 06:53:46 PDT