In reply to Dharak:
property assert_check;
int v; // variable "delay" can be >0
// If set to "0", then no delay,
@(posedge clk) disable iff(disable_assertion)
($rose(a), v=delay+1'b1) |-> (1, v=v-1'b1)[*0:$] ##1 v==0 ##0 b == 1;
endproperty : assert_check
I want something like…
Assertion should start with $rose(a)
Then after “Delay” value ‘b’ should be high. ‘b’ must be high only after specific “Delay”. {Delay is a variable".
I am trying to inject an error but it is not firing.
Can you please confirm that its doing same thing.
When I first looked at your code, I concentrated on the property. Looking again at your code, I see that your “a” is a 4-bit vector. So if “a” goes from 4’b1000 to 4’b0100 the $rose(a) is 0, no change. In my first look, I assumed that “a” was a single bit.
Thus, the point I am making is that our $rose(a) is ambiguous. If you mean a change in “a”, you could use " $changed(a) " or " !$statble(a) " instead of " $rose(a) ".
What I wrote says that if a rose of a (i.e., vector goes from a value of 0 to a value of 1, then if the dealy has a value of 3, v=4; then in the same cycle, v gets decremented immediately, and then after every cycle until v==0. So, in 3 cycles, v==0, and at that time. b vector should be ==1 (i.e., the “b” should be greater than 0.
Watch your “bits” and “bit vectors”, there is a difference. If your vector b should be equal to your original vector a after a delay, you can do the following:
logic [3:0] delay,a,b;
property assert_check;
int v_delay, v_b; // variable "delay" can be 0
@(posedge clk) disable iff(disable_assertion)
($changed(a), v=delay+1'b1, v_b=a) |-> (1, v_delay=v_delay-1'b1)[*0:$]
##1 v_delay==0 ##0 b == v_b;
endproperty : assert_check