Thanks, ed > -----Original Message----- > From: Thomas.Thatcher@Sun.COM [mailto:Thomas.Thatcher@Sun.COM] > Sent: Thursday, March 08, 2007 4:10 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 > > Hi Ed, > > I reviewed the modified proposal. It looks good now. > > Tom > > Eduard Cerny wrote On 03/08/07 09:40,: > > Hi Tom, > > > > I have updated the examples. Hope it will fly now :-) Attached and > > uploaded. > > > > 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 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_assert; > >> > >> @(*posedge* mclk)a |-> ((q != d) ##1 ack); > >> > >> *endproperty* > >> > >> *property* r3_cover; > >> > >> @(*posedge* mclk) *not* (a |-> *not* ((q != d) ##1 ack)); > >> > >> *endproperty* > >> > >> r3_p: *assert* *property* (r3_assert); > >> > >> r3_c: *cover* *property* (r3_cover); > >> > >> *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_assert; > >> > >> @(*posedge* mclk)(a==1) |-> ((q != d) ##1 ack); > >> > >> *endproperty* > >> > >> *property* r4_cover; > >> > >> @(*posedge* mclk) *not*((a==1) |-> *not* ((q != d) ##1 ack)); > >> > >> *endproperty* > >> > >> r4_p: *assert* *property* (r4_assert); > >> > >> r4_c: *cover* *property* (r4_cover); > >> > >> *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.Received on Thu Mar 8 14:55:37 2007
This archive was generated by hypermail 2.1.8 : Thu Mar 08 2007 - 14:55:47 PST