Subject: Re: [sv-ac] The case for retaining check
From: Prakash Narain (prakash@realintent.com)
Date: Wed Feb 19 2003 - 10:36:20 PST
Adam,
I disagree with Steve's comment that assert() and check() are equivalent.
We have to maintain maximal consistency between cycle-based evaluation
used for formal analysis and event-driven semantics for simulation. Hence
the cycle-based model should mimic the event driven scheduling, which
in the case of assert() schedules the first evaluation at the end of the
current/
beginning of the next clock cycle. The cycle-based model will schedule the
evaluation of check() at the beginning of the current clock cycle. The
event-driven
semantics will schedule the evaluation of check() in the current simulation
cycle.
In the absense of check(), there is no way to procedurally specify for a
cycle-based tool to check for a condition at the beginning of the current
cycle when the procedural block is a sequential block.
See the comment inlined below.
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. This is not true. Given my understanding of how the procedural
assert() is
scheduled, they are not the same. There is a cycle difference in the
scheduling
of the two. If we have modified the scheduling of assert() in a
sequential block,
then that should be reflected in the LRM. Without that, there is no way
to pose
the same cycle problem to a cycle based tool.
>
>
> 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
>
> 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.
>
> 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.
>
>
> Thanks Steve, Cindy, Prakash
>
> Adam Krolnik
> Verification Mgr.
> LSI Logic COrp.
> Plano TX. 75074
>
>
>
>
>
>
This archive was generated by hypermail 2b28 : Wed Feb 19 2003 - 10:37:53 PST