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

Shalom,
 
Thanks for this explanation.
Now I see the true meaning of this text and how the example fits to these
rules.
Indeed, the requirement 3 text could be reworded as you proposed; with
current text more people may become confused too ...
 
Regards,
Mirek

  _____  

From: Bresticker, Shalom [mailto:shalom.bresticker@intel.com] 
Sent: 23 grudnia 2008 08:58
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  <http://www.mailscanner.info/> MailScanner, and is 
believed to be clean. 
-- 
This message has been scanned for viruses and 
dangerous content by  <http://www.mailscanner.info/> MailScanner, 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.