Fix docs about sel4 boot.

2 files changed, 53 insertions, 4 deletions

diff --git a/os-boot/README.md b/os-boot/README.md
index 618312d..7077b4a 100644
--- a/os-boot/README.md
+++ b/os-boot/README.md
@@ -75,12 +75,16 @@ The 64-bit Linux image can then be booted as:
 tail -f /tmp/console.log
 ```
 
-The 64-bit seL4 image runs its test-suite, which can take a very long time in a simulator:
+The 64-bit FreeBSD image requires hardware PTE update support (`-d`):
 ```
-./c_emulator/riscv_sim_RV64 -b os-boot/rv64-64mb.dtb -t /tmp/console.log os-boot/sel4-rv64.bbl > >(gzip -c - > /tmp/exec-trace.log.gz) 2>&1
+./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 FreeBSD image requires hardware PTE update support (`-d`):
+The 64-bit seL4 image runs its test-suite and requires more memory (`-z`):
 ```
-./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
+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/rv64-2gb.dts b/os-boot/rv64-2gb.dts
new file mode 100644
index 0000000..4cbb2d4
--- /dev/null
+++ b/os-boot/rv64-2gb.dts
@@ -0,0 +1,45 @@
+/dts-v1/;
+
+/ {
+  #address-cells = <2>;
+  #size-cells = <2>;
+  compatible = "ucbbar,spike-bare-dev";
+  model = "ucbbar,spike-bare";
+  cpus {
+    #address-cells = <1>;
+    #size-cells = <0>;
+    timebase-frequency = <10000000>;
+    CPU0: cpu@0 {
+      device_type = "cpu";
+      reg = <0>;
+      status = "okay";
+      compatible = "riscv";
+      riscv,isa = "rv64imac";
+      mmu-type = "riscv,sv39";
+      clock-frequency = <1000000000>;
+      CPU0_intc: interrupt-controller {
+        #interrupt-cells = <1>;
+        interrupt-controller;
+        compatible = "riscv,cpu-intc";
+      };
+    };
+  };
+  memory@80000000 {
+    device_type = "memory";
+    reg = <0x0 0x80000000 0x0 0x80000000>;
+  };
+  soc {
+    #address-cells = <2>;
+    #size-cells = <2>;
+    compatible = "ucbbar,spike-bare-soc", "simple-bus";
+    ranges;
+    clint@2000000 {
+      compatible = "riscv,clint0";
+      interrupts-extended = <&CPU0_intc 3 &CPU0_intc 7 >;
+      reg = <0x0 0x2000000 0x0 0xc0000>;
+    };
+  };
+  htif {
+    compatible = "ucb,htif0";
+  };
+};