In reply to Mechanic:
In reply to ben@SystemVerilog.us:
- 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 don’t get the enabling condition then we will end-up with vacuous pass.
True. The antecedent is a sequence of one or more terms.
But in case of clock delay operator if the antecedent fails then the property will fail (a ##0 b).*
In
ap: assert property(@ (posedge clk) (a ##0 b) );
there is NO antecedent. (a ##0 b) is a sequence. An assertion of a property that is a sequence can never be vacuous; its evaluation is either true or false.
- 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.
1800 defines s_eventually as:
(s_eventually p) equivalent to (not (always(not p))
This means that it is NOT the case that the property p is always FALSE; it can be true. If I use the assert statement using the s_eventually property operator, then I am saying that there must be a case hen the property is true. See
If the property is a sequence then
req |-> s_eventually ack // equivalent to
req |-> strong(##[*0:$] ack) // Terminates or error if incomplete
req |-> s_eventually[1:5] ack // equivalent to
req |-> strong (##[1:5] ack)
It is used for formal verification.
]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
- 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.
Correct
- 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.
correct
*
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…”.
I would not call it the latest features. I see it as expressing assertions in more readable options. Many of these properties express safety and livneess. see slide 22 of
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr
- SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
- A Pragmatic Approach to VMM Adoption 2006 ISBN 0-9705394-9-5
- Using PSL/SUGAR for Formal and Dynamic Verification 2nd Edition, 2004, ISBN 0-9705394-6-0
- Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 978-1539769712
- Component Design by Example ", 2001 ISBN 0-9705394-0-1
- VHDL Coding Styles and Methodologies, 2nd Edition, 1999 ISBN 0-7923-8474-1
- VHDL Answers to Frequently Asked Questions, 2nd Edition ISBN 0-7923-8115
- SVA Alternative for Complex Assertions
https://verificationacademy.com/news/verification-horizons-march-2018-issue - SVA: Package for dynamic and range delays and repeats - SystemVerilog - Verification Academy
- SVA in a UVM Class-based Environment
https://verificationacademy.com/verification-horizons/february-2013-volume-9-issue-1/SVA-in-a-UVM-Class-based-Environment