data/full_repos/permissive/470816788/verilog/rtl/wrapped_hack_soc/hack_soc/spi_sram_encoder.v
data/verilator_xmls/f052f44f-c02f-4e89-8c3f-32e6627e0289.xml
module spi_sram_encoder #(
	parameter WORD_WIDTH = 16,
	parameter ADDRESS_WIDTH = 16
) (
	input wire clk,
	input wire reset, 	

	input wire request,
	output wire busy,
	output reg initialized,


	input wire [ADDRESS_WIDTH-1:0] address,
	input wire write_enable,
	output reg [WORD_WIDTH-1:0] data_in,
	input wire [WORD_WIDTH-1:0] data_out,



	output reg sram_cs_n,
	output sram_sck,

	output reg sram_sio_oe,

	input wire sram_sio0_i,
	input wire sram_sio1_i,
	input wire sram_sio2_i,
	input wire sram_sio3_i,

	output wire sram_sio0_o,
	output wire sram_sio1_o,
	output wire sram_sio2_o,
	output wire sram_sio3_o
);


`define INS_READ      8'b0000_0011
`define INS_WRMR      8'b0000_0001
`define INS_WRITE     8'b0000_0010
`define INS_RDMR      8'b0000_0101
`define INS_EDIO      8'b0011_1011
`define INS_EQIO      8'b0011_1000
`define INS_RSTIO     8'b1111_1111

`define BYTEMODE  2'b00
`define PAGEMODE  2'b10
`define SEQMODE   2'b01

