RE: [sv-ac] RE: Call to vote. Due September 13

Hi Dana:

My recollection is that SV-AC was asked to clarify the meaning of
vacuous/non-vacuous evaluation because of the requirement for tools to
report counts of these things.

J.H.

From: Dana Fisman [mailto:Dana.Fisman@synopsys.com]
Sent: Monday, September 13, 2010 4:26 PM
To: Havlicek John-R8AAAU; Korchemny, Dmitry; sv-ac@eda.org
Subject: RE: [sv-ac] RE: Call to vote. Due September 13

Hi Dmitry,

I agree with John. Moreover, I am not sure why the LRM decided to
include a definition for vacuity and what criteria was it set to meet.

Put that aside, I think the defs of the aborts follow the general
intuition of vacuity. A property is vacuous if there exists a subformula
that need not be checked in order to conclude whether the whole formula
holds (or fails).

Take a general abort formula

abort_op(cond) subprop.

Then if cond holds in some clock of the evaluation attempt then surely
some parts of subprop need not be checked. Thus it should be vacuous. If
cond does not hold during the evaluation attempt, then subprop needs to
be checked, we can know whether some parts of it need not be checked
following the recursive definition. Cond was checked as well, thus
subprop determines vacuity in this case.

Dana

From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of
Havlicek John-R8AAAU
Sent: Monday, September 13, 2010 8:05 PM
To: Korchemny, Dmitry; sv-ac@eda.org
Subject: RE: [sv-ac] RE: Call to vote. Due September 13

Hi Dmitry:

I am not sure that any definition of vacuity for the abort operators
will be ideal in all cases. I have not been too worried because our
vacuity definition is fairly crude; more refined notions of formula and
subformula coverage can be defined and are useful.

For fails, I think that all of them require analysis, whether vacuous or
not.

J.H.

From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of
Korchemny, Dmitry
Sent: Monday, September 13, 2010 10:43 AM
To: Seligman, Erik; sv-ac@eda.org
Subject: [sv-ac] RE: Call to vote. Due September 13

I think that this is first of all a specific question about aborts: if
the abort condition is true, should we consider the property evaluation
as vacuous? Of course, there are many different definitions of vacuity,
we should select the most basic one.

According to our definition (scan || read_cond) is never vacuous as a
Boolean expression. 16.15.8 Nonvacuous evaluations reads:

An evaluation attempt of a property that is a sequence is always
nonvacuous.

If we rewrite you property as (scan or read_cond) it will still have
only nonvacuous evaluations:

An evaluation attempt of a property of the form property_expr1 or
property_expr2 is nonvacuous if, and only if, either the underlying
evaluation attempt of property_expr1 is nonvacuous or the

underlying evaluation attempt of property_expr2 is nonvacuous.

since property_expr1, 2 are Boolean in our case.

Thanks,

Dmitry

From: Seligman, Erik
Sent: Monday, September 13, 2010 5:17 PM
To: Korchemny, Dmitry; Korchemny, Dmitry; sv-ac@eda.org
Subject: RE: Call to vote. Due September 13

Isn't this a common problem for vacuity though, if the user decides to
'cheat' and use parts of the definition in different ways than intended?

We also see bogus vacuity reports when we have combo assertions that
account for enable bits, such as (scan || real_cond), always having a
vacuous term when scan is tied low for FPV.

I think there is a bigger question here, about whether we should
consider some language mechanism for better vacuity checking control.

From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of
Korchemny, Dmitry
Sent: Sunday, September 12, 2010 1:38 PM
To: Korchemny, Dmitry; sv-ac@eda.org
Subject: [sv-ac] RE: Call to vote. Due September 13

Hi all,

Some thoughts about vacuity definition for aborts.

Sometimes the only possible success or failure of a property with aborts
is a vacuous one. This is not specific to synchronous aborts. Consider
the following example:

sig should remain high at least n clock ticks after rise.

!sig ##1 sig |-> reject_on(!sig) 1'b1[*n + 1]

According to our definition this property may have only vacuous
failures, though I would not define them as such.

Thanks,

Dmitry

From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of
Korchemny, Dmitry
Sent: Wednesday, September 08, 2010 12:13 PM
To: sv-ac@eda.org
Subject: [sv-ac] Call to vote. Due September 13

-You have until 11.59 pm PDT, Monday, September 13, 2010 to respond
-An issue passes if there are zero NO votes and half of the eligible
 voters respond with a YES vote.
-If you vote NO on any issue, your vote must be accompanied by a reason.
 The issue will then be up for discussion during a future conference
call.
-Note: For some issues, the proposed action is captured in the bug note
       (resolve as duplicate, already addressed, etc.).
 
As of the September 7, 2010 meeting, the eligible voters are:
 
Laurence Bisht
Eduard Cerny
Ben Cohen
Surrendra Dudani
John Havlicek
Tapan Kapoor
Manisha Kulshrestha
Scott Little
Anupam Prabhakar
Erik Seligman
Samik Sengupta
Tom Thatcher
 
SVDB 2452 ___Yes ___No

http://www.eda-stds.org/mantis/view.php?id=2452

http://www.eda-stds.org/mantis/file_download.php?file_id=4379&type=bug

---------------------------------------------------------------------
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 <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 <http://www.mailscanner.info/> , and is
believed to be clean. 
-- 
This message has been scanned for viruses and 
dangerous content by MailScanner <http://www.mailscanner.info/> , and is
believed to be clean. 
-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.