The next step in the preparations to get Inferno running on the MicroMod Teensy board is to blink the LED in response to a system timer interrupt. Dropping the usual handler function into the code and enabling the timer didn't result in a blinking LED.
The first dead end was reading the Cortex-M7 Devices Generic User Guide, where section 4.4.5 says that if the low power clock is stopped, SysTick stops. In the i.MX RT1060 Processor Reference Manual, section 14.2 contains a diagram that shows the Low Power Clock Gating (LPCG) unit controlling access to the system clocks. The question is: which clock is being used for SysTick? It should be the same clock keeping the ARM core running, I think, but the Teensy Arduino code claims to use the external oscillator as the source of SysTick.
Setting the SysTick reload value to 0xffffff and performing tests against high bits to switch the LED on or off showed that the timer is counting down. Adding a hard fault vector handler showed that the SysTick exception is potentially being escalated to a hard fault. Debugging using the LED to display the contents of registers caused the bootloader's diagnostic codes to appear again, complaining about a hard fault, it seems.
It turns out that the vector table needs to be aligned with a 128 byte boundary. Fixing that causes the SysTick exception to work. It seems strange that the hard fault handler worked fine despite the misalignment.
I noticed that I hadn't set the stack pointer at all. Setting the stack pointer would cause a hard fault. Using a blinking LED to read out the stack pointer, when not setting it in the start-up code, showed that it was set to some default value near the top of OCRAM. Setting it to a value in this memory region worked. Setting it to a value outside this region resulted in a hard fault. Bizarrely, using memory addresses in Data Tightly Coupled Memory (DTCM) to store the stack pointer value early in the boot process and retrieve it later didn't cause a problem.
Checking the Arduino code showed that there was some additional early boot configuration of the different regions of RAM. This uses IOMUX registers GPR16 and GPR17 to select RAM banks that map to the DTCM. I'm not sure I'll need to use the DTCM for anything specific in Inferno, but I suppose it's useful to know a bit about what's going on with memory. There's an application note from NXP, Using the i.MX RT FlexRAM, that goes into detail about how to configure RAM on these processors. One part that seems useful is where it says, in section 3.1.3.1 (Considering Cortex-M7 TCM size limitations), this:
If there is a request to have 0 kB of any TCM memory, disable the corresponding TCM before setting the size to 0 kB. If not, omit this step: Use the INT_xTCM_EN fields in the IOMUXC_GPR_GPR16 register to disable the corresponding xTCM memory before configuring it to 0 kB.
Unfortunately, the Processor Reference Manual's description of GPR16 doesn't show any fields for doing this. I suspect that bits 0 and 1 have an effect because the Arduino code explicitly sets them while enabling DTCM.
It's just one more mystery to put on the pile and maybe look at later.