#define TCG_HELPER_PROTO
void TCG_HELPER_PROTO helper_tlb_update(uint32_t T0);