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

Iam not sure that restricting it buys much... people do not have to use
it...

Best regards,
ed
 

> -----Original Message-----
> From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On 
> Behalf Of Kulshrestha, Manisha
> Sent: Tuesday, January 29, 2008 3:00 AM
> To: Lisa Piper; Bustan, Doron; john.havlicek@freescale.com; 
> sv-ac@eda.org
> Subject: RE: [sv-ac] call to vote on Mantis 1932
> 
> Yes, I agree. It is better to start with restrictions and then later
> relax them as people become comfortable with them.
> 
> Thanks.
> Manisha
> 
> -----Original Message-----
> From: Lisa Piper [mailto:piper@cadence.com] 
> Sent: Monday, January 28, 2008 11:29 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.