In reply to ben@SystemVerilog.us:
I think the OP is talking about assumptions that don’t always hold on the “outside environment”. These assumptions are there to be able to write more focused properties, which shouldn’t always hold. I’d say it’s easier to understand this fact if such assumptions are part of the property/assertion itself.
I hear OneSpin’s ITL had some nice syntax to easily enable this, but in SV this would probably be more work, depending on the type of assumption. Simple things like “P holds after X but not if Y” are easily modeled in antecedents, but stuff like “P holds after X, but not if at any point in time Y” might be more difficult to write (though it might be possible using property operators, e.g. in this case ‘(X |=> P) or (Y)’ - never tried anything like this out). You could take these shortcut assumptions out into own “assume” properties (maybe even better, as “restrict” properties), but you’d have to make sure they’re only active for the evaluations of your focused properties, which implies you have to do a lot of scripting outside of the SV language.