

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"
	
	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'b1100011: begin // beq, bne, blt, bge, bltu, bgeu
						assert(op_a == instr[19:15]);
						assert(op_b == instr[24:20]);
						assert(op_c == imm_b);
						assert(op >= OP_EQ && op <= OP_GEU);
						case (instr[14:12])
							3'b000: assert(op == OP_EQ);
							3'b001: assert(op == OP_NE);
							3'b100: assert(op == OP_LT);
							3'b101: assert(op == OP_GE);
							3'b110: assert(op == OP_LTU);
							3'b111: assert(op == OP_GEU);
							default: assert(0);
						endcase
						cover(op == OP_EQ);
						cover(op == OP_NE);
						cover(op == OP_LT);
						cover(op == OP_GE);
						cover(op == OP_LTU);
						cover(op == OP_GEU);
					end
						
					default: begin
						assert(0);
					end
				endcase
				// 
			end
		end
	end
	
endmodule