Booting OS images
=================

The Sail model implements a very simple platform based on the one
implemented by the Spike reference simulator.  It implements a console
output port similar to Spike's HTIF (host-target interface) mechanism,
and an interrupt controller based on Spike's CLINT (core-local
interrupt controller).  Console input is not currently supported.

32-bit OS boots require a workaround for the 64-bit HTIF interface,
which is currently not supported.

OS boots use device-tree binary blobs generated by the `dtc` compiler,
installable on Ubuntu and Debian machines with

```
sudo apt install device-tree-compiler
```

Booting Linux with the C backend
--------------------------------

The C model needs an ELF-version of the BBL (Berkeley-Boot-Loader)
that contains the Linux kernel as an embedded payload.  It also needs
a DTB (device-tree blob) file describing the platform (say in the file
`spike.dtb`).  Once those are available (see below for suggestions),
the model should be run as:

```
$ ./c_emulator/riscv_sim_<arch> -t console.log -b spike.dtb bbl > execution-trace.log 2>&1 &
$ tail -f console.log
```
The `console.log` file contains the console boot messages. For maximum
performance and benchmarking a model without any execution tracing is
available on the optimize branch (`git checkout optimize`) of this
repository. This currently requires the latest Sail built from source.

Booting Linux with the OCaml backend
------------------------------------

The OCaml model only needs the ELF-version of the BBL, since it can generate its
own DTB.
```
$ ./ocaml_emulator/riscv_ocaml_sim_<arch> bbl > execution-trace.log 2> console.log
```

Caveats for OS boot
-------------------

- Some OS toolchains generate obsolete LR/SC instructions with now
  illegal combinations of `.aq` and `.rl` flags.  You can work-around
  this by changing `riscv_mem.sail` to accept these flags.

- One needs to manually ensure that the DTB used for the C model
  accurately describes the physical memory map implemented in the C
  platform.  This will not be needed once the C model can generate its
  own DTB.

Sample Linux image
------------------

`rv64-linux-4.15.0-gcc-7.2.0-64mb.bbl` contains a sample Linux RV64
image that can be booted as follows, after first generating the
device-tree blob for a 64MB RV64 machine using `dtc`:

```
dtc < os-boot/rv64-64mb.dts > os-boot/rv64-64mb.dtb
./c_emulator/riscv_sim_RV64 -b os-boot/rv64-64mb.dtb -t /tmp/console.log os-boot/rv64-linux-4.15.0-gcc-7.2.0-64mb.bbl > >(gzip -c > execution-trace.log.gz) 2>&1
tail -f /tmp/console.log
```