126 	uint32_t first_high, first_low;  in vr41xx_read_rtclong1_counter()  local
131 		first_high = (uint32_t)read_rtc1(RTCL1CNTHREG);  in vr41xx_read_rtclong1_counter()
134 	} while (first_low != second_low || first_high != second_high);  in vr41xx_read_rtclong1_counter()
136 	return (first_high << 16) | first_low;  in vr41xx_read_rtclong1_counter()
147 	uint32_t first_high, first_low;  in vr41xx_read_rtclong2_counter()  local
152 		first_high = (uint32_t)read_rtc1(RTCL2CNTHREG);  in vr41xx_read_rtclong2_counter()
155 	} while (first_low != second_low || first_high != second_high);  in vr41xx_read_rtclong2_counter()
157 	return (first_high << 16) | first_low;  in vr41xx_read_rtclong2_counter()
168 	uint32_t first_high, first_low;  in vr41xx_read_tclock_counter()  local
173 		first_high = (uint32_t)read_rtc2(TCLKCNTHREG);  in vr41xx_read_tclock_counter()
176 	} while (first_low != second_low || first_high != second_high);  in vr41xx_read_tclock_counter()
178 	return (first_high << 16) | first_low;  in vr41xx_read_tclock_counter()