Hi Folks:
My understanding for a long time has been aligned with Dana's: that the
result of a non-disabled property evaluation is characterized in two
dimensions, the "pass/fail" dimension and the "vacuous/non-vacuous"
dimension. A priori, all pairs combining a disposition from the first
dimension with a disposition from the second dimension are possible.
This leads to the possible outcomes
(pass, vacuous)
(pass, non-vacuous)
(fail, vacuous)
(fail, non-vacuous)
I think that this perspective is consistent with the way the research
literature has approached the taxonomy: the primary outcome is whether
the evaluation passed or failed; the secondary outcome is whether the
evaluation was vacuous or non-vacuous. I thought we had language in the
LRM to express this perspective, but I have not been able to search for
it.
Other people have expressed some different opinions: see the discussion
with Ben Cohen.
Best regards,
John Havlicek
From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of Dana
Fisman
Sent: Tuesday, July 13, 2010 12:15 PM
To: Tapan Kapoor; Dana Fisman; 'Korchemny, Dmitry'; sv-ac@eda.org
Subject: [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 <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.Received on Sat Jul 17 05:45:27 2010
This archive was generated by hypermail 2.1.8 : Sat Jul 17 2010 - 05:46:27 PDT