`define SPIMODE   2'b00
`define SDIMODE   2'b01
`define SQIMODE   2'b10


function [31:0] max3(input [31:0] x, y, z);
    begin
        max3 = x > y ? (x > z ? x :z) : (y > z ? y : z);
    end
endfunction


localparam SRAM_ADDRESS_WIDTH = 24;
localparam SRAM_INSTRUCTION_WIDTH = 8;
localparam OUTPUT_BUFFER_WIDTH = max3(SRAM_ADDRESS_WIDTH, SRAM_INSTRUCTION_WIDTH ,WORD_WIDTH);
localparam INPUT_BUFFER_WIDTH = WORD_WIDTH;
localparam INPUT_DUMMY_WIDTH = 8;
localparam BITS_PER_CLK = 4;


localparam [2:0]
	state_idle 			= 3'b000,
	state_start			= 3'b001,
	state_instruction 	= 3'b010,
	state_address 		= 3'b011,
	state_read 			= 3'b100,
	state_write 		= 3'b101,	
	state_reset 		= 3'b110,
	state_set_SQI_mode 	= 3'b111
	;

reg [2:0] current_state;
reg [4:0] initializing_step;


reg [ADDRESS_WIDTH-1:0] request_address;
reg [WORD_WIDTH-1:0] request_data_out;
reg request_write;

reg [OUTPUT_BUFFER_WIDTH-1:0] output_buffer;
reg [$clog2(OUTPUT_BUFFER_WIDTH)-1:0] output_bits_left;

reg [INPUT_BUFFER_WIDTH-1:0] input_buffer;
reg [$clog2(INPUT_BUFFER_WIDTH + INPUT_DUMMY_WIDTH)-1:0] input_bits_left;


reg toggled_sram_sck;

assign sram_sck = ~sram_cs_n & toggled_sram_sck;







wire [3:0] sio_i = {sram_sio3_i, sram_sio2_i, sram_sio1_i, sram_sio0_i};
wire [3:0] sio_o = output_buffer[OUTPUT_BUFFER_WIDTH-1:OUTPUT_BUFFER_WIDTH-4];




assign {sram_sio3_o, sram_sio2_o, sram_sio1_o, sram_sio0_o} = sio_o;

assign busy = (current_state!=state_idle);





always @(posedge clk) begin
	
	

	if (reset) begin

		current_state <= state_reset;		

		initialized <= 1'b0;
		sram_cs_n <= 1'b1;				
		sram_sio_oe <= 1'b1;
		initializing_step <= 0;


		output_buffer[OUTPUT_BUFFER_WIDTH-1:OUTPUT_BUFFER_WIDTH-4] <= 4'b1111;
		
		input_buffer <= 0;
		data_in <= 0;

		toggled_sram_sck <= 0;
	end else begin
	
		toggled_sram_sck <= ~toggled_sram_sck;


		if(toggled_sram_sck==1'b1) begin

			case (current_state) 

				state_reset:
					begin
						if(sram_cs_n==1'b1) 
							sram_cs_n <= 1'b0;								
						
						initializing_step <= initializing_step + 1;


						case (initializing_step)
							0: output_buffer <= {`INS_RSTIO, {(OUTPUT_BUFFER_WIDTH-SRAM_INSTRUCTION_WIDTH){1'b0}}};
							1: output_buffer <= output_buffer << BITS_PER_CLK;
							default: 
								begin
									current_state <= state_set_SQI_mode;
									sram_cs_n <= 1'b1;
									initializing_step <= 0;
								end

						endcase

					end
				
				state_set_SQI_mode:
					begin

						if(sram_cs_n==1'b1)
							sram_cs_n <= 1'b0;		
						
						initializing_step <= initializing_step + 1;


						case (initializing_step)
							0: output_buffer[20] <= 0;
							1: output_buffer[20] <= 0;
							2: output_buffer[20] <= 1;
							3: output_buffer[20] <= 1;
							4: output_buffer[20] <= 1;
							5: output_buffer[20] <= 0;
							6: output_buffer[20] <= 0;
							7: output_buffer[20] <= 0;
							8: 	begin
									current_state <= state_idle;
									sram_cs_n <= 1'b1;	
									initialized <= 1'b1;								
								end

						endcase
					end

				state_idle:
					begin
						if(request && !busy) begin
							current_state <= state_start;


							request_address <= address;
							request_write <= write_enable;
							request_data_out <= data_out;

							

							sram_sio_oe <= 1'b1;
						end
					end
				
				state_start:					
					begin

						sram_cs_n <= 1'b0;		

						current_state <= state_instruction;


						if(request_write) begin
							output_buffer <= {`INS_WRITE, {(OUTPUT_BUFFER_WIDTH-SRAM_INSTRUCTION_WIDTH){1'b0}}};
							output_bits_left <= SRAM_INSTRUCTION_WIDTH;
						end else begin
							output_buffer <= {`INS_READ,  {(OUTPUT_BUFFER_WIDTH-SRAM_INSTRUCTION_WIDTH){1'b0}}};
							output_bits_left <= SRAM_INSTRUCTION_WIDTH;					
						end			
					end
				
				state_instruction:
					begin
						

						if(output_bits_left == BITS_PER_CLK) begin
							current_state <= state_address;			


							output_buffer <= { {(OUTPUT_BUFFER_WIDTH-ADDRESS_WIDTH-1){1'b0}}, request_address[ADDRESS_WIDTH-1:0] , 1'b0};
							output_bits_left <= SRAM_ADDRESS_WIDTH;
						end else begin

							output_buffer <= output_buffer << BITS_PER_CLK;
							output_bits_left <= output_bits_left - BITS_PER_CLK;							
						end					
					end
				
				state_address:
					begin
						

						if(output_bits_left == BITS_PER_CLK) begin
							if(request_write) begin
								current_state <= state_write;


								output_buffer <= {request_data_out, {(OUTPUT_BUFFER_WIDTH-WORD_WIDTH){1'b0}}};
								output_bits_left <= WORD_WIDTH;
							end else begin
								current_state <= state_read;
								

								sram_sio_oe <= 1'b0;
								input_bits_left <= INPUT_BUFFER_WIDTH + INPUT_DUMMY_WIDTH;
							end
							
						end else begin

							output_buffer <= output_buffer << BITS_PER_CLK;
							output_bits_left <= output_bits_left - BITS_PER_CLK;							
						end			
					end

				state_write:
					begin
						

						if(output_bits_left == BITS_PER_CLK) begin
							current_state <= state_idle;


							data_in <= request_data_out;


							sram_cs_n <= 1'b1;
							
						end else begin

							output_buffer <= output_buffer << BITS_PER_CLK;
							output_bits_left <= output_bits_left - BITS_PER_CLK;							

							
						end					
					end

				state_read:
					begin

						input_buffer <= {input_buffer[INPUT_BUFFER_WIDTH-BITS_PER_CLK-1:0] , sio_i};


						if(input_bits_left == BITS_PER_CLK) begin

							data_in <= {input_buffer[INPUT_BUFFER_WIDTH-BITS_PER_CLK-1:0] , sio_i};

							current_state <= state_idle;


							sram_cs_n <= 1'b1;

						end else begin
							input_bits_left <= input_bits_left - BITS_PER_CLK;
						end
					end


				
				

			endcase

		end
	
	end
	
end





`ifdef FORMAL

    reg f_past_valid = 0;

    initial assume(reset);
    initial assume(current_state==0);

    always @(posedge clk) begin 

		assume(address==16'hAED0);

    	f_past_valid <= 1;







		
 		
 		if(!reset && sram_cs_n==1'b0) begin
 			ASSERT_BUSY: assert(busy);
 		end
		
		if(current_state==state_read) begin
			ASSERT_OUTPUT_DISABLED_ON_READ: assert(sram_sio_oe==0);
		end

 		if(f_past_valid) begin
 			
 			COVER_READ: cover($past(current_state)==state_read && current_state==state_idle);
 			COVER_WRITE: cover($past(current_state)==state_write && current_state==state_idle);

 			COVER_INITIALIZED: cover(initialized);

 			if(current_state!=state_reset && current_state!=state_start && current_state!=state_set_SQI_mode) begin
 				ASSERT_INITILIZED: assert(initialized);
 			end

	 		if(sram_cs_n==1'b0 && toggled_sram_sck==1'b1) begin
	 			ASSERT_SRAM_INPUT_SET_BEFORE_CLOCK: 
	 				assert($past(sio_o)==sio_o); 			
	 		end

	 		if(!$past(reset) && current_state==state_idle) begin
				ASSERT_SRAM_OFF_ON_IDLE:
					assert(sram_cs_n==1'b1);

				if(!reset && $past(current_state)==state_write) begin
					ASSERT_OUTPUT_EQUAL_INPUT_ON_WRITE: assert(data_in==request_data_out);
				end
			end

			
	 	end
 		
    end
`endif    
	
endmodule
module spi_sram_encoder #(
	parameter WORD_WIDTH = 16,
	parameter ADDRESS_WIDTH = 16
) (
	input wire clk,
	input wire reset, 	

	input wire request,
	output wire busy,
	output reg initialized,


	input wire [ADDRESS_WIDTH-1:0] address,
	input wire write_enable,
	output reg [WORD_WIDTH-1:0] data_in,
	input wire [WORD_WIDTH-1:0] data_out,



	output reg sram_cs_n,
	output sram_sck,

	output reg sram_sio_oe,

	input wire sram_sio0_i,
	input wire sram_sio1_i,
	input wire sram_sio2_i,
	input wire sram_sio3_i,

	output wire sram_sio0_o,
	output wire sram_sio1_o,
	output wire sram_sio2_o,
	output wire sram_sio3_o
);



`define INS_READ      8'b0000_0011
`define INS_WRMR      8'b0000_0001
`define INS_WRITE     8'b0000_0010
`define INS_RDMR      8'b0000_0101
`define INS_EDIO      8'b0011_1011
`define INS_EQIO      8'b0011_1000
`define INS_RSTIO     8'b1111_1111

`define BYTEMODE  2'b00
`define PAGEMODE  2'b10
`define SEQMODE   2'b01

`define SPIMODE   2'b00
`define SDIMODE   2'b01
`define SQIMODE   2'b10


function [31:0] max3(input [31:0] x, y, z);
    begin
        max3 = x > y ? (x > z ? x :z) : (y > z ? y : z);
    end
endfunction


localparam SRAM_ADDRESS_WIDTH = 24;
localparam SRAM_INSTRUCTION_WIDTH = 8;
localparam OUTPUT_BUFFER_WIDTH = max3(SRAM_ADDRESS_WIDTH, SRAM_INSTRUCTION_WIDTH ,WORD_WIDTH);
localparam INPUT_BUFFER_WIDTH = WORD_WIDTH;
localparam INPUT_DUMMY_WIDTH = 8;
localparam BITS_PER_CLK = 4;


localparam [2:0]
	state_idle 			= 3'b000,
	state_start			= 3'b001,
	state_instruction 	= 3'b010,
	state_address 		= 3'b011,
	state_read 			= 3'b100,
	state_write 		= 3'b101,	
	state_reset 		= 3'b110,
	state_set_SQI_mode 	= 3'b111
	;

reg [2:0] current_state;
reg [4:0] initializing_step;


reg [ADDRESS_WIDTH-1:0] request_address;
reg [WORD_WIDTH-1:0] request_data_out;
reg request_write;

reg [OUTPUT_BUFFER_WIDTH-1:0] output_buffer;
reg [$clog2(OUTPUT_BUFFER_WIDTH)-1:0] output_bits_left;

reg [INPUT_BUFFER_WIDTH-1:0] input_buffer;
reg [$clog2(INPUT_BUFFER_WIDTH + INPUT_DUMMY_WIDTH)-1:0] input_bits_left;


reg toggled_sram_sck;

assign sram_sck = ~sram_cs_n & toggled_sram_sck;







wire [3:0] sio_i = {sram_sio3_i, sram_sio2_i, sram_sio1_i, sram_sio0_i};
wire [3:0] sio_o = output_buffer[OUTPUT_BUFFER_WIDTH-1:OUTPUT_BUFFER_WIDTH-4];




assign {sram_sio3_o, sram_sio2_o, sram_sio1_o, sram_sio0_o} = sio_o;

assign busy = (current_state!=state_idle);





always @(posedge clk) begin
	
	

	if (reset) begin

		current_state <= state_reset;		

		initialized <= 1'b0;
		sram_cs_n <= 1'b1;				
		sram_sio_oe <= 1'b1;
		initializing_step <= 0;


		output_buffer[OUTPUT_BUFFER_WIDTH-1:OUTPUT_BUFFER_WIDTH-4] <= 4'b1111;
		
		input_buffer <= 0;
		data_in <= 0;

		toggled_sram_sck <= 0;
	end else begin
	
		toggled_sram_sck <= ~toggled_sram_sck;


		if(toggled_sram_sck==1'b1) begin

			case (current_state) 

				state_reset:
					begin
						if(sram_cs_n==1'b1) 
							sram_cs_n <= 1'b0;								
						
						initializing_step <= initializing_step + 1;


						case (initializing_step)
							0: output_buffer <= {`INS_RSTIO, {(OUTPUT_BUFFER_WIDTH-SRAM_INSTRUCTION_WIDTH){1'b0}}};
							1: output_buffer <= output_buffer << BITS_PER_CLK;
							default: 
								begin
									current_state <= state_set_SQI_mode;
									sram_cs_n <= 1'b1;
									initializing_step <= 0;
								end

						endcase

					end
				
				state_set_SQI_mode:
					begin

						if(sram_cs_n==1'b1)
							sram_cs_n <= 1'b0;		
						
						initializing_step <= initializing_step + 1;


						case (initializing_step)
							0: output_buffer[20] <= 0;
							1: output_buffer[20] <= 0;
							2: output_buffer[20] <= 1;
							3: output_buffer[20] <= 1;
							4: output_buffer[20] <= 1;
							5: output_buffer[20] <= 0;
							6: output_buffer[20] <= 0;
							7: output_buffer[20] <= 0;
							8: 	begin
									current_state <= state_idle;
									sram_cs_n <= 1'b1;	
									initialized <= 1'b1;								
								end

						endcase
					end

				state_idle:
					begin
						if(request && !busy) begin
							current_state <= state_start;


							request_address <= address;
							request_write <= write_enable;
							request_data_out <= data_out;

							

							sram_sio_oe <= 1'b1;
						end
					end
				
				state_start:					
					begin

						sram_cs_n <= 1'b0;		

						current_state <= state_instruction;


						if(request_write) begin
							output_buffer <= {`INS_WRITE, {(OUTPUT_BUFFER_WIDTH-SRAM_INSTRUCTION_WIDTH){1'b0}}};
							output_bits_left <= SRAM_INSTRUCTION_WIDTH;
						end else begin
							output_buffer <= {`INS_READ,  {(OUTPUT_BUFFER_WIDTH-SRAM_INSTRUCTION_WIDTH){1'b0}}};
							output_bits_left <= SRAM_INSTRUCTION_WIDTH;					
						end			
					end
				
				state_instruction:
					begin
						

						if(output_bits_left == BITS_PER_CLK) begin
							current_state <= state_address;			


							output_buffer <= { {(OUTPUT_BUFFER_WIDTH-ADDRESS_WIDTH-1){1'b0}}, request_address[ADDRESS_WIDTH-1:0] , 1'b0};
							output_bits_left <= SRAM_ADDRESS_WIDTH;
						end else begin

							output_buffer <= output_buffer << BITS_PER_CLK;
							output_bits_left <= output_bits_left - BITS_PER_CLK;							
						end					
					end
				
				state_address:
					begin
						

						if(output_bits_left == BITS_PER_CLK) begin
							if(request_write) begin
								current_state <= state_write;


								output_buffer <= {request_data_out, {(OUTPUT_BUFFER_WIDTH-WORD_WIDTH){1'b0}}};
								output_bits_left <= WORD_WIDTH;
							end else begin
								current_state <= state_read;
								

								sram_sio_oe <= 1'b0;
								input_bits_left <= INPUT_BUFFER_WIDTH + INPUT_DUMMY_WIDTH;
							end
							
						end else begin

							output_buffer <= output_buffer << BITS_PER_CLK;
							output_bits_left <= output_bits_left - BITS_PER_CLK;							
						end			
					end

				state_write:
					begin
						

						if(output_bits_left == BITS_PER_CLK) begin
							current_state <= state_idle;


							data_in <= request_data_out;


							sram_cs_n <= 1'b1;
							
						end else begin

							output_buffer <= output_buffer << BITS_PER_CLK;
							output_bits_left <= output_bits_left - BITS_PER_CLK;							

							
						end					
					end

				state_read:
					begin

						input_buffer <= {input_buffer[INPUT_BUFFER_WIDTH-BITS_PER_CLK-1:0] , sio_i};


						if(input_bits_left == BITS_PER_CLK) begin

							data_in <= {input_buffer[INPUT_BUFFER_WIDTH-BITS_PER_CLK-1:0] , sio_i};

							current_state <= state_idle;


							sram_cs_n <= 1'b1;

						end else begin
							input_bits_left <= input_bits_left - BITS_PER_CLK;
						end
					end


				
				

			endcase

		end
	
	end
	
end





`ifdef FORMAL

    reg f_past_valid = 0;

    initial assume(reset);
    initial assume(current_state==0);

    always @(posedge clk) begin 

		assume(address==16'hAED0);

    	f_past_valid <= 1;







		
 		
 		if(!reset && sram_cs_n==1'b0) begin
 			ASSERT_BUSY: assert(busy);
 		end
		
		if(current_state==state_read) begin
			ASSERT_OUTPUT_DISABLED_ON_READ: assert(sram_sio_oe==0);
		end

 		if(f_past_valid) begin
 			
 			COVER_READ: cover($past(current_state)==state_read && current_state==state_idle);
 			COVER_WRITE: cover($past(current_state)==state_write && current_state==state_idle);

 			COVER_INITIALIZED: cover(initialized);

 			if(current_state!=state_reset && current_state!=state_start && current_state!=state_set_SQI_mode) begin
 				ASSERT_INITILIZED: assert(initialized);
 			end

	 		if(sram_cs_n==1'b0 && toggled_sram_sck==1'b1) begin
	 			ASSERT_SRAM_INPUT_SET_BEFORE_CLOCK: 
	 				assert($past(sio_o)==sio_o); 			
	 		end

	 		if(!$past(reset) && current_state==state_idle) begin
				ASSERT_SRAM_OFF_ON_IDLE:
					assert(sram_cs_n==1'b1);

				if(!reset && $past(current_state)==state_write) begin
					ASSERT_OUTPUT_EQUAL_INPUT_ON_WRITE: assert(data_in==request_data_out);
				end
			end

			
	 	end
 		
    end
`endif    
	
endmodule