I am guessing the behavior you want is for “data” (bit?) to go high, stay high for 3 cycles, and then go low. If so you want to check the whole sequence not just the end case.
You don’t have to call $rose, or posedge clock in the sequence declaration; it’s step delays already reference the clock from the @(posedge clk) code. ##1, etc, are inferred clock cycles.
I haven’t mastered assertion writing, so anyone feel free to verify the following line, but I think you want something more like:
Can Someone help me out in getting this right? ANd also suggest me if I can use posedge(clk) instead of $rose(clk)? If so, How the code looks like?
There are several things wrong with your property:
You declare a local variable and try to use this variable dynamically. In SVA, the delays and repeat operators have to be static.
$rose(data) would work well if data is a single bit, and not a vector.
$rose(clk) interprets “clk” as the signal, and that is sampled in the Preponed region, a delta time just BEFORE the posedge of clk, thus $rose(clk) is always ZERO.
Below is code that you can simulate.
import uvm_pkg::*; `include "uvm_macros.svh"
module mrose;
int data, numbx=4;
bit clk, a, b, reset=0, felld, rosed;
default clocking @(posedge clk); endclocking
initial forever #10 clk=!clk;
/* property a;
int no_of_times = 4
disable iff (reset)
@(posedge clk)
$rose(data) |-> ($rose(clk))[*no_of_times] |-> $fell(data)
endproperty */
property a_data;
// int no_of_times = 4
disable iff (reset)
@(posedge clk)
$rose(data[0]) |-> ##4 $fell(data[0]) // <-- FIXED DELAY
endproperty
ap_adata: assert property(a_data);
property pdata0_v;
int v;
disable iff (reset)
@(posedge clk)
($rose(data[0]), v=numbx) |-> // <-- variable delay
first_match((1, v =v- 1)[*0:$] ##1 v<=0) ##0 $fell(data[0]);
endproperty
apdata0_v : assert property(pdata0_v );
property p_v; // a generic property for
// $rose(a) |-> ##w b; // w is a module variable
// This in intended to be in 1800'2018
int v;
disable iff (reset)
@(posedge clk)
($rose(a), v=numbx) |->
first_match( (1, v =v- 1)[*0:$] ##1 v<=0 ) ##0 b;
endproperty
ap_v : assert property(p_v );
initial begin // testbench for the assertions
repeat(200) begin
@(posedge clk);
#1 if (!randomize(data, a, b) with
{ data dist {2:=1, 5 :=3};
a dist {1'b1:=1, 1'b0:=5};
a dist {1'b1:=1, 1'b0:=2};
}) `uvm_error("MYERR", "This is a randomize error")
end
$finish;
end
endmodule
($rose(a), v=numbx) |-> ((1, v =v- 1)[*0:$] ##1 v<=0)
// if rose(a) then v gets set to numbx
// in the consequent, expression "1" is true, and you have a repeat operator.
// Also,
(1, v =v- 1)[*0:$] ##1 v<=0 // is same as
(1, v =v- 1)[*0] ##1 v<=0 // same as v<=0
(1, v =v- 1)[*1] ##1 v<=0
(1, v =v- 1)[*1] ##1 v<=0
..
(1, v =v- 1)[*infinity] ##1 v<=0
// and at each cycle, when the consequent fail, v gets decremented.
Another option to have the range be linked to a dynamic module variable is to use the generate statement, which works OK for reasonable max values for the module variable. Example:
parameter N=2;
bit clk, a, b, c;
bit[2:0] v=3; // Max delay set to 7
default clocking @(posedge clk); endclocking
// ap_delay: assert property( $rose(a) |-> ##v b); // 1800'2018, illegal now
generate for (genvar g_i=0; g_i<8; g_i++) begin
ap_delay_gen: assert property (v==g_i && $rose(a) |-> ##g_i b);
end endgenerate
How to solve this:
The limitation is that: In SVA, the delays and repeat operators have to be static.So I am looking for an alternative code to replace the “cfg_p_cnt_and_fifo_depth”
variable
property check_interrupts(bit cfg_hb_en,int cfg_p_cnt_and_fifo_depth);
@(posedge clk) disable iff (!arst_n)
cfg_hb_en |-> i_p_dec[0][->cfg_p_cnt_and_fifo_depth] ##1 o_p_halt[0];
endproperty:check_interrupts
SVA: sig[->dynamic_var] // goto
int p1, f1, count=2, dbg;
bit w, b, clk;
function automatic void f(); dbg=dbg +1; endfunction
// b [->m] is equivalent to ( !b [*0:$] ##1 b)[*m]
// m must be static per 1800
sequence s_goto(bit a, int rpt);
int v =rpt;
@(posedge clk)
(!a[*0:$] ##1 (a, v=v-1'b1, f()))[*1:$] ##0 v<=0;
endsequence
ap_test: assert property (@(posedge clk)
$rose(w) |-> s_goto(b, count)) p1++;
else f1++;