RE: [sv-ac] weak sequence

I guess it brings us back to the fact that we do not have a defined
semantics for coverage.

My understanding was that w|= cover property(P) if for some i<|w| w^i..
|= P.

 

In this case if for some I w^i.. |= P because of the end of simulation
then it considered as a cover hit.

 

Maybe the right solution is to define coverage and weak strong
satisfaction for it, and say that for finite 

words the default is to require strong satisfaction.

 

Doron

 

________________________________

From: Lisa Piper [mailto:piper@cadence.com] 
Sent: Monday, September 24, 2007 3:15 PM
To: Bustan, Doron; sv-ac@eda-stds.org
Subject: RE: [sv-ac] weak sequence

 

Hi Doron,

 

I don't understand why "cover property" will lose its meaning.  Are you
thinking that weak means it will "pass" at the end of simulation? I am
thinking that it will neither pass nor fail, similar to what disable iff
does.

 

Lisa

 

________________________________

From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of
Bustan, Doron
Sent: Monday, September 24, 2007 8:58 AM
To: sv-ac@eda-stds.org
Subject: [sv-ac] weak sequence

 

All,

 

Dmitry rise a good point that in most cover properties we expect
sequences to be strong.

Once we change the default semantics of plain sequential property from
strong to weak, many

cover property will lose their meaning.

 

This backward compatibility problem is serious and we must do something
about it.

 

We thought about several options:

 

1.	Leave the default semantics strong - which mean that assertions
will need "weak" in many cases or that tools will continue to ignore

failures at the end of simulation.

2.	Make a distinction between the cover (expect?) statement and the
assume, assert statement, for the former use strong default and for the 

      later use weak.  This is problematic in case that not is used.

3.	try to define strong and weak for properties and then define
cover property to always be strong. The disadvantage here is that we
will not 

      be able to specify cover properties like (eventually always a)
that may be useful in formal.

 

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.