Assertions

SystemVerilog
3

In reply to ben@SystemVerilog.us:

  1. what is the purpose of an antecedent?
    Antecedent acts as an enabling condition for the assertion. In case of Implication operator (a|->b)if we dont get the enbling condition then we will end-up with vacuous pass.But in case of clock delay operator if the antecedent fails then the property will fail (a ##0 b).

  2. what is the definition of the s_eventually?
    Is it a sequence or a property?
    S_eventually [cyclle delay constant range] property_expression (strong form with unbounded range).
    I am not clear with eventually definition.

  3. what is the meaning of the “s_”
    It is a strong property operator which means if we run out of simulation tics then the property will fail

  4. when is it desirable to define a consequent as “strong”?
    a|->##[1:$]b if b is not true until the end the simulation then the assertion wont fail.But if we use strong then the assertion will fail.

  5. what is the definition of the “until”?
    *A property “property_expression_1 until property_expression_2” (req until gnt)evaluates to true if and only if req must be true until gnt is true. req need not be true at the clock tick when gnt is true.

[quote]

Yes, SVA is rich in options i would like to know whether the above manipulated assertions for S_eventually and until are correct.
As for my understanding instead of walk-around with manipulated assertions we simply use the latest features that is the only advantage of the “eventually and until…nexttime…so onn…”.

Please let me know

Thanks in advance