[sv-ac] RE: Mantis 2804

Hi Anupam-

I don't quite see how these rules would help in this case:

Checker c1 (event e1);
...
Always @(e1)
     P1: assert property (foo);
...
Endchecker

c1 myc1(posedge s1 or negedge s2 or posedge s3 or s4);

In this case, I want e1 to be used as the clocking event for P1, regardless of what weird expression is passed in to the checker. How would the change below allow this, if we are uniformly applying the rule after substitution?

Also, if we are allowing 'more than one' for part (c), I think that breaks the whole concept of this rule, since it leaves no way to choose which of the events is the clocking event to infer. Am I missing something?

From: Prabhakar, Anupam [mailto:anupam_prabhakar@mentor.com]
Sent: Wednesday, February 16, 2011 10:54 AM
To: Seligman, Erik
Subject: Mantis 2804

Hi Eric,

Here is the relevant part of the change that I would propose for Mantis 2804

 A clock shall be inferred for the context of an always or initial procedure that satisfies the following

requirements:

a) There is no blocking timing control in the procedure.

b) There is exactly one event control in the procedure.

c) Within the event control of the procedure, there is exactly one event expression, except if the procedure is inside a checker there can be more than one, that satisfies both of

the following conditions:

1) The event expression consists solely of an event variable, consists solely of a clocking block event, or is of the form edge_identifier expression1 [ iff expression2 ] and is not a proper subexpression of an event expression of this form.

2) No term in expression1 appears anywhere else in the body of the procedure other than as a clocking event or within assertion statements.

This should provide the same flexibility that you are proposing except that now all the rules can be uniformly applied after substitution. Let me know what you think.

Anupam

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