Doc updates

. add a dependency diagram to the reading guide
. simplify the OS boot instructions using the new Linux image
. put funding ack in top-level readme

2 files changed, 52 insertions, 36 deletions

diff --git a/os-boot/README.md b/os-boot/README.md
index 4d80d39..087abac 100644
--- a/os-boot/README.md
+++ b/os-boot/README.md
@@ -10,6 +10,13 @@ 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
 --------------------------------
 
@@ -49,45 +56,15 @@ Caveats for OS boot
   platform.  This will not be needed once the C model can generate its
   own DTB.
 
-Sample OS images
-----------------
-
-This directory contains some sample OS images and support files built
-for the basic platform implemented by the model.  They were built with
-toolchains that emitted illegal instructions, and require the model to
-be patched to boot them:
+Sample Linux image
+------------------
 
-```
-patch -p1 < os-boot/os-boot-patch.diff
-```
-
-The device-tree for the 64-bit Sail model is described in `rv64-64mb.dts`.  This file
-can be generated using:
-```
-./ocaml_emulator/riscv_ocaml_sim_RV64 -dump-dts > os-boot/rv64-64mb.dts
-```
+`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`:
 
-The device-tree binary for OS boots can be compiled from that source file:
 ```
 dtc < os-boot/rv64-64mb.dts > os-boot/rv64-64mb.dtb
-```
-
-The 64-bit Linux image can then be booted as:
-```
-./c_emulator/riscv_sim_RV64 -b os-boot/rv64-64mb.dtb -t /tmp/console.log os-boot/linux-rv64-64mb.bbl > >(gzip -c - > /tmp/exec-trace.log.gz) 2>&1
+./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
 ```
-
-The 64-bit FreeBSD image requires hardware PTE update support (`-d`):
-```
-./c_emulator/riscv_sim_RV64 -d -b os-boot/rv64-64mb.dtb -t /tmp/console.log os-boot/freebsd-rv64.bbl > >(gzip -c - > /tmp/exec-trace.log.gz) 2>&1
-```
-
-The 64-bit seL4 image runs its test-suite and requires more memory (`-z`):
-```
-dtc < os-boot/rv64-2gb.dts > os-boot/rv64-2gb.dtb
-./c_emulator/riscv_sim_RV64 -z 2048 -b os-boot/rv64-2gb.dtb -t /tmp/console.log os-boot/sel4-rv64.bbl > >(gzip -c - > /tmp/exec-trace.log.gz) 2>&1
-```
-
-Note that the consistency of the `-z` argument and the contents of the
-DTB have to be ensured manually for now.
diff --git a/os-boot/image-notes.txt b/os-boot/image-notes.txt
new file mode 100644
index 0000000..f517f87
--- /dev/null
+++ b/os-boot/image-notes.txt
@@ -0,0 +1,39 @@
+This directory contains some sample OS images and support files built
+for the basic platform implemented by the model.  They were built with
+toolchains that emitted illegal instructions, and require the model to
+be patched to boot them:
+
+```
+patch -p1 < os-boot/os-boot-patch.diff
+```
+
+The device-tree for the 64-bit Sail model is described in `rv64-64mb.dts`.  This file
+can be generated using:
+```
+./ocaml_emulator/riscv_ocaml_sim_RV64 -dump-dts > os-boot/rv64-64mb.dts
+```
+
+The device-tree binary for OS boots can be compiled from that source file:
+```
+dtc < os-boot/rv64-64mb.dts > os-boot/rv64-64mb.dtb
+```
+
+The 64-bit Linux image can then be booted as:
+```
+./c_emulator/riscv_sim_RV64 -b os-boot/rv64-64mb.dtb -t /tmp/console.log os-boot/linux-rv64-64mb.bbl > >(gzip -c - > /tmp/exec-trace.log.gz) 2>&1
+tail -f /tmp/console.log
+```
+
+The 64-bit FreeBSD image requires hardware PTE update support (`-d`):
+```
+./c_emulator/riscv_sim_RV64 -d -b os-boot/rv64-64mb.dtb -t /tmp/console.log os-boot/freebsd-rv64.bbl > >(gzip -c - > /tmp/exec-trace.log.gz) 2>&1
+```
+
+The 64-bit seL4 image runs its test-suite and requires more memory (`-z`):
+```
+dtc < os-boot/rv64-2gb.dts > os-boot/rv64-2gb.dtb
+./c_emulator/riscv_sim_RV64 -z 2048 -b os-boot/rv64-2gb.dtb -t /tmp/console.log os-boot/sel4-rv64.bbl > >(gzip -c - > /tmp/exec-trace.log.gz) 2>&1
+```
+
+Note that the consistency of the `-z` argument and the contents of the
+DTB have to be ensured manually for now.