test_vcuxwfp128_1:
  # Convert 0 to float
  #_ REGISTER_IN v0 [00000000, 00000000, 00000000, 00000000]
  vcuxwfp128 v3, v0, 0
  blr
  #_ REGISTER_OUT v0 [00000000, 00000000, 00000000, 00000000]
  #_ REGISTER_OUT v3 [00000000, 00000000, 00000000, 00000000]

test_vcuxwfp128_2:
  # Convert 1 to float (1.0)
  #_ REGISTER_IN v0 [00000001, 00000001, 00000001, 00000001]
  vcuxwfp128 v3, v0, 0
  blr
  #_ REGISTER_OUT v0 [00000001, 00000001, 00000001, 00000001]
  #_ REGISTER_OUT v3 [3F800000, 3F800000, 3F800000, 3F800000]

test_vcuxwfp128_3:
  # Convert 2 to float (2.0)
  #_ REGISTER_IN v0 [00000002, 00000002, 00000002, 00000002]
  vcuxwfp128 v3, v0, 0
  blr
  #_ REGISTER_OUT v0 [00000002, 00000002, 00000002, 00000002]
  #_ REGISTER_OUT v3 [40000000, 40000000, 40000000, 40000000]

test_vcuxwfp128_4:
  # Convert 100 to float (100.0)
  #_ REGISTER_IN v0 [00000064, 00000064, 00000064, 00000064]
  vcuxwfp128 v3, v0, 0
  blr
  #_ REGISTER_OUT v0 [00000064, 00000064, 00000064, 00000064]
  #_ REGISTER_OUT v3 [42C80000, 42C80000, 42C80000, 42C80000]

test_vcuxwfp128_5:
  # Convert 0x7FFFFFFF (as unsigned)
  #_ REGISTER_IN v0 [7FFFFFFF, 7FFFFFFF, 7FFFFFFF, 7FFFFFFF]
  vcuxwfp128 v3, v0, 0
  blr
  #_ REGISTER_OUT v0 [7FFFFFFF, 7FFFFFFF, 7FFFFFFF, 7FFFFFFF]
  #_ REGISTER_OUT v3 [4F000000, 4F000000, 4F000000, 4F000000]

test_vcuxwfp128_6:
  # Convert 0x80000000 (as unsigned = 2^31)
  #_ REGISTER_IN v0 [80000000, 80000000, 80000000, 80000000]
  vcuxwfp128 v3, v0, 0
  blr
  #_ REGISTER_OUT v0 [80000000, 80000000, 80000000, 80000000]
  #_ REGISTER_OUT v3 [4F000000, 4F000000, 4F000000, 4F000000]

test_vcuxwfp128_7:
  # Convert max unsigned (0xFFFFFFFF = 2^32-1)
  #_ REGISTER_IN v0 [FFFFFFFF, FFFFFFFF, FFFFFFFF, FFFFFFFF]
  vcuxwfp128 v3, v0, 0
  blr
  #_ REGISTER_OUT v0 [FFFFFFFF, FFFFFFFF, FFFFFFFF, FFFFFFFF]
  #_ REGISTER_OUT v3 [4F800000, 4F800000, 4F800000, 4F800000]

test_vcuxwfp128_8:
  # Convert mixed values
  #_ REGISTER_IN v0 [00000001, 00000002, 00000064, FFFFFFFF]
  vcuxwfp128 v3, v0, 0
  blr
  #_ REGISTER_OUT v0 [00000001, 00000002, 00000064, FFFFFFFF]
  #_ REGISTER_OUT v3 [3F800000, 40000000, 42C80000, 4F800000]