module __float32__max_normal(
  input wire sign,
  output wire [31:0] out
);
  assign out = {sign, 8'hfe, 23'h7f_ffff};
endmodule