hi all,
I’m writing a formal environment for an arbiter.
Some of my assertions need to be constrained to very specific situations (e.g. in_1==0 && in_2!=0 &&… etc.).
To my understanding I can either:
model the specific situation to check the specific assertion (this can be done inline the property itself but will result in a very robust property or outside the property with some extra logic)
2.write assumptions for the different situations and use the relevant assumptions when running the assertion (separating the design to different ‘zones’).
My question is in general what would be a better practice?
In reply to gidon:
I would think that for formal verification, your 2nd suggestion is best because you document the assumptions of your design or zones. 2.write assumptions for the different situations and use the relevant assumptions when running the assertion (separating the design to different ‘zones’).
When you say model the specific situation to check the specific assertion (this can be done inline the property itself but will result in a very robust property or outside the property with some extra logic)
Are you saying that the property itself takes into account the assumptions?
That looks complex. Also, it does not separate the properties from the assumptions that model the outside environment. By documenting and reviewing the assumptions, you get a higher level of assurance that this is indeed the expected environment. The formal verification tool should be able to handle the analysis of all scenarios.
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.