

module fwrisc_decode_formal_checker(
		// TODO: fill in port list
		input				clock,
		input				reset,
		input[31:0]			instr,
		input				instr_c,
		
		input				decode_valid,
		input[31:0]			op_a, 		// operand a (immediate or register)
		input[31:0]			op_b, 		// operand b (immediate or register)
		input[31:0]			op_c,		// immediate operand
		input[3:0]			op,
		input[5:0]			rd_raddr, 	// Destination register address
		input[4:0]			op_type
		);
	`include "fwrisc_op_type.svh"
	`include "fwrisc_alu_op.svh"
	`include "fwrisc_mul_div_shift_op.svh"
	
	reg[5:0]			count = 0;
	
	wire[31:0]			u_imm = {instr[31:12], 12'b0};
	wire[31:0]			imm_11_0_s = $signed(instr[31:20]);
	wire[31:0]			imm_11_0_u = instr[31:20];
	wire[31:0]			imm_b = $signed({instr[31], instr[7], instr[30:25], instr[11:8], 1'b0});
	
	always @(posedge clock) begin
		if (reset == 0) begin
			count <= count + 1;
			cover(count == 15);
			cover(decode_valid);
			if (decode_valid) begin
				case (instr[6:0]) 
					7'b0010011: begin // ADDI, SLTI, SLTIU, XORI, ORI, ANDI
						assert(op_a == instr[19:15]);
						cover (op == OP_ADD);
						cover (op == OP_LT);
						cover (op == OP_LTU);
						cover (op == OP_XOR);
						cover (op == OP_OR);
						cover (op == OP_AND);
						case (instr[14:12])
							3'b000: assert(op == OP_ADD);
							3'b010: assert(op == OP_LT);
							3'b011: assert(op == OP_LTU);
							3'b100: assert(op == OP_XOR);
							3'b110: assert(op == OP_OR);
							3'b111: assert(op == OP_AND);
						endcase
						if (instr[14:12] == 3'b011) begin // SLTIU
							assert(op_b == imm_11_0_u);
						end else begin
							assert(op_b == imm_11_0_s);
							assert(op_type == OP_TYPE_ARITH);
						end
						assert(op_a == instr[19:15]); // op_a == regs[rs1]
						assert(rd_raddr == instr[11:7]);
						cover(rd_raddr != 0);
					end
						
					default: begin
						assert(0);
					end
				endcase
				// 
			end
		end
	end
	
endmodule