Hi Jeff, Comments inline: On Tue, 2017-01-31 at 18:25 +0000, Brandon, Jeffrey - 0553 - MITLL wrote:

Thanks Alex,

So in this JTAG example does the run command begin the 3 step boot process you outlined?

------------ 1. connect arm hw 2. rst # Reset the device 3. fpga -f hardware/bitstream.bit 4. source hardware/ps7_init.tcl 5. ps7_init 6. ps7_post_config 7. dow images/sel4bench-image-arm-zynq7000 8. run 9. exit ------------- 1-2: Connect to the processor and put it in a known state 3-6: Program the FPGA and perform some early initialisation. I am not sure if this is still required for a PS only project. 7: Performs step 2: load the elf sections. There is no reason to load the entire elf file into memory first in this case 8: Performs step 3: jump to the program entry point. The image must be an ELF file, otherwise the entry point can not be determined by the tool.

Also how should I be generating sel4bench-image-arm-zynq7000?

Replace the argument to the 'dow' command with the location of the image that you wish to run (probably images/sel4test-image-arm-zynq7000 in your case).

Right now I am working from the sel4test repository https://github.com/seL4/sel4test configured to target Zynq-7000.

When I try the "dow images/sel4bench-image-arm-zynq7000" on images generated using the standard make command and also with make build-binary and make build-uBoot, I get an error: Code 16 Time 1485875053070 Format {Invalid context}.

Looking at the configuration this seems to be designed for the Xilinx ZC706, ARMv7a, Cortex A9. However the zed board has a ZC702. Would this be the source of my problem or should sel4 work with the ZC702 as well?

Although ZC702 is not a supported platform, the processors are generally compatible. Actually, the XMD commands that I provided are what I have been using for my development on the Zedboard. - Alex

Thanks again,

Jeff

-----Original Message----- From: Alexander.Kroh@data61.csiro.au [mailto:Alexander.Kroh@data61.csiro.au] Sent: Monday, January 30, 2017 5:40 PM To: Brandon, Jeffrey - 0553 - MITLL Cc: devel@sel4.systems Subject: Re: [seL4] seL4 on Zedboard

Hi Jeff,

The boot process is as follows: 1) u-boot loads the seL4 ELF file into memory at ${loadaddr} 2) u-boot reads the ELF file and copies the appropriate sections to the correct address for program execution 3) u-boot reads the entry point from the ELF file and jumps to the address to start execution.

So ${loadaddr} can be anything that you like, as long as it does not overwrite any part of u-boot or occupy the space at which the ELF sections will be copied.

Loading from SD can be quite awkward during development. I recommend using JTAG via the XMD tool. Here is an example of the required XMD commands: ------------ connect arm hw rst fpga -f hardware/bitstream.bit source hardware/ps7_init.tcl ps7_init ps7_post_config dow images/sel4bench-image-arm-zynq7000 run exit -------------

- Alex

On Mon, 2017-01-30 at 16:04 +0000, Brandon, Jeffrey - 0553 - MITLL wrote:

...

Hi,

I’ve been trying to get seL4 running on a Zedboard and I was wondering if there was any documentation on how to boot sle4 from an SD card.

I’ve read

http://sel4.systems/pipermail/devel/2016-December/001160.html

and

https://sel4.systems/Info/Hardware/General/

which mentions using ${loadaddr} but that doesn’t seem to be defined on the Zedboard’s u-boot.

So far I’ve compiled the image targeting the zynq7000 and used the mkimage command from the general hardware page to try u-boot’s fastboot, but fastboot doesn’t seem to be available on the zynq either.

I am a bit of a novice here. I worry that the solution may be simple but I am currently taking shots in the dark. I wanted to ask this list for any resources you may be aware of for getting sel4 test cases running on the Zed.

Thanks for the help,

Jeff Brandon

05-53 Secure Resilient Systems and Technology

_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel