
module fwrisc_mul_div_shift_formal_checker(
		input			clock,
		input			reset,
		input[31:0]		in_a,
		input[31:0]		in_b,
		input[3:0]		op,
		input			in_valid,
		input[31:0]		out,
		input			out_valid);
	
	always @(posedge clock) begin
		if (!reset && out_valid) begin
			assert(op >= 4'b0011 && op <= 4'b0011);
			if (op == 4'b0011) begin
				assert(out == ((in_a * in_b) & 32'hFFFFFFFF));
			end else if (op == 4'b0100) begin // mulh
				assert(out == (((in_a * in_b) >> 32) & 32'hFFFFFFFF));
			end else if (op == 4'b0101) begin // muls
				assert(out == (($signed(in_a) * $signed(in_b)) & 32'hFFFFFFFF));
			end else if (op == 4'b0110) begin // mulsh
				assert(out == ((($signed(in_a) * $signed(in_b)) >> 32) & 32'hFFFFFFFF));
			end
			cover(out_valid);
		end

		assume (s_eventually (!reset && out_valid));
	end
	
	
endmodule