Hi all, I uploaded an updated version of the checker proposal. It has the following changes: * Added the formal semantics of local variable assignment * Modified the definition of the sequence dependency on a free variable: instead of saying that a sequence depends on a free variable if the last cycle of the sequence depends on this free variable I introduced a coarser definition saying that a sequence depends on a free variable if this free variable enters the sequence expression. The reason for doing that is that we don't have a definition of the last cycle of the sequence. * Replaced "If targeted for simulation the checker shall not contain non-deterministic free variables." with "In simulation the assertions containing non-deterministic free variables shall be checked for all the possible values of these free variables complying the constraints imposed to them by the assumptions and by the assignments (see 16.18.5.1)." * Fixed several typos and stylistic mistakes pointed out by Erik. Thanks, Dmitry --------------------------------------------------------------------- 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.Received on Sun Nov 4 04:34:27 2007
This archive was generated by hypermail 2.1.8 : Sun Nov 04 2007 - 04:34:54 PST