Clause: 17.11, 17.33.3, 29.4.3

Description

Currently, LRM mentions that if disable iff condition becomes true, the evaluation of property spec is true.

 

This makes it difficult for the users to identify the difference in match due to disable iff condition vs. match due to complete property evaluation. Therefore we propose to introduce another match condition called “disabled match”. This type of match only occurrs when disable iff condition of the property becomes true.

Suggested Resolution

Clause 17.11, replace the following on page 267:

 

For an evaluation of the property_spec, there is an evaluation of the underlying

property_expr. If prior to the completion of that evaluation the reset expression becomes true, then the overall

evaluation of the property_spec is true.

 

By

 

For an evaluation of the property_spec, there is an evaluation of the underlying

property_expr. If prior to the completion of that evaluation the reset expression becomes true, then the overall evaluation

of the property results in disabled success and returns true. A property has disabled success if it was preempted due to disable iff condition.

 

 

Clause 17.13.3, change the following on page 288:

 

The results of coverage statement for a property shall contain the following:

—      Number of times attempted

—      Number of times succeeded

      —   Number of times failed

—      Number of times succeeded because of vacuity

—   Number of times succeeded because of disabling

In addition, statement_or_null is executed every time a property succeeds.

Vacuity rules are applied only when implication operator is used. A property succeeds nonvacuously only if

the consequent of the implication contributes to the success. A property has disabled success if

it was preempted due to disable iff condition.

 

Clause 29.4.3, change the following on page 482:

 

vpi_get(vpiAssertSuccessCovered, assertion_handle)

returns the number of times the assertion has succeeded nonvacuously and without disabled success or, if the assertion handle corresponds

to a cover sequence, the number of times the sequence has been matched. Refer to 17.11.2 and 17.13 for the

definition of vacuity. Refer to 17.11 for the definition of disabled success.

 

vpi_get(vpiAssertDisabledSuccessCovered, assertion_handle)

returns the number of times the assertion has succeeded due to disable condition. Refer to 17.11 for the definition of disabled success.

 

 

For any assertion, the number of attempts that have not

yet reached any conclusion (success or failure) can be derived from the formula:

in progress = attempts - (successes + vacuous success + disabled successs + failures)

The example below illustrates some of these queries:

 

Clause 29.4.2, Add the following on page 481:

 

vpiAssertAttemptCovered

vpiAssertSuccessCovered

vpiAssertFailureCovered

vpiAssertVacuousSuccessCovered

vpiAssertDisabledSuccessCovered

 

Annex I, add the following:

 

#define vpiAssertAttemptCovered 770

#define vpiAssertSuccessCovered 771

#define vpiAssertFailureCovered 772

#define vpiAssertVacuousSuccessCovered 773

#define vpiAssertDisabledSuccessCovered 774

 

Clause 28.4.2, Add the following:

 

cbAssertionSuccess

when an assertion attempt reaches a success state.

cbAssertionVacuousSuccess

when an assertion attempt reaches a vacuous success state.

cbAssertionDisabledSuccess

when an assertion attempt reaches a disabled success state.