RE: [sv-ac] Updated proposal for #1737: inferred enabling condition

Hello Tom,

the use of ! and ##0 works only if the original property is a boolean,
not in general. 
You have a good point about the examples, I completely forgot about the
old ones. I will change that too.

Change of name - fine.

I will redeposit later today.

ed
 

> -----Original Message-----
> From: Thomas.Thatcher@Sun.COM [mailto:Thomas.Thatcher@Sun.COM] 
> Sent: Thursday, March 08, 2007 12:11 PM
> To: Eduard Cerny
> Cc: john.havlicek@freescale.com; sv-ac@eda-stds.org
> Subject: Re: [sv-ac] Updated proposal for #1737: inferred 
> enabling condition
> 
> Hello Everyone,
> 
> I have reviewed the updated proposal.  Here are my comments
> 
> 
> In the example, the equivalent cover property after inference is
> shown as
>     cover property  (@(posedge clk) not (!rst |-> not (a && b));
> 
> Isn't this equivalent to
>     cover property  (@(posedge clk) !rst ##0 (a && b);
> 
> The last form seems easier to understand to me.  This would also
> allow some simplification in the text description for the equivalent
> inferred verification statement for the cover property
> 
> 
> The second thought is that the proposal contains a new example showing
> the inferring of an enabling condition for both an assert 
> property and a
> cover property.  I think this makes the first existing 
> example redundant,
> as is shows the inference of an enabling condition inside an 
> if statement
> for an assert property only.
> 
> Finally, in the example, consider using something like "en" 
> for the enabling
> condition, rather than "!rst"  just to avoid any possible 
> confusion with
> a "disable iff rst" kind of structure.
> 
> Thanks,
> 
> Tom
> 
> Eduard Cerny wrote On 03/08/07 07:14,:
> > Hello,
> > I have uploaded a new version of the proposal, attached here for
> > convenience. It distinguishes between assert, assume and 
> cover property.
> > Regards,
> > ed
> > 
> > 
> > 
> > 
> --------------------------------------------------------------
> ----------
> > 
> > This proposal corrects an incomplete fix for item 1381 
> regarding when an
> > evaluation attempt takes place under inferred enabling 
> condition from an
> > always block.
> > 
> >  
> > 
> > *P1800-2008-draft1, 17.13.5, p. 289  (**IEEE Std 1800(tm)-2005**)*
> > 
> > *Replace*
> > 
> > Another inference made from the context is the enabling 
> condition for a
> > property. Such derivation takes place when a property is 
> placed in an
> > *if..else* block or a *case* block. The enabling condition 
> assumed from
> > the context is used as the antecedent of the property. A concurrent
> > assertion embedded in procedural code specifies that a new 
> evaluation
> > attempt of the underlying property_spec begins at every 
> occurrence of
> > the inferred clocking event.
> > 
> > *With*
> > 
> > Another inference made from the context is the enabling 
> condition for a
> > verification statement. Such derivation takes place when a 
> verification
> > statement is placed in an *if..else* block or a *case* block. The
> > enabling condition assumed from the context is used to modify the
> > property_expr of the verification statement as follows:
> > 
> >  
> > 
> > - If the verification statement is assume property or 
> assert property
> > then the enabling condition is used as the antecedent of an 
> overlapping
> > implication of which the consequent is the property_expr 
> stated in the
> > verification statement.
> > 
> >  
> > 
> > - If the verification statement is cover property then the enabling
> > condition is used as the antecedent of a negated 
> overlapping implication
> > of which the consequent is the negated property_expr stated in the
> > verification statement. The double negation used in the property
> > expression represents the dual property to the overlapping 
> implication
> > and it is often called "followed by".
> > 
> >  
> > 
> > The resulting new property_expr then replaces the original 
> property_expr
> > in the verification statement. A concurrent assertion embedded in
> > procedural code in an *if...else* block or a *case* block 
> specifies that
> > a new evaluation attempt of the underlying property_spec 
> begins at every
> > occurrence of the (inferred) clocking event.
> > 
> >  
> > 
> > For example,
> > 
> >  
> > 
> > *always* @(*posedge* clk) *begin*
> > 
> >   *if* (rst) ...
> > 
> >   *else* *begin*
> > 
> >     ...
> > 
> >    aa: *assert* *property* (a |-> b);
> > 
> >    cc: *cover* *property* (a && b);
> > 
> >    ...
> > 
> >   *end*
> > 
> > *end*
> > 
> >  
> > 
> > The equivalent concurrent verification statements after clock and
> > enabling condition inference are as follows:
> > 
> >  
> > 
> >    aa: *assert* *property* (@(*posedge* clk) !rst |-> (a |-> b));
> > 
> >    cc: *cover* *property*  (@(*posedge* clk) *not* (!rst 
> |-> *not* (a &&
> > b));
> > 
> >  
> > 
> >  
> > 
> 
> -- 
> ------------------
> Thomas J. Thatcher
> Sun Microsystems
> 408-616-5589
> ------------------
> 
> 

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.