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 |-> ##1 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)
begin
	$display();
end
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