I am new to Assertions, I wanted to write an assertion for rate counter. The requirement is the sig a should be high for 5 out of 6 sys_clk cycles. The 5 cycles can be of any pattern.
As I understand within can be helpful in writing the above assertion
The following is the code I have comeup with but its failing
Your requirements are ambiguous. When you say ““a” should be high for 5 out of 6 sys_clk cycles. The 5 cycles can be of any pattern”, what do you mean by 5 cycles can be of any pattern. If they are not contiguous, meaning you can have any 5 non-contiguous ONEs within any 6 cycles, then there is a need for a frame signal for those 6 cycles.
Commenting on your code, $rose(clk)[*6] is always false, as the rose of a signal cannot be repeated more than once, by definition of the rose; it has to be a ZERO in the previous cycle.
Wrote some code for the repeat.
see my papers links in my signature.
// the sig a should be high for 5 out of 6 sys_clk cycles.
// The 5 cycles can be of any pattern.
// this link offers an interesting approach to handle dynamic repeats
// and delays for sequences.
// http://systemverilog.us/vf/SolvingComplexUsersAssertions.pdf
package sva_delay_repeat_pkg;
sequence dynamic_repeat(q_s, count);
int v=count;
(1, v=count) ##0 first_match((q_s, v=v-1'b1) [*1:$] ##0 v<=0);
endsequence
sequence dynamic_delay(count);
int v;
(1, v=count) ##0 first_match((1, v=v-1'b1) [*0:$] ##1 v<=0);
endsequence
endpackage
import uvm_pkg::*; `include "uvm_macros.svh"
import sva_delay_repeat_pkg::*;
module top;
timeunit 1ns; timeprecision 100ps;
bit clk, a, b;
int rpt=5;
default clocking @(posedge clk); endclocking
initial forever #10 clk=!clk;
// a==1 for 5 consecutive cycles
ap_4out_of5: assert property(@ (posedge clk)
$rose(a) |-> a[*5] ##1 $fell(a) );
// a==1 for rpt consecutive cycles
ap_4out_of5_rpt: assert property(@ (posedge clk)
$rose(a) |-> dynamic_repeat(a, rpt) ##1 $fell(a) );
initial begin
bit va, vb;
repeat(200) begin
@(posedge clk);
if (!randomize(va, vb) with
{ va dist {1'b1:=5, 1'b0:=1};
vb dist {1'b1:=1, 1'b0:=2};
}) `uvm_error("MYERR", "This is a randomize error")
a <= va;
b <= vb;
end
$stop;
end
endmodule
I tried your sample testbench on edaplayground. Few changes I have to make inside sequence I was not able to assign value.
line 3 int v=count; Also I tried moving the sequence inside the module and it worked fine. There was no need for a package.
Below is the link for the same.
The requirement is ambiguous and yes there will be a fixed pattern but that pattern can change in future, so from your code, I wanted to know how are we making sure the 5 times a is high out of 6 clk cycles as see we are using [*1:$] which makes it check till the end.
If you want to know to make sure that a occurs 5 times in a framed zone, you can use code as shown below.
The complete test code is below. The issue with the package is that the edaplayground uses old simulators and does not handle UVM. If you comment out the uvm stuff, it should work ok.
ap_4out_of5_framed: assert property(@ (posedge clk)
$rose(b) |-> a && b [=5] intersect
first_match($rose(b) ##[1:$] $fell(b)));
// the sig a should be high for 5 out of 6 sys_clk cycles.
// The 5 cycles can be of any pattern.
package sva_delay_repeat_pkg;
sequence dynamic_repeat(q_s, count);
int v=count;
(1, v=count) ##0 first_match((q_s, v=v-1'b1) [*1:$] ##0 v<=0);
endsequence
sequence dynamic_delay(count);
int v;
(1, v=count) ##0 first_match((1, v=v-1'b1) [*0:$] ##1 v<=0);
endsequence
endpackage
import uvm_pkg::*; `include "uvm_macros.svh"
import sva_delay_repeat_pkg::*;
module top;
timeunit 1ns; timeprecision 100ps;
bit clk, a, b;
bit[2:0] rpt=5;
event e;
default clocking @(posedge clk); endclocking
initial forever #10 clk=!clk;
ap_a2b: assert property(@ (posedge clk)
$rose(a) |=> b[=2] intersect 1'b1 ##4 1'b1);
// a==1 for 5 consecutive cycles
ap_4out_of5: assert property(@ (posedge clk)
$rose(a) |-> a[*5] ##1 $fell(a) );
ap_4out_of5_framed: assert property(@ (posedge clk)
$rose(b) |-> a && b [=5] intersect
first_match($rose(b) ##[1:$] $fell(b)));
ap_4out_of5_framedfm: assert property(@ (posedge clk)
$rose(b) |-> a && b [=5] intersect
first_match($rose(b) ##[1:$] $fell(b)));
// a==1 for rpt consecutive cycles
ap_4out_of5_rpt: assert property(@ (posedge clk)
$rose(a) |-> dynamic_repeat(a, rpt) ##1 $fell(a) );
ap_4out_of5_framed_rpt: assert property(@ (posedge clk)
$rose(b) |-> (dynamic_repeat(a && b[->1], rpt-1'b1) ##1 a && b[=1])
intersect first_match($rose(b) ##[1:$] $fell(b)));
initial begin
bit va, vb;
repeat(200) begin
@(posedge clk);
if (!randomize(va, vb) with
{ va dist {1'b1:=5, 1'b0:=1};
vb dist {1'b1:=10, 1'b0:=1};
}) `uvm_error("MYERR", "This is a randomize error")
a <= va;
b <= vb;
end
$stop;
end
endmodule