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

That's what I meant.

Shalom

________________________________
From: Seligman, Erik
Sent: Monday, December 29, 2008 10:55 PM
To: Bresticker, Shalom; 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 comment contradicts the given rules ?

Did anyone reply to this comment?
Anyway, I think the example is still legal-- r2 is just some wire from elsewhere 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 Behalf 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 comment contradicts the given rules ?

By the way, in example r4:


property r4;

(q != d);

endproperty

always_ff @(clock iff reset == 0 or posedge reset) begin

r1 <= reset ? 0 : r2 + 1;

q <= $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 <= 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.org
Subject: RE: [sv-sc] RE: [sv-ac] assertion clock inferrence example with comment contradicts the given rules ?

Strictly speaking, I think the text is correct, but I agree it can be confusing.

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 rather that there can be many event expressions but one and only one that meets 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 satisfies both of the following conditions:"

As to whether (e1 or e2) is one event expression or two, the BNF says,

event_expression27 ::=

[ 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 clarification more specific.

However, it is not too complex to expect the tool to extract the clock, though. That is exactly what synthesis and other tools do today. Once the rules 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 Behalf 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 comment contradicts the given rules ?

Hi Mike,

I agree that this example is confusing.  There are two event expressions, but the second event expression uses reset which appears in the body(and therefore violates 3b), so there is only one event expression that meets 3a AND 3b.   I guess the real question is whether (event1 or event2) is viewed as one event or two events.  I personally think this is too complex to expect the tool to extract the clock though.

Lisa

________________________________
From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org] On Behalf 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 contradicts the given rules ?

Hi,

I've noticed a following issue in 16.15.6 Embedding concurrent assertions in 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 expression that satisfies both of

the following conditions:

a) The event expression is of the form edge_identifier expression1 [ iff expression2 ] 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 procedure.



and an example with comment:



Another, more complex example that is legal is as follows:

property r3;

(q != d);

endproperty

always_ff @(posedge clock iff reset == 0 or posedge reset) begin

r1 <= reset ? 0 : r1 + 1;

q <= $past(d1);

r3_p: assert property (r3);

end



In the example above, the inferred clock is posedge clock iff reset == 0. The inferred clock is not

posedge clock because posedge clock is a proper subexpression of posedge clock iff

reset == 0.



But the event control in example: @(posedge clock iff reset == 0 or posedge reset)  seems to violate:

- rule 3) in general: "there is exactly one event expression" - here we have 2 event expressions ("posedge clock iff reset == 0" and "posedge reset") I guess, otherwise what would be an example of more than one event expressions that would violate the rule ?

- and in particular: rule 3a): the event expression here is more complex (includes "or" operator) and thus it does not fit the "edge_identifier expression1 [ 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<http://www.mailscanner.info/>, and is
believed to be clean.
--
This message has been scanned for viruses and
dangerous content by MailScanner<http://www.mailscanner.info/>, and is
believed to be clean.

---------------------------------------------------------------------
Intel Israel (74) Limited

This e-mail and any attachments may contain confidential material for
the sole use of the intended recipient(s). Any review or distribution
by others is strictly prohibited. If you are not the intended
recipient, please contact the sender and delete all copies.


--
This message has been scanned for viruses and
dangerous content by MailScanner<http://www.mailscanner.info/>, and is
believed to be clean.
---------------------------------------------------------------------
Intel Israel (74) Limited

This e-mail and any attachments may contain confidential material for
the sole use of the intended recipient(s). Any review or distribution
by others is strictly prohibited. If you are not the intended
recipient, please contact the sender and delete all copies.

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