module test_unit_sva (
	input clk_i, rst_i, en_i,
	input [3:0] some_data_i,
	output [7:0] some_data_o
);
//counter is incremented at each posedge clock when en_i is asserted by the input value
//some_data_i

property incrementCnt;
	(en_i) |=> some_data_o == $past(some_data_i) + $past(some_data_o);
endproperty
//counter is reset at posedge rst
property rstCnt;
	@(posedge (clk_i)) $rose(rst_i) |=> (some_data_o == 0);
endproperty

check_rstCnt_label: assert property (rstCnt)
else $display ($time,,,"\t %m Failed reset init.!");

incrementCnt_labe: assert property (@(posedge (clk_i)) disable iff (rst_i) incrementCnt)
else $display ($time,,,"\t %m Failed counter increment");
endmodule