module __float64__max_normal_exp(
  output wire [10:0] out
);
  assign out = 11'h3ff;
endmodule