diff options
Diffstat (limited to 'riscv')
| -rw-r--r-- | riscv/Makefile | 15 | ||||
| -rw-r--r-- | riscv/platform.ml | 90 | ||||
| -rw-r--r-- | riscv/platform_impl.ml | 155 | ||||
| -rw-r--r-- | riscv/platform_main.ml | 91 | ||||
| -rw-r--r-- | riscv/prelude.sail | 4 | ||||
| -rw-r--r-- | riscv/riscv_platform.sail | 120 |
6 files changed, 471 insertions, 4 deletions
diff --git a/riscv/Makefile b/riscv/Makefile index 436fa0dc..c80c0758 100644 --- a/riscv/Makefile +++ b/riscv/Makefile @@ -1,15 +1,21 @@ -SAIL_SRCS = prelude.sail riscv_types.sail riscv_sys.sail riscv_mem.sail riscv_vmem.sail riscv.sail riscv_step.sail +SAIL_SRCS = prelude.sail riscv_types.sail riscv_sys.sail riscv_platform.sail riscv_mem.sail riscv_vmem.sail riscv.sail riscv_step.sail SAIL_DIR ?= $(realpath ..) export SAIL_DIR -all: riscv Riscv.thy +all: riscv.ml platform # Riscv.thy check: $(SAIL_SRCS) main.sail Makefile $(SAIL_DIR)/sail $(SAIL_SRCS) main.sail -riscv: $(SAIL_SRCS) main.sail Makefile - $(SAIL_DIR)/sail -ocaml -o riscv $(SAIL_SRCS) main.sail +riscv.ml: $(SAIL_SRCS) Makefile main.sail + $(SAIL_DIR)/sail -ocaml -ocaml-nobuild -o riscv $(SAIL_SRCS) + +platform_main.native: riscv.ml platform.ml platform_main.ml Makefile _tags + ocamlbuild -use-ocamlfind $@ + +platform: platform_main.native + rm -f $@ && ln -s $^ $@ riscv_duopod_ocaml: prelude.sail riscv_duopod.sail $(SAIL_DIR)/sail -ocaml -o $@ $^ @@ -58,3 +64,4 @@ clean: -rm -f Riscv_duopod.thy Riscv_duopod_types.thy riscv_duopod.lem riscv_duopod_types.lem -rm -f riscvScript.sml riscv_typesScript.sml riscv_extrasScript.sml -Holmake cleanAll + ocamlbuild -clean diff --git a/riscv/platform.ml b/riscv/platform.ml new file mode 100644 index 00000000..919900f4 --- /dev/null +++ b/riscv/platform.ml @@ -0,0 +1,90 @@ +(**************************************************************************) +(* Sail *) +(* *) +(* Copyright (c) 2013-2017 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) +(* Alasdair Armstrong *) +(* Brian Campbell *) +(* Thomas Bauereiss *) +(* Anthony Fox *) +(* Jon French *) +(* Dominic Mulligan *) +(* Stephen Kell *) +(* Mark Wassell *) +(* *) +(* All rights reserved. *) +(* *) +(* This software was developed by the University of Cambridge Computer *) +(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) +(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) +(**************************************************************************) + +open Sail_lib;; +module P = Platform_impl;; +module Elf = Elf_loader;; + +(* Mapping to Sail externs *) + +let bits_of_int i = + get_slice_int (Big_int.of_int 64, Big_int.of_int i, Big_int.zero) + +let bits_of_int64 i = + get_slice_int (Big_int.of_int 64, Big_int.of_int64 i, Big_int.zero) + +let rom_size_ref = ref 0 +let make_rom start_pc = + let reset_vec = List.concat (List.map P.uint32_to_bytes (P.reset_vec_int start_pc)) in + let dtb = P.make_dtb P.dts in + let rom = reset_vec @ dtb in + ( rom_size_ref := List.length rom; + rom ) + +let rom_base () = bits_of_int64 P.rom_base +let rom_size () = bits_of_int !rom_size_ref + +let dram_base () = bits_of_int64 P.dram_base +let dram_size () = bits_of_int64 P.dram_size + +(* returns starting value for PC, i.e. start of reset vector *) +let init elf_file = + Elf.load_elf elf_file; + let start_pc = Elf.Big_int.to_int64 (Elf.elf_entry ()) in + let rom = make_rom start_pc in + let rom_base = Big_int.of_int64 P.rom_base in + let rec write_rom ofs = function + | [] -> () + | h :: tl -> let addr = Big_int.add rom_base (Big_int.of_int ofs) in + (wram addr h); + write_rom (ofs + 1) tl + in ( write_rom 0 rom; + get_slice_int (Big_int.of_int 64, rom_base, Big_int.zero) + ) diff --git a/riscv/platform_impl.ml b/riscv/platform_impl.ml new file mode 100644 index 00000000..342eab35 --- /dev/null +++ b/riscv/platform_impl.ml @@ -0,0 +1,155 @@ +(* FIXME: copyright header *) + +(* int->byte converters in little-endian order *) + +let uint32_to_bytes u = let open Int32 in + List.map to_int + [ logand u 0xffl; + logand (shift_right u 8) 0xffl; + logand (shift_right u 16) 0xffl; + logand (shift_right u 24) 0xffl; + ] + +let uint64_to_bytes u = let open Int64 in + List.map to_int + [ logand u 0xffL; + logand (shift_right u 8) 0xffL; + logand (shift_right u 16) 0xffL; + logand (shift_right u 24) 0xffL; + logand (shift_right u 32) 0xffL; + logand (shift_right u 40) 0xffL; + logand (shift_right u 48) 0xffL; + logand (shift_right u 56) 0xffL; + ] + +(* reset vector for the rom *) + +let reset_vec_size = 8l;; + +let reset_vec_int start_pc = [ + 0x267l; (* auipc t0, 0x0 *) + (let open Int32 in + add 0x28593l (shift_left (mul reset_vec_size 4l) 20)); (* addi a1, t0, ofs(dtb) *) + 0xf1402573l; (* csrr a0, mhartid *) + 0x0182b283l; (* ld t0, 24(t0) *) + 0x28067l; (* jr t0 *) + 0x0l; + (let open Int64 in to_int32 (logand start_pc 0xffffffffL)); + (let open Int64 in to_int32 (shift_right_logical start_pc 32)); +] + +(* address map *) + +let dram_base = 0x80000000L;; (* Spike::DRAM_BASE *) +let dram_size = Int64.(shift_left 2048L 20) +let clint_base = 0x02000000L;; (* Spike::CLINT_BASE *) +let clint_size = 0x000c0000L;; (* Spike::CLINT_SIZE *) +let rom_base = 0x00001000L;; (* Spike::DEFAULT_RSTVEC *) + +type mem_region = { + addr : Int64.t; + size : Int64.t +} + +(* dts from spike *) +let spike_dts isa_spec cpu_hz insns_per_rtc_tick mems = + "/dts-v1/;\n" + ^ "\n" + ^ "/ {\n" + ^ " #address-cells = <2>;\n" + ^ " #size-cells = <2>;\n" + ^ " compatible = \"ucbbar,spike-bare-dev\";\n" + ^ " model = \"ucbbar,spike-bare\";\n" + ^ " cpus {\n" + ^ " #address-cells = <1>;\n" + ^ " #size-cells = <0>;\n" + ^ " timebase-frequency = <" ^ string_of_int (cpu_hz/insns_per_rtc_tick) ^ ">;\n" + ^ " CPU0: cpu@0 {\n" + ^ " device_type = \"cpu\";\n" + ^ " reg = <0>;\n" + ^ " status = \"okay\";\n" + ^ " compatible = \"riscv\";\n" + ^ " riscv,isa = \"" ^ isa_spec ^ "\";\n" + ^ " mmu-type = \"riscv,sv39\";\n" + ^ " clock-frequency = <" ^ string_of_int cpu_hz ^ ">;\n" + ^ " CPU0_intc: interrupt-controller {\n" + ^ " #interrupt-cells = <1>;\n" + ^ " interrupt-controller;\n" + ^ " compatible = \"riscv,cpu-intc\";\n" + ^ " };\n" + ^ " };\n" + ^ " };\n" + ^ (List.fold_left (^) "" + (List.map (fun m -> + " memory@" ^ Printf.sprintf "%Lx" m.addr ^ " {\n" + ^ " device_type = \"memory\";\n" + ^ " reg = <0x" ^ Printf.sprintf "%Lx" Int64.(shift_right_logical m.addr 32) ^ " 0x" ^ Printf.sprintf "%Lx" Int64.(logand m.addr 0xffffffffL) + ^ " 0x" ^ Printf.sprintf "%Lx" Int64.(shift_right_logical m.size 32) ^ " 0x" ^ Printf.sprintf "%Lx" Int64.(logand m.size 0xffffffffL) ^ ">;\n" + ^ " };\n") mems)) + ^ " soc {\n" + ^ " #address-cells = <2>;\n" + ^ " #size-cells = <2>;\n" + ^ " compatible = \"ucbbar,spike-bare-soc\", \"simple-bus\";\n" + ^ " ranges;\n" + ^ " clint@" ^ Printf.sprintf "%Lx" clint_base ^ " {\n" + ^ " compatible = \"riscv,clint0\";\n" + ^ " interrupts-extended = <&CPU0_intc 3 &CPU0_intc 7 >;\n" + ^ " reg = <0x" ^ Printf.sprintf "%Lx" Int64.(shift_right_logical clint_base 32) ^ " 0x" ^ Printf.sprintf "%Lx" Int64.(logand clint_base 0xffffffffL) + ^ " 0x" ^ Printf.sprintf "%Lx" Int64.(shift_right_logical clint_size 32) ^ " 0x" ^ Printf.sprintf "%Lx" Int64.(logand clint_size 0xffffffffL) ^ ">;\n" + ^ " };\n" + ^ " };\n" + ^ " htif {\n" + ^ " compatible = \"ucb,htif0\";\n" + ^ " };\n" + ^ "};\n" + +let cpu_hz = 1000000000;; +let insns_per_tick = 100;; + +let mems = [ { addr = dram_base; + size = dram_size } ];; +let dts = spike_dts "rv64imac" cpu_hz insns_per_tick mems;; + +let bytes_to_string bytes = + String.init (List.length bytes) (fun i -> Char.chr (List.nth bytes i)) + +let make_dtb dts = (* Call the dtc compiler, assumed to be at /usr/bin/dtc *) + try + let (cfrom, cto, cerr) = + Unix.open_process_full "/usr/bin/dtc -I dts" [||] + in ( + output_string cto dts; + (* print_endline " sent dts to dtc ..."; *) + close_out cto; + (* simple and stupid for now *) + let rec accum_bytes cin acc = + match ( + try Some (input_byte cfrom) + with End_of_file -> None + ) with + | Some b -> accum_bytes cin (b :: acc) + | None -> List.rev acc + in + (* let _ = print_endline " accumulating dtb ..." in *) + let dtb = accum_bytes cfrom [] in + (* let _ = print_endline " accumulating emsg ..." in *) + let emsg = bytes_to_string (accum_bytes cerr []) in + match Unix.close_process_full (cfrom, cto, cerr) with + | Unix.WEXITED 0 -> dtb + | _ -> (Printf.printf "%s\n" ("Error executing dtc: " ^ emsg); + exit 1) + ) + with Unix.Unix_error (e, fn, _) -> + (Printf.printf "%s\n" ("Error executing dtc: " ^ fn ^ ": " ^ Unix.error_message e); + exit 1) + +(* +let save_string_to_file s fname = + let out = open_out fname in + output_string out s; + close_out out;; + +let _ = + save_string_to_file dts "/tmp/platform.dts"; + save_string_to_file (bytes_to_string (get_dtb dts)) "/tmp/platform.dtb"; + *) diff --git a/riscv/platform_main.ml b/riscv/platform_main.ml new file mode 100644 index 00000000..73497aa5 --- /dev/null +++ b/riscv/platform_main.ml @@ -0,0 +1,91 @@ +(**************************************************************************) +(* Sail *) +(* *) +(* Copyright (c) 2013-2017 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) +(* Alasdair Armstrong *) +(* Brian Campbell *) +(* Thomas Bauereiss *) +(* Anthony Fox *) +(* Jon French *) +(* Dominic Mulligan *) +(* Stephen Kell *) +(* Mark Wassell *) +(* *) +(* All rights reserved. *) +(* *) +(* This software was developed by the University of Cambridge Computer *) +(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) +(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) +(**************************************************************************) + +open Elf_loader +open Sail_lib +open Riscv;; + +(* OCaml driver for generated RISC-V model. *) + +let opt_file_arguments = ref ([] : string list) + +let options = Arg.align [] + +let usage_msg = "RISC-V platform options:" + +let elf_arg = + Arg.parse options (fun s -> + opt_file_arguments := !opt_file_arguments @ [s]) + usage_msg; + ( match !opt_file_arguments with + | f :: _ -> print_endline ("Loading ELF file " ^ f); f + | _ -> (prerr_endline "Please provide an ELF file."; exit 0) + ) + +let () = + Random.self_init (); + + zPC := Platform.init elf_arg; + + sail_call + (fun r -> + begin + zPC := (z__GetSlice_int ((Big_int.of_string "64"), (Elf_loader.elf_entry ()), (Big_int.of_string "0"))); + begin + try ( zinit_sys (); + zloop (Elf_loader.elf_tohost ()) + ) + with + | ZError_not_implemented (zs) -> + print_string ("Error: Not implemented: ", zs) + | ZError_internal_error (_) -> + prerr_endline "Error: internal error" + end + end) diff --git a/riscv/prelude.sail b/riscv/prelude.sail index c92497c1..c6fb1054 100644 --- a/riscv/prelude.sail +++ b/riscv/prelude.sail @@ -401,3 +401,7 @@ function shift_right_arith64 (v : bits(64), shift : bits(6)) -> bits(64) = function shift_right_arith32 (v : bits(32), shift : bits(5)) -> bits(32) = let v64 : bits(64) = EXTS(v) in (v64 >> shift)[31..0] + +/* Copied from arith.sail. */ +val mult_atom = {ocaml: "mult", lem: "integerMult", c: "mult_int"} : forall 'n 'm. + (atom('n), atom('m)) -> atom('n * 'm) diff --git a/riscv/riscv_platform.sail b/riscv/riscv_platform.sail new file mode 100644 index 00000000..cfb3b535 --- /dev/null +++ b/riscv/riscv_platform.sail @@ -0,0 +1,120 @@ +/* Platform and devices */ + +/* Current constraints on this implementation are: + - it cannot access memory directly, but instead provides definitions for the physical memory model + - it can access system register state, needed to manipulate interrupt bits + - it relies on externs to get platform address information and doesn't hardcode them. +*/ + +/* Main memory */ +val plat_ram_base = {ocaml: "Platform.dram_base"} : unit -> xlenbits +val plat_ram_size = {ocaml: "Platform.dram_size"} : unit -> xlenbits + +/* ROM holding reset vector and device-tree DTB */ +val plat_rom_base = {ocaml: "Platform.rom_base"} : unit -> xlenbits +val plat_rom_size = {ocaml: "Platform.rom_size"} : unit -> xlenbits + +/* Location of clock-interface, which should match with the spec in the DTB */ +val plat_clint_base = {ocaml: "Platform.clint_base"} : unit -> xlenbits +val plat_clint_size = {ocaml: "Platform.clint_size"} : unit -> xlenbits + +val phys_mem_segments : unit -> (xlenbits, xlenbits) +function phys_mem_segments() = +// FIXME +// (plat_rom_base (), plat_rom_base ()) :: + (plat_ram_base (), plat_ram_size ()) +// :: [||] + +val plat_insns_per_tick = {ocaml: "Platform.insns_per_tick"} : unit -> int + +/* CLINT clock device interface, based on Spike. */ + +// assumes a single hart, since this typically is a vector of per-hart registers. +register mtimecmp : xlenbits // memory-mapped internal clint register. + +/* CLINT memory-mapped IO */ + +let MSIP_BASE : xlenbits = 0x0000000000000000 +let MTIMECMP_BASE : xlenbits = 0x0000000000004000 +let MTIME_BASE : xlenbits = 0x000000000000bff8 + +/* 0000 msip hart 0 + * 0004 msip hart 1 + * 4000 mtimecmp hart 0 lo + * 4004 mtimecmp hart 0 hi + * 4008 mtimecmp hart 1 lo + * 400c mtimecmp hart 1 hi + * bff8 mtime lo + * bffc mtime hi + */ + +val clint_load : forall 'n, 'n > 0. (xlenbits, int('n)) -> MemoryOpResult(bits(8 * 'n)) effect {rreg} +function clint_load(addr, width) = { + /* FIXME: For now, only allow exact aligned access. + I couldn't make the more general access pass the type-checker. + */ + if addr == MSIP_BASE & ('n == 8 | 'n == 4) + then MemValue(zero_extend(mip.MSI(), sizeof(8 * 'n))) + /* FIXME: + else if addr == MTIMECMP_BASE & ('n == 8) + then MemValue(mtimecmp) + */ + /* FIXME: + else if addr == MTIME_BASE & ('n == 8) + then MemValue(mtime) + */ + else MemException(E_Load_Access_Fault) +} + +val clint_store: forall 'n, 'n > 0. (xlenbits, int('n), bits(8 * 'n)) -> MemoryOpResult(unit) effect {wreg} +function clint_store(addr, width, data) = { + if addr == MSIP_BASE & ('n == 8 | 'n == 4) then { + mip->MSI() = data[0] == 0b1; + MemValue(()) + } else if addr == MTIMECMP_BASE & 'n == 8 then { + /* FIXME: + mtimecmp = data; + */ + MemValue(()) + } else MemException(E_SAMO_Access_Fault) +} + +/* Spike's HTIF device interface. */ + +bitfield htif_cmd : bits(64) = { + device : 63 .. 56, + cmd : 55 .. 48, + payload : 47 .. 0 +} + +// no support yet for terminal input +val htif_load : forall 'n, 'n > 0. (xlenbits, int('n)) -> MemoryOpResult(bits(8 * 'n)) +function htif_load(addr, width) = MemValue(EXTZ(0b0)) + +val htif_store: forall 'n, 'n > 0. (xlenbits, int('n), bits(8 * 'n)) -> MemoryOpResult(unit) +function htif_store(addr, width, data) = { + // since htif is only available at a single address, we'll assume here that physical memory + // model has correctly dispatched the address. + let cbits : xlenbits = /* if 'n == 4 then EXTZ(data) else data */ EXTZ(0b0); + let cmd = Mk_htif_cmd(cbits); + match cmd.device() { + 0x00 => { /* syscall-proxy */ + if cmd.payload()[0] == 0b1 + then /* TODO: exit command + * for e.g. set a flag that's checked by the top-level loop. + * but that might appear to be a register write effect triggered by a memory write. + */ + () + else () + }, + 0x01 => { /* terminal */ + match cmd.cmd() { + 0x00 => /* input */ (), + 0x01 => /* TODO: output data */ (), + c => print("Unknown term cmd: " ^ BitStr(c)) + } + }, + d => print("Unknown htif device:" ^ BitStr(d)) + }; + MemValue(()) +} |