Re: [sv-sc] RE: [sv-ac] assertion clock inferrence example with comment contradicts the given rules ?

Hi Erik:

I agree with your comments on this thread.

J.H.

> X-eda.org-MailScanner-Watermark: 1231188960.2019@VmXdSC+nI67gUUXXuEGwiw
> X-Authentication-Warning: server.eda.org: majordom set sender to owner-sv-ac@eda.org using -f
> X-eda.org-MailScanner-Watermark: 1231188927.57019@1jd2EJlEM5ghu1f5Du/unw
> X-ExtLoop1: 1
> X-IronPort-AV: E=Sophos;i="4.36,297,1228118400"; 
>    d="scan'208,217";a="653373870"
> From: "Seligman, Erik" <erik.seligman@intel.com>
> Date: Mon, 29 Dec 2008 12:55:23 -0800
> Thread-Topic: [sv-sc] RE: [sv-ac] assertion clock inferrence example with
>  comment contradicts the given rules ?
> Thread-Index: AclazyHdlr61co+jTKSeK+Ynm4j8QgACoTDQAmGQ3fAAFYWOkAAHAPcQAACcYLABSL44wA==
> Accept-Language: en-US
> Content-Language: en-US
> X-MS-Has-Attach: 
> X-MS-TNEF-Correlator: 
> acceptlanguage: en-US
> X-eda.org-MailScanner: Found to be clean, Found to be clean
> X-Spam-Status: No, No
> Sender: owner-sv-ac@eda.org
> X-eda.org-MailScanner-Information: Please contact the ISP for more information
> X-MailScanner-ID: mBTKtvLH005131
> X-eda.org-MailScanner-From: owner-sv-ac@server.eda.org
> X-OriginalArrivalTime: 29 Dec 2008 20:57:55.0930 (UTC) FILETIME=[1F92F3A0:01C969F8]
> 
> 
> --_000_D4A21C1D05FCC64D8648615B5082F89B1B801FD3orsmsx502amrcor_
> Content-Type: text/plain; charset="us-ascii"
> Content-Transfer-Encoding: quoted-printable
> 
> Did anyone reply to this comment?
> Anyway, I think the example is still legal-- r2 is just some wire from else=
> where in the code.  It might make more sense with r1, but since it's legal =
> either way, I don't think it's worth worrying about at this stage.
> 
> ________________________________
> From: owner-sv-sc@server.eda.org [mailto:owner-sv-sc@server.eda.org] On Beh=
> alf Of Bresticker, Shalom
> Sent: Tuesday, December 23, 2008 12:02 AM
> To: Lisa Piper; 'Mirek Forczek'; sv-ac@server.eda.org; sv-sc@server.eda.org
> Subject: RE: [sv-sc] RE: [sv-ac] assertion clock inferrence example with co=
> mment contradicts the given rules ?
> 
> By the way, in example r4:
> 
> 
> property r4;
> 
> (q !=3D d);
> 
> endproperty
> 
> always_ff @(clock iff reset =3D=3D 0 or posedge reset) begin
> 
> r1 <=3D reset ? 0 : r2 + 1;
> 
> q <=3D $past(d1); // no inferred clock
> 
> r4_p: assert property (r4); // no inferred clock
> 
> end
> 
> I imagine the statement in the always_ff procedure should have been
> 
> r1 <=3D reset ? 0 : r1 + 1;
> 
> Shalom
> ________________________________
> From: Bresticker, Shalom
> Sent: Tuesday, December 23, 2008 9:58 AM
> To: 'Lisa Piper'; 'Mirek Forczek'; sv-ac@server.eda.org; sv-sc@server.eda.o=
> rg
> Subject: RE: [sv-sc] RE: [sv-ac] assertion clock inferrence example with co=
> mment contradicts the given rules ?
> 
> Strictly speaking, I think the text is correct, but I agree it can be confu=
> sing.
> 
> As Lisa points out, the meaning of requirement 3 is not that there is only =
> one event expression and that event expression must meet 3a and 3b, but rat=
> her that there can be many event expressions but one and only one that meet=
> s 3a and 3b.
> 
> The examples are intended to clarify the meaning of the requirement.
> 
> Requirement 3 could be reworded to something like
> 
> "One and only one of the event expressions within the event control satisfi=
> es both of the following conditions:"
> 
> As to whether (e1 or e2) is one event expression or two, the BNF says,
> 
> event_expression27 ::=3D
> 
> [ edge_identifier ] expression [ iff expression ]
> 
> | sequence_instance [ iff expression ]
> 
> | event_expression or event_expression
> 
> | event_expression , event_expression
> 
> | ( event_expression )
> 
> So strictly, it is both one and two event expressions, but the intent is to=
>  regard it as two. I'm not sure it is worth trying to make that clarificati=
> on more specific.
> 
> However, it is not too complex to expect the tool to extract the clock, tho=
> ugh. That is exactly what synthesis and other tools do today. Once the rule=
> s are clearly defined, as here, simulators should be able to do so also.
> 
> Shalom
> 
> ________________________________
> From: owner-sv-sc@server.eda.org [mailto:owner-sv-sc@server.eda.org] On Beh=
> alf Of Lisa Piper
> Sent: Tuesday, December 23, 2008 6:32 AM
> To: 'Mirek Forczek'; sv-ac@server.eda.org; sv-sc@server.eda.org
> Subject: [sv-sc] RE: [sv-ac] assertion clock inferrence example with commen=
> t contradicts the given rules ?
> 
> Hi Mike,
> 
> I agree that this example is confusing.  There are two event expressions, b=
> ut the second event expression uses reset which appears in the body(and the=
> refore violates 3b), so there is only one event expression that meets 3a AN=
> D 3b.   I guess the real question is whether (event1 or event2) is viewed a=
> s one event or two events.  I personally think this is too complex to expec=
> t the tool to extract the clock though.
> 
> Lisa
> 
> ________________________________
> From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org] On Beh=
> alf Of Mirek Forczek
> Sent: Monday, December 22, 2008 1:26 PM
> To: sv-ac@server.eda.org; sv-sc@server.eda.org
> Subject: [sv-ac] assertion clock inferrence example with comment contradict=
> s the given rules ?
> 
> Hi,
> 
> I've noticed a following issue in 16.15.6 Embedding concurrent assertions i=
> n procedural code:
> 
> There are assertion clock inferrence rules given:
> 
> 
> A clock shall be inferred for the context of an always or initial procedure=
>  that satisfies the following requirements:
> 
> 1) There is no blocking timing control in the procedure.
> 
> 2) There is exactly one event control in the procedure.
> 
> 3) Within the event control of the procedure, there is exactly one event ex=
> pression that satisfies both of
> 
> the following conditions:
> 
> a) The event expression is of the form edge_identifier expression1 [ iff ex=
> pression2 ] and is not a
> 
> proper subexpression of an event expression of this form.
> 
> b) No term in expression1 appears anywhere else in the body of the procedur=
> e.
> 
> 
> 
> and an example with comment:
> 
> 
> 
> Another, more complex example that is legal is as follows:
> 
> property r3;
> 
> (q !=3D d);
> 
> endproperty
> 
> always_ff @(posedge clock iff reset =3D=3D 0 or posedge reset) begin
> 
> r1 <=3D reset ? 0 : r1 + 1;
> 
> q <=3D $past(d1);
> 
> r3_p: assert property (r3);
> 
> end
> 
> 
> 
> In the example above, the inferred clock is posedge clock iff reset =3D=3D =
> 0. The inferred clock is not
> 
> posedge clock because posedge clock is a proper subexpression of posedge cl=
> ock iff
> 
> reset =3D=3D 0.
> 
> 
> 
> But the event control in example: @(posedge clock iff reset =3D=3D 0 or pos=
> edge reset)  seems to violate:
> 
> - rule 3) in general: "there is exactly one event expression" - here we hav=
> e 2 event expressions ("posedge clock iff reset =3D=3D 0" and "posedge rese=
> t") I guess, otherwise what would be an example of more than one event expr=
> essions that would violate the rule ?
> 
> - and in particular: rule 3a): the event expression here is more complex (i=
> ncludes "or" operator) and thus it does not fit the "edge_identifier expres=
> sion1 [ iff expression2 ]" form.
> 
> Considering above: no clock shall be inferred in the example or the example=
>  code shall be changed (?).
> 
> 
> 
> Regards,
> 
> Mirek
> 

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.