In reply to Jung Ik Moon:
In reply to ben@SystemVerilog.us:
Some more questions on your answer.
- The use of not of a sequence can be confusing. Why not making it a positive type of requirement. Thus instead of
- "my_seq to my_seq delay should not be less than my_timing.", use
- "my_seq to my_seq delay should be >= than my_timing."
- By modifying "should not be < than" to "should be >= than", isn't it more likely to become an incomplete assertion at the end of the simulation?
- How should I interpret incomplete assertions in this case? Can I just say it PASSED?
An assertion can be in one of the following states:
- pass or success
- in execution;
- Incomplete if the simulation ends and the assertion has not succeeded or failed.
An incomplete assertion will be identified as FAIL if the sequence is marked as strong.
Assertions are written to express requirements. I don't see a difference in expressing that a delay should not be less than or equal to5 cycles
and delay should be greater or equal to 5 cycles
. Where is the INCOMPLETION? An assertion is incomplete if you have not provided enough cycles in the simulation to complete.
Is is possible to write a property sticking to "should not be < than"? This is just to solve the incompleteness issue, IF needed.
- i.e., "when my_seq is issued, my_seq cannot be issued within my_timing."
int t, count=0;
@(negedge clk) disable iff (!rstn)
(my_seq, t = my_timing -1 ) |-> strong( // <--- the strong !!!!!
##1 first_match((1, count=count+1'b1)[*0:$] ##1 my_seq) ##0 (count >= t));
From my SVA Handbook Guideline
: Qualify as strong
properties that are sequences and have range delays or consecutive repetition operators (e.g., [*, [->, [= ) and are consequents in an assertion. This is important when it is necessary to qualify an assertion as a failure if the consequent never terminates at the end of simulation. Example:
ap_ab_recommend: assert property(@ (posedge clk) a |-> strong([1:$] b)); //
ap_ab_weak: assert property(@ (posedge clk) a |-> ([1:$] b)); //
ap_abc_recommend: assert property(@ (posedge clk) a |-> strong(b[*) ##1 c); //
ap_abc_weak: assert property(@ (posedge clk) a |-> (b[*) ##1 c); //
For training, consulting, services: contact http://cvcblr.com/home
* SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
* Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 978-1539769712
* 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
* 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