Subject: Re: [sv-ac] The case for retaining check
From: Stephen Meier (Stephen.Meier@synopsys.com)
Date: Wed Feb 19 2003 - 12:02:35 PST
Adam:
Please see embedded comments. I am not saying that check and assert are
the same, in fact they are distinctly different in their sampling and
evaluation.
At 10:45 AM 2/19/2003 -0600, Adam Krolnik wrote:
>Hi Steve;
>
>
>You comments,
>
>hey behave as if they are extracted and evaluated as concurrent
>assertions, but
>it's up to implemention how it really works in the tools.
>
>Are saying that Prakash's example will work with either assert() or
>check(). Correct?
No I'm not saying that.
>always @(posedge clk)
> case(sig1)
> junk1:
> if (sig2) begin
> .
> .
> .
> if (sig3) begin
> assert(foo);
> check(foo) ;
> //desired behavior if (!foo) $display("assertion failed");
> //simulation solution if (!foo) $error("assertion failed") ;
> .
> end
> end
> endcase
These are not equivalent. check is checked immediately when the check
statement is executed. Whatever value of foo which exists at that moment
in simulation is the value that is checked.
Whereas the value of foo checked by the assert is as you have described
just below.
>The equivalent being
>
>assert @(posedge clk)
> (sig1 == junk && sig2 && sig3 => foo) else $error();
>
>
>You also wrote:
>
> >check is useful to check for things that occur within the processing of
> events within
> >the simulation event queue processing. So if you have conditions like
> mutex, onehot
> >that are NEVER allowed to be true even in a temporary sense then check
> could check for
> >these.
>
>The artifacts of the simulation queue model do not model real life. Thus
>checking for mutex on selects this way is bad methodology. We have shown
>real examples where you can
>get false firings due to the simulation scheduling semantics but in real
>life can never
>get an illegal value.
Yes, simulation event queue is absolutely an artifact, but I can imagine a
desire to check for potential glitches that cannot be caught by sampled
assertions. Right now you cannot check if a bus remains onehot for
duration of clock cycle. All that can be checked is that the bus is onehot
at the sampling clock.
>The only place I see check useful is for something like this:
>
>task dosomething;
> inputs ...
>
> begin
> @(posedge clk)
> #2; <drive a signal.>
> @(negedge clk);
> check (bus_signal === 1'bz)
> else $error ("Bus did not tristate signal on negative edge.");
>
> @(posedge clk);
> #2 <drive another signal>
> #2 check (busy === 1'b1)
> else $error("Bus was not busy after X condition asserted.");
>
>
>If all of this is true, then I conclude:
>
>1. The assert() statement is a sufficient alternative for check() to be able
> to perform property checking within a procedural context.
>2. The assert() statement has superior capabilities that allow for more than
> simple boolean property checking. The advantages of sequences allow for
> multi-clock properties to be checked within a procedural context that
> check()
> simply does not allow.
>
>3. The design community only needs to learn the assert statement and can
>confidently
> use it in any context (declarative or procedural) with equal abilities.
If we are clear on what check is technically that is good baseline.
I reach a slightly different conclusion, which is that check is an explicit
and useful form
to document immediate assertion checks. Because it is explicit the spec is
clearly
separated from the design code.
> Thanks Steve, Cindy, Prakash
>
> Adam Krolnik
> Verification Mgr.
> LSI Logic COrp.
> Plano TX. 75074
>
>
>
>
Steve Meier (stephen.meier@synopsys.com) W: 650-584-4476, Cell: 408-393-8246
This archive was generated by hypermail 2b28 : Wed Feb 19 2003 - 12:06:14 PST