How to use dynamic ##delay in assertion in questa formal propcheck tool

SystemVerilog
,
1

Hi Guys,

I am trying to use ##delay , where delay is updated dynamically. Now in Questa Sim SVA assertion i can do this like this and it work well over there.

property setbuck_low_after_max_duty;
int v;
@(posedge clk_bbctrl) disable iff (!rst_n) (rose(start_pulse),v=max_duty_cycle) |=> ((v>0,v=v-1)[*0:] ##1 v==0) ##0 !set_buck;
endproperty

But unfortunately in Questa formal tool is not able to handle this. And i am getting below warning.

Warning : Construct not supported by assertion compiler. File ‘/proj/gpfs/styv/CCG7S/styv_mxusbpd_s8_dev_116/vmxusbpd_s8/tb/fnv/formal/mxusbpd_bbctrl_top/propchk/mxusbpd_bbctrl_top_assert.sv’ line 123: this usage of local variables is not supported. [ac-3]

: Skipping construct.

Is these kind of constructs is not supported in formal verification. How do we address these issues?

Thanks,
Siddhant

2

In reply to Siddhant yadav:

This Siemens supported forum is not for tool related issues. Please refer to your tool documentation or contact your vendor support team for additional assistance.

3

In reply to Siddhant yadav:

  1. we don’t discuss tools in this forum.
  2. SVA does not support dynamic delays. However, it si possible to use
    dynamic delays using local variables. I encapsulated this concept
    in a package. See the link below:
    SVA Package: Dynamic and range delays and repeats
    SVA: Package for dynamic and range delays and repeats | Verification Academy

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
…

  1. SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats | Verification Academy
  2. Free books: Component Design by Example FREE BOOK: Component Design by Example … A Step-by-Step Process Using VHDL with UART as Vehicle | Verification Academy
    Real Chip Design and Verification Using Verilog and VHDL($3) https://rb.gy/cwy7nb
  3. Papers:

Udemy courses by Srinivasan Venkataramanan (http://cvcblr.com/home.html)
https://www.udemy.com/course/sva-basic/
https://www.udemy.com/course/sv-pre-uvm/