Subject: Re: [sv-ac] The case for retaining check
From: Stephen Meier (Stephen.Meier@synopsys.com)
Date: Tue Feb 18 2003 - 18:30:44 PST
Adam: Thanks for your comments, please see embedded comments.
At 12:27 PM 2/18/2003 -0600, Adam Krolnik wrote:
>Hi Steve, Cindy;
>
>One other issue with check().
>
>If we see the utility of check(), then why is there no equivalent to the
>cover directive?
>
>Steve, your response brings to mind 2 questions.
>
>
>1. If only simulation will use check() then why have it - the user will
>need to
> write it another way for other tools to use. If they are not using other
> tools then there's very little difference betweeen check() and if().
Agreed, the only difference is for dynamic simulation users to have clear
distinction
between design code and verification code.
>2. You wrote:
>
> >When concurrent assertions appear in module then any procedural context
> >is extracted and used as sampling condition and/or the antecedent of a
> >boolean implication. The LRM is light on this explanation, we will discuss
> >more details at next SV-AC meeting.
>
>and
>
> >The reason is that when unclocked assertions appear in procedural
> >context then their sampling clock is inferred from context.
>
>Please consider this example. If unclocked assertions in a procedural context
>obtain the inferred clock then are #1 and #2 equivalent?
>
>
>always @(posedge clk)
> begin
> case(state)
> WRITING:
> begin
> ...
>
> if (stall) assert (req); (1)
> assert (stall => req); (2)
Yes these are equivalent.
>Are #1 and #2 equivalent?
Yes, the if(stall) is extracted and converted to an implication and evaluated
the same as all concurrent assertions.
>Are they evaluated in the procedural flow, or are they extracted
>and simulated/evaluated as an independent process?
They behave as if they are extracted and evaluated as concurrent
assertions, but
it's up to implemention how it really works in the tools.
>It seems to me the answer is no. The if() statement samples stall in the
>previous
>cycle as compared with req. The assert statement #2 samples both stall and
>req at the same time.
Both assert statements sample stall and req at the same time i.e @(posedge
clk) - just
at the point that posedge clk occurs.
>If the answers are, #1 and #2 are equivalent because they are extracted and
>simulated/evaluated as a separate flow, they why do we need check() ?
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 list of details being explained in email is growing and it is making
>the proposal
>more confusing. Has the proposal been updated recently with any results of
>these
>discussions?
Draft 3 of LRM was just released, but no update to the sections on context,
clock
extraction. I will send out presentation for SV-AC in a moment, which if
approved will
result in more text description.
>I still don't understand the template facilities because there have
>been 2 or 3 different thoughts on how they work, but no wording. If we are
>supposed
>to be voting soon on this proposal, then it must be written out.
Agreed the templates section still needs review and additional semantic support
of how the variable substitution works.
>It would be very helpful to see an update to the proposal that addresses:
>
>1. How exactly (with an example - like above) assert statements should
>operate within
> various contexts (edge triggered, combinatorial procedural
This is the presentation, which needs to be written into language document.
>2. What does an instantiated template look like? What can be attached to a
>port
> of a template? How do var declarations, nonblocking assignments,
> clocking blocks,
> etc. work in a template? We need a good example.
This section needs review and additional language semantic description in
areas you are suggesting.
>Can you also send out the current issue spreadsheet.
Just did :)!
> Thanks Steve.
>
> 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 : Tue Feb 18 2003 - 18:31:25 PST