atf_check_sbttoms
atf_check_sbttoms(0, 0);
atf_check_sbttoms(0, 1);
atf_check_sbttoms(1, (1ll << 32) / 1000);
atf_check_sbttoms(999, (1ll << 32) - 1);
atf_check_sbttoms(1000, 1ll << 32);
atf_check_sbttoms(1999, (1ll << 33) - 1);
atf_check_sbttoms(2000, 1ll << 33);
atf_check_sbttoms(3999, (1ll << 34) - 1);
atf_check_sbttoms(4000, 1ll << 34);
atf_check_sbttoms(1ll << 31, (1ull << 63) / 1000);
atf_check_sbttoms(1ll << 31, (1ull << 63) / 1000 + 1);
atf_check_sbttoms((1ll << 31) * 1000, (1ull << 63) - 1);