I have assertion where for one antecedent state A there are two possible ways to reach state B .
Way one is timeout through time p. And another is if we see rise in signal q.
Can I wrote a assertion saying
In reply to Satputesb:
Two solutions, one for the static delay and another one for the dynamic delay.
The sva_delay_repeat_range_pkg is available in my signature below.
// Compile sva_delay_repeat_range_pkg.sv before the module
module m;
import sva_delay_repeat_range_pkg::*; // for use in dynamic delaya
typedef enum {A, B} st_e;
st_e st;
bit clk, rst, q;
int delay=5;
// Way one is timeout through STATIC time p. And another is if we see rise in signal q.
let p=4;
ap_stAB_static: assert property(@ (posedge clk)
disable iff(rst)
st==A |-> (##p st==8) or ($rose(q)[->1] ##1 st==B));
// If the delay is dynamic, use the package
/* Application: $rose(a) |-> q_dynamic_delay(d1) ##0 my_sequence;
ap_dyn_delay: assert property(@ (posedge clk)
$rose(a) |-> q_dynamic_delay(d1) ##0 my_sequence); */
ap_stAB_dynamic: assert property(@ (posedge clk)
disable iff(rst)
st==A |-> (q_dynamic_delay(delay) ##0 st==8) or ($rose(q)[->1] ##1 st==B));
endmodule : m
a. Is it possible to write it in a manner that by chance state is shifted to st=b without timeout p or without q is asserted , and thus assertion shows failure?
b. Is it possible to write (#p st==8) or ($rose(q)[->1] in antecedent?
In part a. I mean to say that assertion should fail if it is forced to move to next state without both the conditions met ie without the timeout or without arrival of signal q.
. For both part this failure criteria is the same requirment
In reply to Satputesb:
Two solutions, one for the static delay and another one for the dynamic delay.
The sva_delay_repeat_range_pkg is available in my signature below.
// Compile sva_delay_repeat_range_pkg.sv before the module
module m;
import sva_delay_repeat_range_pkg::*; // for use in dynamic delaya
typedef enum {A, B} st_e;
st_e st;
bit clk, rst, q;
int delay=5;
// Way one is timeout through STATIC time p. And another is if we see rise in signal q.
let p=4;
ap_stAB_static: assert property(@ (posedge clk)
disable iff(rst)
st==A |-> (##p st==8) or ($rose(q)[->1] ##1 st==B));
// If the delay is dynamic, use the package
/* Application: $rose(a) |-> q_dynamic_delay(d1) ##0 my_sequence;
ap_dyn_delay: assert property(@ (posedge clk)
$rose(a) |-> q_dynamic_delay(d1) ##0 my_sequence); */
ap_stAB_dynamic: assert property(@ (posedge clk)
disable iff(rst)
st==A |-> (q_dynamic_delay(delay) ##0 st==8) or ($rose(q)[->1] ##1 st==B));
endmodule : m
This assertion with static time delay is failing
ap_stAB_static: assert property(@ (posedge clk)
disable iff(rst)
st==A |-> (##p st==8) or ($rose(q)[->1] ##1 st==B));
at time p even if q is asserted before the timeout . Error says offending st == B