module __float64__max_normal(
  input wire sign,
  output wire [63:0] out
);
  assign out = {sign, 11'h7fe, 52'hf_ffff_ffff_ffff};
endmodule