[sv-ac] RE: Mantis 2804

Anupam-I don't think you addressed my last comment in the previous email (other than moving it from c to d):
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?

Also, I think the p3 example you point out below is actually fairly likely to occur in real code: we have a procedure with a traditional-style event control that includes a reset plus the real clocking event, and we want to infer the correct clock and reset.

From: Prabhakar, Anupam [mailto:anupam_prabhakar@mentor.com]
Sent: Wednesday, February 16, 2011 1:52 PM
To: Seligman, Erik
Cc: sv-ac@eda.org
Subject: RE: Mantis 2804

Hi Eric,

If s4 is not an event variable then the rule below does not help. Your example below will work if we re-write the rules as

 c) If the procedure is not inside a checker, within the event control of the procedure, there is exactly one event expression 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.
d) If the procedure is inside a checker, only those events within the event control of the procedure will be inferred which do not have any term that appears anywhere else in the body of the procedure other than as a clocking event or within assertion statements.

However there is another example in your proposal which will not work and I hope this is not a real-life example that we need to solve.
------------------------
always @(rst or e3) begin: p3_block
local_sig <= rst;
p3: assert property (sig1 == sig2);
end
- Assertion p3 will be clocked by negedge rst. This is because the event control of p3_block satisfies the conditions in 16.15.6 before the formal argument e3 is substituted with the actual argument negedge rst, with e3 being the unique event expression satisfying condition (c).
------------------------

Anupam

From: Seligman, Erik [mailto:erik.seligman@intel.com]
Sent: Wednesday, February 16, 2011 11:32 AM
To: Prabhakar, Anupam
Cc: sv-ac@eda.org
Subject: 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.