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 MailScanner, and is
believed to be clean.