FPMaxNormal should be returned instead of FPInfinity vcvt[t|b] instructions (to half precision) when roundingMode is round-to-zero.

The inconsistency with real device has existed since time ago. ARMv8 has enabled double-precision to half-precision - vcvt[t|b].f16.f64 also exposes such bug.

According to Page.5020 (DDI0487A), in FPRound():
// Deal with overflow and generate result.
if N != 16 || fpcr.AHP == '0' then // Single, double or IEEE half precision
  if biased_exp >= 2^E - 1 then
    result = if overflow_to_inf then FPInfinity(sign) else FPMaxNormal(sign);
    FPProcessException(FPExc_Overflow, fpcr);
    error = 1.0; // Ensure that an Inexact exception occurs
  else
    result = sign : biased_expN-F-2:0 : int_mantF-1:0;

When round-to-zero, overflow_to_inf is FALSE, FPMaxNormal should be returned.