diff options
| -rw-r--r-- | riscv/main.sail | 10 | ||||
| -rw-r--r-- | riscv/riscv_platform.sail | 22 |
2 files changed, 22 insertions, 10 deletions
diff --git a/riscv/main.sail b/riscv/main.sail index dbf41f49..a72eb3f3 100644 --- a/riscv/main.sail +++ b/riscv/main.sail @@ -1,13 +1,3 @@ -val elf_tohost = { - ocaml: "Elf_loader.elf_tohost", - c: "elf_tohost" -} : unit -> int - -val elf_entry = { - ocaml: "Elf_loader.elf_entry", - c: "elf_entry" -} : unit -> int - val main : unit -> unit effect {barr, eamem, escape, exmem, rmem, rreg, wmv, wreg} function main () = { diff --git a/riscv/riscv_platform.sail b/riscv/riscv_platform.sail index 80f546b8..728b25f9 100644 --- a/riscv/riscv_platform.sail +++ b/riscv/riscv_platform.sail @@ -6,14 +6,29 @@ - it relies on externs to get platform address information and doesn't hardcode them. */ +val elf_tohost = { + ocaml: "Elf_loader.elf_tohost", + interpreter: "Elf_loader.elf_tohost", + c: "elf_tohost" +} : unit -> int + +val elf_entry = { + ocaml: "Elf_loader.elf_entry", + interpreter: "Elf_loader.elf_entry", + c: "elf_entry" +} : unit -> int + /* Main memory */ val plat_ram_base = {c: "plat_ram_base", ocaml: "Platform.dram_base", lem: "plat_ram_base"} : unit -> xlenbits +function plat_ram_base () = 0x0000000080000000 val plat_ram_size = {c: "plat_ram_size", ocaml: "Platform.dram_size", lem: "plat_ram_size"} : unit -> xlenbits +function plat_ram_size () = 0x0000000000000800 << 0x14 /* whether the MMU should update dirty bits in PTEs */ val plat_enable_dirty_update = {ocaml: "Platform.enable_dirty_update", c: "plat_enable_dirty_update", lem: "plat_enable_dirty_update"} : unit -> bool +function plat_enable_dirty_update () = false /* whether the platform supports misaligned accesses without trapping to M-mode. if false, * misaligned loads/stores are trapped to Machine mode. @@ -21,17 +36,23 @@ val plat_enable_dirty_update = {ocaml: "Platform.enable_dirty_update", val plat_enable_misaligned_access = {ocaml: "Platform.enable_misaligned_access", c: "plat_enable_misaligned_access", lem: "plat_enable_misaligned_access"} : unit -> bool +function plat_enable_misaligned_access () = false /* ROM holding reset vector and device-tree DTB */ val plat_rom_base = {ocaml: "Platform.rom_base", c: "plat_rom_base", lem: "plat_rom_base"} : unit -> xlenbits +function plat_rom_base () = 0x0000000000001000 val plat_rom_size = {ocaml: "Platform.rom_size", c: "plat_rom_size", lem: "plat_rom_size"} : unit -> xlenbits +function plat_rom_size () = 0x0000000000000100 /* Location of clock-interface, which should match with the spec in the DTB */ val plat_clint_base = {ocaml: "Platform.clint_base", c: "plat_clint_base", lem: "plat_clint_base"} : unit -> xlenbits +function plat_clint_base () = 0x0000000002000000 val plat_clint_size = {ocaml: "Platform.clint_size", c: "plat_clint_size", lem: "plat_clint_size"} : unit -> xlenbits +function plat_clint_size () = 0x00000000000c0000 /* Location of HTIF ports */ val plat_htif_tohost = {ocaml: "Platform.htif_tohost", c: "plat_htif_tohost", lem: "plat_htif_tohost"} : unit -> xlenbits +function plat_htif_tohost () = to_bits(64, elf_tohost ()) // todo: fromhost val phys_mem_segments : unit -> list((xlenbits, xlenbits)) @@ -65,6 +86,7 @@ function within_htif_readable(addr : xlenbits, width : atom('n)) -> forall 'n. b /* CLINT (Core Local Interruptor), based on Spike. */ val plat_insns_per_tick = {ocaml: "Platform.insns_per_tick", c: "plat_insns_per_tick", lem: "plat_insns_per_tick"} : unit -> int +function plat_insns_per_tick () = 100 // assumes a single hart, since this typically is a vector of per-hart registers. register mtimecmp : xlenbits // memory-mapped internal clint register. |