RE: [sv-ac] call to vote on Mantis 1932

I also agree that we should restrict it for now. I have not given any
thought to recursion with these new operators.

lisa

-----Original Message-----
From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of
Kulshrestha, Manisha
Sent: Monday, January 28, 2008 11:43 AM
To: Bustan, Doron; john.havlicek@freescale.com; sv-ac@eda.org
Subject: RE: [sv-ac] call to vote on Mantis 1932

Hi,

I just wanted to understand the restriction for strong property in
recursive properties and not weak ones. I do not think we should
introduce it now. I even feel that combining these new operators (like
until and always) in recursive properties is going to be very confusing.
I was just wondering if we should restrict it for even weak properties.
What do you think ? Do you think we loose anything important here by not
allowing weak forms of these new operators ? Since PSL did not have a
concept of recursive anyway, I think no one has written these
combinations yet.

Thanks.
Manisha

-----Original Message-----
From: Bustan, Doron [mailto:doron.bustan@intel.com] 
Sent: Monday, January 28, 2008 6:16 PM
To: Kulshrestha, Manisha; john.havlicek@freescale.com;
sv-ac@server.eda.org
Subject: RE: [sv-ac] call to vote on Mantis 1932

Hi Manisha,

>>1. In 16.12.1, it is mentioned that 'not' operator switches the
strength
>>of a property. I think it will be useful to have this information in
>>16.12.2 also.

[[DB:]] Ed and Dmitry have the same comment so I have moved this
paragraph to the negation part.


>>2. Why are weak forms of these new operators  allowed in recursive 
>>properties (and not strong ones) ?

[[DB:]] We only allow weak constructs in recursive properties because
alternating strong and weak in a "recursive cycle" makes it difficult to
define the semantics. I guess that "strong" could be an exception
because it cannot be applied on properties, and thus cannot be part of a
"recursive cycle". I am a little afraid to get it in at this time in
case I missing something. Do you think it is important to have it now?
We can always put it latter (there are other restrictions that can be
lifted as well.)

>>3. In the changes for multiclocked properties, it does have 'until' as

>>one of the operators which requires special care but not 'until_with'.
>>Is that an oversight ?


[[DB:]] I guess it is an oversight, I have add it now.

Thanks

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, and is
believed to be clean.



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