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