Hi Jon,

Sorry for the late response -- this email came in when the University was closing in on its end of year shutdown. Your steps look fairly good, but you will most likely also have to write mux, clock and other drivers for the TX1 -- or if the drivers are similar enough between the TK1 and TX1, you can probably reuse large portions of the existing TK1 drivers. I don't think you'll need SMMU support unless you plan to virtualize some hardware on your target system using passthrough. I'd need a better description of your target system to answer more authoritatively.

For `ps_io_ops_t` -- thankfully this is just a virtual memory mapping operation, so you shouldn't need to do anything since libsel4platsupport already provides the common backend implementation for it (see `__map_device_page`). You should be able to just call `sel4platsupport_new_io_ops()`.

Setting up a test environment for your drivers will be a bit of a challenge, but you can use seL4test to get you started (https://wiki.sel4.systems/Testing). What you would do is set up your own new, "fake" test app and call your driver routines from within that test app.

I'm not sure I can give you a good answer on a C project to look at because looking at C projects targeted at conventional monolithic and hybrid kernels may not be very helpful in understanding how to do the same thing on a microkernel.

-- 

Kofi Doku Atuah
Kernel engineer
DATA61 | CSIRO