data/full_repos/permissive/147974511/src/encryption_top.v
 line:164: before: "begin"
1: b"%Error: data/full_repos/permissive/147974511/src/encryption_top.v:32: Cannot find file containing module: 'addRoundKey'\n addRoundKey addRoundKeyInst(.key(modulesKeyIn),.state(modulesStateIn),.clk(clk),.reset(reset),.enable(roundKeyEn),.state_out(roundKeyStateOut),.done(roundKeyFinish));\n ^~~~~~~~~~~\n        ... Looked in:\n             data/full_repos/permissive/147974511/src,data/full_repos/permissive/147974511/addRoundKey\n             data/full_repos/permissive/147974511/src,data/full_repos/permissive/147974511/addRoundKey.v\n             data/full_repos/permissive/147974511/src,data/full_repos/permissive/147974511/addRoundKey.sv\n             addRoundKey\n             addRoundKey.v\n             addRoundKey.sv\n             obj_dir/addRoundKey\n             obj_dir/addRoundKey.v\n             obj_dir/addRoundKey.sv\n%Error: data/full_repos/permissive/147974511/src/encryption_top.v:37: Cannot find file containing module: 'subByte'\n   subByte subByteInst (.state(roundKeyStateOut[itr +:32]) , .state_out(subByteStateOut[itr +:32]));\n   ^~~~~~~\n%Error: data/full_repos/permissive/147974511/src/encryption_top.v:40: Cannot find file containing module: 'shiftRows'\n shiftRows shiftRowsInst (.enable(shiftRowsEn),.clk(clk),.reset(reset),.Data(subByteStateOut),.Shifted_Data(shiftRowsStateOut),.done(shiftRowsFinish) );\n ^~~~~~~~~\n%Error: data/full_repos/permissive/147974511/src/encryption_top.v:41: Cannot find file containing module: 'mixColumns'\n mixColumns mixColumnsInst (.state(modulesStateIn),.clk (clk),.enable(mixColumnsEn), .reset(reset),.state_out(mixColumnsStateOut),.done(mixColumnsFinish));\n ^~~~~~~~~~\n%Error: data/full_repos/permissive/147974511/src/encryption_top.v:43: Cannot find file containing module: 'singleKeyExpansion'\n singleKeyExpansion singleKeyExpansionInst ( .keyInput(modulesKeyIn),.clk (clk),.enable(keyExpansionEn),.reset (reset),.keyNum (keyNum),.keyOutput(keyExpansionOut));\n ^~~~~~~~~~~~~~~~~~\n%Error: Exiting due to 5 error(s)\n"
module AES_encryption
(
input [7:0] key_byte, state_byte,
input clk,reset,enable,
output reg [7:0] state_out_byte,
output reg load,ready
);

	integer i,j;
	reg [1:0] encryptionCycleFSM;
	reg [1:0] dataioFSM;
	reg [127:0] key, state;
	reg roundKeyEn,shiftRowsEn,mixColumnsEn,keyExpansionEn;
	wire roundKeyFinish,shiftRowsFinish,mixColumnsFinish;
	reg  finish;
	reg [127:0] modulesStateIn, stateOutput;
	reg [127:0] modulesKeyIn;
	wire [127:0] keyExpansionOut,roundKeyStateOut,subByteStateOut,shiftRowsStateOut,mixColumnsStateOut;
	reg [3:0] keyNum;
	reg loadFinish;

	addRoundKey addRoundKeyInst(.key(modulesKeyIn),.state(modulesStateIn),.clk(clk),.reset(reset),.enable(roundKeyEn),.state_out(roundKeyStateOut),.done(roundKeyFinish));

  genvar itr;
	generate
		for (itr = 0 ; itr <= 127; itr = itr+32)
			subByte subByteInst (.state(roundKeyStateOut[itr +:32]) , .state_out(subByteStateOut[itr +:32]));
	endgenerate
	
	shiftRows shiftRowsInst (.enable(shiftRowsEn),.clk(clk),.reset(reset),.Data(subByteStateOut),.Shifted_Data(shiftRowsStateOut),.done(shiftRowsFinish) );
	mixColumns mixColumnsInst (.state(modulesStateIn),.clk (clk),.enable(mixColumnsEn), .reset(reset),.state_out(mixColumnsStateOut),.done(mixColumnsFinish));

	singleKeyExpansion singleKeyExpansionInst ( .keyInput(modulesKeyIn),.clk (clk),.enable(keyExpansionEn),.reset (reset),.keyNum (keyNum),.keyOutput(keyExpansionOut));


    initial load <= 1'b0;
    initial ready <= 1'b0;
    initial state_out_byte <= 8'h00;







