The following code is from a class that I taught. It is very similar to your requirements, thus you should be able to modify it as needed.
requirements:
// Loadable counter, reset to 0 if reset_n==0,
// Min count -2, Max count ==5
// This is an activity counter, thus count must change at least
// every 8 cycles (i.e., cannot stay forever at max value)
module counter_max #(MAX_COUNT=9, MIN_COUNT=2)( // parameter port list
input logic[3:0] data_in,
input logic ld,
output logic[3:0] counter,
input logic clk, rst_n) ;
int cover_count=0;
int fail_count=0;
// ap_P: assert property(@ (posedge clk) P )
// parameter MIN_COUNT=2; // module item parameter
// If use of parameter port list, then can't use defparam
default disable iff !rst_n;
property p_load;
logic[3:0] v_data_in; // local variable to property
(ld, v_data_in=data_in) |=> counter==v_data_in;
endproperty : p_load
ap_load: assert property ( @(posedge clk) p_load);
ap_count: assert property(@(posedge clk)
!ld && (counter!=MAX_COUNT) |=> counter==$past(counter)+1'b1);
ap_hold: assert property(@(posedge clk)
counter==MAX_COUNT |=> counter==$past(counter));
ap_min_load: assume property(@(posedge clk) disable iff (!rst_n)
ld |-> not(data_in<MIN_COUNT));
ap_max_load: assume property(@ (posedge clk) disable iff(!rst_n)
ld |-> not(data_in > MAX_COUNT))
cover_count++; else fail_count++ ;
ap_statble8: assume property(@(posedge clk)
$stable(counter)|-> ##[1:8] !$stable(counter));
always @(posedge clk) begin : counter1
if(!rst_n) counter <= 0;
else if (ld) counter <= data_in;
else begin : counter2
counter <= counter + 1'b1;
end : counter2
end : counter1
endmodule : counter_max
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
- SystemVerilog Assertions Handbook 3rd Edition, 2013 ISBN 878-0-9705394-3-6
- A Pragmatic Approach to VMM Adoption 2006 ISBN 0-9705394-9-5
- Using PSL/SUGAR for Formal and Dynamic Verification 2nd Edition, 2004, ISBN 0-9705394-6-0
- Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 0-9705394-2-8
- Component Design by Example ", 2001 ISBN 0-9705394-0-1
- VHDL Coding Styles and Methodologies, 2nd Edition, 1999 ISBN 0-7923-8474-1
- VHDL Answers to Frequently Asked Questions, 2nd Edition ISBN 0-7923-8115