Cheshire

Cheshire is a 6-stage RISC-V CPU. For details, refer to https://github.com/pulp-platform/cheshire

seL4 currently only provides Cheshire support for the Genesys 2 board.

Building the GCC toolchain

It is recommended to build the toolchain from source.

git clone https://github.com/riscv/riscv-gnu-toolchain.git
cd riscv-gnu-toolchain
git submodule update --init --recursive
export RISCV=/opt/riscv
./configure --prefix="${RISCV}" --enable-multilib
make linux

After it is built, add the $RISCV/bin folder to your PATH. The built toolchain works for both 32-bit and 64-bit.

Alternatively, any pre-built toolchain with multilib enabled should work.

Building seL4test

Checkout the sel4test project using repo as per seL4Test

repo init -u https://github.com/seL4/sel4test-manifest.git
repo sync
mkdir cbuild
cd cbuild
../init-build.sh -DPLATFORM=cheshire -DRISCV64=1
# The default cmake wrapper sets up a default configuration for the target platform.
# To change individual settings, run `ccmake .` and change the configuration
# parameters to suit your needs.
ninja

Generated binaries can be found in the images/ directory.

Running seL4test

Synthesising hardware for the Genesys 2 requires a Vivado Enterprise license. Unfortunately there are no prebuilt bitstreams available. Vivado 2023.2 is recommended.

1. Synthesise the bitstream from source following the instructions from the Cheshire Manual. Follow setup instructions then run

   make chs-xilinx-genesys2
   

2. Program the FPGA using the Vivado Hardware Manager. Open the hardware manager GUI and choose /path/to/cheshire/target/xilinx/out/cheshire.genesys2.bit as the bitstream file in the “Program Device” dialog.

3. Prepare a device tree blob for OpenSBI.

   make sw/boot/cheshire.genesys2.dtb
   

4. In a new terminal, connect an OpenOCD session to the board over the JTAG micro-USB port.

   openocd -f /path/to/cheshire/util/openocd.genesys2.tcl
   

5. In another terminal, connect to OpenOCD using GDB from the RISC-V toolchain.

   riscv64-unknown-elf-gdb --eval-command "target extended-remote localhost:3333"
   

6. Use GDB to reset the board, then load the DTB, load OpenSBI and allow it to run.

   # Reset CPU and halt
   (gdb) monitor reset halt
   
   # Load DTB to 0x70000000
   (gdb) restore /path/to/cheshire.dtb binary 0x70000000
   
   # Set location of DTB and hart ID for OpenSBI when it boots. This step is normally
   # performed by the zero stage bootloader.
   (gdb) set $a0=0x70000000
   (gdb) set $a1=0
   
   # Load OpenSBI and run
   (gdb) load /path/to/opensbi
   
   # Run OpenSBI to allow it to do preliminary setup
   (gdb) c
   (CTRL+C) # Stop running once SBI prints "Running test payload"
   

7. Finally, load the seL4test binary, set the PC and run.

   (gdb) restore /path/to/sel4test-driver-image-riscv-cheshire binary 0x80200000
   (gdb) j *0x80200000
   

Booting via GDB

This process can be expedited by using a GDB command file. If you paste the below into a file, it may be used as riscv64-unknown-elf-gdb --command=/path/to/run_sel4test.gdb to complete step 6 and 7, up to the final jump which must be done manually:

run_sel4test.gdb

target extended-remote localhost:3333
monitor reset halt
restore /path/to/cheshire.dtb binary 0x70000000
set $a0=0x70000000
set $a1=0
restore /path/to/sel4test-driver-image-riscv-cheshire binary 0x80200000
load /path/to/opensbi
c

Finish with

   (gdb) j *0x80200000

Notes

If you encounter issues such as OpenOCD failing to connect, you should attempt to reset the JTAG connection with lsusb. The JTAG device should have a name similar to Future Technology Devices International, Ltd FT2232C/D/H Dual UART/FIFO IC. Note the Bus XXX Device YYY next to the device and reset it with

sudo usbreset XXX/YYY