veryl icon indicating copy to clipboard operation
veryl copied to clipboard

Add `unique`, `unique0`, and `priority` keywords

Open nblei opened this issue 5 months ago • 20 comments

Consider

module test (
	input [2:0] onehot,
	output logic [1:0] idx
);
always_comb begin
	case (onehot)
		3'b001: idx = 2'b01;
		3'b010: idx = 2'b10;
		3'b100: idx = 2'b11;
	endcase
end
endmodule : test

Synthesizing this with dc_shell results in inferred latches (ignore for a moment the fact that DC doesn't error out when latches are inferred in an always_comb block) because only three out of eight possible mux selects are handled in the switch statement. This can be fixed by adding a default case, or by adding a default assignment prior to the switch statement. However, this infers unnecessary logic when we are guaranteed the external controllability constraint that onehot is, in fact, one-hot.

However, adding the unique keyword solves this problem optimally:

	unique case (onehot)
		3'b001: idx = 2'b01;
		3'b010: idx = 2'b10;
		3'b100: idx = 2'b11;
	endcase

The unique case is a mechanism for the RTL designer to encode controllability constraints. It encodes the designer's guarantee to the synthesis tool / simulator / model checker that for each evaluation of the switch control signal, exactly one case in the switch statement will match. Similarly, unique can be used to qualify if-else if*-else statements.

Other SV2009 keywords unique0 and priority also modify the semantics of control statements.

nblei avatar Sep 04 '24 15:09 nblei