atf_check_nstosbt
atf_check_nstosbt(0, 0);
atf_check_nstosbt(4, 1);
atf_check_nstosbt((1ll << 32) - 4, 999999999);
atf_check_nstosbt(1ll << 32, 1000000000);
atf_check_nstosbt((1ll << 33) - 4, 1999999999);
atf_check_nstosbt(1ll << 33, 2000000000);
atf_check_nstosbt((1ll << 34) - 4, 3999999999);
atf_check_nstosbt((1ll << 34), 4000000000);
atf_check_nstosbt(((1ll << 31) - 1) << 32,