System Verilog assertion [1:$] query

[aman_intel]

Hi ,

I have written a property
with logic rose(a) |-> ##[1:] ($rose(b) || $rose (c)) |-> ( (c&~d) || (b&d));

Expectation is : On rose of a , wait for rose of b or c , whichever comes first , if b came, d should be 1. if c came d should be zero.
Issue Faced :
in case of rose of a followed by rose of b followed by rose of c , assertion fails at rose of c.

But shouldn’t rose of b kill that thread which was triggered on rose of a.

Thanks
Aman

[sharvil111]

In reply to aman_intel:

Can you please post an MCVE and a waveform snapshot for the issue.

I believe that we can use first_match over here.

[user49]

In reply to aman_intel:
If a multi-threaded sequence is used in an antecedent (e.g., a ##1 b[*1:3] ##1 c |-> d), then all threads must be tested with its consequent for the assertion to terminate as successful.
Two possibles fixed:

1. Use first_match()
2. Use the goto operator ( expr[->1] )

On style, use logical operator (e.g., &&, !) instead of bitwise operators (e.g., &, ~)

$rose(a) |-> first_match(##[1:$] ($rose(b) || $rose (c))) |-> (c&& !d) || (b &&d)
// I prefer the goto in this case
$rose(a) |-> (($rose(b) || $rose (c)))[->1] |-> (c&& !d) || (b &&d)
 

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

---

1. SVA Alternative for Complex Assertions
   Verification Horizons - March 2018 Issue | Verification Academy
2. SVA: Package for dynamic and range delays and repeats | Verification Academy
3. SVA in a UVM Class-based Environment
   SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy

[user49]

In reply to ben@SystemVerilog.us:
One more comment on the coding form

$rose(a) |-> (($rose(b) || $rose (c)))[->1] |-> (c&& !d) || (b &&d)
// or more simply
sequence1 |-> sequence2 |-> sequence3

In general, I see no need to break the property (sequence2 |-> sequence3) as 2 sequences with an implication operator. I generally prefer to change that to (sequence2 ##0 sequence3)
The differences between the two is vacuity.

 
sequence1 |-> sequence2 |-> sequence3  // vacuous if sequence2 is a non_match
sequence1 |-> sequence2 ##0 sequence3 //  Fail if sequence2 is a non_match

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

---

1. SVA Alternative for Complex Assertions
   https://verificationacademy.com/news/verification-horizons-march-2018-issue
2. SVA: Package for dynamic and range delays and repeats - SystemVerilog - Verification Academy
3. 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