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™-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.