always @(posedge clk)
	begin 
		if (reset) 
		begin
			loadFinish <= 0;
			key<=128'd0;
			state<=128'd0;
			load<=1'd0;
			ready<=1'd0;
			i <= 128;
			state_out_byte <= 8'h00;
			j <= 128; 
			dataioFSM <= 0 ;
		end 
		else if (enable) 
		begin

		case(dataioFSM)
			0:
			begin 

				dataioFSM <= 1;
				i <= 128;
                loadFinish <= 0;
			end 
			1:
			begin 

				if (i>0) begin				
					load<=1'd1;
					loadFinish <= 0;
					key[i-1 -: 8]<=key_byte;
					state[i-1 -: 8]<=state_byte;
					i<=i-8;				
				end 
				else  
					begin 

					load<=1'd0;
					loadFinish <= 1;
					dataioFSM <= 2; 
					end
			end
			2: begin 

					if(finish)
					begin

						ready <= 1;
						dataioFSM <= 3;
						j <= 128;
						loadFinish <= 0;
					end else 
                        begin
                            ready <= 0;
                            dataioFSM <= 2; 
                        end
			end 
			3: begin

						if ( j > 0)
						begin
							ready <= 1; 
							state_out_byte <= stateOutput [j-1 -: 8]; 
							j <= j - 8;
						end 
						else begin 

								ready <= 0;
								dataioFSM <= 0;
						end 
                        loadFinish <= 0;
			end 
			
			endcase
		end else dataioFSM <= 0;
end 













    initial 
    begin 
		keyNum <= 0;
		encryptionCycleFSM <= 0;
		mixColumnsEn <= 0;
		keyExpansionEn <= 0;
		roundKeyEn <= 0;
		shiftRowsEn <= 0;
		stateOutput <= 0;
		finish <= 0;
	end
