Legal ways to specify the leading clock in SVA

In reply to Have_A_Doubt:

1800 16.16 and 16.16.1 exhaustively go thru al the rules for inferred leading clocking event (LCE). It is tiresome to read and fully comprehend. Byt in simple terms, and as a guideline, if the property does not have a clocking event then the inferred LCE is only in an always in the style of always @(clocing_event)
Just stick to this rule if you do not want to include the clocking event in the assertion.
You’re making life too complicated if you violate simple design rules; and that is true for SV in general. Funky stuff can lead to funky behavior.
Ben