[sv-ac] RE: Mantis 2804

Hi Eric,

As per the LRM the mechanism for passing arguments to a checker is
similar to the mechanism for passing arguments to a property the
semantics are applied after substitution. With your proposal the rules
for inferring a clock in a procedure is applied before substitution (and
then apply after substitution if clock cannot be inferred) which implies
if the following always inside a checker a1 will infer (posedge clk1 or
posedge clk2) as the clocking event

c1 i1(posedge clk1 or posedge clk2)

checker c1(Event e1);

always @(e1)

                a1:assert property(p1);

....

'If' we applied the rules after substitution then no clock would have
been inferred. In my opinion the fact the clock is getting inferred in
this case breaks the 'synthesis' motivation of rule c). While I see the
merit of having a rule which would allow clock inference for this case I
would prefer a rule for checkers would be consistent after substitution.

To answer your question of 'since it leaves no way to choose which of
the events is the clocking event to infer' - the event control of a
procedure can be complex but it is pretty much a list of event
expressions. A tool will need analyze each event expression to see is
any can be used to infer the clock. The current rules restricts that
there can be only one such event expression which satisfied the
condition in c). However for checkers we do not want this to be
restricted to only one event expression. For this case (inside a
checker) (e1 or e2) will be inferred as a clock for a2.

always@(e1 or e2 or negedge rst)

if (!rst)

                ...

else

                a2:assert property(p2);

I agree that you should be able to infer the correct clock and reset -
the above example shows that. However the p3 example is a little
different and after substitution it would be

always @(rst or negedge rst) begin: p3_block

local_sig <= rst;

p3: assert property (sig1 == sig2);

end

In this case the clock will not be inferred as per the rules that I
proposed - but I doubt the writer of the checker intended it to simulate
this way.

Also, while I agree that the writer of the checker would be different
person than the person who uses it, it is obvious that the interface of
the checker would be clearly defined specially which argument is a clock
and which is a reset and in my opinion we would never see the p3 case
above after substitution.

Anupam

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