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™-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 13:10:31 2007
This archive was generated by hypermail 2.1.8 : Thu Mar 08 2007 - 13:10:44 PST