[sv-ac] 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.