util_libs
util_libs copied to clipboard
seL4
Add Support for Banana Pi BPI-F3
related to https://github.com/seL4/seL4/pull/1535
This driver is based on the implementations in PR #167 and PR #190, with necessary updates, such as address and configuration changes applied according to the current DTS for this platform added here https://github.com/seL4/seL4/blob/772179e4e639fec1c48a01c69ea6cea144cab02a/tools/dts/bananapi-f3.dts
TIMER tests are not passing with these changes and I would like some help with that .. (as its my first time writing timer driver)
So, without TIMER when I run sel4test I can see these prints ..
Test suite passed. 116 tests passed. 49 tests disabled.
All is well in the universe
But when run TIMER tests, it gets stuck waiting for interrupt I believe ...
../init-build.sh -DPLATFORM=bananapi-f3 -DRELEASE=FALSE -DSIMULATION=0 -DRISCV64=1 -DLibSel4TestPrinterRegex=TIMER && ninja
... (skiping the build/and transfer of image cmds etc part)
...
...
Switching to a safer, bigger stack...
seL4 Test
=========
[email protected]:738 vspace is NULL
[email protected]:245 Failed to make reservation: 0x10000, 815104
[email protected]:438 Failed to create reservations
[email protected]:465 Failed to reserve regions
Starting test suite sel4test
Starting test 0: Test that there are tests
[DEBUG] Total Tests: 2
[DEBUG] Start Test #: 0, TIMER0001
Starting test 1: TIMER0001
[DEBUG] Waiting for timer interrupt... <- This is here : [sel4test-driver/src/timer.c#L69](https://github.com/seL4/sel4test/blob/827af3847588e47e81866969f80874655892b1d1/apps/sel4test-driver/src/timer.c#L69)
Some more details:
In the DTS I see the timer node as :
timer@d4014000 {
spacemit,timer-frequency = <0xc35000>;
resets = <0x1d 0x1c>;
clocks = <0x03 0x62>;
compatible = "spacemit,soc-timer";
status = "ok";
spacemit,timer-apb-frequency = <0x3197500>;
spacemit,timer-id = <0x00>;
spacemit,timer-fastclk-frequency = <0xc35000>;
reg = <0x00 0xd4014000 0x00 0xc8>;
counter0 {
spacemit,timer-broadcast;
interrupts = <0x17>;
interrupt-parent = <0x1e>;
compatible = "spacemit,timer-match";
status = "ok";
spacemit,timer-counter-id = <0x00>;
};
};
and accordingly, I've set the addresses over in platsupport/mach/timer.h#L12
/* These values correspond to the DTS node 'soc/timer@0xd4014000' */
#define SPACEMIT_TIMER_BASE 0xd4014000
#define SPACEMIT_TIMER_SIZE 0xc8
#define SPACEMIT_TIMER_IRQ 0x17
/* This is 12.8MHz */
#define SPACEMIT_TIMER_TICKS_PER_SECOND 0xc35000
Can someone please help me debug this? I can create issue on sel4test for better track if you want.
I can have a look if you can provide a datasheet that describes the timer hardware.
It's not an sel4test issue, but an problem with your driver, so it should stay here till proven otherwise.
I can have a look if you can provide a datasheet that describes the timer hardware.
It's not an sel4test issue, but an problem with your driver, so it should stay here till proven otherwise.
There is not such good details but I'been using these:
https://docs.banana-pi.org/en/BPI-F3/SpacemiT_K1_datasheet https://developer.spacemit.com/documentation?token=Alhewa0fai7lvbk9sajcumNqn4f
btw I also reviewed the linux kernel patches and I still see incomplete dts for this hardware (I compared the once in their latest bianbu OS vs what in linux kernel / riscv linux tree has), What I believe is they are still working on finalizing this and that is why we don't see any details so far, specially about peripherals.
So, I was thinking can we probably go with https://github.com/seL4/seL4/pull/1535 as it is? as I can confirm all tests passes except timer (I can try skip the tests for this board until timer is fixed?)
I would add debug
printf()severywhere to check that your code is being executed as expected, both init as well as IRQ handling.
I've kind of localized the issue already, It looks like the addressing I used (as mentioned in the DTS) not correct for TIMER either or the TIMER is not being initialized at all, because every time I read the timer using get_time() I see nothing but same value, it should however keep incrementing. Further checking I found the timer registers always read as 0s, which means they were not written/updated at all.
I've kind of localized the issue already, It looks like the addressing I used (as mentioned in the DTS) not correct for TIMER either or the TIMER is not being initialized at all, because every time I read the timer using
get_time()I see nothing but same value, it should however keep incrementing. Further checking I found the timer registers always read as 0s, which means they were not written/updated at all.
But were your driver functions called at all?
Is there a functioning Linux timer driver that works? Is it doing anything you aren't, like enabling or configuring the clock source? Bianbu OS is based on Linux, so the source code should be available.
There's a lot of information on those pages, but it's near impossible to find what you're looking for. Not proper datasheets anyway. Where did you got the register definitions from?
I would prefer that there is a working timer before merging this.
Is there a functioning Linux timer driver that works? Is it doing anything you aren't, like enabling or configuring the clock source? Bianbu OS is based on Linux, so the source code should be available. There's a lot of information on those pages, but it's near impossible to find what you're looking for. Not proper datasheets anyway. Where did you got the register definitions from?
not sure but I could not find any for now.
Also I used v3.0.1 as base, this is latest bianbu works on BPI-F3 and first extracted the dts from by
sudo dtc -I fs -O dts -o extracted.dts /proc/device-tree
and based on this I got the addresses, registers size etc details but structurally I followed the hifive-p550 style while writing.
But were your driver functions called at all?
Yes, I believe, btw let me drop the logs from u-boot when I load the sel4 image .. I've added multiple prints to find the issue...
View code
Starting kernel ...
ELF-loader started on (HART 0) (NODES 1)
paddr=[a64000..d71fff]
Looking for DTB in CPIO archive...found at a89160.
Loaded DTB from a89160.
paddr=[a8000..bdfff]
ELF-loading image 'kernel' to 80000
paddr=[80000..a7fff]
vaddr=[ffffffff80080000..ffffffff800a7fff]
virt_entry=ffffffff80080000
ELF-loading image 'rootserver' to be000
paddr=[be000..4c3fff]
vaddr=[10000..415fff]
virt_entry=1c136
Enabling MMU and paging
Jumping to kernel-image entry point...
Init local IRQ
Bootstrapping kernel
Initializing PLIC...
available phys memory regions: 4
[80000..100000)
[600000..2ff40000)
[30000000..7f000000)
[100000000..480000000)
reserved virt address space regions: 3
[ffffffc000080000..ffffffc0000a8000)
[ffffffc0000a8000..ffffffc0000bdbed)
[ffffffc0000be000..ffffffc0004c4000)
Booting all finished, dropped to user space
[ltimer] >>> init start
[ltimer] IRQ trigger.number=23, PLIC source=23
[ltimer] ps_irq_register ret=0 (IRQ line=23)
[ltimer] mapping pmem: paddr=0xd4014000 size=0xc8
[ltimer] vaddr=0x10064000
[ltimer] first regs: [0]=0x00000000 [1]=0x00000000 [2]=0x00000000
[ltimer] all timers disabled
[ltimer] COUNTER_TIMER enabled
[ltimer] TIMEOUT_TIMER init done
[ltimer] <<< init complete
BindNotification ret=0 cap=0x4df
TIMER ntfn raw cap=0x4df, badged[0]=0x4ce (badge set)
Node 0 of 1
IOPT levels: 0
IPC buffer: 0x416000
Empty slots: [1143 --> 8192)
sharedFrames: [0 --> 0)
userImageFrames: [42 --> 1072)
userImagePaging: [16 --> 20)
untypeds: [1072 --> 1143)
Initial thread domain: 0
Initial thread cnode size: 13
List of untypeds
------------------
Paddr | Size | Device
0 | 19 | 1
0x4c4000 | 14 | 1
0x4c8000 | 15 | 1
0x4d0000 | 16 | 1
0x4e0000 | 17 | 1
0x500000 | 20 | 1
0x2ff40000 | 18 | 1
0x2ff80000 | 19 | 1
0x7f000000 | 24 | 1
0x80000000 | 30 | 1
0xc0000000 | 29 | 1
0xe4200000 | 21 | 1
0xe4400000 | 22 | 1
0xe4800000 | 23 | 1
0xe5000000 | 24 | 1
0xe6000000 | 25 | 1
0xe8000000 | 27 | 1
0xf0000000 | 28 | 1
0x480000000 | 31 | 1
0x500000000 | 32 | 1
0x600000000 | 33 | 1
0x800000000 | 35 | 1
0x1000000000 | 36 | 1
0x2000000000 | 37 | 1
0x4000000000 | 38 | 1
0x80000 | 13 | 0
0x82000 | 12 | 0
0xbdbf0 | 4 | 0
0xbdc00 | 10 | 0
0x600000 | 21 | 0
0x800000 | 23 | 0
0x1000000 | 24 | 0
0x2000000 | 25 | 0
0x4000000 | 26 | 0
0x8000000 | 27 | 0
0x10000000 | 28 | 0
0x20000000 | 27 | 0
0x28000000 | 26 | 0
0x2c000000 | 25 | 0
0x2e000000 | 24 | 0
0x2f000000 | 23 | 0
0x2f800000 | 22 | 0
0x2fc00000 | 21 | 0
0x2fe00000 | 20 | 0
0x2ff00000 | 18 | 0
0x30000000 | 28 | 0
0x40000000 | 29 | 0
0x60000000 | 28 | 0
0x70000000 | 27 | 0
0x78000000 | 26 | 0
0x7c000000 | 25 | 0
0x7e000000 | 24 | 0
0x100000000 | 32 | 0
0x200000000 | 33 | 0
0x400000000 | 30 | 0
0x440000000 | 29 | 0
0x460000000 | 28 | 0
0x470000000 | 27 | 0
0x478000000 | 26 | 0
0x47c000000 | 25 | 0
0x47e000000 | 24 | 0
0x47f000000 | 23 | 0
0x47f800000 | 22 | 0
0x47fc00000 | 21 | 0
0x47fe00000 | 20 | 0
0x47ff00000 | 19 | 0
0x47ffe8800 | 11 | 0
0x47ffe9000 | 12 | 0
0x47ffea000 | 13 | 0
0x47ffec000 | 14 | 0
0x47fff0000 | 16 | 0
Untyped summary
1 untypeds of size 4
1 untypeds of size 10
1 untypeds of size 11
2 untypeds of size 12
2 untypeds of size 13
2 untypeds of size 14
1 untypeds of size 15
2 untypeds of size 16
1 untypeds of size 17
2 untypeds of size 18
3 untypeds of size 19
3 untypeds of size 20
4 untypeds of size 21
3 untypeds of size 22
4 untypeds of size 23
6 untypeds of size 24
5 untypeds of size 25
4 untypeds of size 26
5 untypeds of size 27
5 untypeds of size 28
3 untypeds of size 29
2 untypeds of size 30
1 untypeds of size 31
2 untypeds of size 32
2 untypeds of size 33
1 untypeds of size 35
1 untypeds of size 36
1 untypeds of size 37
1 untypeds of size 38
Switching to a safer, bigger stack...
seL4 Test
=========
[email protected]:738 vspace is NULL
[email protected]:245 Failed to make reservation: 0x10000, 815104
[email protected]:438 Failed to create reservations
[email protected]:465 Failed to reserve regions
Starting test suite sel4test
Starting test 0: Test that there are tests
[DEBUG] Total Tests: 2
[DEBUG] Start Test #: 0, TIMER0001
Starting test 1: TIMER0001
[spacemit_timer_get_time] ---- START ----
[spacemit_timer_get_time] regs=0x10064000
[spacemit_timer_get_time] raw value=0x00000000 value_l=0x00000000ffffffff value_h=0x0000000000000000
[spacemit_timer_get_time] int_status=0xffffffff
[spacemit_timer_get_time] incrementing value_h (unhandled interrupt)
[spacemit_timer_get_time] combined ticks=0x00000001ffffffff (8589934591)
[spacemit_timer_get_time] ticks_per_sec=12800000
[spacemit_timer_get_time] -> seconds=671 subseconds_ns=88639921
[spacemit_timer_get_time] -> total_ns=671088639921
[spacemit_timer_get_time] ---- END ----
[ltimer] get_time: 671088639921 ns
[spacemit_timer_get_time] ---- START ----
[spacemit_timer_get_time] regs=0x10064000
[spacemit_timer_get_time] raw value=0x00000000 value_l=0x00000000ffffffff value_h=0x0000000000000000
[spacemit_timer_get_time] int_status=0xffffffff
[spacemit_timer_get_time] incrementing value_h (unhandled interrupt)
[spacemit_timer_get_time] combined ticks=0x00000001ffffffff (8589934591)
[spacemit_timer_get_time] ticks_per_sec=12800000
[spacemit_timer_get_time] -> seconds=671 subseconds_ns=88639921
[spacemit_timer_get_time] -> total_ns=671088639921
[spacemit_timer_get_time] ---- END ----
[DEBUG] Waiting for timer interrupt...
[DEBUG] Here 0 ...
[spacemit_timer_get_time] ---- START ----
[spacemit_timer_get_time] regs=0x10064000
[spacemit_timer_get_time] raw value=0x00000000 value_l=0x00000000ffffffff value_h=0x0000000000000000
[spacemit_timer_get_time] int_status=0xffffffff
[spacemit_timer_get_time] incrementing value_h (unhandled interrupt)
[spacemit_timer_get_time] combined ticks=0x00000001ffffffff (8589934591)
[spacemit_timer_get_time] ticks_per_sec=12800000
[spacemit_timer_get_time] -> seconds=671 subseconds_ns=88639921
[spacemit_timer_get_time] -> total_ns=671088639921
[spacemit_timer_get_time] ---- END ----
[ltimer] get_time: 671088639921 ns
[spacemit_timer_get_time] ---- START ----
[spacemit_timer_get_time] regs=0x10064000
[spacemit_timer_get_time] raw value=0x00000000 value_l=0x00000000ffffffff value_h=0x0000000000000000
[spacemit_timer_get_time] int_status=0xffffffff
[spacemit_timer_get_time] incrementing value_h (unhandled interrupt)
[spacemit_timer_get_time] combined ticks=0x00000001ffffffff (8589934591)
[spacemit_timer_get_time] ticks_per_sec=12800000
[spacemit_timer_get_time] -> seconds=671 subseconds_ns=88639921
[spacemit_timer_get_time] -> total_ns=671088639921
[spacemit_timer_get_time] ---- END ----
[ltimer] get_time: 671088639921 ns
[DEBUG] ltimer time delta = 0 ns
Where did you got the register definitions from?
not sure but I could not find any for now. [..] but structurally I followed the hifive-p550 style while writing.
So you don't know the register layout and can't write a timer driver. There is no point in trying to write one if you don't know what registers to read and what they mean!
But were your driver functions called at all?
Yes, I believe, btw let me drop the logs from u-boot when I load the sel4 image .. I've added multiple prints to find the issue...
Well, at least you wired it correctly to the util_libs driver infrastructure, so the problem is not on the seL4 side of things.
The closest thing to a technical reference manual for the Spacemit K1 SoC I can find is here.
Unfortunately I can't see a description of the peripheral timers anywhere.
It seems the only source of truth would be the Linux driver in their fork.
So you don't know the register layout and can't write a timer driver. There is no point in trying to write one if you don't know what registers to read and what they mean!
No, I meant I didnt find the compatible driver so far and the only K1 SoC details I could find is below as I mentioned earliar ..
https://docs.banana-pi.org/en/BPI-F3/SpacemiT_K1_datasheet https://developer.spacemit.com/documentation?token=Alhewa0fai7lvbk9sajcumNqn4f
same which @Ivan-Velickovic shared.
The problem is what I configure (as per their datasheet) it's not working, when read from the timer registers, I get no value. I'll figure this out .. the only reason I posted the problem here thought I would get some help :).
The register layout is described in the user manual, as well as the address map.
https://developer.spacemit.com/documentation?token=T7TnwVZz1iPBk1kKwAPc6lyKnNb
So the best TRM pdf would be this:
https://cloud.spacemit.com/prod-api/release/download/tools?token=K1_User_Manual
The register layout is described in the user manual, as well as the address map. https://developer.spacemit.com/documentation?token=T7TnwVZz1iPBk1kKwAPc6lyKnNb
Ah thanks I missed that.
Me too. I found the documents, but not the right timer info.
So at first guess, what's seems missing is configuration of the Timer Clock Control Register?
The timer you need to use is probably:
https://developer.spacemit.com/documentation?token=T7TnwVZz1iPBk1kKwAPc6lyKnNb#11.2-timer-%26-watchdog
and doesn't match the register layout of the timer in this PR.
This is PR is ready to review I believe.
Timer tests also pass on sel4test with these changes.
Not sure why Style is failing. Can someone please help me with this?
Edit: I think because I forced pushed in last commit, it was comparing with branch head and found difference, it should be fixed now.
Just some nitpicks, nothing important.
Let me know when you're happy with it. Don't forget to redo a final sel4test run to catch last second mistakes.
Thanks for the review.
btw I did not remove the spacemit_timer_t i think it's fine this way too.
This PR is ready now.
let me know if needed any change from myside, Thanks!
Please squash the history into one commit. Ignore the line too long error for the link to the spec, that's okay, but fix the other errors.
Please squash the history into one commit. Ignore the line too long error for the link to the spec, that's okay, but fix the other errors.
updated.
You may have tabs instead of spaces and that's what the style checker chokes on.
You may have tabs instead of spaces and that's what the style checker chokes on.
I think style fails because of force push as also mentioned in https://github.com/seL4/ci-actions/tree/master/style
This breaks for force-push, where the previous head of the branch might not exist any more.
I think style fails because of force push as also mentioned in https://github.com/seL4/ci-actions/tree/master/style
This breaks for force-push, where the previous head of the branch might not exist any more.
I don't think we use the diff_only option, otherwise we wouldn't get style errors for unchanged lines in touched files, which we generally do. I think my theory is more likely and it are genuine style errors.
Yes, the style error is genuine, please replace the tabs with spaces. In the sel4_tools repo, there is a script style_all.sh that you can run on the file to make it style compliant (sel4_tools/misc/style-all.sh <filename>). You need to have python sel4-deps installed and the rest of the dev dependencies, but if you have been compiling seL4 that will already be there.
For the commit message it is Ok to ignore CI on this one. I'm not a fan of links in commit messages (extremely unlikely that this link is still going to work in 10 years, and no way to update it), but there doesn't seem to be a better kind of reference. What could work is putting the link into a comment in the code somewhere at the top. Then it can at least in theory be updated when it breaks.
