/* Get CNTPCT This function returns the value of the 64 bits PL1 Physical Count Register (CNTPCT). return CNTPCT Register value  */
static rt_uint64_t __get_cntpct(void)
/* Get CNTPCT This function returns the value of the 64 bits PL1 Physical Count Register (CNTPCT). return CNTPCT Register value  */
static rt_uint64_t __get_cntpct(void)
{
    rt_uint64_t result;
    __get_cp64(15, 0, result, 14);
    return result;
}