diff options
| -rw-r--r-- | README.md | 67 | ||||
| -rw-r--r-- | c_emulator/riscv_sim.c | 2 | ||||
| -rw-r--r-- | os-boot/README.md | 90 | ||||
| -rw-r--r-- | os-boot/freebsd-rv64.bbl | bin | 0 -> 24118552 bytes | |||
| -rwxr-xr-x | os-boot/linux-rv64-64mb.bbl | bin | 0 -> 9711152 bytes | |||
| -rw-r--r-- | os-boot/os-boot-patch.diff | 42 | ||||
| -rw-r--r-- | os-boot/rv64-64mb.dts | 45 | ||||
| -rwxr-xr-x | os-boot/sel4-rv64.bbl | bin | 0 -> 9692592 bytes |
8 files changed, 189 insertions, 57 deletions
@@ -54,6 +54,12 @@ The files in the OCaml and C simulators implement ELF-loading and the platform devices, define the physical memory map, and use command-line options to select implementation-specific ISA choices. +Provers +------- + +The files under `handwritten_support` provide library definitions for +Coq, Isabelle and HOL4. + Building the model ------------------ @@ -99,60 +105,9 @@ $ ./c_emulator/riscv_sim_<arch> <elf-file> Some information on additional configuration options for each simulator is available from `./ocaml_emulator/riscv_ocaml_sim_<arch> -h` and `./c_emulator/riscv_sim_<arch> -h`. -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 -``` - -Generating input files for Linux boot -------------------------------------- - -One could directly build Linux and the toolchain using -`https://github.com/sifive/freedom-u-sdk`. The built `bbl` -will be available in `./work/riscv-pk/bbl`. You will need to configure -a kernel that can be booted on Spike; in particular, it should be -configured to use the HTIF console. - -The DTB can be generated using Spike and the DeviceTree compiler -`dtc` as: - -``` -spike --dump-dts . | dtc > spike.dtb -``` - -(The '.' above is to work around a minor Spike bug and may not be -needed in future Spike versions.) - -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. +Some useful options are: configuring whether misaligned accesses trap +(--enable-misaligned for C and -enable-misaligned for OCaml), and +whether page-table walks update PTE bits (--enable-dirty-update for C +and -enable-dirty-update for OCaml). -- 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. +For booting operating system images, see the information under `os-boot`. diff --git a/c_emulator/riscv_sim.c b/c_emulator/riscv_sim.c index ac14cb5..2291ec3 100644 --- a/c_emulator/riscv_sim.c +++ b/c_emulator/riscv_sim.c @@ -74,7 +74,7 @@ struct timeval init_start, init_end, run_end; int total_insns = 0; static struct option options[] = { - {"enable-dirty", no_argument, 0, 'd'}, + {"enable-dirty-update", no_argument, 0, 'd'}, {"enable-misaligned", no_argument, 0, 'm'}, {"ram-size", required_argument, 0, 'z'}, {"disable-compressed", no_argument, 0, 'C'}, diff --git a/os-boot/README.md b/os-boot/README.md new file mode 100644 index 0000000..72b84af --- /dev/null +++ b/os-boot/README.md @@ -0,0 +1,90 @@ +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 +``` + +Generating input files for Linux boot +------------------------------------- + +One could directly build Linux and the toolchain using +`https://github.com/sifive/freedom-u-sdk`. The built `bbl` +will be available in `./work/riscv-pk/bbl`. You will need to configure +a kernel that can be booted on Spike; in particular, it should be +configured to use the HTIF console. + +The DTB can be generated using Spike and the DeviceTree compiler +`dtc` as: + +``` +spike --dump-dts . | dtc > spike.dtb +``` + +(The '.' above is to work around a minor Spike bug and may not be +needed in future Spike versions.) + +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 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: + +``` +patch -p1 < os-boot/os-boot-patch.diff +``` + +The device-tree can be compiled from its source: +``` +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 seL4 image runs its test-suite, which can take a very long time in a simulator: +``` +./c_emulator/riscv_sim_RV64 -d -b os-boot/rv64-64mb.dtb -t /tmp/console.log os-boot/sel4-rv64.bbl > /tmp/exec-trace.log 2>&1 & +``` + +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 > /tmp/exec-trace.log 2>&1 +``` diff --git a/os-boot/freebsd-rv64.bbl b/os-boot/freebsd-rv64.bbl Binary files differnew file mode 100644 index 0000000..fc261c9 --- /dev/null +++ b/os-boot/freebsd-rv64.bbl diff --git a/os-boot/linux-rv64-64mb.bbl b/os-boot/linux-rv64-64mb.bbl Binary files differnew file mode 100755 index 0000000..fe01cda --- /dev/null +++ b/os-boot/linux-rv64-64mb.bbl diff --git a/os-boot/os-boot-patch.diff b/os-boot/os-boot-patch.diff new file mode 100644 index 0000000..03d0c30 --- /dev/null +++ b/os-boot/os-boot-patch.diff @@ -0,0 +1,42 @@ +diff --git a/model/prelude_mem.sail b/model/prelude_mem.sail +index 8e483f8..8c68192 100644 +--- a/model/prelude_mem.sail ++++ b/model/prelude_mem.sail +@@ -29,8 +29,8 @@ function __RISCV_write (addr, width, data, aq, rl, con) = + (false, true, true) => __WriteRAM_conditional_release(sizeof(xlen), width, EXTZ(0x0), addr, data), + (true, true, false) => __WriteRAM_strong_release(sizeof(xlen), width, EXTZ(0x0), addr, data), + (true, true, true) => __WriteRAM_conditional_strong_release(sizeof(xlen), width, EXTZ(0x0), addr, data), +- (true, false, false) => false, +- (true, false, true) => false ++ (true, false, false) => __WriteRAM(sizeof(xlen), width, EXTZ(0x0), addr, data),//false ++ (true, false, true) => __WriteRAM(sizeof(xlen), width, EXTZ(0x0), addr, data) //false + } + + val __TraceMemoryWrite : forall 'n 'm. +diff --git a/model/riscv_mem.sail b/model/riscv_mem.sail +index 3549e80..1d77e6b 100644 +--- a/model/riscv_mem.sail ++++ b/model/riscv_mem.sail +@@ -88,9 +88,9 @@ function mem_write_ea (addr, width, aq, rl, con) = { + (false, true, false) => MemValue(MEMea_release(addr, width)), + (false, false, true) => MemValue(MEMea_conditional(addr, width)), + (false, true , true) => MemValue(MEMea_conditional_release(addr, width)), +- (true, false, false) => throw(Error_not_implemented("store.aq")), ++ (true, false, false) => MemValue(MEMea(addr, width)),//throw(Error_not_implemented("store.aq")), + (true, true, false) => MemValue(MEMea_strong_release(addr, width)), +- (true, false, true) => throw(Error_not_implemented("sc.aq")), ++ (true, false, true) => MemValue(MEMea(addr, width)),//throw(Error_not_implemented("sc.aq")), + (true, true , true) => MemValue(MEMea_conditional_strong_release(addr, width)) + } + } +@@ -133,8 +133,8 @@ function mem_write_value (addr, width, value, aq, rl, con) = { + if (rl | con) & (~ (is_aligned_addr(addr, width))) + then MemException(E_SAMO_Addr_Align) + else match (aq, rl, con) { +- (true, false, false) => throw(Error_not_implemented("store.aq")), +- (true, false, true) => throw(Error_not_implemented("sc.aq")), ++ (true, false, false) => checked_mem_write(addr, width, value, aq, rl, con),//throw(Error_not_implemented("store.aq")), ++ (true, false, true) => checked_mem_write(addr, width, value, aq, rl, con),//throw(Error_not_implemented("sc.aq")), + (_, _, _) => checked_mem_write(addr, width, value, aq, rl, con) + } + } diff --git a/os-boot/rv64-64mb.dts b/os-boot/rv64-64mb.dts new file mode 100644 index 0000000..84969e4 --- /dev/null +++ b/os-boot/rv64-64mb.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 0x4000000>; + }; + 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"; + }; +}; diff --git a/os-boot/sel4-rv64.bbl b/os-boot/sel4-rv64.bbl Binary files differnew file mode 100755 index 0000000..04735f1 --- /dev/null +++ b/os-boot/sel4-rv64.bbl |