test_vcuxwfp128_unsigned_edges:
  #_ REGISTER_IN v3 [00000000, 00000001, 7FFFFFFF, 80000000]
  vcuxwfp128 v4, v3, 0
  blr
  #_ REGISTER_OUT v3 [00000000, 00000001, 7FFFFFFF, 80000000]
  #_ REGISTER_OUT v4 [00000000, 3F800000, 4F000000, 4F000000]

test_vcuxwfp128_unsigned_max:
  #_ REGISTER_IN v3 [FFFFFFFF, FFFFFFFE, 00FFFFFF, 01000000]
  vcuxwfp128 v4, v3, 0
  blr
  #_ REGISTER_OUT v3 [FFFFFFFF, FFFFFFFE, 00FFFFFF, 01000000]
  #_ REGISTER_OUT v4 [4F800000, 4F800000, 4B7FFFFF, 4B800000]