module counter ( clk, rst, mode, cnt);
	
	input wire clk;
	input wire rst;
	input wire mode;
	output reg signed[10-1:0] cnt;
	
	reg signed[10-1:0] add_val;

	always @*
	begin
		add_val = 10'sd0;
		if (mode) begin
			if (cnt!=10'sd14) begin 
				if (cnt <=10'sd218) begin
					add_val <= 10'sd5;
				end 			
			end else if (cnt <= 10'sd213 ) begin
				add_val <= 10'sd10;
			end 
		end else  begin
			if (cnt!=10'sd28) begin
				if (cnt>=-10'sd233) begin
					add_val<=-10'sd9;
				end 			
			end else if (cnt >= -10'sd224) begin
				add_val <= -10'sd18;
			end 

		end 
	end
	
	always @(posedge clk) begin
		if (rst) 
			cnt <= -10'sd62;
		else begin
			cnt<= cnt + add_val;
		end
	end

    `ifdef FORMAL
        reg init = 1;
        always @(posedge clk) begin
            if (init)    assume(rst);
            else assume(!rst);
            init <= 0;
        end
    
        always @(posedge clk) begin
    
            if (rst) begin
                assert (cnt == -10'sd62);
            end
    
            if (!rst) begin
    
		assert (cnt <= 10'sd223);
		assert (cnt >= -10'sd242);
		assert (cnt != 10'sd19);



		if ($past(mode)) begin
			if (!$past(rst)) begin
				if ($past(cnt) == (10'sd19-10'sd5)) begin
					assert ((cnt - $past(cnt)) == (10'sd10));
				end else if ($past(cnt) <= 10'sd223 && $past(cnt) > (10'sd223-10'sd5)) begin
					assert ((cnt - $past(cnt)) == 0);
				end else begin
					assert ((cnt - $past(cnt)) == 10'sd5);
				end
			end
		end

		// Counting down
		if (!$past(mode)) begin
			if (!$past(rst)) begin
				if ($past(cnt) == (10'sd19+10'sd9)) begin
					assert (($past(cnt) - cnt) == (10'sd18));
				end else if ($past(cnt) >= -10'sd242 && $past(cnt) < (-10'sd242+10'sd9)) begin 
					assert (($past(cnt) - cnt) == 0);
				end else begin
					assert (($past(cnt) - cnt) == 10'sd9);
				end
			end
		end
    
            end
        end

    `endif 
endmodule

/*   Number of wires:                 14
   Number of wire bits:             59
   Number of public wires:           5
   Number of public wire bits:      23
   Number of ports:                  4
   Number of port bits:             13
   Number of memories:               0
   Number of memory bits:            0
   Number of processes:              0
   Number of cells:                 11
     $add                            1
     $adff                           1
     $ge                             2
     $le                             2
     $mux                            3
     $ne                             2*/