SVA sequence doubt

[Bhaskar44]

systemverilog]property tester (res, res_exp);
@(posedge clk)
rose(opcode_add) |-> (instr == 200)[*1:] ##1 (instr == 205)[*1:$] ##1 ((instr==210) throughout $fell(opcode_add)[->1]);
endproperty

The objective of the above SVA was to check that during an opcode_add, instr=200, 205, 210. 

1. Pass scenario: 200,205,210
2. Fail scenario: 
- 200,206,210
- 200,205

But the problem is the SVA doesn't end at the falling edge of opcode_add (irrespective of if the sequence was finished or not) and still continues. 
Ex: 200, fall edge of opcode_add - Sequence drag continues. 

It would really help, if the there is a way I could do it.

[ben2]

In reply to Sirius44:

You need the intersect
rose(opcode_add) |-> ((instr == 200)[*1:] ##1 (instr == 205)[*1:$] ##1 (instr==210)) intersect $fell(opcode_add)[->1];

BTW, the syntax for the use of the throughout is
| expression_or_dist throughout sequence_expr
Thus,

   ap_ILLEGAL: assert property($rose(a) |-> (a[*2] ##[1:$] b) throughout d[->1]);  
Compiler: near "throughout": syntax error, unexpected "SystemVerilog keyword 'throughout'"

ap_abc: assert property($rose(a) |-> (a[*2] ##[1:$] b) intersect d[->1]) ; // OK 

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
• 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

---

See Paper: 1) VF Horizons:PAPER: SVA Alternative for Complex Assertions | Verification Academy
2) http://systemverilog.us/vf/SolvingComplexUsersAssertions.pdf

[Bhaskar44]

In reply to ben@SystemVerilog.us:

Dear Ben

Thanks for the reply. I understand that intersect would work but I have a concern:
What if both (a[*2] ##[1:$] b) and $fell(d) didn’t occur but $rose (a) occured ? I am facing a similar issue and hence trying to understand the solution.

Thanks!

[ben2]

In reply to Sirius44:
I don’t understand your question.

ap_abc2: assert property($rose(a) |-> (a[*2] ##[1:$] b) intersect d[->1]) ; 
   // What if both (a[*2] ##[1:$] b) and $fell(d) didn't occur 
   // but $rose (a) occured ? 
   // I am facing a similar issue and hence trying to understand the solution.
 

What are your requirements? Assertion ap_abc2 states that upon a rose(a), then “a” is true at the current (which it is because of the rose(a)), and also true at the next cycle; This is then followed by b sometime later. All of that consequent is within *!d[0:d] ##1 d.
If *(a[2] ##[1:$] b)) fails at any time, the assertion fails. The intersect is like an and, but more specific in that the LHS and RHS sequences match in those time frames (rather than at any time (for the and).
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
• 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

---

See Paper: 1) VF Horizons:PAPER: SVA Alternative for Complex Assertions | Verification Academy
2) http://systemverilog.us/vf/SolvingComplexUsersAssertions.pdf