Wow, I seem to be working on the exact same problem on the exact same day as you! Also working on an HC-SR04. As far as I have figured out, I think the real-time clock won’t work, as it has a frequency of 32,768 Hz (or a period of ~30 microseconds), which is much too slow for getting a 10 microsecond pulse or for measuring the duration of the echo pulse.
These are other resources in this forum that may be of (minor) help:
I’m going to try metal_timer_get_cyclecount(hartid, &cyclecount) or metal_cpu_get_timer(cpu) and I’ll update if it works or not.