always @(posedge clk)
	begin 
	if (reset)
	begin 
		keyNum <= 0;
		encryptionCycleFSM <= 0;
		mixColumnsEn <= 0;
		keyExpansionEn <= 0;
		roundKeyEn <= 0;
		shiftRowsEn <= 0;
		stateOutput <= 0;
		finish <= 0;
	end
	else if( (enable == 1 ) && (loadFinish == 1))
	begin 
			if ( keyNum <= 11 )
			begin 


			case (encryptionCycleFSM)
				2'b00:
					begin 

							modulesKeyIn <= key;
							modulesStateIn <= state;
							keyNum <= 4'h1;
							roundKeyEn <= 1;
                            mixColumnsEn <= 0;
                            shiftRowsEn <= 0;
							keyExpansionEn <= 1;
							encryptionCycleFSM <= 2'b01;
							finish <= 0;
					end 
				2'b01:
					begin 

						if (roundKeyFinish == 1)
						begin
							modulesStateIn <= roundKeyStateOut;
							modulesKeyIn <= keyExpansionOut;
							keyExpansionEn <= 0;
							roundKeyEn <= 0;
							shiftRowsEn <= 1;
							if ( keyNum < 10)  encryptionCycleFSM <= 2'b10;
							else encryptionCycleFSM <= 2'b11;
						end 			
						finish <= 0;
					end 
				2'b10:
				begin

						if (shiftRowsFinish == 1)
						begin
							modulesStateIn <= shiftRowsStateOut;
							shiftRowsEn <= 0;
							mixColumnsEn <= 1;
							encryptionCycleFSM <= 2'b11;
						end 
						finish <= 0;
				end 
				2'b11:
				begin 

						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;
							keyNum <= keyNum + 1;
						end 
						finish <= 0;
				end 

				endcase 		
				end 
				else 
				begin 

					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;
    initial f_past_valid = 0;

    initial assume(reset);


    always @(posedge clk)
        f_past_valid = 1;




    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





    always @(posedge clk)
        assume(enable);
 





    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
    

    always @(posedge clk)
        if(f_past_valid && $past(finish) == 1'b1 && !$past(reset))
            assert(ready);




    always @(*)
        assert(keyNum <= 12);




    always @(posedge clk)
        if(f_past_valid && keyNum > 0 && $rose(keyExpansionEn) && !$past(reset))
            assert(keyNum == $past(keyNum)+1);
`endif


endmodule
module AES_encryption
(
input [7:0] key_byte, state_byte,
input clk,reset,enable,
output reg [7:0] state_out_byte,
output reg load,ready
);


	integer i,j;
	reg [1:0] encryptionCycleFSM;
	reg [1:0] dataioFSM;
	reg [127:0] key, state;
	reg roundKeyEn,shiftRowsEn,mixColumnsEn,keyExpansionEn;
	wire roundKeyFinish,shiftRowsFinish,mixColumnsFinish;
	reg  finish;
	reg [127:0] modulesStateIn, stateOutput;
	reg [127:0] modulesKeyIn;
	wire [127:0] keyExpansionOut,roundKeyStateOut,subByteStateOut,shiftRowsStateOut,mixColumnsStateOut;
	reg [3:0] keyNum;
	reg loadFinish;

	addRoundKey addRoundKeyInst(.key(modulesKeyIn),.state(modulesStateIn),.clk(clk),.reset(reset),.enable(roundKeyEn),.state_out(roundKeyStateOut),.done(roundKeyFinish));

  genvar itr;
	generate
		for (itr = 0 ; itr <= 127; itr = itr+32)
			subByte subByteInst (.state(roundKeyStateOut[itr +:32]) , .state_out(subByteStateOut[itr +:32]));
	endgenerate
	
	shiftRows shiftRowsInst (.enable(shiftRowsEn),.clk(clk),.reset(reset),.Data(subByteStateOut),.Shifted_Data(shiftRowsStateOut),.done(shiftRowsFinish) );
	mixColumns mixColumnsInst (.state(modulesStateIn),.clk (clk),.enable(mixColumnsEn), .reset(reset),.state_out(mixColumnsStateOut),.done(mixColumnsFinish));

	singleKeyExpansion singleKeyExpansionInst ( .keyInput(modulesKeyIn),.clk (clk),.enable(keyExpansionEn),.reset (reset),.keyNum (keyNum),.keyOutput(keyExpansionOut));


    initial load <= 1'b0;
    initial ready <= 1'b0;
    initial state_out_byte <= 8'h00;







always @(posedge clk)
	begin 
		if (reset) 
		begin
			loadFinish <= 0;
			key<=128'd0;
			state<=128'd0;
			load<=1'd0;
			ready<=1'd0;
			i <= 128;
			state_out_byte <= 8'h00;
			j <= 128; 
			dataioFSM <= 0 ;
		end 
		else if (enable) 
		begin

		case(dataioFSM)
			0:
			begin 

				dataioFSM <= 1;
				i <= 128;
                loadFinish <= 0;
			end 
			1:
			begin 

				if (i>0) begin				
					load<=1'd1;
					loadFinish <= 0;
					key[i-1 -: 8]<=key_byte;
					state[i-1 -: 8]<=state_byte;
					i<=i-8;				
				end 
				else  
					begin 

					load<=1'd0;
					loadFinish <= 1;
					dataioFSM <= 2; 
					end
			end
			2: begin 

					if(finish)
					begin

						ready <= 1;
						dataioFSM <= 3;
						j <= 128;
						loadFinish <= 0;
					end else 
                        begin
                            ready <= 0;
                            dataioFSM <= 2; 
                        end
			end 
			3: begin

						if ( j > 0)
						begin
							ready <= 1; 
							state_out_byte <= stateOutput [j-1 -: 8]; 
							j <= j - 8;
						end 
						else begin 

								ready <= 0;
								dataioFSM <= 0;
						end 
                        loadFinish <= 0;
			end 
			
			endcase
		end else dataioFSM <= 0;
end 













    initial 
    begin 
		keyNum <= 0;
		encryptionCycleFSM <= 0;
		mixColumnsEn <= 0;
		keyExpansionEn <= 0;
		roundKeyEn <= 0;
		shiftRowsEn <= 0;
		stateOutput <= 0;
		finish <= 0;
	end
always @(posedge clk)
	begin 
	if (reset)
	begin 
		keyNum <= 0;
		encryptionCycleFSM <= 0;
		mixColumnsEn <= 0;
		keyExpansionEn <= 0;
		roundKeyEn <= 0;
		shiftRowsEn <= 0;
		stateOutput <= 0;
		finish <= 0;
	end
	else if( (enable == 1 ) && (loadFinish == 1))
	begin 
			if ( keyNum <= 11 )
			begin 


			case (encryptionCycleFSM)
				2'b00:
					begin 

							modulesKeyIn <= key;
							modulesStateIn <= state;
							keyNum <= 4'h1;
							roundKeyEn <= 1;
                            mixColumnsEn <= 0;
                            shiftRowsEn <= 0;
							keyExpansionEn <= 1;
							encryptionCycleFSM <= 2'b01;
							finish <= 0;
					end 
				2'b01:
					begin 

						if (roundKeyFinish == 1)
						begin
							modulesStateIn <= roundKeyStateOut;
							modulesKeyIn <= keyExpansionOut;
							keyExpansionEn <= 0;
							roundKeyEn <= 0;
							shiftRowsEn <= 1;
							if ( keyNum < 10)  encryptionCycleFSM <= 2'b10;
							else encryptionCycleFSM <= 2'b11;
						end 			
						finish <= 0;
					end 
				2'b10:
				begin

						if (shiftRowsFinish == 1)
						begin
							modulesStateIn <= shiftRowsStateOut;
							shiftRowsEn <= 0;
							mixColumnsEn <= 1;
							encryptionCycleFSM <= 2'b11;
						end 
						finish <= 0;
				end 
				2'b11:
				begin 

						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;
							keyNum <= keyNum + 1;
						end 
						finish <= 0;
				end 

				endcase 		
				end 
				else 
				begin 

					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;
    initial f_past_valid = 0;

    initial assume(reset);


    always @(posedge clk)
        f_past_valid = 1;




    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





    always @(posedge clk)
        assume(enable);
 





    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
    

    always @(posedge clk)
        if(f_past_valid && $past(finish) == 1'b1 && !$past(reset))
            assert(ready);




    always @(*)
        assert(keyNum <= 12);




    always @(posedge clk)
        if(f_past_valid && keyNum > 0 && $rose(keyExpansionEn) && !$past(reset))
            assert(keyNum == $past(keyNum)+1);
`endif


endmodule