Porting sel4 on RISCV architecture
Hi Experts, This is Sathya from IIT Madras. We are working on porting SEL4 on RISCV architecture running on FPGA. We have ported linux on the FPGA. I have some doubts regarding OS porting. I am stuck at the end. Before my actual query, let me tell my platform. Hardware - 64 bit RISCV design running on FPGA. It doesn't support compressed instn and multiarch. Operating system - SEL4, repo synced from latest official repository. Tools - Latest synched from RISCV official repo. Query - I simulated sel4test on spike and then I am trying to port it on FPGA. We have UART to be mapped to 0x11400 address location. I set scan->reg to this value. I understood, incase of simulation, the DTB argument passed to init_first_hart function comes from spike simulator (file - sim.cc). Now, for FPGA I want to pass the DTB value to the init_first_hart() function. I am planning to write a DTS file and somehow read the data from DTS file here. I am trying to know, what is the right method to do for SEL4 ? Can you please let me understand, how you went ahead for SEL4 ? Is there any changes, I have to do in the repo code ? any readings would you suggest to proceed ahead ? -- regards, Sathya
"Sathya" == Sathya Narayanan N <sathya281@gmail.com> 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)
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, <Peter.Chubb@data61.csiro.au> wrote:
"Sathya" == Sathya Narayanan N <sathya281@gmail.com> 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
"Sathya" == Sathya Narayanan N <sathya281@gmail.com> 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. Peter C -- Dr Peter Chubb Tel: +61 2 9490 5852 http://ts.data61.csiro.au/ Trustworthy Systems Group Data61, CSIRO (formerly NICTA)
Hi Sathya, On Mon, Jul 16, 2018 at 10:54 AM, <Peter.Chubb@data61.csiro.au> wrote:
"Sathya" == Sathya Narayanan N <sathya281@gmail.com> 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
participants (3)
-
Hesham Almatary -
Peter.Chubb＠data61.csiro.au -
Sathya Narayanan N