[sv-ac] RE: Mantis issue assignment

Hi Tapan,

I did not mean that attempt evaluation and property evaluation are orthogonal. Clearly, property evaluation relies on attempts evaluations. What I meant is orthogonal is whether the property (or an attempt) are evaluated to true/false and whether they are evaluated as vacuous/non-vacuous.

The meaning of "vacuous false" would be that the property is evaluated to false, but actually, there is a sub-property of it that need not be evaluated at all to reach that conclusion. For instance, a property which is a conjunction of a very complicated property and the property p would be vacuous false on a design where p does not hold (since one needs not evaluate the complicated sub-property to reach that decision).

Regarding the confusion between 16.13.14 and 16.15.8 are you referring to the fact that 16.13.14 involves both "disabled" and "true"? What are the "two constructs" you say are considered equivalent in 16.15.8?

Thanks,
Dana

From: Tapan Kapoor [mailto:tkapoor@cadence.com]
Sent: Tuesday, July 13, 2010 5:58 PM
To: Dana Fisman; 'Korchemny, Dmitry'; sv-ac@eda.org
Subject: RE: Mantis issue assignment

Hi Dana,

I do not understand this "orthogonal" definition of attempt evaluation and property evaluation. The evaluation attempt is on a property and checks/verifies it's expression (property-expression) i.e. if the design complies to property-expression. The property's evaluation is an outcome of the attempt's result. Also, if we take this definition, what would be the interpretation of "vacuous false"?

I think the confusion has it's root in the seemingly conflicting definitions in sections 16.13.14 and 16.15.8. Section 16.13.14 differentiates abort properties from disable-iff as:
While a disable condition of a disable iff in a property_spec may cause an evaluation of the
property_spec to be disabled, an abort condition of accept_on in a property_expr may cause the
evaluation of the property_expr to be true.

Whereas, section 16.15.8 seems to consider the two constructs equivalent...

Warm regards,
Tapan
"You must be the change you want to see in the world" : Mahatma Gandhi
From: Dana Fisman [mailto:Dana.Fisman@synopsys.com]
Sent: Tuesday, July 13, 2010 6:54 PM
To: Tapan Kapoor; Dana Fisman; 'Korchemny, Dmitry'; sv-ac@eda.org
Subject: RE: Mantis issue assignment

Tapan,

To my understanding the two are orthogonal. An evaluation attempt can be either vacuous or nonvacuous.
A property is evaluated either to true or false. All 4 combinations are possible. And when it reads that a property evaluates to "true" it does not say whether it is vacuously true or nonvacuoulsy true. This is the purpose of Section 16.15.8.

The only sentence I found relating the two concepts is at the end of 16.15.8 saying "An evaluation attempt of a property succeeds nonvacuously if, and only if, the property evaluates to true and the evaluation attempt is nonvacuous." But note that it reads " ***succeeds*** nonvacuously".

Is there a connection made in the LRM that I am missing?

Dana

From: Tapan Kapoor [mailto:tkapoor@cadence.com]
Sent: Tuesday, July 13, 2010 3:38 PM
To: Dana Fisman; 'Korchemny, Dmitry'; sv-ac@eda.org
Subject: RE: Mantis issue assignment

Dana,

My point is - the two definitions does not seem consistent. The LRM says result is "true", whereas your proposal makes it "vacuous true". Also, if we consider sync_reject_on, the LRM says result (when abort expression is true) is "false", whereas the proposal makes it "vacuous false" (a term perhaps needed to be defined/explained).

Warm regards,
Tapan
"You must be the change you want to see in the world" : Mahatma Gandhi
From: Dana Fisman [mailto:Dana.Fisman@synopsys.com]
Sent: Tuesday, July 13, 2010 5:00 PM
To: Tapan Kapoor; Dana Fisman; 'Korchemny, Dmitry'; sv-ac@eda.org
Subject: RE: Mantis issue assignment

Hi Tapan,

The proposal regards this case. It says

" - An evaluation attempt of a property of the form sync_accept_on(expression_or_dist) property_expr is
nonvacuous if, and only if, the underlying evaluation attempt of property_expr is nonvacuous and
expression_or_dist does not hold in any clock event of that evaluation attempt."

Thus, if expression_or_dist is true the evaluation attempt is vacuous true.

Am I missing something?

Dana

From: Tapan Kapoor [mailto:tkapoor@cadence.com]
Sent: Tuesday, July 13, 2010 1:57 PM
To: Dana Fisman; 'Korchemny, Dmitry'; sv-ac@eda.org
Subject: RE: Mantis issue assignment

Hi Dana,

Regarding #2452:

What about the case where "expression_or_dist" is true? For example, in case of sync_accept_on LRM says:
If during the evaluation, the abort condition becomes true, then the overall evaluation of the property results in true.

