Hi Ed, I reviewed the proposal. I think that the substance is good. I guess it is a matter of taste but I would write the equivalent properties as ------------------------------------- *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: 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: 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* ------------------------------------------- regards Doron Eduard Cerny wrote: >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 15:13:29 2007
This archive was generated by hypermail 2.1.8 : Thu Mar 08 2007 - 15:13:37 PST