test_vaddsws_saturates:
  #_ REGISTER_IN v3 [7FFFFFFF, 7FFFFFFE, 80000000, 80000001]
  #_ REGISTER_IN v4 [00000001, 00000001, FFFFFFFF, FFFFFFFF]
  vaddsws v3, v3, v4
  blr
  #_ REGISTER_OUT v3 [7FFFFFFF, 7FFFFFFF, 80000000, 80000000]
  #_ REGISTER_OUT v4 [00000001, 00000001, FFFFFFFF, FFFFFFFF]

test_vaddsws_mixed:
  #_ REGISTER_IN v3 [40000000, C0000000, 12345678, 87654321]
  #_ REGISTER_IN v4 [40000000, C0000000, EDCBA988, 789ABCDF]
  vaddsws v3, v3, v4
  blr
  #_ REGISTER_OUT v3 [7FFFFFFF, 80000000, 00000000, 00000000]
  #_ REGISTER_OUT v4 [40000000, C0000000, EDCBA988, 789ABCDF]