Doron, I see, not to modify the property spec, just the inlined version. I just followed how the original example in the LRM was constructed. what do others say? ed > -----Original Message----- > From: Doron Bustan [mailto:dbustan@freescale.com] > Sent: Thursday, March 08, 2007 6:13 PM > To: Eduard Cerny > Cc: Thomas.Thatcher@Sun.COM; 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 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:19:13 2007
This archive was generated by hypermail 2.1.8 : Thu Mar 08 2007 - 15:19:25 PST