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.
@(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;
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?