module __float64__zero(
  input wire sign,
  output wire [63:0] out
);
  assign out = {sign, 11'h000, 52'h0_0000_0000_0000};
endmodule