Hi All,
I want to write an assertion which checks a value continuously for a variable number of cycles as shown below :
@posedge (clock) ($rose(a)) |=> ((data == 4'h5)[*cycles]);
Can you tell me how to implement this in SVA?
Thanks
Hi All,
I want to write an assertion which checks a value continuously for a variable number of cycles as shown below :
@posedge (clock) ($rose(a)) |=> ((data == 4'h5)[*cycles]);
Can you tell me how to implement this in SVA?
Thanks
I provide 2 solutions in my SVA Handbook 4th Edition, 2016
*Simple repeat (e.g., a[v]]
ap_repeat_fix: assert property( $rose(a) |-> b[*v] ##1 c); //1800'2018 property
// Above is illegal in 1800'2012
p_repeat_equivalent; // /11.4/m5067_gen_options.sv. works in 1800'2012
int local_v; //
$rose(a) |->
(1, local_v = v) ##0 first_match((b, local_v=local_v - 1)[*0:$] ##1 local_v<=0)
##0 c; //
endproperty
ap_repeat_equivalent: assert property(p_repeat_equivalent); // with default clocking
generate option
If the variable used to define the repeat has values that are within a constraint range, such as between 0 and 7 (or 15, or at most 32) one can use the generate statement, which appears much simpler than the use of local variables and the sequence_match_item.
generate for (genvar g_i=0; g_i<8; g_i++) begin
ap_repeat_gen: assert property (v==g_i && $rose(a) |-> b[*g_i] ##1 c);
end endgenerate
The generate
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr
In reply to ben@SystemVerilog.us:
Hi Ben,
Thanks for your answer. In your second method, can you tell me what does first_match do? Though I don’t know the exact functioning of that, I tried to imitate it in my example below. Can you tell me if I’m right?
p_repeat_equivalent;
int local_v; //
$rose(a) |->
(1, local_v = v) ##0 first_match((b == 4'h5, local_v=local_v - 1)[*0:$];
endproperty
ap_repeat_equivalent: assert property(p_repeat_equivalent);
Thanks,
In reply to szy0014:
In my model (see below), if b==1 at all cycles (i.e., dc), and c==0 at all cycles, then without the first_match()the assertion will never complete, even if v==1 (the repeat will keep on trying searching for a c==1).
(1, local_v = v) ##0 first_match((b, local_v=local_v - 1)[*0:$] ##1 local_v<=0)
##0 c; //
Your case does not have “c”. thus, the following will work
p_repeat_equivalent;
int local_v; //
$rose(a) |->
(1, local_v = v) ##0 (b == 4'h5, local_v=local_v - 1)[*0:$] ##1 local_v<=0;
endproperty
ap_repeat_equivalent: assert property(p_repeat_equivalent);
The first_match() is not needed because if b==0 at any cycle, the assertion will fail. If b==1 at all cycles (i.e., dc), the assertion will terminate successfully after v cycles.
If You had a term after the repeat, like my “c”, then the first_match() would terminate the count (because, eventually, local_v will be <=0 if b==1 during those cycles), and then you would test for he other terms in the sequence. remember
b[*0:$] ##1 c// is same as
c or (b ##1 c) or (b ##2 c) or (b ##n c)
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr