Hi Peter, Thanks. I am trying to port it to a RISCV running FPGA and show the output through UART ? Is it possible with just the upstreamed code or something I need to do ? regards, sathya On Mon, Jul 16, 2018 at 12:38 PM, wrote:

...

...

...

...

...

"Sathya" == Sathya Narayanan N writes:

Sathya> Query - I simulated sel4test on spike and then I am trying to Sathya> port it on FPGA. We have UART to be mapped to 0x11400 address Sathya> location. I set scan-> reg to this value.

The Spike platform has only a UART and a timer, both of which are stolen by the proxy-tk kernel. seL4 calls into the proxy kernel, which runs in machine mode, to use them.

Sathya> I understood, incase of simulation, the DTB argument passed to Sathya> init_first_hart function comes from spike simulator (file - Sathya> sim.cc). Now, for FPGA I want to pass the DTB value to the Sathya> init_first_hart() function. I am planning to write a DTS file Sathya> and somehow read the ​data from ​ DTS file here. ​ I am trying Sathya> to know, what is the right method to do for SEL4 ?​

seL4 doesn't use the DTB at all. And so far we haven't ported seL4 to a RSIC-V platform with any real devices.

-- Dr Peter Chubb Tel: +61 2 9490 5852 http://ts.data61.csiro.au/ Trustworthy Systems Group Data61, CSIRO (formerly NICTA)

-- regards, Sathya

Hi Sathya, On Mon, Jul 16, 2018 at 10:54 AM, wrote:

...

...

...

...

...

"Sathya" == Sathya Narayanan N writes:

Sathya> Hi Peter,

Sathya> Thanks. I am trying to port it to a RISCV running FPGA and Sathya> show the output through UART ? Is it possible with just the Sathya> upstreamed code or something I need to do ?

If there is a proxy-kernel that handles the UART on your FPGA then I'd expect the upstream code to work. But as I said, we haven't tried this yet. Dur Adding to Peter's reply, the current implementation of seL4 relies on riscv-pk for outputing characters. The current behaviour of the proxy kernel is that it uses the UART device if found, otherwise it uses HTIF. seL4 isn't affected by any of this.

So assuming that you have a proper UART device that riscv-pk can inspect (from DTB), riscv-pk will use it whenever seL4 wants to output characters. I've tried this on QEMU -freedomu and -virt platforms that use SiFive UART and UART16550 respectively, and on VC707 FPGA with SiFive's UART.

Peter C -- Dr Peter Chubb Tel: +61 2 9490 5852 http://ts.data61.csiro.au/ Trustworthy Systems Group Data61, CSIRO (formerly NICTA) _______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel

-- Hesham