RE: [sv-ac] LTL 1932

Tej,

 

Currently it is defined as a match. If somebody mean to write

cover property (p0 and p1) then in my opinion he should write so
explicitly.

 

The same goes for |->

 

I would not write r|-> p as a cover in most cases. 

 

I agree that for assert property (p0 implies p1) it is more intuitive to
count attempts where p0 does not 

hold as a vacuous match. However, I am not sure about (not p0 or p1).

 

We had some discussion about defining the non-vacuous relation
explicitly for derived forms. 

Maybe that what we need to do.

 

Doron

 

________________________________

From: Singh, Tej [mailto:tej_singh@mentor.com] 
Sent: Tuesday, October 09, 2007 5:28 PM
To: Bustan, Doron; sv-ac@server.eda-stds.org
Subject: RE: [sv-ac] LTL 1932

 

Doron,

So if I write

cover property (p0 implies p1)

and p0 is false then is it a 'vacuous match' or 'match'?
Since implies is defined in terms of 'or' and 'not' this
should be 'match' but I would expect it to behave similar to '|->'

Tej


-----Original Message-----
From: Bustan, Doron [mailto:doron.bustan@intel.com]
Sent: Mon 10/8/2007 11:20 PM
To: Singh, Tej; sv-ac@server.eda-stds.org
Subject: RE: [sv-ac] LTL 1932

Hi Tej,



>>I think it is misleading to say that 'implies' is similar to '->' when
both operands are boolean

>>because

>>1. implies can still result in vacuous matches whereas '->' cannot.



[DB]I disagree, with Boolean operands it will never be vacuous. The
Boolean expressions themselves are no vacuous and "not' and "or"

do not turn non-vacuous into vacuous.



>>2. when property_expr1 is 'x', property_expr1 -> property_expr2 will
be 'x' whereas property_expr1 implies property_expr2 will be false.



[DB] I agree that it is a bit misleading, do you think that
(property_expr1 === 1) -> (property_expr2 === 1) is better?

or should we remove this sentence completely?



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.

---------------------------------------------------------------------
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.