
`include "fwrisc_exec_formal_defines.svh"


module fwrisc_exec_formal_mem_test(
		input					clock,
		input					reset,
		output 					decode_valid,
		input	 				instr_complete,
		
		input[31:0]				pc,

		// Indicates whether the instruction is compressed
		output reg				instr_c,

		output reg[4:0]			op_type,
		
		output reg[31:0]		op_a,
		output reg[31:0]		op_b,
		output reg[5:0]			op,
		output reg[31:0]		op_c,
		output reg[5:0]			rd,
		output reg[31:0]		mtvec,

		input					dvalid,
		output reg[31:0]		drdata,
		output reg				dready
		);
	`include "fwrisc_op_type.svh"
	`include "fwrisc_mem_op.svh"
	
	reg[1:0]		dstate;
	wire[31:0]		drdata_w = `anyconst;
	
	always @(posedge clock) begin
		if (reset) begin
			dstate <= 0;
			dready <= 0;
		end else begin
			case (dstate)
				0: begin
					// Wait for a memory request
					if (dvalid) begin
						drdata <= drdata_w;
						dready <= 1;
						dstate <= 1;
					end
				end
				1: begin
					dstate <= 0;
					dready <= 0;
				end
			endcase
		end
	end

	reg[1:0]		state;
	reg				decode_valid_r;
	wire[31:0]		st_data = `anyconst;
	wire[31:0]		mem_base = `anyconst;
	wire[7:0]		mem_off = `anyconst;
	
	wire[5:0]		rd_w;
	assign rd_w[5] = 0;
	assign rd_w[4:0] = `anyconst;
	wire[3:0]		mem_op = `anyconst;
	
	assign decode_valid = (decode_valid_r && !instr_complete);
	
	always @(posedge clock) begin
		if (reset) begin
			state <= 0;
			instr_c <= 0;
			op_type <= OP_TYPE_LDST;
			op_a <= 0; 
			op_b <= 0; 
			op <= 0; 
			op_c <= 0; 
			rd <= 0;
			decode_valid_r <= 0;
			mtvec <= 0;
		end else begin
			case (state)
				0: begin
					// Send out a new instruction
					decode_valid_r <= 1;
					state <= 1;

`ifdef FORMAL
					op <= (mem_op % OP_NUM_MEM);
					op_b <= st_data;
`else
					op <= 0;
					op_b <= 0;
`endif
					
					// Specify where the load is going
					rd <= rd_w;
					
					// Select base address and offset
					case (mem_op % OP_NUM_MEM)
						OP_LB, OP_LBU, OP_SB: begin
							op_a <= mem_base;
							op_c <= $signed(mem_off);
						end
						OP_LH, OP_SH: begin
							// Keep aligned
							op_a <= {mem_base[31:1], 1'b0};
							op_c <= $signed({mem_off, 1'b0});
						end
						OP_LW, OP_SW: begin
							// Keep aligned
							op_a <= {mem_base[31:2], 2'b0};
							op_c <= $signed({mem_off, 2'b0});
						end
					endcase
				end
				1: begin
					if (instr_complete) begin
						/*
						`cover(op == OP_LB);
						`cover(op == OP_LH);
						`cover(op == OP_LW);
						`cover(op == OP_LBU);
						`cover(op == OP_LHU);
						`cover(op == OP_SB);
						`cover(op == OP_SH);
						`cover(op == OP_SW);
						 */
						decode_valid_r <= 0;
						state <= 0;
					end
				end
			endcase
			
`ifdef FORMAL
			assert(s_eventually instr_complete);
`endif
		end
	end
	
	
endmodule