[sv-ac] RE: Mantis 3135: Verbal explanation of nexttime and always is misleading for multiple clocks

Thanks Shalom. Proposal has been fixed.

Dana

From: Bresticker, Shalom [mailto:shalom.bresticker@intel.com]
Sent: Tuesday, February 08, 2011 2:08 PM
To: Dana Fisman; Korchemny, Dmitry; sv-ac@eda.org
Cc: sv-champions@eda.org
Subject: RE: Mantis 3135: Verbal explanation of nexttime and always is misleading for multiple clocks

Thanks, Dana.

Editorial corrections:

On "always":

"The above explanations refer to the case where the always property is evaluated in a time step that is a tick of the clock of the always property. When the always property is evaluated in a time step that is not a tick of the clock of the always property then an alignment to the tick of the clock of the always property should be applied before the above description. Thus, it is more precise to say that s_always[n:m] property_expr evaluates to true if, and only if, there exists (* SHOULD BE "exist" *) m+1 ticks of the clock of the always property, including the current time step, and property_expr evaluates to true beginning in all of the n+1'th to m+1'th clocks (* SHOULD BE "clock" *) ticks, where counting starts at the current time step."

On "eventually":

"The above explanations refer to the case where the eventually property is evaluated in a time step that is a tick of the clock of the eventually property. When the eventually property is evaluated in a time step that is not a tick of the clock of the eventually property then an alignment to the tick of the clock of the eventually property should be applied before the above description. Thus, it is more precise to say that s_eventually[n:m] property_expr evaluates to true if, and only if, there exists (* SHOULD BE "exist" *) at least n+1 ticks of the clock of the eventually property, including the current time step, and property_expr evaluates to true beginning in one of the n+1'th to m+1'th clocks (* SHOULD BE "clock" *) ticks, where counting starts at the current time step."

Thanks,
Shalom

From: Dana Fisman [mailto:Dana.Fisman@synopsys.com]
Sent: Tuesday, February 08, 2011 10:05 AM
To: Korchemny, Dmitry; Dana Fisman; Bresticker, Shalom; sv-ac@eda.org
Cc: sv-champions@eda.org
Subject: RE: Mantis 3135: Verbal explanation of nexttime and always is misleading for multiple clocks

Item has been re-opened and the proposal was updated to apply to 'eventually' as well.
http://www.eda-twiki.org/mantis/view.php?id=3135.

Regards,
Dana
---------------------------------------------------------------------
Intel Israel (74) Limited

This e-mail and any attachments may contain confidential material for
the sole use of the intended recipient(s). Any review or distribution
by others is strictly prohibited. If you are not the intended
recipient, please contact the sender and delete all copies.

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