RE: [sv-ac] LTL 1932

From: Bresticker, Shalom <shalom.bresticker_at_.....>
Date: Sat Oct 06 2007 - 23:33:23 PDT
Doron,
 
The proposal adds a bunch of new keywords that are not listed in the
changes to Annex B.
 
Regards,
Shalom


________________________________

	From: owner-sv-ac@server.eda.org
[mailto:owner-sv-ac@server.eda.org] On Behalf Of Bustan, Doron
	Sent: Sunday, October 07, 2007 8:28 AM
	To: sv-ac@server.eda-stds.org
	Subject: [sv-ac] LTL 1932
	
	

	Hi,

	 

	I 

	1.	Replaced next[range] with eventually[range] 
	2.	Add example for weak sequential property under not. 
	3.	Change the definition for vacuity for weak sequential
properties and until. I find it hard to get a good definition for until
so I wrote a very conservative one that will not give unnecessarily
false negatives. 

	 

	Doron

	
---------------------------------------------------------------------
	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 <http://www.mailscanner.info/>
, and is 
	believed to be clean. 

---------------------------------------------------------------------
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 Sat Oct 6 23:34:39 2007

This archive was generated by hypermail 2.1.8 : Sat Oct 06 2007 - 23:34:48 PDT