Are these evaluations non-vacuous or vacuous true?

Similarly, in case of sync_reject_on, (the case when abort expression is true) result could be considered vacuous or non-vacuous false. (I am not sure if vacuous false is a well understood term).

Warm regards,
Tapan
"You must be the change you want to see in the world" : Mahatma Gandhi
From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of Dana Fisman
Sent: Tuesday, July 13, 2010 12:25 PM
To: 'Korchemny, Dmitry'; sv-ac@eda.org
Subject: [sv-ac] RE: Mantis issue assignment

Proposals for the following mantis items have been uploaded.

0002452: No vacuity information about synchronous aborts
http://www.eda-twiki.org/mantis/view.php?id=2452

0002904: Clarify when disable iff condition must occur relative to starting and ending of an attempt http://www.eda-twiki.org/mantis/view.php?id=2904

0003134: sequence and property range parameters are erroneously defined
http://www.eda-twiki.org/mantis/view.php?id=3134

0003135: Verbal explanation of nexttime and always is misleading for multiple clocks.
http://www.eda-twiki.org/mantis/view.php?id=3135

Please review and comment.

Thanks,
Dana

From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of Korchemny, Dmitry
Sent: Monday, June 28, 2010 8:16 AM
To: sv-ac@eda.org
Subject: [sv-ac] Mantis issue assignment

Hi all,

Below is the list of Mantis items along to their assignment to the committee members. I also updated the ownership in Mantis except for those people who do not have a developer Mantis account.

Actions required:

* Address each Mantis item assigned. This may be done in one of the following ways:

o Write a solution proposal

o Argue that the Mantis item does not need to be implemented

o Argue that the Mantis item resolution may be postponed to the next PAR

* Present and discuss the resolution in SV-AC meetings or request an email ballot.

Effort allocation

* One Mantis item resolution in two weeks per person. Larger Mantis items may require more time to address.

2353

 'classes' missing from description

Anupam

2546

 'empty match' and 'vacuous success' are not clearly defined in LRM

Anupam

2934

 Precedence and associativity of case operator is not shown in the table

Anupam

2825

 16.16 Disable iff checkers not included in list of default extensions

Ben

2927

 Precedence between sequence/property operator and normal expression operator

Ben

2452

 No vacuity information about synchronous aborts

Dana

2904

 Clarify when disable iff condition must occur relative to starting and ending of an attempt

Dana

2476

 Need clarification about system functions $onehot, etc

Dmitry

2551

 trivial example error

Dmitry

2552

 Confusing comments regarding nexttime operator

Dmitry

3008

 In $past BNF, "expression" should be "expression1"

Dmitry

3015

 Examples of $fatal have bad arguments

Dmitry

1756

 The LRM does not indicate how the control tasks $asserton/off/kill affect verification statements in initial blocks

Ed

1763

 The LRM does not define whether assertion control tasks affect sequence methods and events

Ed

2839

 Contradictory statement of increment/decrement operators usage.

Ed

2491

 Conflicting rules in 16.17 (D7)

Erik

2557

 Rules for passing automatic variables to sequence subroutines are not clear

Erik

2938

 Surprising (to some users) interaction between deferred assertions & short-circuiting

Erik

2248

 Champions feedback - items related to Mantis item 1683

John

2479

 Annex F.5.2.1 conflicts with changes from 2434

John

2871

 Clause 16 does not forbid assertion local variables within clocking event expressions

John

2556

 Explicit package scope indication is not allowed for checkers

Laurence

2809

 Checker instantiation in checkers' always procedure

Laurence

1627

17.16 clarify that expect statement not allowed in functions

Manisha

2255

 clarifications on expect

Manisha

3117

make it clear that rewriting algorithm (F.4.1) applies to checker and let

Manisha

1678

 Clarify that rewriting algorithm doesn't replace name resolution

Scott

2386

 Rename 16.9 to "Local variables"?

Scott

2571

 confusing assertion clock inference rule

Scott

1853

 BNF for calls to $rose and other sample value system functions

Surrendra

2485

 terminology related to immediate and deferred assertions

Surrendra

2558

 Restriction inside checker construct

Surrendra

2271

 sequence events require a clocked sequence

Tapan

2340

 clarifications needed on vpi_control for non-temporal and immediate assertions

Tapan

2494

 37.44 Assertion diagram missing restrict

Tapan

2095

 Clarify meaning of distribution as condition for "disable iff"

Tom

2722

 Errors in Figures 16-14, 16-15, and 16-16

Tom

2754

 P1800-2009 Can clock change in conditional branch of 'if' operator

Tom

Thanks,
Dmitry

---------------------------------------------------------------------

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