							modulesStateIn <= shiftRowsStateOut;
							shiftRowsEn <= 0;
							mixColumnsEn <= 1;
							encryptionCycleFSM <= 2'b11;
						end 
						finish <= 0;
				end 
				2'b11:
				begin 
					/* round AddroundKey */
						if (mixColumnsFinish == 1 || (shiftRowsFinish == 1 && keyNum >= 10))
						begin
						  if(keyNum < 10) modulesStateIn <= mixColumnsStateOut;
							else 	modulesStateIn <= shiftRowsStateOut;
							mixColumnsEn <= 0;
							shiftRowsEn <= 0;
							keyExpansionEn <= 1;
							roundKeyEn <= 1;
							encryptionCycleFSM <= 2'b01; // return to state 1 shift rows
							keyNum <= keyNum + 1;
						end 
						finish <= 0;
				end 
//				default: 
				endcase 		
				end 
				else 
				begin 
					/* keyNum > 10 */
					stateOutput <= roundKeyStateOut;
					finish <= 1;
					keyNum <= 0;
					encryptionCycleFSM <= 0;
					mixColumnsEn <= 0;
					keyExpansionEn <= 0;
					roundKeyEn <= 0;
					shiftRowsEn <= 0;
				end 
		end else 
		begin
			keyNum <= 0;
			encryptionCycleFSM <= 0;
			mixColumnsEn <= 0;
			keyExpansionEn <= 0;
			roundKeyEn <= 0;
			shiftRowsEn <= 0;
			finish <= 0;
		end
		

		end 


`ifdef FORMAL

    reg f_past_valid; // to know if the $past value is valid to process
    initial f_past_valid = 0;

    initial assume(reset);


    always @(posedge clk)
        f_past_valid = 1;

    // sync reset
    // the design starts at reset state so if no f_past_valid it should be on reset
    // if the past cycle had reset then it should be in reset state
    always @(posedge clk)
        if(!f_past_valid || $past(reset))
        begin
            assert(state_out_byte == 8'd0);
            assert(load == 1'b0);
            assert(ready == 1'b0);
        end


    // sync enable

    // enable signal should be up for the circuit to work  
    always @(posedge clk)
        assume(enable);
 
    // assume never reset 
//    always @(posedge clk)
//        assume(!reset);

    // check that not all modules enabled at the same time 
    always @(*)
        if(roundKeyEn)
        begin
            assert(!shiftRowsEn);
            assert(!mixColumnsEn);
        end
    
    always @(*)
        if(mixColumnsEn)
        begin
            assert(!roundKeyEn);
            assert(!shiftRowsEn);
        end
    
    always @(*)
        if(shiftRowsEn)
        begin
            assert(!roundKeyEn);
            assert(!mixColumnsEn);
        end
    
    // when finish check if the ready flag is raised for the out to receive the data
    always @(posedge clk)
        if(f_past_valid && $past(finish) == 1'b1 && !$past(reset))
            assert(ready);


/*
    // assume an intermediate state after getting the inputs
    (* anyconst *) wire [127:0] keyInt;
    (* anyconst *) wire [127:0] stateInt;

    reg stateAssumed;
    initial stateAssumed = 0;

    always @(posedge clk)
        if(f_past_valid)
        begin
            assume(key == keyInt);
            assume(state == stateInt);
        end
    always @(posedge clk)
        if(f_past_valid && !stateAssumed)
        begin
            //assume(load==1'b0);
            assume(loadFinish == 1'b1);
            assume(dataioFSM == 2'd2);
            stateAssumed <= 1'b1;
        end
*/
    // maximum generated keys 10
    always @(*)
        assert(keyNum <= 12);


    //key num should be increased by 1
    // each time single key expansion module is enabled (keyExpansionEn) the keyNum must be increased by one
    always @(posedge clk)
        if(f_past_valid && keyNum > 0 && $rose(keyExpansionEn) && !$past(reset))
            assert(keyNum == $past(keyNum)+1);
`endif


endmodule