diff options
| -rw-r--r-- | riscv/riscv_extras.lem | 29 | ||||
| -rw-r--r-- | riscv/riscv_platform.sail | 12 |
2 files changed, 29 insertions, 12 deletions
diff --git a/riscv/riscv_extras.lem b/riscv/riscv_extras.lem index 491dd56d..b93073de 100644 --- a/riscv/riscv_extras.lem +++ b/riscv/riscv_extras.lem @@ -44,12 +44,29 @@ let read_ram addrsize size hexRAM address = let speculate_conditional_success () = excl_result () -val get_slice_int : forall 'a. Size 'a => integer -> integer -> integer -> bitvector 'a -let get_slice_int len n lo = - (* TODO: Is this the intended behaviour? *) - let hi = lo + len - 1 in - let bits = bits_of_int (hi + 1) n in - of_bits_failwith (subrange_list false bits hi lo) +val plat_ram_base : forall 'a. Size 'a => unit -> bitvector 'a +let plat_ram_base () = wordFromInteger 0 +declare ocaml target_rep function plat_ram_base = `Platform.dram_base` + +val plat_ram_size : forall 'a. Size 'a => unit -> bitvector 'a +let plat_ram_size () = wordFromInteger 0 +declare ocaml target_rep function plat_ram_size = `Platform.dram_size` + +val plat_rom_base : forall 'a. Size 'a => unit -> bitvector 'a +let plat_rom_base () = wordFromInteger 0 +declare ocaml target_rep function plat_rom_base = `Platform.rom_base` + +val plat_rom_size : forall 'a. Size 'a => unit -> bitvector 'a +let plat_rom_size () = wordFromInteger 0 +declare ocaml target_rep function plat_rom_size = `Platform.rom_size` + +val plat_clint_base : forall 'a. Size 'a => unit -> bitvector 'a +let plat_clint_base () = wordFromInteger 0 +declare ocaml target_rep function plat_clint_base = `Platform.clint_base` + +val plat_clint_size : forall 'a. Size 'a => unit -> bitvector 'a +let plat_clint_size () = wordFromInteger 0 +declare ocaml target_rep function plat_clint_size = `Platform.clint_size` val shift_bits_right : forall 'a 'b. Size 'a, Size 'b => bitvector 'a -> bitvector 'b -> bitvector 'a let shift_bits_right v m = shiftr v (uint m) diff --git a/riscv/riscv_platform.sail b/riscv/riscv_platform.sail index 75cf9b03..009090f1 100644 --- a/riscv/riscv_platform.sail +++ b/riscv/riscv_platform.sail @@ -7,16 +7,16 @@ */ /* Main memory */ -val plat_ram_base = {ocaml: "Platform.dram_base"} : unit -> xlenbits -val plat_ram_size = {ocaml: "Platform.dram_size"} : unit -> xlenbits +val plat_ram_base = {ocaml: "Platform.dram_base", lem: "plat_ram_base"} : unit -> xlenbits +val plat_ram_size = {ocaml: "Platform.dram_size", lem: "plat_ram_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 +val plat_rom_base = {ocaml: "Platform.rom_base", lem: "plat_rom_base"} : unit -> xlenbits +val plat_rom_size = {ocaml: "Platform.rom_size", lem: "plat_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 plat_clint_base = {ocaml: "Platform.clint_base", lem: "plat_clint_base"} : unit -> xlenbits +val plat_clint_size = {ocaml: "Platform.clint_size", lem: "plat_clint_size"} : unit -> xlenbits val phys_mem_segments : unit -> (xlenbits, xlenbits) function phys_mem_segments() = |