
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'b0000 && op <= 4'b0010);
			if (op == 4'b0000) begin
				assert(out == (in_a << in_b[4:0]));
			end else if (op == 4'b0001) begin // srl
				assert(out == (in_a >> in_b[4:0]));
			end else if (op == 4'b0010) begin // sra
				assert(out == (in_a >>> in_b[4:0]));
			end
			cover(out_valid);
		end

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