atf_check_ustosbt
atf_check_ustosbt(0, 0);
atf_check_ustosbt(4295, 1);
atf_check_ustosbt((1ll << 32) - 4295, 999999);
atf_check_ustosbt(1ll << 32, 1000000);
atf_check_ustosbt((1ll << 33) - 4295, 1999999);
atf_check_ustosbt(1ll << 33, 2000000);
atf_check_ustosbt((1ll << 34) - 4295, 3999999);
atf_check_ustosbt(1ll << 34, 4000000);
atf_check_ustosbt(((1ull << 31) - 1) << 32,