anyone tell me about
How many time we can use non-overlapping operator in single line assertion property?
I don’t think there is any such restriction…but not recommended, this will make your assertion complicated, i.e tough to debug and to check for vacuous success
you could break this down into many simpler assertions…
In reply to ssureshg_:
The answer to this question is the understanding of the definition of a property.
essentially, a property is one of the following
property_expr ::=
sequence_expr
| strong ( sequence_expr )
| weak ( sequence_expr )
| ( property_expr )
| not property_expr
| property_expr or property_expr
| property_expr and property_expr
| sequence_expr |-> property_expr
| sequence_expr |=> property_expr
....
more options
Thus, since a property expression is sequence_expr |=> property_expr, one could then say
a property expression is one of the following:
sequence_expr |=> property_expr
sequence_expr |=> (sequence_expr |=> property_expr)
sequence_expr |=> (sequence_expr |=> (sequence_expr |=> property_expr))
and so on
However, the following would be illegal
a |=> not(c & d) |=> e;
This is becuase {not(c & d)} is a property and it is not a sequence,
and property_expression |=> property_expression is illegal.
I provide such explanation in my SVA Handbook
http://systemverilog.us/vf/seq_prop.pdf is a link to one page that explains this.
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
In reply to ssureshg_:
so for example
i want to checked sequence like
first at positive edge of clock check ‘A’ and if ‘A’ high then
in very next positive edge of clock check ‘B’ and if ‘B’ high
in very next positive edge of clock check ‘C’ and if ‘C’ high
then my Assertion pass
so can i write
A|=>B|=>C
or
can i write
A ##1B ##1C
which one right??
with this requirement
i want to checked sequence like
first at positive edge of clock check ‘A’ and if ‘A’ high then
in very next positive edge of clock check ‘B’ and if ‘B’ high
in very next positive edge of clock check ‘C’ and if ‘C’ high
you can write as:
A |=> B |=> C
If you write like this
A ##1 B ##1 C
then if at positive edge of clock your A change from 0 to 1 then it will offend and will fail.
It is like race condition in this case.
Thank you
- A ##1 B ##1 C will pass even if all signals are tied high - not sure if that is what you want…
- sequence will be triggered on all clocks as long as these signals are high, leading to performance hit. typically you should qualify triggers with $rose, $fell etc to
In reply to ssureshg_:
What bothers me about the original question is that the author lacks understanding of the basics in assertions. Those basics include the concepts of vacuity, attempts, multi-threading, and the language syntax (e.g., property, sequence).
I strongly suggest a good book on the topic. I wrote some, but there are many books and free courses and videos that address assertions.
I recently published a paper that helps in the understanding of assertions.
PAPER: Understanding the SVA Engine + Simple alternate solutions | Verification Academy
Abstract: Understanding the engine behind SVA provides not only a better appreciation and limitations of SVA, but in some situations provide features that cannot be simply implemented with the current definition of SVA. This paper first explains, by example, how a relatively simple assertion example can be written without SVA with the use of SystemVerilog tasks; this provides the basis for understanding the concepts of multithreading and exit of threads upon a condition, such as an error in the assertion. The paper then provides examples that uses computational variables within threads; those variables can cause, in some cases, errors in SVA. The strictly emulation model with tasks solves this issue.
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
In reply to ben@SystemVerilog.us:
thank you so much for your time and valuable response.
i always respect of your dedication.