16 Jul
2018
16 Jul
'18
3:17 p.m.
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
16 Jul
16 Jul
5:08 p.m.
>>>> "Sathya" == Sathya Narayanan
N <sathya281(a)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)
7:38 p.m.
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(a)data61.csiro.au> wrote:
--
regards,
Sathya
>>>> "Sathya" == Sathya Narayanan N <sathya281(a)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)
7:54 p.m.
>>>> "Sathya" == Sathya Narayanan
N <sathya281(a)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)
8:19 p.m.
Hi Sathya,
On Mon, Jul 16, 2018 at 10:54 AM, <Peter.Chubb(a)data61.csiro.au> wrote:
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.
>>>> "Sathya" == Sathya Narayanan N <sathya281(a)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 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(a)sel4.systems
https://sel4.systems/lists/listinfo/devel
--
Hesham
1448
days inactive
1448
days old
4 comments
3 participants
participants (3)
-
Hesham Almatary -
Peter.Chubb＠data61.csiro.au -
Sathya Narayanan N