[sv-ac] RE: clock on disable iff condition

Hi Dana:

Thanks for this clarification.

I agree with you that if we infer a default clock for some terms in the
disable iff, then we should have the whole structure of clock flow,
including inferred and explicit clocks, participate in the clock
resolution for such terms.

I also agree that we do not have to make this change now. We can leave
the current rule in place and make this change later without breaking
backward compatibility.

J.H.

-----Original Message-----
From: Dana Fisman [mailto:Dana.Fisman@synopsys.com]
Sent: Tuesday, July 27, 2010 4:23 PM
To: Havlicek John-R8AAAU; Dana Fisman
Cc: sv-ac@eda.org
Subject: RE: clock on disable iff condition

Hi John,

The way I see it, an arbitrary expression is not necessarily associated
with a clock. Of course, when a formula is evaluated there is at least
one clock (maybe several) which at the end affect when each
subexpression is evaluated. On the other hand, there are certain
expression that are always associated with a clock, these are those
which may receive a clock as a parameter (e.g. $past()), and once the
clock parameter is absent the corresponding clock is inferred by the
clock inference rules.

Writing this email, I see that I was confused about the sequence methods
(e.g .triggered). These do not have a clock as a parameter. In PSL
ended() does have an optional clock parameter - this is where my
confusion came from.

Put that aside, what I was trying to say is that if the disable iff
condition contains a subexpression with an optional clock parameter, and
that parameter is absent, it is more uniform to rule that the
corresponding clock is inferred by the same rules as if this expression
appeared somewhere else in the formula. The disable iff expression is
still evaluated asynchronously.

So, for instance, the following property
        assert property (@(clk_a) disable iff (p && $past(e)) a ##1 b
|=> c); will be equivalent to
      assert property (@(clk_a) disable iff (p && $past(e,clk_a)) a ##1
b |=> c);

so if a holds on some tick of clk_a and b holds on the next tick of
clk_a and the expression (p && $past(e,clk_a)) holds somewhere between
the tick where b held and the next tick of clk_a (and not necessarily on
a tick of clk_a) then the property should pass.

I am not sure what is the value of $past(e,clk_a) at that time, but
whatever it is, this is the meaning.

I agree that this may be confusing, and thus am not against leaving the
current restriction disallowing usage of assertion functions / sequence
methods where the clock is not specified within the disable iff
condition. A motivation for allowing this is what Anupam said - in
singly clocked designs, one usually does not specify a clock in such
functions/methods, and he may want to use an asynchronous reset. This
restriction may annoy him.

Anyway, I am fine with leaving this restriction. What I object to is
inferring the default clock rather than the clock of the assertion if
exists - this does not make sense to me.

Dana

-----Original Message-----
From: Havlicek John-R8AAAU [mailto:r8aaau@freescale.com]
Sent: Tuesday, July 27, 2010 8:37 PM
To: Dana Fisman
Cc: sv-ac@eda.org
Subject: clock on disable iff condition

Hi Dana:

A question that I was not able to ask in today's meeting is the
following: If a clock flows into the disable iff expression, then to
which subexpressions of the disable iff expression does the clock apply
and is there a way to make this intuitive to the user? In order to be
able to represent asynchronous resets, I think that the clock should not
apply to subexpressions that are not sampled value functions. But then
this rule is not really consistent with the body of the assertion.

J.H.

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