[sv-ac] placement of "disable iff"

All:

We currently require that "disable iff" be placed only at the top
level.

Discussions in P1800 about the relation of "disable iff" to coverage
and action blocks seem to have converged (or be converging) to
treating a disabled evaluation as neither "true" nor "false".

The formal semantics currently allows "disable iff" to be nested.  The
main reason for this was to simplify the inductive definition of the
semantics.

In the past, I have had the vision of relaxing the rules on "disable
iff" to make it nestable and an analog of PSL "abort".  However, this
will not work well with the "neither true nor false" treatment of
disabled evaluations.

Now my vision is different--that "disable iff" be restricted to the
top level eternally.  In the future, we can add accept/reject as in
ForSpec, or the PSL abort syntax, to serve as the nestable operators
that yield "true" or "false" results.

Assuming that we will keep "disable iff" at the top level eternally,
there is little or no use in putting it inside property declarations.
To me, it seems we should think of "disable iff" as attached to the
assertion directives.

What do people think about making this change syntactically?  

The change would introduce a backwards compatibility problem -- people
who have written "disable iff" expressions inside property
declarations would have to move them to the relevant assertion
directives.

The benefit would be a syntactic enforcement of the top-level rule.
And I think the usage of "disable iff" would be simplified.  People
would not have to worry about not being able to instantiate a property
with a "disable iff" inside another property.

I think we should also add a default "disable iff" at the module level
(and in other scopes where it makes sense) and have the default apply
to all the assertion directives that do not have otherwise specified
"disable iff" expressions.

Best regards,

John H.