read_verilog -sv << EOF
module top (input A, B, C, D, E, F, output reg W, X, Y, Z);
	always_comb begin
		W = F;
		priority if (C == A)
			W = D;
		else if (C == B)
			W = E;
	end

	always_comb begin
		X = F;
		if (C == A)
			X = D;
		else if (C == B)
			X = E;
	end

	always_comb begin
		Y = F;
		unique if (C == A)
			Y = D;
		else if (C == B)
			Y = E;
	end

	always_comb begin
		Z = F;
		unique0 if (C == A)
			Z = D;
		else if (C == B)
			Z = E;
	end
endmodule
EOF
prep
# For the ones which use priority/unique, the F signal shouldn't be included in
# the input cone of W and Y.
select -set full o:W o:Y %u %ci*
select -assert-none i:F @full %i
select -assert-count 1 o:X %ci* i:F %i
select -assert-count 1 o:Z %ci* i:F %i

# And for unique/unique0 there should be 1 $pmux compared to the 2 $mux
# cells without.
select -assert-none o:W %ci* t:$pmux %i
select -assert-none o:X %ci* t:$pmux %i
select -assert-count 1 o:Y %ci* t:$pmux %i
select -assert-count 1 o:Z %ci* t:$pmux %i

select -assert-count 2 o:W %ci* t:$mux %i
select -assert-count 2 o:X %ci* t:$mux %i
select -assert-none o:Y %ci* t:$mux %i
select -assert-none o:Z %ci* t:$mux %i
