Is there a reliable way to generate one-hot multiplexers?

[tilk]

If a signal is known to be one-hot (only a single bit is set), a multiplexer controlled by this signal has a simpler implementation if it's a one-hot multiplexer. A one-hot multiplexer is defined only for valid one-hot select signals, and undefined otherwise. One-hot signals tend to pop up in hardware in many places (basically each time we have a set of mutually exclusive conditions), so it can pay off to handle them well.

One-hot multiplexers can be specified like this in SystemVerilog (there are other ways but this is pretty obvious):

module m_one_hot_mux3 (
    input  logic       i_a,
    input  logic       i_b,
    input  logic       i_c,
    input  logic [2:0] i_sel,
    output logic       o_out
  );

  always_comb begin
    unique case (1'b1)
      i_sel[0]: o_out = i_a;
      i_sel[1]: o_out = i_b;
      i_sel[2]: o_out = i_c;
    endcase
  end
endmodule

Note the unique keyword - this tells to the synthesis tool that only one of the conditions will be true. When given this code, Yosys generates a $pmux cell, which preserves the designer's intention and is optimized accordingly.

Finally, to the question. Is it possible to reliably generate $pmux cells from Amaranth code (preferably, switch statements)? I found this small test in Amaranth repo, but this code synthesizes to priority logic in Amaranth 0.5. If it's not possible, is some support planned?

I'm aware that one-hot multiplexers, as an element relying on having undefined behavior on some cases, might be in opposition to the idea that every value in the circuit must be defined to ensure simulation and synthesis behaviors match. I would argue that the "undefinedness" here is rather weak, and a runtime check in the Amaranth simulator would be enough to detect problems and avoid mismatches.

[whitequark]

I'm aware that one-hot multiplexers, as an element relying on having undefined behavior on some cases, might be in opposition to the idea that every value in the circuit must be defined to ensure simulation and synthesis behaviors match. I would argue that the "undefinedness" here is rather weak, and a runtime check in the Amaranth simulator would be enough to detect problems and avoid mismatches.

This is the crux of the matter. As of right now, there is no undefined behavior in Amaranth at all (which is a useful property in some cases, and annoying in others). In other words, there is no equivalent of the unique case construct.

We could introduce it via the RFC process, like any other new language construct.

I found this small test in Amaranth repo, but this code synthesizes to priority logic in Amaranth 0.5.

(I don't think this test ever properly optimized to a $pmux cell; it is very old and I think at the time I did not properly understand the semantics of the $pmux cell.)