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

But what is the problem of allowing it with weak operators only? Other
than initially people may not know what to use it for? There seem to be
no semantic problems with it.

Regards,

ed
 

> -----Original Message-----
> From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On 
> Behalf Of Lisa Piper
> Sent: Monday, January 28, 2008 12:59 PM
> To: Kulshrestha, Manisha; Bustan, Doron; 
> john.havlicek@freescale.com; sv-ac@eda.org
> Subject: 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.
> 
> 
> 

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