You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Hello, I've been having an issue with running sel4test according to the updated documentation, and shared my findings on the sel4 Discourse.
Expected Behavior: config.txt without the dtoverlay=disable-bt allows u-boot.bin to load on Raspberry Pi 4B 4GB.
Actual Behavior: u-boot.bin does not load.
Solution: Re-adding the line dtoverlay=disable-bt causes u-boot to load and get to the next phase, which is running sel4test on the PI 4B
Secondary issue:
Expected Behavior: Running sel4test with go 0x10000000 shows the testing over UART on serial0
Actual Behavior: No output is observed
Solution: Implementing the kernel patch mentioned in this revision of the documentation yields the sel4test outputting as expected and succeeding all tests over the UART on serial0
I'd be more than happy to continue discussion, contribute a PR to the documentation or kernel if necessary. Thank you!
The text was updated successfully, but these errors were encountered:
I was the one who removed those instructions in the documentation as I saw them unnecessary and I was able to get a Raspberry Pi 4B working without them.
What's weird is that I've seen one person who hasn't actually been able to run seL4 with the dtoverlay=disable-bt line in their config.txt.
I wish this hardware platform wasn't so fragile. I don't have access to a Raspberry Pi right now but will get back to you next week.
Thank you for your response! I'm not exactly sure what the reason for this strange behavior might be, but one of the things I'm thinking could be a possibility is different firmware versions; I bought a new Pi 4B to try seL4 on, and this Pi has never had its firmware upgraded nor installed Raspbian on it. I will try to provide exact firmware versions, update the Pi, and then retry the steps in the tutorial tonight.
Hello, I've been having an issue with running sel4test according to the updated documentation, and shared my findings on the sel4 Discourse.
Expected Behavior:
config.txt
without thedtoverlay=disable-bt
allowsu-boot.bin
to load on Raspberry Pi 4B 4GB.Actual Behavior:
u-boot.bin
does not load.Solution: Re-adding the line
dtoverlay=disable-bt
causesu-boot
to load and get to the next phase, which is runningsel4test
on the PI 4BSecondary issue:
Expected Behavior: Running
sel4test
withgo 0x10000000
shows the testing over UART onserial0
Actual Behavior: No output is observed
Solution: Implementing the kernel patch mentioned in this revision of the documentation yields the
sel4test
outputting as expected and succeeding all tests over the UART onserial0
I'd be more than happy to continue discussion, contribute a PR to the documentation or kernel if necessary. Thank you!
The text was updated successfully, but these errors were encountered: