More definitions for the physical memory map.

3 files changed, 40 insertions, 3 deletions

diff --git a/riscv/platform.ml b/riscv/platform.ml
index 485acb76..15b28abb 100644
--- a/riscv/platform.ml
+++ b/riscv/platform.ml
@@ -74,6 +74,12 @@ 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
 
+let htif_tohost () =
+  bits_of_int64 (Big_int.to_int64 (Elf.elf_tohost ()))
+
+let clint_base () = bits_of_int64 P.clint_base
+let clint_size () = bits_of_int64 P.clint_size
+
 (* terminal I/O *)
 let term_write char_bits =
   let big_char = Big_int.bitwise_and (uint char_bits) (Big_int.of_int 255) in
diff --git a/riscv/riscv_extras.lem b/riscv/riscv_extras.lem
index 553b7508..fc72ca2b 100644
--- a/riscv/riscv_extras.lem
+++ b/riscv/riscv_extras.lem
@@ -68,6 +68,10 @@ 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 plat_htif_tohost : forall 'a. Size 'a => unit -> bitvector 'a
+let plat_htif_tohost () = wordFromInteger 0
+declare ocaml target_rep function plat_htif_tohost = `Platform.htif_tohost`
+
 val plat_term_write : forall 'a. Size 'a => bitvector 'a -> unit
 let plat_term_write _ = ()
 declare ocaml target_rep function plat_term_write = `Platform.term_write`
diff --git a/riscv/riscv_platform.sail b/riscv/riscv_platform.sail
index a002341a..8be3a52c 100644
--- a/riscv/riscv_platform.sail
+++ b/riscv/riscv_platform.sail
@@ -18,16 +18,43 @@ val plat_rom_size = {ocaml: "Platform.rom_size", lem: "plat_rom_size"} : unit ->
 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
 
+/* Location of HTIF ports */
+val plat_htif_tohost = {ocaml: "Platform.htif_tohost", lem: "plat_htif_tohost"} : unit -> xlenbits
+// todo: fromhost
+
 val phys_mem_segments : unit -> list((xlenbits, xlenbits))
 function phys_mem_segments() =
   (plat_rom_base (), plat_rom_size ()) ::
   (plat_ram_base (), plat_ram_size ()) ::
   [||]
 
-val plat_insns_per_tick = {ocaml: "Platform.insns_per_tick"} : unit -> int
+/* Physical memory map predicates */
+
+function within_phys_mem(addr : xlenbits, width : atom('n)) -> forall 'n. bool =
+  /* todo: iterate over segment list */
+  if (  plat_ram_base() <=_u addr
+      & (addr + sizeof('n)) <=_u (plat_ram_base() + plat_ram_size ()))
+       then true
+  else if (  plat_rom_base() <=_u addr
+           & (addr + sizeof('n)) <=_u (plat_rom_base() + plat_rom_size()))
+       then true
+  else false
+
+function within_clint(addr : xlenbits, width : atom('n)) -> forall 'n. bool =
+    plat_clint_base() <=_u addr
+  & (addr + sizeof('n)) <=_u (plat_clint_base() + plat_clint_size())
+
+function within_htif_writable(addr : xlenbits, width : atom('n)) -> forall 'n. bool =
+    plat_htif_tohost() == addr
+
+/* TODO */
+function within_htif_readable(addr : xlenbits, width : atom('n)) -> forall 'n. bool =
+    false
 
 /* CLINT (Core Local Interruptor), based on Spike. */
 
+val plat_insns_per_tick = {ocaml: "Platform.insns_per_tick"} : unit -> int
+
 // assumes a single hart, since this typically is a vector of per-hart registers.
 register mtimecmp : xlenbits  // memory-mapped internal clint register.
 
@@ -47,7 +74,7 @@ let MTIME_BASE    : xlenbits = 0x000000000000bff8
  * bffc mtime hi
  */
 
-val clint_load : forall 'n, 'n > 0. (xlenbits, int('n)) -> MemoryOpResult(bits(8 * 'n)) effect {rreg}
+val clint_load : forall 'n. (xlenbits, int('n)) -> MemoryOpResult(bits(8 * 'n)) effect {rreg}
 function clint_load(addr, width) = {
   /* FIXME: For now, only allow exact aligned access. */
   if addr == MSIP_BASE & ('n == 8 | 'n == 4)
@@ -86,7 +113,7 @@ bitfield htif_cmd : bits(64) = {
 register htif_done : bool
 register htif_exit_code : xlenbits
 
-val htif_load : forall 'n, 0 < 'n <= 64. (xlenbits, int('n)) -> MemoryOpResult(bits(8 * 'n))
+val htif_load : forall 'n, 'n > 0. (xlenbits, int('n)) -> MemoryOpResult(bits(8 * 'n))
 function htif_load(addr, width) = MemValue(EXTZ(0b0))
 
 /* FIXME: The wreg effect is an artifact of using 'register' to implement device state. */