[sv-ac] Mantis 1900 (checkers) updated

From: Korchemny, Dmitry <dmitry.korchemny_at_.....>
Date: Sun Nov 04 2007 - 04:33:02 PST
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