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

Hi Shalom:

I agree with you.

Regarding (e1 or e2), I would say that in the general consideration
of event expressions, this is one event expression with two proper
event subexpressions.

However, in the context of the discussion of these particular rules,
I agree with you that we should interpret this as two expressions
because the rule 3a) does not allow "or" as a top-level operator in
isolating the inferred event expression.

J.H.

> X-eda.org-MailScanner-Watermark: 1230623998.99834@9xcCkm7E2CLtRMuNb5QBgw
> X-Authentication-Warning: server.eda.org: majordom set sender to owner-sv-ac@eda.org using -f
> X-eda.org-MailScanner-Watermark: 1230623968.59719@10Jt456tsgtT8Q2bIcz5hg
> X-ExtLoop1: 1
> X-IronPort-AV: E=Sophos;i="4.36,269,1228118400"; 
>    d="scan'208,217";a="93134799"
> From: "Bresticker, Shalom" <shalom.bresticker@intel.com>
> Date: Tue, 23 Dec 2008 09:58:20 +0200
> Thread-Topic: [sv-sc] RE: [sv-ac] assertion clock inferrence example with
>  comment contradicts the given rules ?
> Thread-Index: AclazyHdlr61co+jTKSeK+Ynm4j8QgACoTDQAmGQ3fAAFYWOkAAHAPcQ
> 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-eda.org-MailScanner-SpamScore: s
> 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: mBN7xun9025706
> X-eda.org-MailScanner-From: owner-sv-ac@server.eda.org
> X-OriginalArrivalTime: 23 Dec 2008 08:06:14.0021 (UTC) FILETIME=[5301D350:01C964D5]
> 
> 
> --_000_940E0C7800FA8342B435C63EEED4A3D824CC8275hasmsx501gercor_
> Content-Type: text/plain; charset="us-ascii"
> Content-Transfer-Encoding: quoted-printable
> 
> 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.