# Test "casez to if/elif/else conversion" in backend

read_verilog <<EOT
module top(a, b, c, out);
	input wire a, b, c;
	output reg [3:0] out;
	always @(*) begin
		casez ({c, b, a})
			3'b??1: begin
				out = 0;
			end
			3'b?1?: begin
				out = 1;
			end
			3'b1??: begin
				out = 2;
			end
			default: begin
				out = 3;
			end
		endcase
	end
endmodule
EOT
write_verilog roundtrip_proc_1.v
design -stash gold
read_verilog roundtrip_proc_1.v
design -stash gate
design -copy-from gold -as gold top
design -copy-from gate -as gate top
prep
miter -equiv -flatten -make_assert gold gate miter
hierarchy -top miter
sat -prove-asserts -verify

design -reset
read_verilog <<EOT
module top(a, b, c, out);
	input wire a, b, c;
	output reg [3:0] out;
	always @(*) begin
		out <= 0;
		if (a) begin
			if (b)
				out <= 1;
		end else begin
			if (c)
				out <= 2;
			else
				out <= 3;
		end
	end
endmodule
EOT
proc_clean
write_verilog roundtrip_proc_2.v
design -stash gold
read_verilog roundtrip_proc_2.v
design -stash gate
design -copy-from gold -as gold top
design -copy-from gate -as gate top
prep
miter -equiv -flatten -make_assert gold gate miter
hierarchy -top miter
sat -prove-asserts -verify