SVA examples to avoid #[0:N] when N is big

Hello,

I’d have some assertions with something like this

assert property (@(posedge clk) disable iff(reset) a |-> ##[0:50000] b);

As you can see the interval on which b can occur is very big, and I even get warnings from the simulator(s) but this is the timing defined in the specification, I was wondering if there are other ways of work around this, maybe some helper logic but I’m not entire sure how to rewrite the assertion and the how the helper logic would need to look like.

Any pointers are really appreciated,

-R

In reply to rgarcia07:

I don’t know why that is a tool issue since tools can handle the [1:$] and the goto operator.

In any case, consider using the task model described in my paper
SVA Alternative for Complex Assertions
https://verificationacademy.com/news/verification-horizons-march-2018-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

  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

In reply to ben@SystemVerilog.us:

[0:$] would actually be easier to handle than the case where you have an upper bound. It would just mean counting up for a and counting down for b. With a fixed bound, the tool also needs to manage the “timeouts”.

In reply to Tudor Timi:

In reply to ben@SystemVerilog.us:
[0:$] would actually be easier to handle than the case where you have an upper bound. It would just mean counting up for a and counting down for b. With a fixed bound, the tool also needs to manage the “timeouts”.

 
 |-> ##[1:50000] b ##3 c
The consequent is multi-threaded 
   (##1 b ##3 c) or (##2 b ##3 c) or... 
 
This get really messy in terms of multi-threading
 |-> ##[1:50000] b ##[1:10] d
(##1 b ##1 d) or (##1 b ##2 d) or (##1 b ##3 d) or. 

... 
(##1 b ##1 d) or (##2 b ##1 d) or (##3 b ##1 d) or.. 
(##1 b ##2 d) or (##1 b ##3 d) or (##1 b ##3 d) or.. 
.... Lots of threads... 
.. 
(##50000 b ##1 d) or (##50000 b ##2 d) or (##50000 b ##3 d) or

The simulator operates on threads. With the 50k and 10 ranges you have 500k threads.

There is optimization by the tool, maybe something like dynamically created threads depending on dynamic results on clock basis. I am not a tool builder. However, fundamentally, each range creates that many threads and when you compute the combinations, that’s quite a large number.
Ben systemverilog.us