RE: [sv-ac] Sv-AC 1737

Tom,
Thanks. 
John, can you send it for a vote?
Thank you,
ed

> -----Original Message-----
> From: Thomas.Thatcher@Sun.COM [mailto:Thomas.Thatcher@Sun.COM] 
> Sent: Tuesday, March 20, 2007 6:29 PM
> To: Eduard Cerny
> Cc: john.havlicek@freescale.com; sv-ac@eda-stds.org
> Subject: Re: [sv-ac] Sv-AC 1737
> 
> Hi Ed,
> 
> This proposal looks good to me.
> 
> Tom
> 
> Eduard Cerny wrote On 03/20/07 13:51,:
> > HI,
> > 
> > I have uplodade a new version of 1737. Please review and if 
> OK, let's
> > vote...
> > 
> > Thanks,
> > 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.
> > 
> > *property *r3;
> > 
> >       @(*posedge *mclk)(q != d);
> > 
> > *endproperty*
> > 
> > *always *@(*posedge *mclk) *begin*
> > 
> > *      if *(a) *begin*
> > 
> >             q <= d1;
> > 
> >             r3_p: *assert property *(r3);
> > 
> > *      **end*
> > 
> > *end*
> > 
> > * *
> > 
> > The above example is equivalent to the following:
> > 
> >  
> > 
> > *property *r3;
> > 
> >       @(*posedge *mclk)a |-> (q != d);
> > 
> > *endproperty*
> > 
> > r3_p: *assert property *(r3);
> > 
> > *always *@(*posedge *mclk) *begin*
> > 
> > *      if *(a) *begin*
> > 
> >             q <= d1;
> > 
> > *      end*
> > 
> > *end*
> > 
> > * *
> > 
> > Similarly, the enabling condition is also inferred from 
> *case *statements.
> > 
> > * *
> > 
> > *property *r4;
> > 
> >       @(*posedge *mclk)(q != d);
> > 
> > *endproperty*
> > 
> > *always *@(*posedge *mclk) *begin*
> > 
> > *      case *(a)
> > 
> >             1: *begin *q <= d1;
> > 
> >                   r4_p: *assert property *(r4);
> > 
> > *            **end*
> > 
> > *            default*: q1 <= d1;
> > 
> > *      endcase*
> > 
> > *end*
> > 
> > * *
> > 
> > The above example is equivalent to the following:
> > 
> >  
> > 
> > *property *r4;
> > 
> >       @(*posedge *mclk)(a==1) |-> (q != d);
> > 
> > *endproperty*
> > 
> > r4_p: *assert property *(r4);
> > 
> > *always *@(*posedge *mclk) *begin*
> > 
> > *      case *(a)
> > 
> >             1: *begin *q <= d1;
> > 
> > *            **end*
> > 
> > *            default*: q1 <= d1;
> > 
> > *      endcase*
> > 
> > *end*
> > 
> > *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,
> > 
> >  
> > 
> > *property* r3;
> > 
> >       @(*posedge* mclk)((q != d) ##1 ack);
> > 
> > *endproperty*
> > 
> > *always* @(*posedge* mclk) *begin*
> > 
> >       *if* (a) *begin*
> > 
> >             q <= d1;
> > 
> >             r3_p: *assert* *property* (r3);
> > 
> >             r3_c: *cover* *property* (r3);
> > 
> >       *end*
> > 
> > *end*
> > 
> >  
> > 
> > The above example is equivalent to the following:
> > 
> >  
> > 
> > *property* r3;
> > 
> >       @(*posedge* mclk)((q != d) ##1 ack);
> > 
> > *endproperty*
> > 
> > * *
> > 
> > r3_p: *assert property* (@(*posedge* mclk) a |-> r3);
> > 
> > r3_c: *cover property* (@(*posedge* mclk) *not* (a |-> *not* r3));
> > 
> >  
> > 
> > *always* @(*posedge* mclk) *begin*
> > 
> >       *if* (a) *begin*
> > 
> >             q <= d1;
> > 
> >       *end*
> > 
> > *end*
> > 
> >  
> > 
> > Similarly, the enabling condition is also inferred from 
> case statements.
> > 
> >  
> > 
> > *property* r4;
> > 
> >       @(*posedge* mclk)((q != d) ##1 ack);
> > 
> > *endproperty*
> > 
> > *always* @(*posedge* mclk) *begin*
> > 
> >       *case* (a)
> > 
> >             1: *begin* q <= d1;
> > 
> >                   r4_p: *assert* *property* (r4);
> > 
> >                   r4_c: *cover* *property* (r4);
> > 
> >             *end*
> > 
> >             *default*: q1 <= d1;
> > 
> >       *endcase*
> > 
> > *end*
> > 
> >  
> > 
> > The above example is equivalent to the following:
> > 
> >  
> > 
> > *property* r4;
> > 
> >       @(*posedge* mclk)((q != d) ##1 ack);
> > 
> > *endproperty*
> > 
> > * *
> > 
> > r4_p: *assert property* (@(*posedge* mclk)(a==1) |-> r4);
> > 
> > r4_c: *cover property* (@(*posedge* mclk) *not*((a==1) |-> 
> *not* r4));
> > 
> > * *
> > 
> > *always* @(*posedge* mclk) *begin*
> > 
> >       *case* (a)
> > 
> >             1: *begin* q <= d1;
> > 
> >             *end*
> > 
> >             *default*: q1 <= d1;
> > 
> >       *endcase*
> > 
> > *end*
> > 
> >  
> > 
> 
> -- 
> ------------------
> 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.